ILF-SERV

ILF_STATE
	proof_title     "Idempotency"
END_ILF_STATE

SYSTEM otter

TEXOP
struct	_	huntington :- "$Huntington's axiom$"
struct	_	reflexivity :- "$reflexivity$"
struct	_	commutativity :- "$commutativity$"
struct	_	associativity :- "$associativity$"
struct	_	idempotency :- "$idempotency$"
struct	_	involution :- "$involution$"
struct	_	robbins :- "$Robbins' axiom$"
struct	_	unit :- "$unit$"
struct	100	n(X) :- "\\overline{",z(X),"}"
xfy	500	'+' :- "\\cup "
xfy	500	'*' :- "\\cap "
END_TEXOP

FILE .in
set(build_proof_object).
set(auto).

list(usable).
% NAME: reflexivity
x = x.
% NAME: commutativity
x+y = y+x.
% NAME: associativity
(x+y)+z = x+y+z.
% NAME: huntington
n(x+n(y))+n(n(x)+n(y)) = y.
% NAME: goal
a+a != a.
end_of_list.

END_FILE

FILE .opf
----- Otter 3.0.4, August 1995 -----
The job was started by nelson on tea, Sat Feb 15 17:16:03 1997
The command was "otter".

set(build_proof_object).
   dependent: set(order_history).
set(auto).
   dependent: set(process_input).
   dependent: clear(print_kept).
   dependent: clear(print_new_demod).
   dependent: clear(print_back_demod).
   dependent: clear(print_back_sub).
   dependent: set(control_memory).
   dependent: assign(max_mem, 12000).
   dependent: assign(pick_given_ratio, 4).
   dependent: assign(stats_level, 1).
   dependent: assign(max_seconds, 10800).

list(usable).
0 [] x=x.
0 [] x+y=y+x.
0 [] (x+y)+z=x+y+z.
0 [] n(x+n(y))+n(n(x)+n(y))=y.
0 [] a+a!=a.
end_of_list.

SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1.

All clauses are units, and equality is present; the
strategy will be Knuth-Bendix with positive clauses in sos.

   dependent: set(knuth_bendix).
   dependent: set(para_from).
   dependent: set(para_into).
   dependent: clear(para_from_right).
   dependent: clear(para_into_right).
   dependent: set(para_from_vars).
   dependent: set(eq_units_both_ways).
   dependent: set(dynamic_demod_all).
   dependent: set(dynamic_demod).
   dependent: set(order_eq).
   dependent: set(back_demod).
   dependent: set(lrpo).

------------> process usable:
** KEPT (pick-wt=5): 1 [] a+a!=a.

------------> process sos:
** KEPT (pick-wt=3): 2 [] x=x.
** KEPT (pick-wt=7): 3 [] x+y=y+x.
** KEPT (pick-wt=11): 4 [] (x+y)+z=x+y+z.
---> New Demodulator: 5 [new_demod,4] (x+y)+z=x+y+z.
** KEPT (pick-wt=14): 6 [] n(x+n(y))+n(n(x)+n(y))=y.
---> New Demodulator: 7 [new_demod,6] n(x+n(y))+n(n(x)+n(y))=y.
  Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x=x.
  Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x+y=y+x.
>>>> Starting back demodulation with 5.
>>>> Starting back demodulation with 7.

======= end of input processing =======

=========== start of search ===========

given clause #1: (wt=3) 2 [] x=x.

given clause #2: (wt=7) 3 [] x+y=y+x.

given clause #3: (wt=11) 4 [] (x+y)+z=x+y+z.

given clause #4: (wt=11) 8 [para_into,4.1.1.1,3.1.1,demod,5] x+y+z=y+x+z.

given clause #5: (wt=11) 9 [para_into,4.1.1,3.1.1] x+y+z=y+z+x.

given clause #6: (wt=14) 6 [] n(x+n(y))+n(n(x)+n(y))=y.

given clause #7: (wt=11) 10 [copy,9,flip.1] x+y+z=z+x+y.

given clause #8: (wt=11) 13 [para_into,8.1.1,3.1.1,demod,5] x+y+z=x+z+y.

given clause #9: (wt=11) 17 [para_into,9.1.1.2,3.1.1] x+y+z=z+y+x.

given clause #10: (wt=14) 25 [para_into,6.1.1.1.1,3.1.1] n(n(x)+y)+n(n(y)+n(x))=x.

given clause #11: (wt=15) 11 [para_into,8.1.1.2,8.1.1] x+y+z+u=z+x+y+u.

given clause #12: (wt=14) 29 [para_into,6.1.1.2.1,3.1.1] n(x+n(y))+n(n(y)+n(x))=y.

given clause #13: (wt=14) 31 [para_into,6.1.1,3.1.1] n(n(x)+n(y))+n(x+n(y))=y.

given clause #14: (wt=14) 72 [para_into,25.1.1.2.1,3.1.1] n(n(x)+y)+n(n(x)+n(y))=x.

given clause #15: (wt=14) 74 [para_into,25.1.1,3.1.1] n(n(x)+n(y))+n(n(y)+x)=y.

given clause #16: (wt=15) 12 [para_into,8.1.1.2,4.1.1,demod,5] x+y+z+u=y+z+x+u.

given clause #17: (wt=14) 133 [para_into,29.1.1,3.1.1] n(n(x)+n(y))+n(y+n(x))=x.

given clause #18: (wt=14) 202 [para_into,72.1.1,3.1.1] n(n(x)+n(y))+n(n(x)+y)=x.

given clause #19: (wt=15) 14 [para_into,9.1.1.2,9.1.1,demod,5] x+y+z+u=u+y+z+x.

given clause #20: (wt=15) 15 [para_into,9.1.1.2,8.1.1,demod,5] x+y+z+u=z+y+u+x.

given clause #21: (wt=15) 16 [para_into,9.1.1.2,4.1.1,demod,5] x+y+z+u=y+z+u+x.

given clause #22: (wt=15) 18 [para_into,9.1.1,4.1.1] x+y+z+u=z+u+x+y.

given clause #23: (wt=15) 19 [copy,15,flip.1] x+y+z+u=u+y+x+z.

given clause #24: (wt=15) 20 [copy,16,flip.1] x+y+z+u=u+x+y+z.

given clause #25: (wt=15) 38 [para_into,10.1.1.2,8.1.1,demod,5] x+y+z+u=y+u+x+z.

given clause #26: (wt=23) 21 [para_into,6.1.1.1.1,6.1.1] n(x)+n(n(n(y+n(x)))+n(n(y)+n(x)))=n(y)+n(x).

given clause #27: (wt=15) 41 [copy,38,flip.1] x+y+z+u=z+x+u+y.

given clause #28: (wt=15) 42 [para_from,10.1.1,9.1.1.2,demod,5] x+y+z+u=z+u+y+x.

given clause #29: (wt=15) 43 [copy,42,flip.1] x+y+z+u=u+z+x+y.

given clause #30: (wt=15) 44 [para_into,13.1.1.2,13.1.1,demod,5] x+y+z+u=x+u+z+y.

given clause #31: (wt=18) 23 [para_into,6.1.1.1.1,4.1.1] n(x+y+n(z))+n(n(x+y)+n(z))=z.

given clause #32: (wt=15) 45 [para_into,13.1.1.2,10.1.1,demod,5] x+y+z+u=x+u+y+z.

given clause #33: (wt=15) 46 [para_into,13.1.1.2,8.1.1,demod,5] x+y+z+u=x+y+u+z.

given clause #34: (wt=15) 47 [copy,45,flip.1] x+y+z+u=x+z+u+y.

given clause #35: (wt=15) 48 [para_from,13.1.1,9.1.1.2,demod,5] x+y+z+u=y+u+z+x.

given clause #36: (wt=21) 27 [para_into,6.1.1.2.1,6.1.1,demod,5] n(x+n(y)+n(n(x)+n(y)))+n(y)=n(x)+n(y).

given clause #37: (wt=15) 49 [para_from,13.1.1,8.1.1.2] x+y+z+u=y+x+u+z.

given clause #38: (wt=15) 50 [para_from,13.1.1,4.1.1.1,demod,5,5,5] x+y+z+u=x+z+y+u.

given clause #39: (wt=15) 51 [copy,48,flip.1] x+y+z+u=u+x+z+y.

given clause #40: (wt=15) 52 [para_into,17.1.1.2,13.1.1,demod,5] x+y+z+u=u+z+y+x.

given clause #41: (wt=18) 34 [para_from,6.1.1,8.1.1.2,flip.1] n(x+n(y))+z+n(n(x)+n(y))=z+y.

given clause #42: (wt=15) 55 [para_from,17.1.1,10.1.1.2,demod,5] x+y+z+u=z+y+x+u.

given clause #43: (wt=15) 1481 [para_into,34.1.1.2,72.1.1] n(x+n(y))+x=n(n(x)+y)+y.

given clause #44: (wt=15) 1484 [para_into,34.1.1.2,29.1.1] n(x+n(y))+x=n(y+n(x))+y.

given clause #45: (wt=15) 1487 [para_into,34.1.1.2,25.1.1] n(x+n(y))+y=n(n(y)+x)+y.

given clause #46: (wt=18) 36 [para_from,6.1.1,4.1.1.1,flip.1] n(x+n(y))+n(n(x)+n(y))+z=y+z.

given clause #47: (wt=15) 1499 [copy,1481,flip.1] n(n(x)+y)+y=n(x+n(y))+x.

given clause #48: (wt=15) 1500 [copy,1487,flip.1] n(n(x)+y)+x=n(y+n(x))+x.

given clause #49: (wt=15) 1611 [para_into,1481.1.1.1.1,3.1.1] n(n(x)+y)+y=n(n(y)+x)+x.

given clause #50: (wt=15) 1639 [para_into,1481.1.1,3.1.1] x+n(x+n(y))=n(n(x)+y)+y.

given clause #51: (wt=18) 39 [para_into,10.1.1.2,6.1.1,flip.1] n(n(x)+n(y))+z+n(x+n(y))=z+y.

given clause #52: (wt=15) 1668 [copy,1639,flip.1] n(n(x)+y)+y=x+n(x+n(y)).

given clause #53: (wt=15) 1845 [para_into,1484.1.1,1481.1.1] n(n(x)+y)+y=n(y+n(x))+y.

given clause #54: (wt=15) 1873 [para_into,1484.1.1,3.1.1] x+n(x+n(y))=n(y+n(x))+y.

given clause #55: (wt=15) 1876 [copy,1845,flip.1] n(x+n(y))+x=n(n(y)+x)+x.

given clause #56: (wt=22) 56 [para_into,25.1.1.1.1,25.1.1] n(x)+n(n(n(n(y)+n(x)))+n(n(x)+y))=n(x)+y.

given clause #57: (wt=15) 1904 [copy,1873,flip.1] n(x+n(y))+x=y+n(y+n(x)).

Resetting weight limit to 19.

sos_size=3453

given clause #58: (wt=15) 2085 [para_into,1487.1.1,3.1.1] x+n(y+n(x))=n(n(x)+y)+x.

given clause #59: (wt=15) 2117 [copy,2085,flip.1] n(n(x)+y)+x=x+n(y+n(x)).

given clause #60: (wt=15) 2320 [para_into,36.1.1.2,202.1.1] n(x+n(y))+x=y+n(n(x)+y).

given clause #61: (wt=18) 58 [para_into,25.1.1.1.1,17.1.1] n(x+y+n(z))+n(n(y+x)+n(z))=z.

given clause #62: (wt=15) 2321 [para_into,36.1.1.2,74.1.1] n(x+n(y))+y=y+n(n(y)+x).

given clause #63: (wt=15) 2343 [copy,2320,flip.1] x+n(n(y)+x)=n(y+n(x))+y.

given clause #64: (wt=15) 2344 [copy,2321,flip.1] x+n(n(x)+y)=n(y+n(x))+x.

given clause #65: (wt=15) 2973 [para_into,1611.1.1,3.1.1] x+n(n(y)+x)=n(n(x)+y)+y.

given clause #66: (wt=18) 60 [para_into,25.1.1.1.1,13.1.1] n(n(x)+y+z)+n(n(z+y)+n(x))=x.

given clause #67: (wt=15) 3033 [copy,2973,flip.1] n(n(x)+y)+y=x+n(n(y)+x).

given clause #68: (wt=15) 3399 [para_into,1668.1.1,1611.1.1] n(n(x)+y)+y=y+n(y+n(x)).

given clause #69: (wt=15) 3427 [para_into,1668.1.1,3.1.1] x+n(n(y)+x)=y+n(y+n(x)).

given clause #70: (wt=15) 3457 [copy,3399,flip.1] x+n(x+n(y))=n(n(y)+x)+x.

given clause #71: (wt=18) 62 [para_into,25.1.1.1.1,10.1.1] n(x+n(y)+z)+n(n(z+x)+n(y))=y.

given clause #72: (wt=15) 3485 [copy,3427,flip.1] x+n(x+n(y))=y+n(n(x)+y).

given clause #73: (wt=15) 3721 [para_into,1845.1.1,3.1.1] x+n(n(y)+x)=n(x+n(y))+x.

given clause #74: (wt=15) 3776 [copy,3721,flip.1] n(x+n(y))+x=x+n(n(y)+x).

given clause #75: (wt=15) 4441 [para_into,1904.1.1,3.1.1] x+n(x+n(y))=y+n(y+n(x)).

given clause #76: (wt=18) 64 [para_into,25.1.1.1.1,8.1.1] n(x+n(y)+z)+n(n(x+z)+n(y))=y.

given clause #77: (wt=15) 4464 [para_into,2117.1.1,3.1.1] x+n(n(x)+y)=x+n(y+n(x)).

given clause #78: (wt=15) 4470 [copy,4464,flip.1] x+n(y+n(x))=x+n(n(x)+y).

given clause #79: (wt=15) 4481 [para_into,2320.1.1,1904.1.1] x+n(x+n(y))=x+n(n(y)+x).

given clause #80: (wt=15) 4484 [copy,4481,flip.1] x+n(n(y)+x)=x+n(x+n(y)).

given clause #81: (wt=22) 66 [para_into,25.1.1.1.1,6.1.1] n(x)+n(n(n(n(y)+n(x)))+n(y+n(x)))=y+n(x).

given clause #82: (wt=15) 4520 [para_into,3033.1.1,3.1.1] x+n(n(y)+x)=y+n(n(x)+y).

given clause #83: (wt=17) 1477 [para_into,34.1.1.2,202.1.1,flip.1] n(n(x)+n(n(y)))+y=n(x+n(y))+x.

given clause #84: (wt=17) 1479 [para_into,34.1.1.2,133.1.1] n(x+n(y))+y=n(n(y)+n(n(x)))+y.

given clause #85: (wt=17) 1482 [para_into,34.1.1.2,31.1.1,flip.1] n(n(n(x))+n(y))+y=n(x+n(y))+y.

given clause #86: (wt=21) 68 [para_into,25.1.1.2.1,25.1.1] n(n(n(x)+n(y))+n(y)+x)+n(y)=n(x)+n(y).

given clause #87: (wt=17) 2322 [para_into,36.1.1.2,72.1.1,flip.1] x+n(n(y)+n(n(x)))=n(y+n(x))+y.

given clause #88: (wt=17) 2330 [para_into,36.1.1.2,29.1.1] n(x+n(y))+y=y+n(n(y)+n(n(x))).

given clause #89: (wt=17) 2331 [para_into,36.1.1.2,25.1.1] n(x+n(y))+x=y+n(n(n(y))+n(x)).

given clause #90: (wt=17) 2338 [para_into,36.1.1.2,6.1.1,flip.1] x+n(n(n(y))+n(x))=n(y+n(x))+x.

given clause #91: (wt=21) 70 [para_into,25.1.1.2.1,6.1.1] n(n(n(x)+n(y))+x+n(y))+n(y)=n(x)+n(y).

given clause #92: (wt=17) 3302 [para_into,39.1.1.2,202.1.1,demod,1478] n(n(n(x))+n(y))+x=n(x+n(y))+x.

given clause #93: (wt=17) 4577 [para_into,1479.1.1.1.1,3.1.1,flip.1] n(n(x)+n(n(y)))+x=n(n(x)+y)+x.

given clause #94: (wt=17) 4579 [para_into,2330.1.1.1.1,3.1.1,flip.1] x+n(n(x)+n(n(y)))=n(n(x)+y)+x.

given clause #95: (wt=17) 4581 [para_into,2331.1.1.1.1,3.1.1,flip.1] x+n(n(n(x))+n(y))=n(n(x)+y)+y.

given clause #96: (wt=21) 76 [para_from,25.1.1,6.1.1.2.1,demod,5] n(n(x)+y+n(n(y)+n(x)))+n(x)=n(y)+n(x).

given clause #97: (wt=18) 81 [para_from,25.1.1,10.1.1.2,flip.1] n(n(x)+n(y))+z+n(n(y)+x)=z+y.

given clause #98: (wt=18) 84 [para_from,25.1.1,8.1.1.2,flip.1] n(n(x)+y)+z+n(n(y)+n(x))=z+x.

given clause #99: (wt=18) 86 [para_from,25.1.1,4.1.1.1,flip.1] n(n(x)+y)+n(n(y)+n(x))+z=x+z.

given clause #100: (wt=18) 125 [para_into,29.1.1.1.1,4.1.1] n(x+y+n(z))+n(n(z)+n(x+y))=z.

given clause #101: (wt=23) 78 [para_from,25.1.1,6.1.1.1.1] n(x)+n(n(n(n(x)+y))+n(n(y)+n(x)))=n(y)+n(x).

given clause #102: (wt=18) 146 [para_from,29.1.1,10.1.1.2,flip.1] n(n(x)+n(y))+z+n(y+n(x))=z+x.

given clause #103: (wt=9) 4622 [para_into,146.1.1.2,3721.1.1,demod,4576] n(x)+x=n(y)+y.

given clause #104: (wt=5) 4723 [para_from,4622.1.1,133.1.1.2.1,demod,4722] n(n(x))=x.

given clause #105: (wt=9) 4654 [para_into,4622.1.1,3.1.1] x+n(x)=n(y)+y.

given clause #106: (wt=22) 89 [para_into,11.1.1.2.2,25.1.1,flip.1] n(n(x)+y)+z+u+n(n(y)+n(x))=z+u+x.

given clause #107: (wt=9) 4682 [copy,4654,flip.1] n(x)+x=y+n(y).

given clause #108: (wt=9) 5005 [back_demod,4820,demod,4956] x+n(x)=y+n(y).

given clause #109: (wt=13) 4644 [para_into,4622.1.1,17.1.1] x+y+n(y+x)=n(z)+z.

given clause #110: (wt=13) 4648 [para_into,4622.1.1,13.1.1] n(x+y)+y+x=n(z)+z.

given clause #111: (wt=19) 91 [para_into,11.1.1.2.2,17.1.1] x+y+z+u+v=v+x+y+u+z.

given clause #112: (wt=12) 5207 [para_into,4648.1.1.1.1,5005.1.1,demod,4708] x+n(x)+n(x)=n(y)+y.

given clause #113: (wt=11) 5225 [para_into,5207.1.1.2.1,4723.1.1,demod,4724] n(x)+x+x=n(y)+y.

given clause #114: (wt=11) 5229 [copy,5225,flip.1] n(x)+x=n(y)+y+y.

given clause #115: (wt=11) 5304 [para_into,5225.1.1,17.1.1] x+x+n(x)=n(y)+y.

given clause #116: (wt=19) 92 [para_into,11.1.1.2.2,13.1.1] x+y+z+u+v=z+x+y+v+u.

given clause #117: (wt=11) 5411 [para_into,5229.1.1.1,4723.1.1] x+n(x)=n(y)+y+y.

Resetting weight limit to 16.

sos_size=3686

given clause #118: (wt=11) 5440 [copy,5411,flip.1] n(x)+x+x=y+n(y).

given clause #119: (wt=11) 5588 [para_into,5304.1.1.2,5005.1.1] x+y+n(y)=n(z)+z.

given clause #120: (wt=11) 5589 [para_into,5304.1.1.2,4654.1.1] x+n(y)+y=n(z)+z.

given clause #121: (wt=23) 93 [para_into,11.1.1.2.2,11.1.1] x+y+z+u+v+w=u+x+y+v+z+w.

given clause #122: (wt=11) 5590 [copy,5588,flip.1] n(x)+x=y+z+n(z).

given clause #123: (wt=11) 5591 [copy,5589,flip.1] n(x)+x=y+n(z)+z.

given clause #124: (wt=11) 5630 [para_into,5588.1.1,17.1.1] n(x)+x+y=n(z)+z.

given clause #125: (wt=11) 5631 [para_into,5588.1.1,10.1.1] n(x)+y+x=n(z)+z.

given clause #126: (wt=19) 94 [para_into,11.1.1.2.2,10.1.1] x+y+z+u+v=u+x+y+v+z.

given clause #127: (wt=11) 5632 [para_into,5588.1.1,9.1.1] x+n(x)+y=n(z)+z.

given clause #128: (wt=11) 5633 [para_into,5588.1.1,8.1.1] x+y+n(x)=n(z)+z.

given clause #129: (wt=11) 5641 [copy,5630,flip.1] n(x)+x=n(y)+y+z.

given clause #130: (wt=11) 5642 [copy,5631,flip.1] n(x)+x=n(y)+z+y.

given clause #131: (wt=19) 95 [para_into,11.1.1.2.2,9.1.1] x+y+z+u+v=v+x+y+z+u.

given clause #132: (wt=11) 5643 [copy,5632,flip.1] n(x)+x=y+n(y)+z.

given clause #133: (wt=11) 5644 [copy,5633,flip.1] n(x)+x=y+z+n(y).

given clause #134: (wt=11) 5750 [para_into,5590.1.1.1,4723.1.1] x+n(x)=y+z+n(z).

given clause #135: (wt=11) 5757 [copy,5750,flip.1] x+y+n(y)=z+n(z).

given clause #136: (wt=19) 96 [para_into,11.1.1.2.2,8.1.1] x+y+z+u+v=u+x+y+z+v.

given clause #137: (wt=11) 5773 [para_into,5591.1.1.1,4723.1.1] x+n(x)=y+n(z)+z.

Resetting weight limit to 15.

sos_size=3852

given clause #138: (wt=11) 5781 [copy,5773,flip.1] x+n(y)+y=z+n(z).

given clause #139: (wt=11) 5838 [para_into,5641.1.1.1,4723.1.1] x+n(x)=n(y)+y+z.

given clause #140: (wt=11) 5847 [copy,5838,flip.1] n(x)+x+y=z+n(z).

given clause #141: (wt=22) 97 [para_into,11.1.1.2.2,6.1.1,flip.1] n(x+n(y))+z+u+n(n(x)+n(y))=z+u+y.

given clause #142: (wt=11) 5865 [para_into,5642.1.1.1,4723.1.1] x+n(x)=n(y)+z+y.

given clause #143: (wt=11) 5875 [copy,5865,flip.1] n(x)+y+x=z+n(z).

given clause #144: (wt=11) 5894 [para_into,5643.1.1.1,4723.1.1] x+n(x)=y+n(y)+z.

given clause #145: (wt=11) 5905 [copy,5894,flip.1] x+n(x)+y=z+n(z).

given clause #146: (wt=19) 99 [para_into,11.1.1.2.2,4.1.1,demod,5] x+y+z+u+v=z+u+x+y+v.

given clause #147: (wt=11) 5925 [para_into,5644.1.1.1,4723.1.1] x+n(x)=y+z+n(y).

given clause #148: (wt=11) 5937 [copy,5925,flip.1] x+y+n(x)=z+n(z).

given clause #149: (wt=13) 4651 [para_into,4622.1.1,10.1.1] x+n(y+x)+y=n(z)+z.

given clause #150: (wt=13) 4652 [para_into,4622.1.1,9.1.1] x+y+n(x+y)=n(z)+z.

given clause #151: (wt=19) 100 [para_into,11.1.1.2,11.1.1] x+y+z+u+v=u+x+z+y+v.

given clause #152: (wt=13) 4653 [para_into,4622.1.1,8.1.1] x+n(x+y)+y=n(z)+z.

given clause #153: (wt=13) 4672 [copy,4644,flip.1] n(x)+x=y+z+n(z+y).

given clause #154: (wt=13) 4676 [copy,4648,flip.1] n(x)+x=n(y+z)+z+y.

given clause #155: (wt=13) 4679 [copy,4651,flip.1] n(x)+x=y+n(z+y)+z.

given clause #156: (wt=19) 101 [copy,91,flip.1] x+y+z+u+v=y+z+v+u+x.

given clause #157: (wt=13) 4680 [copy,4652,flip.1] n(x)+x=y+z+n(y+z).

given clause #158: (wt=13) 4681 [copy,4653,flip.1] n(x)+x=y+n(y+z)+z.

given clause #159: (wt=13) 4769 [para_from,4622.1.1,202.1.1.1.1,demod,4724] n(n(x)+x)+n(y+y)=n(y).

given clause #160: (wt=13) 4773 [para_from,4622.1.1,72.1.1.2.1,demod,4724] n(x+x)+n(n(y)+y)=n(x).

given clause #161: (wt=19) 102 [copy,92,flip.1] x+y+z+u+v=y+z+x+v+u.

given clause #162: (wt=13) 4932 [para_from,4723.1.1,3399.1.1.1.1.1,demod,4724] n(x+y)+y=y+n(y+x).

given clause #163: (wt=13) 4936 [para_from,4723.1.1,1845.1.1.1.1.1,demod,4724] n(x+y)+y=n(y+x)+y.

given clause #164: (wt=13) 4943 [para_from,4723.1.1,202.1.1.2.1.1,demod,4724] n(x+n(y))+n(x+y)=n(x).

given clause #165: (wt=13) 4949 [para_from,4723.1.1,72.1.1.1.1.1,demod,4724] n(x+y)+n(x+n(y))=n(x).

given clause #166: (wt=23) 103 [copy,93,flip.1] x+y+z+u+v+w=y+z+v+x+u+w.

given clause #167: (wt=13) 4951 [para_from,4723.1.1,25.1.1.1.1.1,demod,4724] n(x+y)+n(n(y)+x)=n(x).

given clause #168: (wt=13) 4957 [para_from,4723.1.1,133.1.1.2.1.2,demod,4724] n(x+n(y))+n(y+x)=n(x).

given clause #169: (wt=13) 4964 [para_from,4723.1.1,4484.1.1.2.1.1,demod,4724] x+n(y+x)=x+n(x+y).

given clause #170: (wt=13) 4965 [para_from,4723.1.1,3721.1.1.2.1.1,demod,4724] x+n(y+x)=n(x+y)+x.

given clause #171: (wt=19) 104 [copy,94,flip.1] x+y+z+u+v=y+z+v+x+u.

given clause #172: (wt=13) 4969 [para_from,4723.1.1,74.1.1.2.1.1,demod,4724] n(n(x)+y)+n(y+x)=n(y).

given clause #173: (wt=13) 4977 [para_from,4723.1.1,29.1.1.2.1.1,demod,4724] n(x+y)+n(y+n(x))=n(y).

given clause #174: (wt=13) 4985 [para_from,4723.1.1,31.1.1.1.1.2,demod,4724] n(n(x)+y)+n(x+y)=n(y).

given clause #175: (wt=13) 4987 [para_from,4723.1.1,6.1.1.2.1.2,demod,4724] n(x+y)+n(n(x)+y)=n(y).

given clause #176: (wt=19) 105 [copy,95,flip.1] x+y+z+u+v=y+z+u+v+x.

given clause #177: (wt=13) 4989 [para_from,4723.1.1,4481.1.1.2.1.2,demod,4724] x+n(x+y)=x+n(y+x).

given clause #178: (wt=13) 4990 [para_from,4723.1.1,4441.1.1.2.1.2,demod,4938] x+n(x+y)=n(y+x)+x.

given clause #179: (wt=13) 4991 [para_from,4723.1.1,3776.1.1.1.1.2,demod,4724] n(x+y)+x=x+n(y+x).

given clause #180: (wt=13) 4995 [para_from,4723.1.1,1904.1.1.1.1.2,demod,4938] n(x+y)+x=n(y+x)+x.

given clause #181: (wt=19) 106 [copy,96,flip.1] x+y+z+u+v=y+z+u+x+v.

given clause #182: (wt=13) 5034 [para_into,4682.1.1,17.1.1] x+y+n(y+x)=z+n(z).

given clause #183: (wt=13) 5038 [para_into,4682.1.1,13.1.1] n(x+y)+y+x=z+n(z).

given clause #184: (wt=13) 5041 [para_into,4682.1.1,10.1.1] x+n(y+x)+y=z+n(z).

given clause #185: (wt=13) 5042 [para_into,4682.1.1,9.1.1] x+y+n(x+y)=z+n(z).

given clause #186: (wt=19) 107 [copy,100,flip.1] x+y+z+u+v=y+u+z+x+v.

given clause #187: (wt=13) 5043 [para_into,4682.1.1,8.1.1] x+n(x+y)+y=z+n(z).

given clause #188: (wt=13) 5061 [copy,5034,flip.1] x+n(x)=y+z+n(z+y).

given clause #189: (wt=13) 5065 [copy,5038,flip.1] x+n(x)=n(y+z)+z+y.

given clause #190: (wt=13) 5068 [copy,5041,flip.1] x+n(x)=y+n(z+y)+z.

given clause #191: (wt=22) 108 [para_from,11.1.1,25.1.1.1.1] n(x+n(y)+z+u)+n(n(z+x+u)+n(y))=y.

given clause #192: (wt=13) 5069 [copy,5042,flip.1] x+n(x)=y+z+n(y+z).

given clause #193: (wt=13) 5070 [copy,5043,flip.1] x+n(x)=y+n(y+z)+z.

given clause #194: (wt=13) 5634 [para_into,5588.1.1,4.1.1] x+y+z+n(z)=n(u)+u.

given clause #195: (wt=13) 5645 [copy,5634,flip.1] n(x)+x=y+z+u+n(u).

given clause #196: (wt=19) 110 [para_from,11.1.1,17.1.1.2,demod,5,5] x+y+z+u+v=u+y+v+z+x.

given clause #197: (wt=13) 5719 [para_into,5589.1.1,4.1.1] x+y+n(z)+z=n(u)+u.

given clause #198: (wt=13) 5745 [copy,5719,flip.1] n(x)+x=y+z+n(u)+u.

given clause #199: (wt=13) 5751 [para_into,5590.1.1,5590.1.1] x+y+n(y)=z+u+n(u).

given clause #200: (wt=13) 5774 [para_into,5591.1.1,5591.1.1] x+n(y)+y=z+n(u)+u.

given clause #201: (wt=19) 111 [para_from,11.1.1,13.1.1.2,demod,5,5] x+y+z+u+v=x+u+y+v+z.

given clause #202: (wt=13) 5775 [para_into,5591.1.1,5590.1.1] x+y+n(y)=z+n(u)+u.

given clause #203: (wt=13) 5782 [copy,5775,flip.1] x+n(y)+y=z+u+n(u).

given clause #204: (wt=13) 5801 [para_into,5630.1.1.2,17.1.1] n(x)+y+z+x=n(u)+u.

given clause #205: (wt=13) 5802 [para_into,5630.1.1.2,10.1.1] n(x)+y+x+z=n(u)+u.

given clause #206: (wt=19) 112 [para_from,11.1.1,10.1.1.2,demod,5,5] x+y+z+u+v=u+y+v+x+z.

given clause #207: (wt=13) 5804 [para_into,5630.1.1,55.1.1] x+y+n(y)+z=n(u)+u.

given clause #208: (wt=13) 5805 [para_into,5630.1.1,51.1.1] x+n(y)+z+y=n(u)+u.

given clause #209: (wt=13) 5806 [para_into,5630.1.1,48.1.1] x+y+z+n(x)=n(u)+u.

given clause #210: (wt=13) 5807 [para_into,5630.1.1,38.1.1] x+y+n(x)+z=n(u)+u.

given clause #211: (wt=19) 113 [para_from,11.1.1,9.1.1.2,demod,5,5] x+y+z+u+v=z+u+y+v+x.

given clause #212: (wt=13) 5808 [para_into,5630.1.1,20.1.1] x+n(y)+y+z=n(u)+u.

given clause #213: (wt=13) 5809 [para_into,5630.1.1,15.1.1] x+y+z+n(y)=n(u)+u.

given clause #214: (wt=13) 5813 [copy,5801,flip.1] n(x)+x=n(y)+z+u+y.

given clause #215: (wt=13) 5814 [copy,5802,flip.1] n(x)+x=n(y)+z+y+u.

given clause #216: (wt=19) 114 [para_from,11.1.1,8.1.1.2] x+y+z+u+v=z+x+u+y+v.

given clause #217: (wt=13) 5816 [copy,5804,flip.1] n(x)+x=y+z+n(z)+u.

given clause #218: (wt=13) 5817 [copy,5805,flip.1] n(x)+x=y+n(z)+u+z.

given clause #219: (wt=13) 5818 [copy,5806,flip.1] n(x)+x=y+z+u+n(y).

given clause #220: (wt=13) 5819 [copy,5807,flip.1] n(x)+x=y+z+n(y)+u.

given clause #221: (wt=19) 115 [copy,110,flip.1] x+y+z+u+v=v+y+u+x+z.

given clause #222: (wt=13) 5820 [copy,5808,flip.1] n(x)+x=y+n(z)+z+u.

given clause #223: (wt=13) 5821 [copy,5809,flip.1] n(x)+x=y+z+u+n(z).

given clause #224: (wt=13) 5839 [para_into,5641.1.1,5641.1.1] n(x)+x+y=n(z)+z+u.

given clause #225: (wt=13) 5840 [para_into,5641.1.1,5591.1.1] x+n(y)+y=n(z)+z+u.

given clause #226: (wt=19) 116 [copy,111,flip.1] x+y+z+u+v=x+z+v+y+u.

given clause #227: (wt=13) 5841 [para_into,5641.1.1,5590.1.1] x+y+n(y)=n(z)+z+u.

given clause #228: (wt=13) 5848 [copy,5840,flip.1] n(x)+x+y=z+n(u)+u.

given clause #229: (wt=13) 5849 [copy,5841,flip.1] n(x)+x+y=z+u+n(u).

given clause #230: (wt=13) 5866 [para_into,5642.1.1,5642.1.1] n(x)+y+x=n(z)+u+z.

given clause #231: (wt=19) 117 [copy,113,flip.1] x+y+z+u+v=v+z+x+y+u.

given clause #232: (wt=13) 5867 [para_into,5642.1.1,5641.1.1] n(x)+x+y=n(z)+u+z.

given clause #233: (wt=13) 5868 [para_into,5642.1.1,5591.1.1] x+n(y)+y=n(z)+u+z.

given clause #234: (wt=13) 5869 [para_into,5642.1.1,5590.1.1] x+y+n(y)=n(z)+u+z.

given clause #235: (wt=13) 5876 [copy,5867,flip.1] n(x)+y+x=n(z)+z+u.

given clause #236: (wt=19) 118 [copy,114,flip.1] x+y+z+u+v=y+u+x+z+v.

given clause #237: (wt=13) 5877 [copy,5868,flip.1] n(x)+y+x=z+n(u)+u.

given clause #238: (wt=13) 5878 [copy,5869,flip.1] n(x)+y+x=z+u+n(u).

given clause #239: (wt=13) 5895 [para_into,5643.1.1,5643.1.1] x+n(x)+y=z+n(z)+u.

given clause #240: (wt=13) 5896 [para_into,5643.1.1,5642.1.1] n(x)+y+x=z+n(z)+u.

given clause #241: (wt=20) 127 [para_into,29.1.1.2.1,29.1.1,demod,5] n(n(x)+n(y)+n(y+n(x)))+n(x)=y+n(x).

given clause #242: (wt=11) 6276 [para_into,127.1.1.1.1,5847.1.1,demod,4724,4724] n(x+n(x))+y=y+y.

----> UNIT CONFLICT at  52.60 sec ----> 6344 [binary,6342.1,1.1] $F.

Length of proof is 56.  Level of proof is 22.

---------------- PROOF ----------------

1 [] a+a!=a.
3 [] x+y=y+x.
5,4 [] (x+y)+z=x+y+z.
6 [] n(x+n(y))+n(n(x)+n(y))=y.
8 [para_into,4.1.1.1,3.1.1,demod,5] x+y+z=y+x+z.
9 [para_into,4.1.1,3.1.1] x+y+z=y+z+x.
10 [copy,9,flip.1] x+y+z=z+x+y.
13 [para_into,8.1.1,3.1.1,demod,5] x+y+z=x+z+y.
17 [para_into,9.1.1.2,3.1.1] x+y+z=z+y+x.
25 [para_into,6.1.1.1.1,3.1.1] n(n(x)+y)+n(n(y)+n(x))=x.
29 [para_into,6.1.1.2.1,3.1.1] n(x+n(y))+n(n(y)+n(x))=y.
34 [para_from,6.1.1,8.1.1.2,flip.1] n(x+n(y))+z+n(n(x)+n(y))=z+y.
36 [para_from,6.1.1,4.1.1.1,flip.1] n(x+n(y))+n(n(x)+n(y))+z=y+z.
72 [para_into,25.1.1.2.1,3.1.1] n(n(x)+y)+n(n(x)+n(y))=x.
127 [para_into,29.1.1.2.1,29.1.1,demod,5] n(n(x)+n(y)+n(y+n(x)))+n(x)=y+n(x).
133 [para_into,29.1.1,3.1.1] n(n(x)+n(y))+n(y+n(x))=x.
146 [para_from,29.1.1,10.1.1.2,flip.1] n(n(x)+n(y))+z+n(y+n(x))=z+x.
202 [para_into,72.1.1,3.1.1] n(n(x)+n(y))+n(n(x)+y)=x.
1477 [para_into,34.1.1.2,202.1.1,flip.1] n(n(x)+n(n(y)))+y=n(x+n(y))+x.
1481 [para_into,34.1.1.2,72.1.1] n(x+n(y))+x=n(n(x)+y)+y.
1484 [para_into,34.1.1.2,29.1.1] n(x+n(y))+x=n(y+n(x))+y.
1487 [para_into,34.1.1.2,25.1.1] n(x+n(y))+y=n(n(y)+x)+y.
1611 [para_into,1481.1.1.1.1,3.1.1] n(n(x)+y)+y=n(n(y)+x)+x.
1845 [para_into,1484.1.1,1481.1.1] n(n(x)+y)+y=n(y+n(x))+y.
1873 [para_into,1484.1.1,3.1.1] x+n(x+n(y))=n(y+n(x))+y.
1904 [copy,1873,flip.1] n(x+n(y))+x=y+n(y+n(x)).
2085 [para_into,1487.1.1,3.1.1] x+n(y+n(x))=n(n(x)+y)+x.
2117 [copy,2085,flip.1] n(n(x)+y)+x=x+n(y+n(x)).
2973 [para_into,1611.1.1,3.1.1] x+n(n(y)+x)=n(n(x)+y)+y.
3033 [copy,2973,flip.1] n(n(x)+y)+y=x+n(n(y)+x).
3721 [para_into,1845.1.1,3.1.1] x+n(n(y)+x)=n(x+n(y))+x.
4441 [para_into,1904.1.1,3.1.1] x+n(x+n(y))=y+n(y+n(x)).
4521 [para_from,3033.1.1,36.1.1.2] n(x+n(y))+x+n(n(n(y))+x)=y+n(y).
4576,4575 [para_from,1477.1.1,36.1.1.2] n(x+n(n(y)))+n(x+n(y))+x=n(y)+y.
4622 [para_into,146.1.1.2,3721.1.1,demod,4576] n(x)+x=n(y)+y.
4648 [para_into,4622.1.1,13.1.1] n(x+y)+y+x=n(z)+z.
4708,4707 [para_from,4622.1.1,36.1.1.2] n(x+n(y))+n(z)+z=y+n(x)+n(y).
4722,4721 [para_from,4622.1.1,29.1.1.2.1] n(x+n(n(x)))+n(n(y)+y)=n(x).
4724,4723 [para_from,4622.1.1,133.1.1.2.1,demod,4722] n(n(x))=x.
4769 [para_from,4622.1.1,202.1.1.1.1,demod,4724] n(n(x)+x)+n(y+y)=n(y).
4820 [back_demod,4521,demod,4724] n(x+n(y))+x+n(y+x)=y+n(y).
4956,4955 [para_from,4723.1.1,146.1.1.2.2.1.2,demod,4724] n(x+n(y))+z+n(y+x)=z+n(x).
5005 [back_demod,4820,demod,4956] x+n(x)=y+n(y).
5207 [para_into,4648.1.1.1.1,5005.1.1,demod,4708] x+n(x)+n(x)=n(y)+y.
5225 [para_into,5207.1.1.2.1,4723.1.1,demod,4724] n(x)+x+x=n(y)+y.
5240 [para_from,5207.1.1,2117.1.1.1.1,demod,4724,4724,5] n(n(x)+x)+y=y+n(y+y+n(y)).
5267 [copy,5240,flip.1] x+n(x+x+n(x))=n(n(y)+y)+x.
5304 [para_into,5225.1.1,17.1.1] x+x+n(x)=n(y)+y.
5588 [para_into,5304.1.1.2,5005.1.1] x+y+n(y)=n(z)+z.
5630 [para_into,5588.1.1,17.1.1] n(x)+x+y=n(z)+z.
5641 [copy,5630,flip.1] n(x)+x=n(y)+y+z.
5838 [para_into,5641.1.1.1,4723.1.1] x+n(x)=n(y)+y+z.
5847 [copy,5838,flip.1] n(x)+x+y=z+n(z).
6105,6104 [para_into,4769.1.1.1.1.1,4723.1.1] n(x+n(x))+n(y+y)=n(y).
6276 [para_into,127.1.1.1.1,5847.1.1,demod,4724,4724] n(x+n(x))+y=y+y.
6279 [para_into,127.1.1.1.1,5630.1.1,demod,4724,4724] n(n(x)+x)+y=y+y.
6287 [copy,6279,flip.1] x+x=n(n(y)+y)+x.
6319,6318 [para_from,6276.1.1,4441.1.1.2.1,demod,6105,4724,4724,flip.1] x+n(x+y+n(y))=x.
6333,6332 [back_demod,5267,demod,6319,flip.1] n(n(x)+x)+y=y.
6342 [back_demod,6287,demod,6333] x+x=x.
6344 [binary,6342.1,1.1] $F.

------------ end of proof -------------


Proof object:
(
(1 (input) ((not (= (+ (a) (a)) (a)))))
(2 (input) ((= (+ v0 v1) (+ v1 v0))))
(3 (input) ((= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2)))))
(4 (input) ((= (+ (n (+ v0 (n v1))) (n (+ (n v0) (n v1)))) v1)))
(5 (instantiate 2 ((v0 . v64)(v1 . v65))) ((= (+ v64 v65) (+ v65 v64))))
(6 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ (+ v64 v65) v66) (+ v64 (+ v65 v66)))))
(7 (paramod 5 (1 1) 6 (1 1 1)) ((= (+ (+ v65 v64) v66) (+ v64 (+ v65 v66)))))
(8 (instantiate 3 ((v0 . v65)(v1 . v64)(v2 . v66))) ((= (+ (+ v65 v64) v66) (+ v65 (+ v64 v66)))))
(9 (paramod 8 (1 1) 7 (1 1)) ((= (+ v65 (+ v64 v66)) (+ v64 (+ v65 v66)))))
(10 (instantiate 9 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (+ v0 (+ v1 v2)) (+ v1 (+ v0 v2)))))
(11 (instantiate 2 ((v0 . (+ v64 v65))(v1 . v66))) ((= (+ (+ v64 v65) v66) (+ v66 (+ v64 v65)))))
(12 (instantiate 3 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ (+ v64 v65) v66) (+ v64 (+ v65 v66)))))
(13 (paramod 11 (1 1) 12 (1 1)) ((= (+ v66 (+ v64 v65)) (+ v64 (+ v65 v66)))))
(14 (instantiate 13 ((v64 . v1)(v65 . v2)(v66 . v0))) ((= (+ v0 (+ v1 v2)) (+ v1 (+ v2 v0)))))
(15 (flip 14 (1)) ((= (+ v1 (+ v2 v0)) (+ v0 (+ v1 v2)))))
(16 (instantiate 2 ((v0 . v64)(v1 . (+ v65 v66)))) ((= (+ v64 (+ v65 v66)) (+ (+ v65 v66) v64))))
(17 (instantiate 10 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (+ v65 v66)) (+ v65 (+ v64 v66)))))
(18 (paramod 16 (1 1) 17 (1 1)) ((= (+ (+ v65 v66) v64) (+ v65 (+ v64 v66)))))
(19 (instantiate 3 ((v0 . v65)(v1 . v66)(v2 . v64))) ((= (+ (+ v65 v66) v64) (+ v65 (+ v66 v64)))))
(20 (paramod 19 (1 1) 18 (1 1)) ((= (+ v65 (+ v66 v64)) (+ v65 (+ v64 v66)))))
(21 (instantiate 20 ((v64 . v2)(v65 . v0)(v66 . v1))) ((= (+ v0 (+ v1 v2)) (+ v0 (+ v2 v1)))))
(22 (instantiate 2 ((v0 . v65)(v1 . v66))) ((= (+ v65 v66) (+ v66 v65))))
(23 (instantiate 14 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (+ v65 v66)) (+ v65 (+ v66 v64)))))
(24 (paramod 22 (1 1) 23 (1 1 2)) ((= (+ v64 (+ v66 v65)) (+ v65 (+ v66 v64)))))
(25 (instantiate 24 ((v64 . v0)(v65 . v2)(v66 . v1))) ((= (+ v0 (+ v1 v2)) (+ v2 (+ v1 v0)))))
(26 (instantiate 2 ((v0 . v64)(v1 . (n v65)))) ((= (+ v64 (n v65)) (+ (n v65) v64))))
(27 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) (n (+ (n v64) (n v65)))) v65)))
(28 (paramod 26 (1 1) 27 (1 1 1 1)) ((= (+ (n (+ (n v65) v64)) (n (+ (n v64) (n v65)))) v65)))
(29 (instantiate 28 ((v64 . v1)(v65 . v0))) ((= (+ (n (+ (n v0) v1)) (n (+ (n v1) (n v0)))) v0)))
(30 (instantiate 2 ((v0 . (n v64))(v1 . (n v65)))) ((= (+ (n v64) (n v65)) (+ (n v65) (n v64)))))
(31 (instantiate 4 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) (n (+ (n v64) (n v65)))) v65)))
(32 (paramod 30 (1 1) 31 (1 1 2 1)) ((= (+ (n (+ v64 (n v65))) (n (+ (n v65) (n v64)))) v65)))
(33 (instantiate 32 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) (n (+ (n v1) (n v0)))) v1)))
(34 (instantiate 10 ((v0 . v64)(v1 . (n (+ v0 (n v1))))(v2 . (n (+ (n v0) (n v1)))))) ((= (+ v64 (+ (n (+ v0 (n v1))) (n (+ (n v0) (n v1))))) (+ (n (+ v0 (n v1))) (+ v64 (n (+ (n v0) (n v1))))))))
(35 (paramod 4 (1 1) 34 (1 1 2)) ((= (+ v64 v1) (+ (n (+ v0 (n v1))) (+ v64 (n (+ (n v0) (n v1))))))))
(36 (flip 35 (1)) ((= (+ (n (+ v0 (n v1))) (+ v64 (n (+ (n v0) (n v1))))) (+ v64 v1))))
(37 (instantiate 36 ((v64 . v2))) ((= (+ (n (+ v0 (n v1))) (+ v2 (n (+ (n v0) (n v1))))) (+ v2 v1))))
(38 (instantiate 3 ((v0 . (n (+ v0 (n v1))))(v1 . (n (+ (n v0) (n v1))))(v2 . v66))) ((= (+ (+ (n (+ v0 (n v1))) (n (+ (n v0) (n v1)))) v66) (+ (n (+ v0 (n v1))) (+ (n (+ (n v0) (n v1))) v66)))))
(39 (paramod 4 (1 1) 38 (1 1 1)) ((= (+ v1 v66) (+ (n (+ v0 (n v1))) (+ (n (+ (n v0) (n v1))) v66)))))
(40 (flip 39 (1)) ((= (+ (n (+ v0 (n v1))) (+ (n (+ (n v0) (n v1))) v66)) (+ v1 v66))))
(41 (instantiate 40 ((v66 . v2))) ((= (+ (n (+ v0 (n v1))) (+ (n (+ (n v0) (n v1))) v2)) (+ v1 v2))))
(42 (instantiate 2 ((v0 . (n v65))(v1 . (n v64)))) ((= (+ (n v65) (n v64)) (+ (n v64) (n v65)))))
(43 (instantiate 29 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ (n v64) v65)) (n (+ (n v65) (n v64)))) v64)))
(44 (paramod 42 (1 1) 43 (1 1 2 1)) ((= (+ (n (+ (n v64) v65)) (n (+ (n v64) (n v65)))) v64)))
(45 (instantiate 44 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) v1)) (n (+ (n v0) (n v1)))) v0)))
(46 (instantiate 33 ((v0 . (+ (n v1) (n v0)))(v1 . (+ v0 (n v1))))) ((= (+ (n (+ (+ (n v1) (n v0)) (n (+ v0 (n v1))))) (n (+ (n (+ v0 (n v1))) (n (+ (n v1) (n v0)))))) (+ v0 (n v1)))))
(47 (paramod 33 (1 1) 46 (1 1 2 1)) ((= (+ (n (+ (+ (n v1) (n v0)) (n (+ v0 (n v1))))) (n v1)) (+ v0 (n v1)))))
(48 (instantiate 3 ((v0 . (n v1))(v1 . (n v0))(v2 . (n (+ v0 (n v1)))))) ((= (+ (+ (n v1) (n v0)) (n (+ v0 (n v1)))) (+ (n v1) (+ (n v0) (n (+ v0 (n v1))))))))
(49 (paramod 48 (1 1) 47 (1 1 1 1)) ((= (+ (n (+ (n v1) (+ (n v0) (n (+ v0 (n v1)))))) (n v1)) (+ v0 (n v1)))))
(50 (instantiate 49 ((v0 . v1)(v1 . v0))) ((= (+ (n (+ (n v0) (+ (n v1) (n (+ v1 (n v0)))))) (n v0)) (+ v1 (n v0)))))
(51 (instantiate 2 ((v0 . (n (+ v64 (n v65))))(v1 . (n (+ (n v65) (n v64)))))) ((= (+ (n (+ v64 (n v65))) (n (+ (n v65) (n v64)))) (+ (n (+ (n v65) (n v64))) (n (+ v64 (n v65)))))))
(52 (instantiate 33 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) (n (+ (n v65) (n v64)))) v65)))
(53 (paramod 51 (1 1) 52 (1 1)) ((= (+ (n (+ (n v65) (n v64))) (n (+ v64 (n v65)))) v65)))
(54 (instantiate 53 ((v64 . v1)(v65 . v0))) ((= (+ (n (+ (n v0) (n v1))) (n (+ v1 (n v0)))) v0)))
(55 (instantiate 15 ((v0 . (n (+ (n v1) (n v0))))(v1 . v65)(v2 . (n (+ v0 (n v1)))))) ((= (+ v65 (+ (n (+ v0 (n v1))) (n (+ (n v1) (n v0))))) (+ (n (+ (n v1) (n v0))) (+ v65 (n (+ v0 (n v1))))))))
(56 (paramod 33 (1 1) 55 (1 1 2)) ((= (+ v65 v1) (+ (n (+ (n v1) (n v0))) (+ v65 (n (+ v0 (n v1))))))))
(57 (flip 56 (1)) ((= (+ (n (+ (n v1) (n v0))) (+ v65 (n (+ v0 (n v1))))) (+ v65 v1))))
(58 (instantiate 57 ((v0 . v1)(v1 . v0)(v65 . v2))) ((= (+ (n (+ (n v0) (n v1))) (+ v2 (n (+ v1 (n v0))))) (+ v2 v0))))
(59 (instantiate 2 ((v0 . (n (+ (n v64) v65)))(v1 . (n (+ (n v64) (n v65)))))) ((= (+ (n (+ (n v64) v65)) (n (+ (n v64) (n v65)))) (+ (n (+ (n v64) (n v65))) (n (+ (n v64) v65))))))
(60 (instantiate 45 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ (n v64) v65)) (n (+ (n v64) (n v65)))) v64)))
(61 (paramod 59 (1 1) 60 (1 1)) ((= (+ (n (+ (n v64) (n v65))) (n (+ (n v64) v65))) v64)))
(62 (instantiate 61 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) (n v1))) (n (+ (n v0) v1))) v0)))
(63 (instantiate 62 ((v0 . v64)(v1 . (n v65)))) ((= (+ (n (+ (n v64) (n (n v65)))) (n (+ (n v64) (n v65)))) v64)))
(64 (instantiate 37 ((v0 . v64)(v1 . v65)(v2 . (n (+ (n v64) (n (n v65))))))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ (n v64) (n (n v65)))) (n (+ (n v64) (n v65))))) (+ (n (+ (n v64) (n (n v65)))) v65))))
(65 (paramod 63 (1 1) 64 (1 1 2)) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ (n v64) (n (n v65)))) v65))))
(66 (flip 65 (1)) ((= (+ (n (+ (n v64) (n (n v65)))) v65) (+ (n (+ v64 (n v65))) v64))))
(67 (instantiate 66 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) (n (n v1)))) v1) (+ (n (+ v0 (n v1))) v0))))
(68 (instantiate 45 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ (n v64) v65)) (n (+ (n v64) (n v65)))) v64)))
(69 (instantiate 37 ((v0 . v64)(v1 . v65)(v2 . (n (+ (n v64) v65))))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ (n v64) v65)) (n (+ (n v64) (n v65))))) (+ (n (+ (n v64) v65)) v65))))
(70 (paramod 68 (1 1) 69 (1 1 2)) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ (n v64) v65)) v65))))
(71 (instantiate 70 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) v0) (+ (n (+ (n v0) v1)) v1))))
(72 (instantiate 33 ((v0 . v65)(v1 . v64))) ((= (+ (n (+ v65 (n v64))) (n (+ (n v64) (n v65)))) v64)))
(73 (instantiate 37 ((v0 . v64)(v1 . v65)(v2 . (n (+ v65 (n v64)))))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ v65 (n v64))) (n (+ (n v64) (n v65))))) (+ (n (+ v65 (n v64))) v65))))
(74 (paramod 72 (1 1) 73 (1 1 2)) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ v65 (n v64))) v65))))
(75 (instantiate 74 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) v0) (+ (n (+ v1 (n v0))) v1))))
(76 (instantiate 29 ((v0 . v65)(v1 . v64))) ((= (+ (n (+ (n v65) v64)) (n (+ (n v64) (n v65)))) v65)))
(77 (instantiate 37 ((v0 . v64)(v1 . v65)(v2 . (n (+ (n v65) v64))))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ (n v65) v64)) (n (+ (n v64) (n v65))))) (+ (n (+ (n v65) v64)) v65))))
(78 (paramod 76 (1 1) 77 (1 1 2)) ((= (+ (n (+ v64 (n v65))) v65) (+ (n (+ (n v65) v64)) v65))))
(79 (instantiate 78 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) v1) (+ (n (+ (n v1) v0)) v1))))
(80 (instantiate 2 ((v0 . v64)(v1 . (n v65)))) ((= (+ v64 (n v65)) (+ (n v65) v64))))
(81 (instantiate 71 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ (n v64) v65)) v65))))
(82 (paramod 80 (1 1) 81 (1 1 1 1)) ((= (+ (n (+ (n v65) v64)) v64) (+ (n (+ (n v64) v65)) v65))))
(83 (instantiate 82 ((v64 . v1)(v65 . v0))) ((= (+ (n (+ (n v0) v1)) v1) (+ (n (+ (n v1) v0)) v0))))
(84 (instantiate 71 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ (n v64) v65)) v65))))
(85 (instantiate 75 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ v65 (n v64))) v65))))
(86 (paramod 84 (1 1) 85 (1 1)) ((= (+ (n (+ (n v64) v65)) v65) (+ (n (+ v65 (n v64))) v65))))
(87 (instantiate 86 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) v1)) v1) (+ (n (+ v1 (n v0))) v1))))
(88 (instantiate 2 ((v0 . (n (+ v64 (n v65))))(v1 . v64))) ((= (+ (n (+ v64 (n v65))) v64) (+ v64 (n (+ v64 (n v65)))))))
(89 (instantiate 75 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v64) (+ (n (+ v65 (n v64))) v65))))
(90 (paramod 88 (1 1) 89 (1 1)) ((= (+ v64 (n (+ v64 (n v65)))) (+ (n (+ v65 (n v64))) v65))))
(91 (instantiate 90 ((v64 . v0)(v65 . v1))) ((= (+ v0 (n (+ v0 (n v1)))) (+ (n (+ v1 (n v0))) v1))))
(92 (flip 91 (1)) ((= (+ (n (+ v1 (n v0))) v1) (+ v0 (n (+ v0 (n v1)))))))
(93 (instantiate 2 ((v0 . (n (+ v64 (n v65))))(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v65) (+ v65 (n (+ v64 (n v65)))))))
(94 (instantiate 79 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v64 (n v65))) v65) (+ (n (+ (n v65) v64)) v65))))
(95 (paramod 93 (1 1) 94 (1 1)) ((= (+ v65 (n (+ v64 (n v65)))) (+ (n (+ (n v65) v64)) v65))))
(96 (instantiate 95 ((v64 . v1)(v65 . v0))) ((= (+ v0 (n (+ v1 (n v0)))) (+ (n (+ (n v0) v1)) v0))))
(97 (flip 96 (1)) ((= (+ (n (+ (n v0) v1)) v0) (+ v0 (n (+ v1 (n v0)))))))
(98 (instantiate 2 ((v0 . (n (+ (n v64) v65)))(v1 . v65))) ((= (+ (n (+ (n v64) v65)) v65) (+ v65 (n (+ (n v64) v65))))))
(99 (instantiate 83 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ (n v64) v65)) v65) (+ (n (+ (n v65) v64)) v64))))
(100 (paramod 98 (1 1) 99 (1 1)) ((= (+ v65 (n (+ (n v64) v65))) (+ (n (+ (n v65) v64)) v64))))
(101 (instantiate 100 ((v64 . v1)(v65 . v0))) ((= (+ v0 (n (+ (n v1) v0))) (+ (n (+ (n v0) v1)) v1))))
(102 (flip 101 (1)) ((= (+ (n (+ (n v0) v1)) v1) (+ v0 (n (+ (n v1) v0))))))
(103 (instantiate 2 ((v0 . (n (+ (n v64) v65)))(v1 . v65))) ((= (+ (n (+ (n v64) v65)) v65) (+ v65 (n (+ (n v64) v65))))))
(104 (instantiate 87 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ (n v64) v65)) v65) (+ (n (+ v65 (n v64))) v65))))
(105 (paramod 103 (1 1) 104 (1 1)) ((= (+ v65 (n (+ (n v64) v65))) (+ (n (+ v65 (n v64))) v65))))
(106 (instantiate 105 ((v64 . v1)(v65 . v0))) ((= (+ v0 (n (+ (n v1) v0))) (+ (n (+ v0 (n v1))) v0))))
(107 (instantiate 2 ((v0 . (n (+ v65 (n v64))))(v1 . v65))) ((= (+ (n (+ v65 (n v64))) v65) (+ v65 (n (+ v65 (n v64)))))))
(108 (instantiate 92 ((v0 . v64)(v1 . v65))) ((= (+ (n (+ v65 (n v64))) v65) (+ v64 (n (+ v64 (n v65)))))))
(109 (paramod 107 (1 1) 108 (1 1)) ((= (+ v65 (n (+ v65 (n v64)))) (+ v64 (n (+ v64 (n v65)))))))
(110 (instantiate 109 ((v64 . v1)(v65 . v0))) ((= (+ v0 (n (+ v0 (n v1)))) (+ v1 (n (+ v1 (n v0)))))))
(111 (instantiate 102 ((v0 . v64)(v1 . (n v65)))) ((= (+ (n (+ (n v64) (n v65))) (n v65)) (+ v64 (n (+ (n (n v65)) v64))))))
(112 (instantiate 41 ((v0 . v64)(v1 . v65)(v2 . (n v65)))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ (n v64) (n v65))) (n v65))) (+ v65 (n v65)))))
(113 (paramod 111 (1 1) 112 (1 1 2)) ((= (+ (n (+ v64 (n v65))) (+ v64 (n (+ (n (n v65)) v64)))) (+ v65 (n v65)))))
(114 (instantiate 113 ((v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) (+ v0 (n (+ (n (n v1)) v0)))) (+ v1 (n v1)))))
(115 (instantiate 67 ((v0 . v64)(v1 . v66))) ((= (+ (n (+ (n v64) (n (n v66)))) v66) (+ (n (+ v64 (n v66))) v64))))
(116 (instantiate 41 ((v0 . v64)(v1 . (n v66))(v2 . v66))) ((= (+ (n (+ v64 (n (n v66)))) (+ (n (+ (n v64) (n (n v66)))) v66)) (+ (n v66) v66))))
(117 (paramod 115 (1 1) 116 (1 1 2)) ((= (+ (n (+ v64 (n (n v66)))) (+ (n (+ v64 (n v66))) v64)) (+ (n v66) v66))))
(118 (instantiate 117 ((v64 . v0)(v66 . v1))) ((= (+ (n (+ v0 (n (n v1)))) (+ (n (+ v0 (n v1))) v0)) (+ (n v1) v1))))
(119 (instantiate 106 ((v0 . (n v64)))) ((= (+ (n v64) (n (+ (n v1) (n v64)))) (+ (n (+ (n v64) (n v1))) (n v64)))))
(120 (instantiate 58 ((v0 . v64)(v1 . (n v1))(v2 . (n v64)))) ((= (+ (n (+ (n v64) (n (n v1)))) (+ (n v64) (n (+ (n v1) (n v64))))) (+ (n v64) v64))))
(121 (paramod 119 (1 1) 120 (1 1 2)) ((= (+ (n (+ (n v64) (n (n v1)))) (+ (n (+ (n v64) (n v1))) (n v64))) (+ (n v64) v64))))
(122 (instantiate 118 ((v0 . (n v64))(v1 . v1))) ((= (+ (n (+ (n v64) (n (n v1)))) (+ (n (+ (n v64) (n v1))) (n v64))) (+ (n v1) v1))))
(123 (paramod 122 (1 1) 121 (1 1)) ((= (+ (n v1) v1) (+ (n v64) v64))))
(124 (instantiate 123 ((v1 . v0)(v64 . v1))) ((= (+ (n v0) v0) (+ (n v1) v1))))
(125 (instantiate 21 ((v0 . (n (+ v1 v2))))) ((= (+ (n (+ v1 v2)) (+ v1 v2)) (+ (n (+ v1 v2)) (+ v2 v1)))))
(126 (instantiate 124 ((v0 . (+ v1 v2))(v1 . v65))) ((= (+ (n (+ v1 v2)) (+ v1 v2)) (+ (n v65) v65))))
(127 (paramod 125 (1 1) 126 (1 1)) ((= (+ (n (+ v1 v2)) (+ v2 v1)) (+ (n v65) v65))))
(128 (instantiate 127 ((v1 . v0)(v2 . v1)(v65 . v2))) ((= (+ (n (+ v0 v1)) (+ v1 v0)) (+ (n v2) v2))))
(129 (instantiate 124 ((v0 . (+ (n v64) (n v65))))) ((= (+ (n (+ (n v64) (n v65))) (+ (n v64) (n v65))) (+ (n v1) v1))))
(130 (instantiate 41 ((v0 . v64)(v1 . v65)(v2 . (+ (n v64) (n v65))))) ((= (+ (n (+ v64 (n v65))) (+ (n (+ (n v64) (n v65))) (+ (n v64) (n v65)))) (+ v65 (+ (n v64) (n v65))))))
(131 (paramod 129 (1 1) 130 (1 1 2)) ((= (+ (n (+ v64 (n v65))) (+ (n v1) v1)) (+ v65 (+ (n v64) (n v65))))))
(132 (instantiate 131 ((v1 . v2)(v64 . v0)(v65 . v1))) ((= (+ (n (+ v0 (n v1))) (+ (n v2) v2)) (+ v1 (+ (n v0) (n v1))))))
(133 (instantiate 124 ((v0 . (n v64)))) ((= (+ (n (n v64)) (n v64)) (+ (n v1) v1))))
(134 (instantiate 33 ((v0 . v64)(v1 . (n v64)))) ((= (+ (n (+ v64 (n (n v64)))) (n (+ (n (n v64)) (n v64)))) (n v64))))
(135 (paramod 133 (1 1) 134 (1 1 2 1)) ((= (+ (n (+ v64 (n (n v64)))) (n (+ (n v1) v1))) (n v64))))
(136 (instantiate 135 ((v64 . v0))) ((= (+ (n (+ v0 (n (n v0)))) (n (+ (n v1) v1))) (n v0))))
(137 (instantiate 124 ((v0 . (n v64)))) ((= (+ (n (n v64)) (n v64)) (+ (n v1) v1))))
(138 (instantiate 54 ((v0 . v64)(v1 . (n (n v64))))) ((= (+ (n (+ (n v64) (n (n (n v64))))) (n (+ (n (n v64)) (n v64)))) v64)))
(139 (paramod 137 (1 1) 138 (1 1 2 1)) ((= (+ (n (+ (n v64) (n (n (n v64))))) (n (+ (n v1) v1))) v64)))
(140 (instantiate 136 ((v0 . (n v64))(v1 . v1))) ((= (+ (n (+ (n v64) (n (n (n v64))))) (n (+ (n v1) v1))) (n (n v64)))))
(141 (paramod 140 (1 1) 139 (1 1)) ((= (n (n v64)) v64)))
(142 (instantiate 141 ((v64 . v0))) ((= (n (n v0)) v0)))
(143 (instantiate 124 ((v0 . (n v65)))) ((= (+ (n (n v65)) (n v65)) (+ (n v1) v1))))
(144 (instantiate 62 ((v0 . (n v65))(v1 . v65))) ((= (+ (n (+ (n (n v65)) (n v65))) (n (+ (n (n v65)) v65))) (n v65))))
(145 (paramod 143 (1 1) 144 (1 1 1 1)) ((= (+ (n (+ (n v1) v1)) (n (+ (n (n v65)) v65))) (n v65))))
(146 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(147 (paramod 146 (1 1) 145 (1 1 2 1 1)) ((= (+ (n (+ (n v1) v1)) (n (+ v65 v65))) (n v65))))
(148 (instantiate 147 ((v1 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) v0)) (n (+ v1 v1))) (n v1))))
(149 (instantiate 142 ((v0 . v1))) ((= (n (n v1)) v1)))
(150 (paramod 149 (1 1) 114 (1 1 2 2 1 1)) ((= (+ (n (+ v0 (n v1))) (+ v0 (n (+ v1 v0)))) (+ v1 (n v1)))))
(151 (instantiate 58 ((v0 . (n v0))(v1 . v65)(v2 . v66))) ((= (+ (n (+ (n (n v0)) (n v65))) (+ v66 (n (+ v65 (n (n v0)))))) (+ v66 (n v0)))))
(152 (paramod 142 (1 1) 151 (1 1 2 2 1 2)) ((= (+ (n (+ (n (n v0)) (n v65))) (+ v66 (n (+ v65 v0)))) (+ v66 (n v0)))))
(153 (paramod 142 (1 1) 152 (1 1 1 1 1)) ((= (+ (n (+ v0 (n v65))) (+ v66 (n (+ v65 v0)))) (+ v66 (n v0)))))
(154 (instantiate 153 ((v65 . v1)(v66 . v2))) ((= (+ (n (+ v0 (n v1))) (+ v2 (n (+ v1 v0)))) (+ v2 (n v0)))))
(155 (instantiate 154 ((v0 . v0)(v1 . v1)(v2 . v0))) ((= (+ (n (+ v0 (n v1))) (+ v0 (n (+ v1 v0)))) (+ v0 (n v0)))))
(156 (paramod 155 (1 1) 150 (1 1)) ((= (+ v0 (n v0)) (+ v1 (n v1)))))
(157 (instantiate 156 ((v0 . v64))) ((= (+ v64 (n v64)) (+ v1 (n v1)))))
(158 (instantiate 128 ((v0 . v64)(v1 . (n v64))(v2 . v66))) ((= (+ (n (+ v64 (n v64))) (+ (n v64) v64)) (+ (n v66) v66))))
(159 (paramod 157 (1 1) 158 (1 1 1 1)) ((= (+ (n (+ v1 (n v1))) (+ (n v64) v64)) (+ (n v66) v66))))
(160 (instantiate 132 ((v0 . v1)(v1 . v1)(v2 . v64))) ((= (+ (n (+ v1 (n v1))) (+ (n v64) v64)) (+ v1 (+ (n v1) (n v1))))))
(161 (paramod 160 (1 1) 159 (1 1)) ((= (+ v1 (+ (n v1) (n v1))) (+ (n v66) v66))))
(162 (instantiate 161 ((v1 . v0)(v66 . v1))) ((= (+ v0 (+ (n v0) (n v0))) (+ (n v1) v1))))
(163 (instantiate 162 ((v0 . (n v0))(v1 . v65))) ((= (+ (n v0) (+ (n (n v0)) (n (n v0)))) (+ (n v65) v65))))
(164 (paramod 142 (1 1) 163 (1 1 2 1)) ((= (+ (n v0) (+ v0 (n (n v0)))) (+ (n v65) v65))))
(165 (paramod 142 (1 1) 164 (1 1 2 2)) ((= (+ (n v0) (+ v0 v0)) (+ (n v65) v65))))
(166 (instantiate 165 ((v65 . v1))) ((= (+ (n v0) (+ v0 v0)) (+ (n v1) v1))))
(167 (instantiate 162 ((v0 . (n v64)))) ((= (+ (n v64) (+ (n (n v64)) (n (n v64)))) (+ (n v1) v1))))
(168 (instantiate 97 ((v0 . v64)(v1 . (+ (n (n v64)) (n (n v64)))))) ((= (+ (n (+ (n v64) (+ (n (n v64)) (n (n v64))))) v64) (+ v64 (n (+ (+ (n (n v64)) (n (n v64))) (n v64)))))))
(169 (paramod 167 (1 1) 168 (1 1 1 1)) ((= (+ (n (+ (n v1) v1)) v64) (+ v64 (n (+ (+ (n (n v64)) (n (n v64))) (n v64)))))))
(170 (instantiate 142 ((v0 . v64))) ((= (n (n v64)) v64)))
(171 (paramod 170 (1 1) 169 (1 2 2 1 1 1)) ((= (+ (n (+ (n v1) v1)) v64) (+ v64 (n (+ (+ v64 (n (n v64))) (n v64)))))))
(172 (instantiate 142 ((v0 . v64))) ((= (n (n v64)) v64)))
(173 (paramod 172 (1 1) 171 (1 2 2 1 1 2)) ((= (+ (n (+ (n v1) v1)) v64) (+ v64 (n (+ (+ v64 v64) (n v64)))))))
(174 (instantiate 3 ((v0 . v64)(v1 . v64)(v2 . (n v64)))) ((= (+ (+ v64 v64) (n v64)) (+ v64 (+ v64 (n v64))))))
(175 (paramod 174 (1 1) 173 (1 2 2 1)) ((= (+ (n (+ (n v1) v1)) v64) (+ v64 (n (+ v64 (+ v64 (n v64))))))))
(176 (instantiate 175 ((v1 . v0)(v64 . v1))) ((= (+ (n (+ (n v0) v0)) v1) (+ v1 (n (+ v1 (+ v1 (n v1))))))))
(177 (flip 176 (1)) ((= (+ v1 (n (+ v1 (+ v1 (n v1))))) (+ (n (+ (n v0) v0)) v1))))
(178 (instantiate 25 ((v0 . (n v64))(v1 . v64)(v2 . v64))) ((= (+ (n v64) (+ v64 v64)) (+ v64 (+ v64 (n v64))))))
(179 (instantiate 166 ((v0 . v64)(v1 . v65))) ((= (+ (n v64) (+ v64 v64)) (+ (n v65) v65))))
(180 (paramod 178 (1 1) 179 (1 1)) ((= (+ v64 (+ v64 (n v64))) (+ (n v65) v65))))
(181 (instantiate 180 ((v64 . v0)(v65 . v1))) ((= (+ v0 (+ v0 (n v0))) (+ (n v1) v1))))
(182 (instantiate 156 ((v0 . v64))) ((= (+ v64 (n v64)) (+ v1 (n v1)))))
(183 (instantiate 181 ((v0 . v64)(v1 . v65))) ((= (+ v64 (+ v64 (n v64))) (+ (n v65) v65))))
(184 (paramod 182 (1 1) 183 (1 1 2)) ((= (+ v64 (+ v1 (n v1))) (+ (n v65) v65))))
(185 (instantiate 184 ((v64 . v0)(v65 . v2))) ((= (+ v0 (+ v1 (n v1))) (+ (n v2) v2))))
(186 (instantiate 25 ((v0 . v64)(v1 . v65)(v2 . (n v65)))) ((= (+ v64 (+ v65 (n v65))) (+ (n v65) (+ v65 v64)))))
(187 (instantiate 185 ((v0 . v64)(v1 . v65)(v2 . v66))) ((= (+ v64 (+ v65 (n v65))) (+ (n v66) v66))))
(188 (paramod 186 (1 1) 187 (1 1)) ((= (+ (n v65) (+ v65 v64)) (+ (n v66) v66))))
(189 (instantiate 188 ((v64 . v1)(v65 . v0)(v66 . v2))) ((= (+ (n v0) (+ v0 v1)) (+ (n v2) v2))))
(190 (flip 189 (1)) ((= (+ (n v2) v2) (+ (n v0) (+ v0 v1)))))
(191 (instantiate 190 ((v0 . v64)(v1 . v65)(v2 . (n v0)))) ((= (+ (n (n v0)) (n v0)) (+ (n v64) (+ v64 v65)))))
(192 (paramod 142 (1 1) 191 (1 1 1)) ((= (+ v0 (n v0)) (+ (n v64) (+ v64 v65)))))
(193 (instantiate 192 ((v64 . v1)(v65 . v2))) ((= (+ v0 (n v0)) (+ (n v1) (+ v1 v2)))))
(194 (flip 193 (1)) ((= (+ (n v1) (+ v1 v2)) (+ v0 (n v0)))))
(195 (instantiate 148 ((v0 . (n v0))(v1 . v65))) ((= (+ (n (+ (n (n v0)) (n v0))) (n (+ v65 v65))) (n v65))))
(196 (paramod 142 (1 1) 195 (1 1 1 1 1)) ((= (+ (n (+ v0 (n v0))) (n (+ v65 v65))) (n v65))))
(197 (instantiate 196 ((v65 . v1))) ((= (+ (n (+ v0 (n v0))) (n (+ v1 v1))) (n v1))))
(198 (instantiate 194 ((v1 . (n v65))(v2 . (n (+ v65 (n (n v65))))))) ((= (+ (n (n v65)) (+ (n v65) (n (+ v65 (n (n v65)))))) (+ v0 (n v0)))))
(199 (instantiate 50 ((v0 . (n v65))(v1 . v65))) ((= (+ (n (+ (n (n v65)) (+ (n v65) (n (+ v65 (n (n v65))))))) (n (n v65))) (+ v65 (n (n v65))))))
(200 (paramod 198 (1 1) 199 (1 1 1 1)) ((= (+ (n (+ v0 (n v0))) (n (n v65))) (+ v65 (n (n v65))))))
(201 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(202 (paramod 201 (1 1) 200 (1 1 2)) ((= (+ (n (+ v0 (n v0))) v65) (+ v65 (n (n v65))))))
(203 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(204 (paramod 203 (1 1) 202 (1 2 2)) ((= (+ (n (+ v0 (n v0))) v65) (+ v65 v65))))
(205 (instantiate 204 ((v65 . v1))) ((= (+ (n (+ v0 (n v0))) v1) (+ v1 v1))))
(206 (instantiate 189 ((v0 . (n v65))(v1 . (n (+ v65 (n (n v65))))))) ((= (+ (n (n v65)) (+ (n v65) (n (+ v65 (n (n v65)))))) (+ (n v2) v2))))
(207 (instantiate 50 ((v0 . (n v65))(v1 . v65))) ((= (+ (n (+ (n (n v65)) (+ (n v65) (n (+ v65 (n (n v65))))))) (n (n v65))) (+ v65 (n (n v65))))))
(208 (paramod 206 (1 1) 207 (1 1 1 1)) ((= (+ (n (+ (n v2) v2)) (n (n v65))) (+ v65 (n (n v65))))))
(209 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(210 (paramod 209 (1 1) 208 (1 1 2)) ((= (+ (n (+ (n v2) v2)) v65) (+ v65 (n (n v65))))))
(211 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(212 (paramod 211 (1 1) 210 (1 2 2)) ((= (+ (n (+ (n v2) v2)) v65) (+ v65 v65))))
(213 (instantiate 212 ((v2 . v0)(v65 . v1))) ((= (+ (n (+ (n v0) v0)) v1) (+ v1 v1))))
(214 (flip 213 (1)) ((= (+ v1 v1) (+ (n (+ (n v0) v0)) v1))))
(215 (instantiate 205 ((v1 . (n v65)))) ((= (+ (n (+ v0 (n v0))) (n v65)) (+ (n v65) (n v65)))))
(216 (instantiate 110 ((v0 . (n (+ v0 (n v0))))(v1 . v65))) ((= (+ (n (+ v0 (n v0))) (n (+ (n (+ v0 (n v0))) (n v65)))) (+ v65 (n (+ v65 (n (n (+ v0 (n v0))))))))))
(217 (paramod 215 (1 1) 216 (1 1 2 1)) ((= (+ (n (+ v0 (n v0))) (n (+ (n v65) (n v65)))) (+ v65 (n (+ v65 (n (n (+ v0 (n v0))))))))))
(218 (instantiate 197 ((v0 . v0)(v1 . (n v65)))) ((= (+ (n (+ v0 (n v0))) (n (+ (n v65) (n v65)))) (n (n v65)))))
(219 (paramod 218 (1 1) 217 (1 1)) ((= (n (n v65)) (+ v65 (n (+ v65 (n (n (+ v0 (n v0))))))))))
(220 (instantiate 142 ((v0 . v65))) ((= (n (n v65)) v65)))
(221 (paramod 220 (1 1) 219 (1 1)) ((= v65 (+ v65 (n (+ v65 (n (n (+ v0 (n v0))))))))))
(222 (instantiate 142 ((v0 . (+ v0 (n v0))))) ((= (n (n (+ v0 (n v0)))) (+ v0 (n v0)))))
(223 (paramod 222 (1 1) 221 (1 2 2 1 2)) ((= v65 (+ v65 (n (+ v65 (+ v0 (n v0))))))))
(224 (flip 223 (1)) ((= (+ v65 (n (+ v65 (+ v0 (n v0))))) v65)))
(225 (instantiate 224 ((v0 . v1)(v65 . v0))) ((= (+ v0 (n (+ v0 (+ v1 (n v1))))) v0)))
(226 (instantiate 225 ((v0 . v1)(v1 . v1))) ((= (+ v1 (n (+ v1 (+ v1 (n v1))))) v1)))
(227 (paramod 226 (1 1) 177 (1 1)) ((= v1 (+ (n (+ (n v0) v0)) v1))))
(228 (flip 227 (1)) ((= (+ (n (+ (n v0) v0)) v1) v1)))
(229 (paramod 228 (1 1) 214 (1 2)) ((= (+ v1 v1) v1)))
(230 (instantiate 229 ((v1 . v0))) ((= (+ v0 v0) v0)))
(231 (instantiate 230 ((v0 . (a)))) ((= (+ (a) (a)) (a))))
(232 (resolve 1 (1) 231 (1)) ())
)
End of proof object.

Search stopped by max_proofs option.

============ end of search ============

-------------- statistics -------------
clauses given                242
clauses generated          65728
clauses kept                5372
clauses forward subsumed   19191
clauses back subsumed        443
Kbytes malloced             5428

----------- times (seconds) -----------
user CPU time         52.71          (0 hr, 0 min, 52 sec)
system CPU time        7.04          (0 hr, 0 min, 7 sec)
wall-clock time       63             (0 hr, 1 min, 3 sec)
para_into time         2.12
para_from time         2.96
for_sub time           2.01
back_sub time          9.77
conflict time          0.55
demod time             9.77

The job finished        Sat Feb 15 17:17:06 1997

END_FILE