1----- Otter 3.3f, August 2004 ----- 2The process was started by mccune on gyro.thornwood, 3Mon Aug 2 15:31:15 2004 4The command was "../../bin/otter". The process ID is 8947. 5 6op(400,xfx,+). 7clear(print_kept). 8clear(print_new_demod). 9clear(print_back_demod). 10assign(pick_given_ratio,4). 11assign(max_mem,20000). 12set(knuth_bendix). 13 dependent: set(anl_eq). 14 dependent: set(para_from). 15 dependent: set(para_into). 16 dependent: clear(para_from_right). 17 dependent: clear(para_into_right). 18 dependent: set(para_from_vars). 19 dependent: set(eq_units_both_ways). 20 dependent: set(dynamic_demod_all). 21 dependent: set(dynamic_demod). 22 dependent: set(order_eq). 23 dependent: set(back_demod). 24 dependent: set(process_input). 25 dependent: set(lrpo). 26set(build_proof_object_2). 27 dependent: set(order_history). 28set(dynamic_demod_lex_dep). 29assign(max_weight,30). 30 31lex([A,B,E,c,d,e,f,g(x),n(x),x+x]). 32 33list(usable). 340 [] x=x. 350 [] x+y=y+x. 360 [] (x+y)+z=x+ (y+z). 370 [] x+ (y+z)=y+ (x+z). 38end_of_list. 39 40list(sos). 410 [] n(n(x+y)+n(x+n(y)))=x. 420 [] c+d=c. 430 [] n(A+n(B))+n(n(A)+n(B))!=B. 44end_of_list. 45assign(bsub_hint_wt,-20). 46 47list(hints). 481 [] n(n(x+ (y+z))+n(y+n(x+z)))=y # label(step_1). 492 [] n(n(x+y)+n(y+n(x)))=y # label(step_2). 503 [] n(n(x+y)+n(x+ (n(y+z)+n(y+n(z)))))=x # label(step_3). 514 [] n(n(x+y)+n(n(y)+x))=x # label(step_4). 525 [] c+ (d+x)=c+x # label(step_5). 536 [] n(n(x+c)+n(c+n(x+d)))=c # label(step_6). 547 [] n(n(x+ (y+z))+n(z+n(x+y)))=z # label(step_7). 558 [] n(n(x+ (y+z))+n(y+n(z+x)))=y # label(step_8). 569 [] n(n(c)+n(d+n(c)))=d # label(step_9). 5710 [] n(n(x+y)+n(n(x)+y))=y # label(step_10). 5811 [] n(n(x+n(y))+n(y+x))=x # label(step_11). 5912 [] n(n(x+ (n(y+z)+n(z+n(y))))+n(z+x))=x # label(step_12). 6013 [] n(n(x+c)+n(c+n(d+x)))=c # label(step_13). 6114 [] n(n(x+ (c+y))+n(d+ (y+n(x+c))))=d+y # label(step_14). 6215 [] n(n(x+ (y+z))+n(z+n(y+x)))=z # label(step_15). 6316 [] n(n(x+ (y+z))+n(n(z+x)+y))=y # label(step_16). 6417 [] n(d+n(c+n(d+n(c))))=n(d+n(c)) # label(step_17). 6518 [] n(d+n(n(c)+ (n(n(d+n(c))+x)+n(n(d+n(c))+n(x)))))=n(c) # label(step_18). 6619 [] n(x+n(y+ (x+n(n(y)+x))))=n(n(y)+x) # label(step_19). 6720 [] n(n(x+ (y+n(z)))+n(x+ (z+y)))=x+y # label(step_20). 6821 [] n(n(x+n(y+n(z)))+n(x+ (y+n(z+ (y+n(y+n(z)))))))=x # label(step_21). 6922 [] n(n(c)+n(d+ (n(x+c)+n(c+n(x)))))=d # label(step_22). 7023 [] n(n(d+n(c))+n(c+n(d+n(c))))=d # label(step_23). 7124 [] n(n(c+n(d+n(c)))+n(c+n(c+n(d+n(c)))))=c # label(step_24). 7225 [] n(d+n(d+ (n(c)+n(c+n(d+n(c))))))=n(c) # label(step_25). 7326 [] n(c+n(d+n(c)))=n(c) # label(step_26). 7427 [] n(n(c)+n(c+n(c)))=c # label(step_27). 7528 [] n(c+n(c+ (n(c)+n(c+ (c+n(c+n(c)))))))=n(c) # label(step_28). 7629 [] n(n(c+n(c))+n(c+ (c+n(c+n(c)))))=c # label(step_29). 7730 [] n(c+ (c+n(c+n(c))))=n(c) # label(step_30). 7831 [] d+n(c+n(c))=d # label(step_31). 7932 [] n(n(x+d)+n(x+ (n(d)+n(c+n(c)))))=x+n(c+n(c)) # label(step_32). 8033 [] x+n(c+n(c))=x # label(step_33). 81end_of_list. 82 83------------> process usable: 84** KEPT (pick-wt=3): 34 [] x=x. 85** KEPT (pick-wt=7): 35 [] x+y=y+x. 86---> New Demodulator: (lex-dependent) 36 [new_demod,35] x+y=y+x. 87** KEPT (pick-wt=11): 37 [] (x+y)+z=x+ (y+z). 88---> New Demodulator: 38 [new_demod,37] (x+y)+z=x+ (y+z). 89** KEPT (pick-wt=11): 39 [] x+ (y+z)=y+ (x+z). 90---> New Demodulator: (lex-dependent) 40 [new_demod,39] x+ (y+z)=y+ (x+z). 91 Following clause subsumed by 34 during input processing: 0 [copy,34,flip.1] x=x. 92 Following clause subsumed by 35 during input processing: 0 [copy,35,flip.1] x+y=y+x. 93>>>> Starting back demodulation with 36. 94>>>> Starting back demodulation with 38. 95 Following clause subsumed by 39 during input processing: 0 [copy,39,flip.1] x+ (y+z)=y+ (x+z). 96>>>> Starting back demodulation with 40. 97 98------------> process sos: 99** KEPT (pick-wt=13): 41 [] n(n(x+y)+n(x+n(y)))=x. 100---> New Demodulator: 42 [new_demod,41] n(n(x+y)+n(x+n(y)))=x. 101** KEPT (pick-wt=5): 43 [] c+d=c. 102---> New Demodulator: 44 [new_demod,43] c+d=c. 103** KEPT (pick-wt=14): 45 [] n(A+n(B))+n(n(A)+n(B))!=B. 104>>>> Starting back demodulation with 42. 105>>>> Starting back demodulation with 44. 106 107======= end of input processing ======= 108 109=========== start of search =========== 110 111given clause #1: (wt=13) 41 [] n(n(x+y)+n(x+n(y)))=x. 112 113given clause #2: (wt=-20) 46 [para_into,41.1.1.1.1.1,39.1.1] n(n(x+ (y+z))+n(y+n(x+z)))=y # label(step_1). 114 115given clause #3: (wt=-20) 50 [para_into,41.1.1.1.1.1,35.1.1] n(n(x+y)+n(y+n(x)))=y # label(step_2). 116 117given clause #4: (wt=-20) 54 [para_into,41.1.1.1.2.1.2,41.1.1,demod,36] n(n(x+y)+n(x+ (n(y+z)+n(y+n(z)))))=x # label(step_3). 118 119given clause #5: (wt=-20) 56 [para_into,41.1.1.1.2.1,35.1.1] n(n(x+y)+n(n(y)+x))=x # label(step_4). 120 121given clause #6: (wt=5) 43 [] c+d=c. 122 123given clause #7: (wt=-20) 64 [para_into,46.1.1.1.1.1.2,35.1.1] n(n(x+ (y+z))+n(z+n(x+y)))=z # label(step_7). 124 125given clause #8: (wt=-20) 70 [para_into,46.1.1.1.2.1.2.1,35.1.1] n(n(x+ (y+z))+n(y+n(z+x)))=y # label(step_8). 126 127given clause #9: (wt=-20) 102 [para_into,50.1.1.1.2.1,35.1.1] n(n(x+y)+n(n(x)+y))=y # label(step_10). 128 129given clause #10: (wt=-20) 106 [para_into,50.1.1.1,35.1.1] n(n(x+n(y))+n(y+x))=x # label(step_11). 130 131given clause #11: (wt=14) 45 [] n(A+n(B))+n(n(A)+n(B))!=B. 132 133given clause #12: (wt=-20) 158 [para_into,56.1.1.1.2.1.1,50.1.1] n(n(x+ (n(y+z)+n(z+n(y))))+n(z+x))=x # label(step_12). 134 135given clause #13: (wt=-20) 196 [para_from,43.1.1,46.1.1.1.1.1.2] n(n(x+c)+n(c+n(x+d)))=c # label(step_6). 136 137given clause #14: (wt=-20) 204 [para_from,43.1.1,50.1.1.1.1.1] n(n(c)+n(d+n(c)))=d # label(step_9). 138 139given clause #15: (wt=-20) 206 [para_from,43.1.1,37.1.1.1,flip.1] c+ (d+x)=c+x # label(step_5). 140 141given clause #16: (wt=19) 48 [para_into,41.1.1.1.1.1,37.1.1,demod,38] n(n(x+ (y+z))+n(x+ (y+n(z))))=x+y. 142 143given clause #17: (wt=-20) 214 [para_into,64.1.1.1.1.1,39.1.1] n(n(x+ (y+z))+n(z+n(y+x)))=z # label(step_15). 144 145given clause #18: (wt=-20) 244 [para_into,70.1.1.1.1.1.2,43.1.1] n(n(x+c)+n(c+n(d+x)))=c # label(step_13). 146 147given clause #19: (wt=-20) 272 [para_into,70.1.1.1.2.1,35.1.1] n(n(x+ (y+z))+n(n(z+x)+y))=y # label(step_16). 148 149given clause #20: (wt=-20) 338 [para_into,102.1.1.1.2,102.1.1,demod,38,36] n(x+n(y+ (x+n(n(y)+x))))=n(n(y)+x) # label(step_19). 150 151given clause #21: (wt=20) 52 [para_into,41.1.1.1.1,41.1.1] n(x+n(n(x+y)+n(n(x+n(y)))))=n(x+y). 152896 back subsumes 860. 153896 back subsumes 824. 154 155given clause #22: (wt=-20) 376 [para_into,106.1.1.1.2.1,39.1.1,demod,38] n(n(x+ (y+n(z)))+n(x+ (z+y)))=x+y # label(step_20). 156 157given clause #23: (wt=-20) 378 [para_from,106.1.1,54.1.1.1.2.1.2.2,demod,40,36,36] n(n(x+n(y+n(z)))+n(x+ (y+n(z+ (y+n(y+n(z)))))))=x # label(step_21). 158 159given clause #24: (wt=-20) 432 [para_into,158.1.1.1.2.1,43.1.1,demod,36] n(n(c)+n(d+ (n(x+c)+n(c+n(x)))))=d # label(step_22). 160 161given clause #25: (wt=-20) 496 [para_from,204.1.1,102.1.1.1.2,demod,36] n(d+n(c+n(d+n(c))))=n(d+n(c)) # label(step_17). 162 163given clause #26: (wt=18) 58 [para_into,41.1.1.1.2,41.1.1,demod,40,36,36] n(x+n(x+ (n(y)+n(x+y))))=n(x+y). 164 165given clause #27: (wt=-20) 528 [para_from,204.1.1,54.1.1.1.1] n(d+n(n(c)+ (n(n(d+n(c))+x)+n(n(d+n(c))+n(x)))))=n(c) # label(step_18). 166 167given clause #28: (wt=-20) 548 [para_from,206.1.1,64.1.1.1.1.1.2,demod,38] n(n(x+ (c+y))+n(d+ (y+n(x+c))))=d+y # label(step_14). 168 169given clause #29: (wt=-20) 832 [para_into,338.1.1.1.2.1.2.2,204.1.1,demod,36,207,205] n(n(d+n(c))+n(c+n(d+n(c))))=d # label(step_23). 170 171given clause #30: (wt=-20) 1278 [para_from,832.1.1,272.1.1.1.2,demod,36,40,36,1043,flip.1] n(c+n(d+n(c)))=n(c) # label(step_26). 172 173given clause #31: (wt=21) 60 [para_into,46.1.1.1.1.1.2,39.1.1] n(n(x+ (y+ (z+u)))+n(z+n(x+ (y+u))))=z. 174 175given clause #32: (wt=-20) 1298 [back_demod,1112,demod,1279,1279] n(n(c)+n(c+n(c)))=c # label(step_27). 176 177given clause #33: (wt=-20) 1404 [para_from,1298.1.1,378.1.1.1.1,demod,40] n(c+n(c+ (n(c)+n(c+ (c+n(c+n(c)))))))=n(c) # label(step_28). 178 179given clause #34: (wt=-20) 1420 [para_from,1298.1.1,338.1.1.1.2.1.2.2,demod,36,1299] n(n(c+n(c))+n(c+ (c+n(c+n(c)))))=c # label(step_29). 180 181given clause #35: (wt=-20) 1482 [para_from,1420.1.1,272.1.1.1.2,demod,36,40,36,1405,flip.1] n(c+ (c+n(c+n(c))))=n(c) # label(step_30). 182 183given clause #36: (wt=23) 62 [para_into,46.1.1.1.1.1.2,37.1.1,demod,38] n(n(x+ (y+ (z+u)))+n(y+ (z+n(x+u))))=y+z. 184 185given clause #37: (wt=-20) 1520 [para_from,1482.1.1,548.1.1.1.1,demod,36,433,flip.1] d+n(c+n(c))=d # label(step_31). 186 187given clause #38: (wt=-20) 1642 [para_from,1520.1.1,54.1.1.1.2.1.2.2.1,demod,40,207,36,1629] x+n(c+n(c))=x # label(step_31). 188 189given clause #39: (wt=5) 1646 [para_from,1520.1.1,46.1.1.1.2.1,demod,207,36,1643] n(n(d))=d. 190 191given clause #40: (wt=5) 1682 [back_demod,1522,demod,1643,1643,1643] n(n(c))=c. 192 193given clause #41: (wt=17) 66 [para_into,46.1.1.1.1.1,35.1.1,demod,38] n(n(x+ (y+z))+n(x+n(z+y)))=x. 194 195given clause #42: (wt=7) 1684 [back_demod,1482,demod,1643] n(c+c)=n(c). 196 197given clause #43: (wt=9) 198 [para_from,43.1.1,39.1.1.2,flip.1] c+ (x+d)=x+c. 198 199given clause #44: (wt=9) 896 [para_into,52.1.1.1.2.1.1.1,35.1.1,demod,113] n(x+y)=n(y+x). 200 201given clause #45: (wt=9) 1698 [para_into,1642.1.1,35.1.1] n(c+n(c))+x=x. 202 203given clause #46: (wt=21) 68 [para_into,46.1.1.1.2.1.2.1,39.1.1] n(n(x+ (y+ (z+u)))+n(y+n(z+ (x+u))))=y. 204 205given clause #47: (wt=7) 1961 [para_from,1698.1.1,52.1.1.1,demod,1699,1699,1753,1699] n(n(n(x)))=n(x). 206 207given clause #48: (wt=5) 2031 [para_into,1961.1.1.1.1,378.1.1,demod,379] n(n(x))=x. 208 209-------- PROOF -------- 210 211----> UNIT CONFLICT at 0.47 sec ----> 2174 [binary,2173.1,34.1] $F. 212 213Length of proof is 37. Level of proof is 17. 214 215---------------- PROOF ---------------- 216 21734 [] x=x. 21836,35 [] x+y=y+x. 21938,37 [] (x+y)+z=x+ (y+z). 22040,39 [] x+ (y+z)=y+ (x+z). 22141 [] n(n(x+y)+n(x+n(y)))=x. 22243 [] c+d=c. 22345 [] n(A+n(B))+n(n(A)+n(B))!=B. 22446 [para_into,41.1.1.1.1.1,39.1.1] n(n(x+ (y+z))+n(y+n(x+z)))=y # label(step_1). 22550 [para_into,41.1.1.1.1.1,35.1.1] n(n(x+y)+n(y+n(x)))=y # label(step_2). 22652 [para_into,41.1.1.1.1,41.1.1] n(x+n(n(x+y)+n(n(x+n(y)))))=n(x+y). 22754 [para_into,41.1.1.1.2.1.2,41.1.1,demod,36] n(n(x+y)+n(x+ (n(y+z)+n(y+n(z)))))=x # label(step_3). 22856 [para_into,41.1.1.1.2.1,35.1.1] n(n(x+y)+n(n(y)+x))=x # label(step_4). 22964 [para_into,46.1.1.1.1.1.2,35.1.1] n(n(x+ (y+z))+n(z+n(x+y)))=z # label(step_7). 23070 [para_into,46.1.1.1.2.1.2.1,35.1.1] n(n(x+ (y+z))+n(y+n(z+x)))=y # label(step_8). 231102 [para_into,50.1.1.1.2.1,35.1.1] n(n(x+y)+n(n(x)+y))=y # label(step_10). 232106 [para_into,50.1.1.1,35.1.1] n(n(x+n(y))+n(y+x))=x # label(step_11). 233158 [para_into,56.1.1.1.2.1.1,50.1.1] n(n(x+ (n(y+z)+n(z+n(y))))+n(z+x))=x # label(step_12). 234205,204 [para_from,43.1.1,50.1.1.1.1.1] n(n(c)+n(d+n(c)))=d # label(step_9). 235207,206 [para_from,43.1.1,37.1.1.1,flip.1] c+ (d+x)=c+x # label(step_5). 236244 [para_into,70.1.1.1.1.1.2,43.1.1] n(n(x+c)+n(c+n(d+x)))=c # label(step_13). 237272 [para_into,70.1.1.1.2.1,35.1.1] n(n(x+ (y+z))+n(n(z+x)+y))=y # label(step_16). 238338 [para_into,102.1.1.1.2,102.1.1,demod,38,36] n(x+n(y+ (x+n(n(y)+x))))=n(n(y)+x) # label(step_19). 239376 [para_into,106.1.1.1.2.1,39.1.1,demod,38] n(n(x+ (y+n(z)))+n(x+ (z+y)))=x+y # label(step_20). 240379,378 [para_from,106.1.1,54.1.1.1.2.1.2.2,demod,40,36,36] n(n(x+n(y+n(z)))+n(x+ (y+n(z+ (y+n(y+n(z)))))))=x # label(step_21). 241433,432 [para_into,158.1.1.1.2.1,43.1.1,demod,36] n(n(c)+n(d+ (n(x+c)+n(c+n(x)))))=d # label(step_22). 242496 [para_from,204.1.1,102.1.1.1.2,demod,36] n(d+n(c+n(d+n(c))))=n(d+n(c)) # label(step_17). 243548 [para_from,206.1.1,64.1.1.1.1.1.2,demod,38] n(n(x+ (c+y))+n(d+ (y+n(x+c))))=d+y # label(step_14). 244832 [para_into,338.1.1.1.2.1.2.2,204.1.1,demod,36,207,205] n(n(d+n(c))+n(c+n(d+n(c))))=d # label(step_23). 2451043,1042 [para_into,378.1.1.1.1,204.1.1,demod,207,40] n(d+n(d+ (n(c)+n(c+n(d+n(c))))))=n(c) # label(step_25). 2461112 [para_from,496.1.1,244.1.1.1.2.1.2,demod,36,36] n(n(c+n(d+n(c)))+n(c+n(c+n(d+n(c)))))=c # label(step_24). 2471279,1278 [para_from,832.1.1,272.1.1.1.2,demod,36,40,36,1043,flip.1] n(c+n(d+n(c)))=n(c) # label(step_26). 2481299,1298 [back_demod,1112,demod,1279,1279] n(n(c)+n(c+n(c)))=c # label(step_27). 2491405,1404 [para_from,1298.1.1,378.1.1.1.1,demod,40] n(c+n(c+ (n(c)+n(c+ (c+n(c+n(c)))))))=n(c) # label(step_28). 2501420 [para_from,1298.1.1,338.1.1.1.2.1.2.2,demod,36,1299] n(n(c+n(c))+n(c+ (c+n(c+n(c)))))=c # label(step_29). 2511482 [para_from,1420.1.1,272.1.1.1.2,demod,36,40,36,1405,flip.1] n(c+ (c+n(c+n(c))))=n(c) # label(step_30). 2521520 [para_from,1482.1.1,548.1.1.1.1,demod,36,433,flip.1] d+n(c+n(c))=d # label(step_31). 2531629,1628 [para_from,1520.1.1,376.1.1.1.2.1.2,demod,36,36] n(n(x+d)+n(x+ (n(d)+n(c+n(c)))))=x+n(c+n(c)) # label(step_32). 2541643,1642 [para_from,1520.1.1,54.1.1.1.2.1.2.2.1,demod,40,207,36,1629] x+n(c+n(c))=x # label(step_31). 2551699,1698 [para_into,1642.1.1,35.1.1] n(c+n(c))+x=x. 2561753,1752 [para_from,1642.1.1,338.1.1.1.2.1.2.2.1,demod,1699,1699,1643] n(n(x+n(n(x))))=n(n(x)). 2571961 [para_from,1698.1.1,52.1.1.1,demod,1699,1699,1753,1699] n(n(n(x)))=n(x). 2582032,2031 [para_into,1961.1.1.1.1,378.1.1,demod,379] n(n(x))=x. 2592144,2143 [para_into,2031.1.1.1,102.1.1,flip.1] n(x+y)+n(n(x)+y)=n(y). 2602173 [back_demod,45,demod,2144,2032] B!=B. 2612174 [binary,2173.1,34.1] $F. 262 263------------ end of proof ------------- 264 265 266;; BEGINNING OF PROOF OBJECT 267( 268(1 (input) (= v0 v0) (34)) 269(2 (input) (= (+ v0 v1) (+ v1 v0)) (35)) 270(3 (input) (= (+ (+ v0 v1) v2) (+ v0 (+ v1 v2))) (37)) 271(4 (input) (= (+ v0 (+ v1 v2)) (+ v1 (+ v0 v2))) (39)) 272(5 (input) (= (n (+ (n (+ v0 v1)) (n (+ v0 (n v1))))) v0) (41)) 273(6 (input) (= (+ (c) (d)) (c)) (43)) 274(7 (input) (not (= (+ (n (+ (A) (n (B)))) (n (+ (n (A)) (n (B))))) (B))) (45)) 275(8 (instantiate 4 ((v0 . v64))) (= (+ v64 (+ v1 v2)) (+ v1 (+ v64 v2))) NIL) 276(9 (instantiate 5 ((v0 . v64)(v1 . (+ v1 v2)))) (= (n (+ (n (+ v64 (+ v1 v2))) (n (+ v64 (n (+ v1 v2)))))) v64) NIL) 277(10 (paramod 8 (1) 9 (1 1 1 1)) (= (n (+ (n (+ v1 (+ v64 v2))) (n (+ v64 (n (+ v1 v2)))))) v64) NIL) 278(11 (instantiate 10 ((v1 . v0)(v64 . v1))) (= (n (+ (n (+ v0 (+ v1 v2))) (n (+ v1 (n (+ v0 v2)))))) v1) (46)) 279(12 (instantiate 2 ((v0 . v64)(v1 . v65))) (= (+ v64 v65) (+ v65 v64)) NIL) 280(13 (instantiate 5 ((v0 . v64)(v1 . v65))) (= (n (+ (n (+ v64 v65)) (n (+ v64 (n v65))))) v64) NIL) 281(14 (paramod 12 (1) 13 (1 1 1 1)) (= (n (+ (n (+ v65 v64)) (n (+ v64 (n v65))))) v64) NIL) 282(15 (instantiate 14 ((v64 . v1)(v65 . v0))) (= (n (+ (n (+ v0 v1)) (n (+ v1 (n v0))))) v1) (50)) 283(16 (instantiate 5 ((v0 . (n (+ v0 v1)))(v1 . (n (+ v0 (n v1)))))) (= (n (+ (n (+ (n (+ v0 v1)) (n (+ v0 (n v1))))) (n (+ (n (+ v0 v1)) (n (n (+ v0 (n v1)))))))) (n (+ v0 v1))) NIL) 284(17 (paramod 5 (1) 16 (1 1 1)) (= (n (+ v0 (n (+ (n (+ v0 v1)) (n (n (+ v0 (n v1)))))))) (n (+ v0 v1))) (52)) 285(18 (instantiate 5 ((v0 . v64)(v1 . (+ (n (+ v0 v1)) (n (+ v0 (n v1))))))) (= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 (n (+ (n (+ v0 v1)) (n (+ v0 (n v1))))))))) v64) NIL) 286(19 (paramod 5 (1) 18 (1 1 2 1 2)) (= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 v0)))) v64) NIL) 287(20 (instantiate 2 ((v0 . (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))))(v1 . (n (+ v64 v0))))) (= (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))) (n (+ v64 v0))) (+ (n (+ v64 v0)) (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))))) NIL) 288(21 (paramod 20 (1) 19 (1 1)) (= (n (+ (n (+ v64 v0)) (n (+ v64 (+ (n (+ v0 v1)) (n (+ v0 (n v1)))))))) v64) NIL) 289(22 (instantiate 21 ((v0 . v1)(v1 . v2)(v64 . v0))) (= (n (+ (n (+ v0 v1)) (n (+ v0 (+ (n (+ v1 v2)) (n (+ v1 (n v2)))))))) v0) (54)) 290(23 (instantiate 2 ((v0 . v64)(v1 . (n v65)))) (= (+ v64 (n v65)) (+ (n v65) v64)) NIL) 291(24 (instantiate 5 ((v0 . v64)(v1 . v65))) (= (n (+ (n (+ v64 v65)) (n (+ v64 (n v65))))) v64) NIL) 292(25 (paramod 23 (1) 24 (1 1 2 1)) (= (n (+ (n (+ v64 v65)) (n (+ (n v65) v64)))) v64) NIL) 293(26 (instantiate 25 ((v64 . v0)(v65 . v1))) (= (n (+ (n (+ v0 v1)) (n (+ (n v1) v0)))) v0) (56)) 294(27 (instantiate 2 ((v0 . v65)(v1 . v66))) (= (+ v65 v66) (+ v66 v65)) NIL) 295(28 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66))) (= (n (+ (n (+ v64 (+ v65 v66))) (n (+ v65 (n (+ v64 v66)))))) v65) NIL) 296(29 (paramod 27 (1) 28 (1 1 1 1 2)) (= (n (+ (n (+ v64 (+ v66 v65))) (n (+ v65 (n (+ v64 v66)))))) v65) NIL) 297(30 (instantiate 29 ((v64 . v0)(v65 . v2)(v66 . v1))) (= (n (+ (n (+ v0 (+ v1 v2))) (n (+ v2 (n (+ v0 v1)))))) v2) (64)) 298(31 (instantiate 2 ((v0 . v64)(v1 . v66))) (= (+ v64 v66) (+ v66 v64)) NIL) 299(32 (instantiate 11 ((v0 . v64)(v1 . v65)(v2 . v66))) (= (n (+ (n (+ v64 (+ v65 v66))) (n (+ v65 (n (+ v64 v66)))))) v65) NIL) 300(33 (paramod 31 (1) 32 (1 1 2 1 2 1)) (= (n (+ (n (+ v64 (+ v65 v66))) (n (+ v65 (n (+ v66 v64)))))) v65) NIL) 301(34 (instantiate 33 ((v64 . v0)(v65 . v1)(v66 . v2))) (= (n (+ (n (+ v0 (+ v1 v2))) (n (+ v1 (n (+ v2 v0)))))) v1) (70)) 302(35 (instantiate 2 ((v0 . v65)(v1 . (n v64)))) (= (+ v65 (n v64)) (+ (n v64) v65)) NIL) 303(36 (instantiate 15 ((v0 . v64)(v1 . v65))) (= (n (+ (n (+ v64 v65)) (n (+ v65 (n v64))))) v65) NIL) 304(37 (paramod 35 (1) 36 (1 1 2 1)) (= (n (+ (n (+ v64 v65)) (n (+ (n v64) v65)))) v65) NIL) 305(38 (instantiate 37 ((v64 . v0)(v65 . v1))) (= (n (+ (n (+ v0 v1)) (n (+ (n v0) v1)))) v1) (102)) 306(39 (instantiate 2 ((v0 . (n (+ v64 v65)))(v1 . (n (+ v65 (n v64)))))) (= (+ (n (+ v64 v65)) (n (+ v65 (n v64)))) (+ (n (+ v65 (n v64))) (n (+ v64 v65)))) NIL) 307(40 (instantiate 15 ((v0 . v64)(v1 . v65))) (= (n (+ (n (+ v64 v65)) (n (+ v65 (n v64))))) v65) NIL) 308(41 (paramod 39 (1) 40 (1 1)) (= (n (+ (n (+ v65 (n v64))) (n (+ v64 v65)))) v65) NIL) 309(42 (instantiate 41 ((v64 . v1)(v65 . v0))) (= (n (+ (n (+ v0 (n v1))) (n (+ v1 v0)))) v0) (106)) 310(43 (instantiate 26 ((v0 . v64)(v1 . (+ (n (+ v0 v1)) (n (+ v1 (n v0))))))) (= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v1 (n v0)))))) (n (+ (n (+ (n (+ v0 v1)) (n (+ v1 (n v0))))) v64)))) v64) NIL) 311(44 (paramod 15 (1) 43 (1 1 2 1 1)) (= (n (+ (n (+ v64 (+ (n (+ v0 v1)) (n (+ v1 (n v0)))))) (n (+ v1 v64)))) v64) NIL) 312(45 (instantiate 44 ((v0 . v1)(v1 . v2)(v64 . v0))) (= (n (+ (n (+ v0 (+ (n (+ v1 v2)) (n (+ v2 (n v1)))))) (n (+ v2 v0)))) v0) (158)) 313(46 (instantiate 15 ((v0 . (c))(v1 . (d)))) (= (n (+ (n (+ (c) (d))) (n (+ (d) (n (c)))))) (d)) NIL) 314(47 (paramod 6 (1) 46 (1 1 1 1)) (= (n (+ (n (c)) (n (+ (d) (n (c)))))) (d)) (204)) 315(48 (instantiate 3 ((v0 . (c))(v1 . (d))(v2 . v66))) (= (+ (+ (c) (d)) v66) (+ (c) (+ (d) v66))) NIL) 316(49 (paramod 6 (1) 48 (1 1)) (= (+ (c) v66) (+ (c) (+ (d) v66))) NIL) 317(50 (flip 49 ()) (= (+ (c) (+ (d) v66)) (+ (c) v66)) NIL) 318(51 (instantiate 50 ((v66 . v0))) (= (+ (c) (+ (d) v0)) (+ (c) v0)) (206)) 319(52 (instantiate 34 ((v0 . v64)(v1 . (c))(v2 . (d)))) (= (n (+ (n (+ v64 (+ (c) (d)))) (n (+ (c) (n (+ (d) v64)))))) (c)) NIL) 320(53 (paramod 6 (1) 52 (1 1 1 1 2)) (= (n (+ (n (+ v64 (c))) (n (+ (c) (n (+ (d) v64)))))) (c)) NIL) 321(54 (instantiate 53 ((v64 . v0))) (= (n (+ (n (+ v0 (c))) (n (+ (c) (n (+ (d) v0)))))) (c)) (244)) 322(55 (instantiate 2 ((v0 . v65)(v1 . (n (+ v66 v64))))) (= (+ v65 (n (+ v66 v64))) (+ (n (+ v66 v64)) v65)) NIL) 323(56 (instantiate 34 ((v0 . v64)(v1 . v65)(v2 . v66))) (= (n (+ (n (+ v64 (+ v65 v66))) (n (+ v65 (n (+ v66 v64)))))) v65) NIL) 324(57 (paramod 55 (1) 56 (1 1 2 1)) (= (n (+ (n (+ v64 (+ v65 v66))) (n (+ (n (+ v66 v64)) v65)))) v65) NIL) 325(58 (instantiate 57 ((v64 . v0)(v65 . v1)(v66 . v2))) (= (n (+ (n (+ v0 (+ v1 v2))) (n (+ (n (+ v2 v0)) v1)))) v1) (272)) 326(59 (instantiate 38 ((v0 . (+ v0 v1))(v1 . (n (+ (n v0) v1))))) (= (n (+ (n (+ (+ v0 v1) (n (+ (n v0) v1)))) (n (+ (n (+ v0 v1)) (n (+ (n v0) v1)))))) (n (+ (n v0) v1))) NIL) 327(60 (paramod 38 (1) 59 (1 1 2)) (= (n (+ (n (+ (+ v0 v1) (n (+ (n v0) v1)))) v1)) (n (+ (n v0) v1))) NIL) 328(61 (instantiate 3 ((v0 . v0)(v1 . v1)(v2 . (n (+ (n v0) v1))))) (= (+ (+ v0 v1) (n (+ (n v0) v1))) (+ v0 (+ v1 (n (+ (n v0) v1))))) NIL) 329(62 (paramod 61 (1) 60 (1 1 1 1)) (= (n (+ (n (+ v0 (+ v1 (n (+ (n v0) v1))))) v1)) (n (+ (n v0) v1))) NIL) 330(63 (instantiate 2 ((v0 . (n (+ v0 (+ v1 (n (+ (n v0) v1))))))(v1 . v1))) (= (+ (n (+ v0 (+ v1 (n (+ (n v0) v1))))) v1) (+ v1 (n (+ v0 (+ v1 (n (+ (n v0) v1))))))) NIL) 331(64 (paramod 63 (1) 62 (1 1)) (= (n (+ v1 (n (+ v0 (+ v1 (n (+ (n v0) v1))))))) (n (+ (n v0) v1))) NIL) 332(65 (instantiate 64 ((v0 . v1)(v1 . v0))) (= (n (+ v0 (n (+ v1 (+ v0 (n (+ (n v1) v0))))))) (n (+ (n v1) v0))) (338)) 333(66 (instantiate 4 ((v0 . v65))) (= (+ v65 (+ v1 v2)) (+ v1 (+ v65 v2))) NIL) 334(67 (instantiate 42 ((v0 . (+ v1 v2))(v1 . v65))) (= (n (+ (n (+ (+ v1 v2) (n v65))) (n (+ v65 (+ v1 v2))))) (+ v1 v2)) NIL) 335(68 (paramod 66 (1) 67 (1 1 2 1)) (= (n (+ (n (+ (+ v1 v2) (n v65))) (n (+ v1 (+ v65 v2))))) (+ v1 v2)) NIL) 336(69 (instantiate 3 ((v0 . v1)(v1 . v2)(v2 . (n v65)))) (= (+ (+ v1 v2) (n v65)) (+ v1 (+ v2 (n v65)))) NIL) 337(70 (paramod 69 (1) 68 (1 1 1 1)) (= (n (+ (n (+ v1 (+ v2 (n v65)))) (n (+ v1 (+ v65 v2))))) (+ v1 v2)) NIL) 338(71 (instantiate 70 ((v1 . v0)(v2 . v1)(v65 . v2))) (= (n (+ (n (+ v0 (+ v1 (n v2)))) (n (+ v0 (+ v2 v1))))) (+ v0 v1)) (376)) 339(72 (instantiate 22 ((v0 . v64)(v1 . (n (+ v0 (n v1))))(v2 . (+ v1 v0)))) (= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ (n (+ v0 (n v1))) (+ v1 v0))) (n (+ (n (+ v0 (n v1))) (n (+ v1 v0))))))))) v64) NIL) 340(73 (paramod 42 (1) 72 (1 1 2 1 2 2)) (= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ (n (+ v0 (n v1))) (+ v1 v0))) v0))))) v64) NIL) 341(74 (instantiate 4 ((v0 . (n (+ v0 (n v1))))(v1 . v1)(v2 . v0))) (= (+ (n (+ v0 (n v1))) (+ v1 v0)) (+ v1 (+ (n (+ v0 (n v1))) v0))) NIL) 342(75 (paramod 74 (1) 73 (1 1 2 1 2 1 1)) (= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ v1 (+ (n (+ v0 (n v1))) v0))) v0))))) v64) NIL) 343(76 (instantiate 2 ((v0 . (n (+ v0 (n v1))))(v1 . v0))) (= (+ (n (+ v0 (n v1))) v0) (+ v0 (n (+ v0 (n v1))))) NIL) 344(77 (paramod 76 (1) 75 (1 1 2 1 2 1 1 2)) (= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ (n (+ v1 (+ v0 (n (+ v0 (n v1)))))) v0))))) v64) NIL) 345(78 (instantiate 2 ((v0 . (n (+ v1 (+ v0 (n (+ v0 (n v1)))))))(v1 . v0))) (= (+ (n (+ v1 (+ v0 (n (+ v0 (n v1)))))) v0) (+ v0 (n (+ v1 (+ v0 (n (+ v0 (n v1)))))))) NIL) 346(79 (paramod 78 (1) 77 (1 1 2 1 2)) (= (n (+ (n (+ v64 (n (+ v0 (n v1))))) (n (+ v64 (+ v0 (n (+ v1 (+ v0 (n (+ v0 (n v1))))))))))) v64) NIL) 347(80 (instantiate 79 ((v0 . v1)(v1 . v2)(v64 . v0))) (= (n (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2))))))))))) v0) (378)) 348(81 (instantiate 45 ((v0 . (d))(v1 . v65)(v2 . (c)))) (= (n (+ (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))) (n (+ (c) (d))))) (d)) NIL) 349(82 (paramod 6 (1) 81 (1 1 2 1)) (= (n (+ (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))) (n (c)))) (d)) NIL) 350(83 (instantiate 2 ((v0 . (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))))(v1 . (n (c))))) (= (+ (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))) (n (c))) (+ (n (c)) (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))))) NIL) 351(84 (paramod 83 (1) 82 (1 1)) (= (n (+ (n (c)) (n (+ (d) (+ (n (+ v65 (c))) (n (+ (c) (n v65)))))))) (d)) NIL) 352(85 (instantiate 84 ((v65 . v0))) (= (n (+ (n (c)) (n (+ (d) (+ (n (+ v0 (c))) (n (+ (c) (n v0)))))))) (d)) (432)) 353(86 (instantiate 38 ((v0 . (c))(v1 . (n (+ (d) (n (c))))))) (= (n (+ (n (+ (c) (n (+ (d) (n (c)))))) (n (+ (n (c)) (n (+ (d) (n (c)))))))) (n (+ (d) (n (c))))) NIL) 354(87 (paramod 47 (1) 86 (1 1 2)) (= (n (+ (n (+ (c) (n (+ (d) (n (c)))))) (d))) (n (+ (d) (n (c))))) NIL) 355(88 (instantiate 2 ((v0 . (n (+ (c) (n (+ (d) (n (c)))))))(v1 . (d)))) (= (+ (n (+ (c) (n (+ (d) (n (c)))))) (d)) (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))) NIL) 356(89 (paramod 88 (1) 87 (1 1)) (= (n (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))) (n (+ (d) (n (c))))) (496)) 357(90 (instantiate 30 ((v0 . v64)(v1 . (c))(v2 . (+ (d) v0)))) (= (n (+ (n (+ v64 (+ (c) (+ (d) v0)))) (n (+ (+ (d) v0) (n (+ v64 (c))))))) (+ (d) v0)) NIL) 358(91 (paramod 51 (1) 90 (1 1 1 1 2)) (= (n (+ (n (+ v64 (+ (c) v0))) (n (+ (+ (d) v0) (n (+ v64 (c))))))) (+ (d) v0)) NIL) 359(92 (instantiate 3 ((v0 . (d))(v1 . v0)(v2 . (n (+ v64 (c)))))) (= (+ (+ (d) v0) (n (+ v64 (c)))) (+ (d) (+ v0 (n (+ v64 (c)))))) NIL) 360(93 (paramod 92 (1) 91 (1 1 2 1)) (= (n (+ (n (+ v64 (+ (c) v0))) (n (+ (d) (+ v0 (n (+ v64 (c)))))))) (+ (d) v0)) NIL) 361(94 (instantiate 93 ((v0 . v1)(v64 . v0))) (= (n (+ (n (+ v0 (+ (c) v1))) (n (+ (d) (+ v1 (n (+ v0 (c)))))))) (+ (d) v1)) (548)) 362(95 (instantiate 65 ((v0 . (n (+ (d) (n (c)))))(v1 . (c)))) (= (n (+ (n (+ (d) (n (c)))) (n (+ (c) (+ (n (+ (d) (n (c)))) (n (+ (n (c)) (n (+ (d) (n (c))))))))))) (n (+ (n (c)) (n (+ (d) (n (c))))))) NIL) 363(96 (paramod 47 (1) 95 (1 1 2 1 2 2)) (= (n (+ (n (+ (d) (n (c)))) (n (+ (c) (+ (n (+ (d) (n (c)))) (d)))))) (n (+ (n (c)) (n (+ (d) (n (c))))))) NIL) 364(97 (instantiate 2 ((v0 . (n (+ (d) (n (c)))))(v1 . (d)))) (= (+ (n (+ (d) (n (c)))) (d)) (+ (d) (n (+ (d) (n (c)))))) NIL) 365(98 (paramod 97 (1) 96 (1 1 2 1 2)) (= (n (+ (n (+ (d) (n (c)))) (n (+ (c) (+ (d) (n (+ (d) (n (c))))))))) (n (+ (n (c)) (n (+ (d) (n (c))))))) NIL) 366(99 (instantiate 51 ((v0 . (n (+ (d) (n (c))))))) (= (+ (c) (+ (d) (n (+ (d) (n (c)))))) (+ (c) (n (+ (d) (n (c)))))) NIL) 367(100 (paramod 99 (1) 98 (1 1 2 1)) (= (n (+ (n (+ (d) (n (c)))) (n (+ (c) (n (+ (d) (n (c)))))))) (n (+ (n (c)) (n (+ (d) (n (c))))))) NIL) 368(101 (paramod 47 (1) 100 (2)) (= (n (+ (n (+ (d) (n (c)))) (n (+ (c) (n (+ (d) (n (c)))))))) (d)) (832)) 369(102 (instantiate 80 ((v0 . (n (c)))(v1 . (d))(v2 . (c)))) (= (n (+ (n (+ (n (c)) (n (+ (d) (n (c)))))) (n (+ (n (c)) (+ (d) (n (+ (c) (+ (d) (n (+ (d) (n (c)))))))))))) (n (c))) NIL) 370(103 (paramod 47 (1) 102 (1 1 1)) (= (n (+ (d) (n (+ (n (c)) (+ (d) (n (+ (c) (+ (d) (n (+ (d) (n (c)))))))))))) (n (c))) NIL) 371(104 (instantiate 51 ((v0 . (n (+ (d) (n (c))))))) (= (+ (c) (+ (d) (n (+ (d) (n (c)))))) (+ (c) (n (+ (d) (n (c)))))) NIL) 372(105 (paramod 104 (1) 103 (1 1 2 1 2 2 1)) (= (n (+ (d) (n (+ (n (c)) (+ (d) (n (+ (c) (n (+ (d) (n (c))))))))))) (n (c))) NIL) 373(106 (instantiate 4 ((v0 . (n (c)))(v1 . (d))(v2 . (n (+ (c) (n (+ (d) (n (c))))))))) (= (+ (n (c)) (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))) (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))) NIL) 374(107 (paramod 106 (1) 105 (1 1 2 1)) (= (n (+ (d) (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))))) (n (c))) (1042)) 375(108 (instantiate 54 ((v0 . (n (+ (c) (n (+ (d) (n (c))))))))) (= (n (+ (n (+ (n (+ (c) (n (+ (d) (n (c)))))) (c))) (n (+ (c) (n (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))))))) (c)) NIL) 376(109 (paramod 89 (1) 108 (1 1 2 1 2)) (= (n (+ (n (+ (n (+ (c) (n (+ (d) (n (c)))))) (c))) (n (+ (c) (n (+ (d) (n (c)))))))) (c)) NIL) 377(110 (instantiate 2 ((v0 . (n (+ (c) (n (+ (d) (n (c)))))))(v1 . (c)))) (= (+ (n (+ (c) (n (+ (d) (n (c)))))) (c)) (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))) NIL) 378(111 (paramod 110 (1) 109 (1 1 1 1)) (= (n (+ (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))) (n (+ (c) (n (+ (d) (n (c)))))))) (c)) NIL) 379(112 (instantiate 2 ((v0 . (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))))(v1 . (n (+ (c) (n (+ (d) (n (c))))))))) (= (+ (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))) (n (+ (c) (n (+ (d) (n (c))))))) (+ (n (+ (c) (n (+ (d) (n (c)))))) (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))))) NIL) 380(113 (paramod 112 (1) 111 (1 1)) (= (n (+ (n (+ (c) (n (+ (d) (n (c)))))) (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))))) (c)) (1112)) 381(114 (instantiate 58 ((v0 . (n (c)))(v1 . (n (+ (c) (n (+ (d) (n (c)))))))(v2 . (d)))) (= (n (+ (n (+ (n (c)) (+ (n (+ (c) (n (+ (d) (n (c)))))) (d)))) (n (+ (n (+ (d) (n (c)))) (n (+ (c) (n (+ (d) (n (c)))))))))) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 382(115 (paramod 101 (1) 114 (1 1 2)) (= (n (+ (n (+ (n (c)) (+ (n (+ (c) (n (+ (d) (n (c)))))) (d)))) (d))) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 383(116 (instantiate 2 ((v0 . (n (+ (c) (n (+ (d) (n (c)))))))(v1 . (d)))) (= (+ (n (+ (c) (n (+ (d) (n (c)))))) (d)) (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))) NIL) 384(117 (paramod 116 (1) 115 (1 1 1 1 2)) (= (n (+ (n (+ (n (c)) (+ (d) (n (+ (c) (n (+ (d) (n (c))))))))) (d))) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 385(118 (instantiate 4 ((v0 . (n (c)))(v1 . (d))(v2 . (n (+ (c) (n (+ (d) (n (c))))))))) (= (+ (n (c)) (+ (d) (n (+ (c) (n (+ (d) (n (c)))))))) (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))) NIL) 386(119 (paramod 118 (1) 117 (1 1 1 1)) (= (n (+ (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))) (d))) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 387(120 (instantiate 2 ((v0 . (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))))(v1 . (d)))) (= (+ (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))) (d)) (+ (d) (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))))) NIL) 388(121 (paramod 120 (1) 119 (1 1)) (= (n (+ (d) (n (+ (d) (+ (n (c)) (n (+ (c) (n (+ (d) (n (c))))))))))) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 389(122 (paramod 107 (1) 121 (1)) (= (n (c)) (n (+ (c) (n (+ (d) (n (c))))))) NIL) 390(123 (flip 122 ()) (= (n (+ (c) (n (+ (d) (n (c)))))) (n (c))) (1278)) 391(124 (paramod 123 (1) 113 (1 1 1)) (= (n (+ (n (c)) (n (+ (c) (n (+ (c) (n (+ (d) (n (c)))))))))) (c)) NIL) 392(125 (paramod 123 (1) 124 (1 1 2 1 2)) (= (n (+ (n (c)) (n (+ (c) (n (c)))))) (c)) (1298)) 393(126 (instantiate 80 ((v0 . (n (c)))(v1 . (c))(v2 . (c)))) (= (n (+ (n (+ (n (c)) (n (+ (c) (n (c)))))) (n (+ (n (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))) (n (c))) NIL) 394(127 (paramod 125 (1) 126 (1 1 1)) (= (n (+ (c) (n (+ (n (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))) (n (c))) NIL) 395(128 (instantiate 4 ((v0 . (n (c)))(v1 . (c))(v2 . (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) (= (+ (n (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))) (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) NIL) 396(129 (paramod 128 (1) 127 (1 1 2 1)) (= (n (+ (c) (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))) (n (c))) (1404)) 397(130 (instantiate 65 ((v0 . (n (+ (c) (n (c)))))(v1 . (c)))) (= (n (+ (n (+ (c) (n (c)))) (n (+ (c) (+ (n (+ (c) (n (c)))) (n (+ (n (c)) (n (+ (c) (n (c))))))))))) (n (+ (n (c)) (n (+ (c) (n (c))))))) NIL) 398(131 (paramod 125 (1) 130 (1 1 2 1 2 2)) (= (n (+ (n (+ (c) (n (c)))) (n (+ (c) (+ (n (+ (c) (n (c)))) (c)))))) (n (+ (n (c)) (n (+ (c) (n (c))))))) NIL) 399(132 (instantiate 2 ((v0 . (n (+ (c) (n (c)))))(v1 . (c)))) (= (+ (n (+ (c) (n (c)))) (c)) (+ (c) (n (+ (c) (n (c)))))) NIL) 400(133 (paramod 132 (1) 131 (1 1 2 1 2)) (= (n (+ (n (+ (c) (n (c)))) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))) (n (+ (n (c)) (n (+ (c) (n (c))))))) NIL) 401(134 (paramod 125 (1) 133 (2)) (= (n (+ (n (+ (c) (n (c)))) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))) (c)) (1420)) 402(135 (instantiate 58 ((v0 . (n (c)))(v1 . (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))(v2 . (c)))) (= (n (+ (n (+ (n (c)) (+ (n (+ (c) (+ (c) (n (+ (c) (n (c))))))) (c)))) (n (+ (n (+ (c) (n (c)))) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))))) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 403(136 (paramod 134 (1) 135 (1 1 2)) (= (n (+ (n (+ (n (c)) (+ (n (+ (c) (+ (c) (n (+ (c) (n (c))))))) (c)))) (c))) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 404(137 (instantiate 2 ((v0 . (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))(v1 . (c)))) (= (+ (n (+ (c) (+ (c) (n (+ (c) (n (c))))))) (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))) NIL) 405(138 (paramod 137 (1) 136 (1 1 1 1 2)) (= (n (+ (n (+ (n (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) (c))) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 406(139 (instantiate 4 ((v0 . (n (c)))(v1 . (c))(v2 . (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) (= (+ (n (c)) (+ (c) (n (+ (c) (+ (c) (n (+ (c) (n (c))))))))) (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) NIL) 407(140 (paramod 139 (1) 138 (1 1 1 1)) (= (n (+ (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) (c))) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 408(141 (instantiate 2 ((v0 . (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))(v1 . (c)))) (= (+ (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))) (c)) (+ (c) (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))) NIL) 409(142 (paramod 141 (1) 140 (1 1)) (= (n (+ (c) (n (+ (c) (+ (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))))))) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 410(143 (paramod 129 (1) 142 (1)) (= (n (c)) (n (+ (c) (+ (c) (n (+ (c) (n (c)))))))) NIL) 411(144 (flip 143 ()) (= (n (+ (c) (+ (c) (n (+ (c) (n (c))))))) (n (c))) (1482)) 412(145 (instantiate 94 ((v0 . (c))(v1 . (n (+ (c) (n (c))))))) (= (n (+ (n (+ (c) (+ (c) (n (+ (c) (n (c))))))) (n (+ (d) (+ (n (+ (c) (n (c)))) (n (+ (c) (c)))))))) (+ (d) (n (+ (c) (n (c)))))) NIL) 413(146 (paramod 144 (1) 145 (1 1 1)) (= (n (+ (n (c)) (n (+ (d) (+ (n (+ (c) (n (c)))) (n (+ (c) (c)))))))) (+ (d) (n (+ (c) (n (c)))))) NIL) 414(147 (instantiate 2 ((v0 . (n (+ (c) (n (c)))))(v1 . (n (+ (c) (c)))))) (= (+ (n (+ (c) (n (c)))) (n (+ (c) (c)))) (+ (n (+ (c) (c))) (n (+ (c) (n (c)))))) NIL) 415(148 (paramod 147 (1) 146 (1 1 2 1 2)) (= (n (+ (n (c)) (n (+ (d) (+ (n (+ (c) (c))) (n (+ (c) (n (c))))))))) (+ (d) (n (+ (c) (n (c)))))) NIL) 416(149 (instantiate 85 ((v0 . (c)))) (= (n (+ (n (c)) (n (+ (d) (+ (n (+ (c) (c))) (n (+ (c) (n (c))))))))) (d)) NIL) 417(150 (paramod 149 (1) 148 (1)) (= (d) (+ (d) (n (+ (c) (n (c)))))) NIL) 418(151 (flip 150 ()) (= (+ (d) (n (+ (c) (n (c))))) (d)) (1520)) 419(152 (instantiate 71 ((v0 . v64)(v1 . (n (+ (c) (n (c)))))(v2 . (d)))) (= (n (+ (n (+ v64 (+ (n (+ (c) (n (c)))) (n (d))))) (n (+ v64 (+ (d) (n (+ (c) (n (c))))))))) (+ v64 (n (+ (c) (n (c)))))) NIL) 420(153 (paramod 151 (1) 152 (1 1 2 1 2)) (= (n (+ (n (+ v64 (+ (n (+ (c) (n (c)))) (n (d))))) (n (+ v64 (d))))) (+ v64 (n (+ (c) (n (c)))))) NIL) 421(154 (instantiate 2 ((v0 . (n (+ (c) (n (c)))))(v1 . (n (d))))) (= (+ (n (+ (c) (n (c)))) (n (d))) (+ (n (d)) (n (+ (c) (n (c)))))) NIL) 422(155 (paramod 154 (1) 153 (1 1 1 1 2)) (= (n (+ (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))) (n (+ v64 (d))))) (+ v64 (n (+ (c) (n (c)))))) NIL) 423(156 (instantiate 2 ((v0 . (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))))(v1 . (n (+ v64 (d)))))) (= (+ (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))) (n (+ v64 (d)))) (+ (n (+ v64 (d))) (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))))) NIL) 424(157 (paramod 156 (1) 155 (1 1)) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))))) (+ v64 (n (+ (c) (n (c)))))) NIL) 425(158 (instantiate 157 ((v64 . v0))) (= (n (+ (n (+ v0 (d))) (n (+ v0 (+ (n (d)) (n (+ (c) (n (c))))))))) (+ v0 (n (+ (c) (n (c)))))) (1628)) 426(159 (instantiate 22 ((v0 . v64)(v1 . (d))(v2 . (+ (c) (n (c)))))) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (+ (d) (+ (c) (n (c))))) (n (+ (d) (n (+ (c) (n (c))))))))))) v64) NIL) 427(160 (paramod 151 (1) 159 (1 1 2 1 2 2 1)) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (+ (d) (+ (c) (n (c))))) (n (d))))))) v64) NIL) 428(161 (instantiate 4 ((v0 . (d))(v1 . (c))(v2 . (n (c))))) (= (+ (d) (+ (c) (n (c)))) (+ (c) (+ (d) (n (c))))) NIL) 429(162 (paramod 161 (1) 160 (1 1 2 1 2 1 1)) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (+ (c) (+ (d) (n (c))))) (n (d))))))) v64) NIL) 430(163 (instantiate 51 ((v0 . (n (c))))) (= (+ (c) (+ (d) (n (c)))) (+ (c) (n (c)))) NIL) 431(164 (paramod 163 (1) 162 (1 1 2 1 2 1 1)) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (+ (c) (n (c)))) (n (d))))))) v64) NIL) 432(165 (instantiate 2 ((v0 . (n (+ (c) (n (c)))))(v1 . (n (d))))) (= (+ (n (+ (c) (n (c)))) (n (d))) (+ (n (d)) (n (+ (c) (n (c)))))) NIL) 433(166 (paramod 165 (1) 164 (1 1 2 1 2)) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))))) v64) NIL) 434(167 (instantiate 158 ((v0 . v64))) (= (n (+ (n (+ v64 (d))) (n (+ v64 (+ (n (d)) (n (+ (c) (n (c))))))))) (+ v64 (n (+ (c) (n (c)))))) NIL) 435(168 (paramod 167 (1) 166 (1)) (= (+ v64 (n (+ (c) (n (c))))) v64) NIL) 436(169 (instantiate 168 ((v64 . v0))) (= (+ v0 (n (+ (c) (n (c))))) v0) (1642)) 437(170 (instantiate 2 ((v0 . v64)(v1 . (n (+ (c) (n (c))))))) (= (+ v64 (n (+ (c) (n (c))))) (+ (n (+ (c) (n (c)))) v64)) NIL) 438(171 (instantiate 169 ((v0 . v64))) (= (+ v64 (n (+ (c) (n (c))))) v64) NIL) 439(172 (paramod 170 (1) 171 (1)) (= (+ (n (+ (c) (n (c)))) v64) v64) NIL) 440(173 (instantiate 172 ((v64 . v0))) (= (+ (n (+ (c) (n (c)))) v0) v0) (1698)) 441(174 (instantiate 169 ((v0 . (n v65)))) (= (+ (n v65) (n (+ (c) (n (c))))) (n v65)) NIL) 442(175 (instantiate 65 ((v0 . (n (+ (c) (n (c)))))(v1 . v65))) (= (n (+ (n (+ (c) (n (c)))) (n (+ v65 (+ (n (+ (c) (n (c)))) (n (+ (n v65) (n (+ (c) (n (c))))))))))) (n (+ (n v65) (n (+ (c) (n (c))))))) NIL) 443(176 (paramod 174 (1) 175 (1 1 2 1 2 2 1)) (= (n (+ (n (+ (c) (n (c)))) (n (+ v65 (+ (n (+ (c) (n (c)))) (n (n v65))))))) (n (+ (n v65) (n (+ (c) (n (c))))))) NIL) 444(177 (instantiate 173 ((v0 . (n (n v65))))) (= (+ (n (+ (c) (n (c)))) (n (n v65))) (n (n v65))) NIL) 445(178 (paramod 177 (1) 176 (1 1 2 1 2)) (= (n (+ (n (+ (c) (n (c)))) (n (+ v65 (n (n v65)))))) (n (+ (n v65) (n (+ (c) (n (c))))))) NIL) 446(179 (instantiate 173 ((v0 . (n (+ v65 (n (n v65))))))) (= (+ (n (+ (c) (n (c)))) (n (+ v65 (n (n v65))))) (n (+ v65 (n (n v65))))) NIL) 447(180 (paramod 179 (1) 178 (1 1)) (= (n (n (+ v65 (n (n v65))))) (n (+ (n v65) (n (+ (c) (n (c))))))) NIL) 448(181 (instantiate 169 ((v0 . (n v65)))) (= (+ (n v65) (n (+ (c) (n (c))))) (n v65)) NIL) 449(182 (paramod 181 (1) 180 (2 1)) (= (n (n (+ v65 (n (n v65))))) (n (n v65))) NIL) 450(183 (instantiate 182 ((v65 . v0))) (= (n (n (+ v0 (n (n v0))))) (n (n v0))) (1752)) 451(184 (instantiate 173 ((v0 . (n (+ (n (+ (n (+ (c) (n (c)))) v65)) (n (n (+ (n (+ (c) (n (c)))) (n v65))))))))) (= (+ (n (+ (c) (n (c)))) (n (+ (n (+ (n (+ (c) (n (c)))) v65)) (n (n (+ (n (+ (c) (n (c)))) (n v65))))))) (n (+ (n (+ (n (+ (c) (n (c)))) v65)) (n (n (+ (n (+ (c) (n (c)))) (n v65))))))) NIL) 452(185 (instantiate 17 ((v0 . (n (+ (c) (n (c)))))(v1 . v65))) (= (n (+ (n (+ (c) (n (c)))) (n (+ (n (+ (n (+ (c) (n (c)))) v65)) (n (n (+ (n (+ (c) (n (c)))) (n v65)))))))) (n (+ (n (+ (c) (n (c)))) v65))) NIL) 453(186 (paramod 184 (1) 185 (1 1)) (= (n (n (+ (n (+ (n (+ (c) (n (c)))) v65)) (n (n (+ (n (+ (c) (n (c)))) (n v65))))))) (n (+ (n (+ (c) (n (c)))) v65))) NIL) 454(187 (instantiate 173 ((v0 . v65))) (= (+ (n (+ (c) (n (c)))) v65) v65) NIL) 455(188 (paramod 187 (1) 186 (1 1 1 1 1)) (= (n (n (+ (n v65) (n (n (+ (n (+ (c) (n (c)))) (n v65))))))) (n (+ (n (+ (c) (n (c)))) v65))) NIL) 456(189 (instantiate 173 ((v0 . (n v65)))) (= (+ (n (+ (c) (n (c)))) (n v65)) (n v65)) NIL) 457(190 (paramod 189 (1) 188 (1 1 1 2 1 1)) (= (n (n (+ (n v65) (n (n (n v65)))))) (n (+ (n (+ (c) (n (c)))) v65))) NIL) 458(191 (instantiate 183 ((v0 . (n v65)))) (= (n (n (+ (n v65) (n (n (n v65)))))) (n (n (n v65)))) NIL) 459(192 (paramod 191 (1) 190 (1)) (= (n (n (n v65))) (n (+ (n (+ (c) (n (c)))) v65))) NIL) 460(193 (instantiate 173 ((v0 . v65))) (= (+ (n (+ (c) (n (c)))) v65) v65) NIL) 461(194 (paramod 193 (1) 192 (2 1)) (= (n (n (n v65))) (n v65)) NIL) 462(195 (instantiate 194 ((v65 . v0))) (= (n (n (n v0))) (n v0)) (1961)) 463(196 (instantiate 195 ((v0 . (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2))))))))))))) (= (n (n (n (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2))))))))))))) (n (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2)))))))))))) NIL) 464(197 (paramod 80 (1) 196 (1 1 1)) (= (n (n v0)) (n (+ (n (+ v0 (n (+ v1 (n v2))))) (n (+ v0 (+ v1 (n (+ v2 (+ v1 (n (+ v1 (n v2)))))))))))) NIL) 465(198 (paramod 80 (1) 197 (2)) (= (n (n v0)) v0) (2031)) 466(199 (instantiate 198 ((v0 . (+ (n (+ v0 v1)) (n (+ (n v0) v1)))))) (= (n (n (+ (n (+ v0 v1)) (n (+ (n v0) v1))))) (+ (n (+ v0 v1)) (n (+ (n v0) v1)))) NIL) 467(200 (paramod 38 (1) 199 (1 1)) (= (n v1) (+ (n (+ v0 v1)) (n (+ (n v0) v1)))) NIL) 468(201 (flip 200 ()) (= (+ (n (+ v0 v1)) (n (+ (n v0) v1))) (n v1)) (2143)) 469(202 (instantiate 201 ((v0 . (A))(v1 . (n (B))))) (= (+ (n (+ (A) (n (B)))) (n (+ (n (A)) (n (B))))) (n (n (B)))) NIL) 470(203 (paramod 202 (1) 7 (1 1)) (not (= (n (n (B))) (B))) NIL) 471(204 (instantiate 198 ((v0 . (B)))) (= (n (n (B))) (B)) NIL) 472(205 (paramod 204 (1) 203 (1 1)) (not (= (B) (B))) (2173)) 473(206 (instantiate 1 ((v0 . (B)))) (= (B) (B)) NIL) 474(207 (resolve 205 () 206 ()) false (2174)) 475 476Search stopped by max_proofs option. 477 478) 479;; END OF PROOF OBJECT 480 481Search stopped by max_proofs option. 482 483============ end of search ============ 484 485-------------- statistics ------------- 486clauses given 48 487clauses generated 3063 488 para_from generated 1790 489 para_into generated 1273 490demod & eval rewrites 6647 491clauses wt,lit,sk delete 773 492tautologies deleted 0 493clauses forward subsumed 1669 494 (subsumed by sos) 16 495unit deletions 0 496factor simplifications 0 497clauses kept 1073 498new demodulators 1067 499empty clauses 1 500clauses back demodulated 423 501clauses back subsumed 2 502usable size 24 503sos size 624 504demodulators size 645 505passive size 0 506hot size 0 507Kbytes malloced 7812 508 509----------- times (seconds) ----------- 510user CPU time 0.48 (0 hr, 0 min, 0 sec) 511system CPU time 0.01 (0 hr, 0 min, 0 sec) 512wall-clock time 0 (0 hr, 0 min, 0 sec) 513 514That finishes the proof of the theorem. 515 516Process 8947 finished Mon Aug 2 15:31:15 2004 517