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