----- Otter 3.3f, August 2004 ----- The process was started by mccune on cleo.thornwood, Mon Nov 14 15:26:22 2005 The command was "otter33f -f thm2.in". The process ID is 16994. % Reading file thm2.in. op(400,xfx,[*,+,^,v,/,\,#]). lrpo_multiset_status([_*_]). set(knuth_bendix). dependent: set(anl_eq). 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(process_input). dependent: set(lrpo). set(hyper_res). set(para_from_units_only). set(para_into_units_only). clear(print_kept). list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] x* (y*x)=y. 0 [] x*y=y*x. 0 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. end_of_list. list(passive). 1 [] ((A*B)*C)*D!= ((D*B)*C)*A. end_of_list. ------------> process usable: ** KEPT (pick-wt=3): 2 [] x=x. Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=7): 3 [] x* (y*x)=y. ---> New Demodulator: 4 [new_demod,3] x* (y*x)=y. ** KEPT (pick-wt=7): 5 [] x*y=y*x. ** KEPT (pick-wt=22): 6 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. >>>> Starting back demodulation with 4. Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] x*y=y*x. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=7) 3 [] x* (y*x)=y. ---> New Demodulator: 8 [new_demod,7] (x*y)*x=y. >>>> Starting back demodulation with 8. given clause #2: (wt=7) 5 [] x*y=y*x. ---> New Demodulator: 10 [new_demod,9] (x*y)*y=x. >>>> Starting back demodulation with 10. ---> New Demodulator: 12 [new_demod,11] x* (x*y)=y. >>>> Starting back demodulation with 12. given clause #3: (wt=7) 7 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. given clause #4: (wt=7) 9 [para_into,5.1.1,3.1.1,flip.1] (x*y)*y=x. given clause #5: (wt=7) 11 [para_from,5.1.1,3.1.1.2] x* (x*y)=y. given clause #6: (wt=22) 6 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. ---> New Demodulator: 15 [new_demod,14] (x* ((y*z)*u))*y= (x*z)*u. >>>> Starting back demodulation with 15. given clause #7: (wt=15) 14 [hyper,6,7] (x* ((y*z)*u))*y= (x*z)*u. ---> New Demodulator: 25 [new_demod,24] (x* ((y*z)*u))*z= (x*y)*u. ---> New Demodulator: 29 [new_demod,28] (x* (y* (z*u)))*z= (x*u)*y. ---> New Demodulator: 32 [new_demod,31] ((x* ((((y*z)*u)*v)*w))*z)*u= ((x*v)*w)*y. ---> New Demodulator: 34 [new_demod,33] ((((x*y)*z)*u)*y)*z=u*x. ---> New Demodulator: 36 [new_demod,35] (((x*y)*z)*u)*x= (u*y)*z. ---> New Demodulator: 38 [new_demod,37] x* (y* ((x*z)*u))= (y*z)*u. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. >>>> Starting back demodulation with 36. >>>> Starting back demodulation with 38. ---> New Demodulator: 46 [new_demod,45] (x* ((y*z)*u))* ((x*z)*u)=y. ---> New Demodulator: 49 [new_demod,48] ((x*y)*z)* (x* ((u*y)*z))=u. >>>> Starting back demodulation with 46. >>>> Starting back demodulation with 49. given clause #8: (wt=15) 16 [hyper,6,5] (x*y)* (z*u)= (x*u)* (z*y). ---> New Demodulator: 81 [new_demod,80] (x* (((y*z)* (u*v))*w))* (y*v)= (x* (u*z))*w. ---> New Demodulator: 83 [new_demod,82] (x*y)* ((x*z)* (u*y))=u*z. ---> New Demodulator: 85 [new_demod,84] ((x*y)* (z*u))* (z*y)=x*u. ---> New Demodulator: 87 [new_demod,86] ((x*y)* (z*u))* (x*u)=z*y. ---> New Demodulator: 89 [new_demod,88] (x*y)* ((z*y)* (x*u))=z*u. >>>> Starting back demodulation with 81. >>>> Starting back demodulation with 83. >>>> Starting back demodulation with 85. >>>> Starting back demodulation with 87. >>>> Starting back demodulation with 89. given clause #9: (wt=15) 21 [para_into,14.1.1.1.2.1,11.1.1] (x* (y*z))*u= (x* (u*y))*z. ---> New Demodulator: 93 [new_demod,92] (x* (y* (z* ((u*v)*w))))*u= (x* ((z*v)*w))*y. ---> New Demodulator: 95 [new_demod,94] (x* (y* (z*u)))*u= (x*z)*y. ---> New Demodulator: 101 [new_demod,100] ((x* (((y*z)*u)*v))* (w*y))*z= ((x*u)*v)*w. ---> New Demodulator: 103 [new_demod,102] ((x* (y*z))* (u*y))*z=x*u. ---> New Demodulator: 105 [new_demod,104] (((x*y)*z)* (u*x))*y=z*u. ---> New Demodulator: 109 [new_demod,108] (x* (((x* (y*z))*u)*y))*z=u. >>>> Starting back demodulation with 93. >>>> Starting back demodulation with 95. >>>> Starting back demodulation with 101. >>>> Starting back demodulation with 103. >>>> Starting back demodulation with 105. >>>> Starting back demodulation with 109. ---> New Demodulator: 121 [new_demod,120] (x* (((y* (z*u))*v)*w))* (y* (u*v))= (x*z)*w. ---> New Demodulator: 125 [new_demod,124] (x* (y*z))* ((x* (u*y))*z)=u. ---> New Demodulator: 127 [new_demod,126] ((x* (y*z))*u)*y=x* (z*u). ---> New Demodulator: 129 [new_demod,128] ((x* (y*z))*u)* (x* (z*u))=y. ---> New Demodulator: 131 [new_demod,130] x* ((y* (x*z))*u)=y* (z*u). >>>> Starting back demodulation with 121. >>>> Starting back demodulation with 125. >>>> Starting back demodulation with 127. >> back demodulating 108 with 127. >>>> Starting back demodulation with 129. >>>> Starting back demodulation with 131. given clause #10: (wt=15) 22 [para_into,14.1.1.1.2.1,9.1.1] (x* (y*z))* (y*u)= (x*u)*z. ---> New Demodulator: 143 [new_demod,142] ((x* (((y*z)*u)*v))*w)*z= ((x*u)*v)* (y*w). ---> New Demodulator: 145 [new_demod,144] ((x* (y*z))*u)*z=x* (y*u). ---> New Demodulator: 147 [new_demod,146] (((x*y)*z)*u)*y=z* (x*u). ---> New Demodulator: 153 [new_demod,152] (x* ((y* ((z*u)*v))*w))* ((y*u)*v)= (x*z)*w. >>>> Starting back demodulation with 143. >> back demodulating 100 with 143. >> back demodulating 31 with 143. >>>> Starting back demodulation with 145. >> back demodulating 102 with 145. >>>> Starting back demodulation with 147. >> back demodulating 104 with 147. >> back demodulating 33 with 147. >>>> Starting back demodulation with 153. ---> New Demodulator: 173 [new_demod,172] (x* (y*z))* ((x*u)*z)=y*u. ---> New Demodulator: 175 [new_demod,174] ((x*y)*z)* (x* (u*z))=u*y. >>>> Starting back demodulation with 173. >> back demodulating 124 with 173. >> back demodulating 45 with 173. >>>> Starting back demodulation with 175. >> back demodulating 128 with 175. >> back demodulating 48 with 175. given clause #11: (wt=15) 23 [para_into,14.1.1.1.2.1,7.1.1] (x* (y*z))* (u*y)= (x*u)*z. 196 back subsumes 194. given clause #12: (wt=11) 195 [para_into,23.1.1.1,11.1.1] x* (y*z)= (z*y)*x. ---> New Demodulator: 250 [new_demod,249] (x*y)* (z* (((y*x)*u)*v))= (z*u)*v. ---> New Demodulator: 252 [new_demod,251] (x*y)* (z* (y*x))=z. ---> New Demodulator: 254 [new_demod,253] (x*y)* ((y*x)*z)=z. >>>> Starting back demodulation with 250. >>>> Starting back demodulation with 252. >>>> Starting back demodulation with 254. ---> New Demodulator: 275 [new_demod,274] ((x*y)*z)* (y*x)=z. >>>> Starting back demodulation with 275. given clause #13: (wt=11) 196 [para_into,23.1.1.1,9.1.1,demod,145] x* (y*z)=x* (z*y). ---> New Demodulator: 294 [new_demod,293] (x* (((y*z)*u)*v))* (z*y)= (x*u)*v. ---> New Demodulator: 296 [new_demod,295] (x* (y*z))* (z*y)=x. >>>> Starting back demodulation with 294. >>>> Starting back demodulation with 296. given clause #14: (wt=11) 214 [copy,195,flip.1] (x*y)*z=z* (y*x). ---> New Demodulator: 328 [new_demod,327] x* (((x*y)*z)*u)= (u*y)*z. >>>> Starting back demodulation with 328. >> back demodulating 78 with 328. >> back demodulating 64 with 328. ---> New Demodulator: 347 [new_demod,346] (x* ((y* (z*u))*v))* (u*z)= (x*y)*v. >>>> Starting back demodulation with 347. given clause #15: (wt=11) 251 [para_into,195.1.1,9.1.1,flip.1] (x*y)* (z* (y*x))=z. ---> New Demodulator: 360 [new_demod,359] (x* (y*z))* (u* (x* (z*y)))=u. ---> New Demodulator: 362 [new_demod,361] (x* (y*z))* (u* ((z*y)*x))=u. ---> New Demodulator: 364 [new_demod,363] ((x*y)*z)* (u* ((y*x)*z))=u. ---> New Demodulator: 366 [new_demod,365] ((x*y)*z)* (u* ((y*v)* (x* (v*z))))=u. ---> New Demodulator: 368 [new_demod,367] ((x*y)*z)* (u* ((v*y)* (x* (v*z))))=u. ---> New Demodulator: 370 [new_demod,369] ((x* (y*z))*u)* (v* (y* (x* (z*u))))=v. ---> New Demodulator: 372 [new_demod,371] ((x*y)* (z*u))* (v* ((z*y)* (x*u)))=v. ---> New Demodulator: 374 [new_demod,373] ((x*y)*z)* (u* (z* (y*x)))=u. ---> New Demodulator: 376 [new_demod,375] ((x*y)* (z* (y*u)))* (v* ((z*x)*u))=v. ---> New Demodulator: 378 [new_demod,377] ((x*y)* (z* (x*u)))* (v* ((z*y)*u))=v. ---> New Demodulator: 380 [new_demod,379] (x* (y* (z*u)))* (v* ((y* (x*z))*u))=v. ---> New Demodulator: 382 [new_demod,381] (x*y)* ((z* ((y*x)*u))*v)=z* (u*v). ---> New Demodulator: 384 [new_demod,383] (x*y)* ((z*x)* (y*u))=z*u. >>>> Starting back demodulation with 360. >>>> Starting back demodulation with 362. >>>> Starting back demodulation with 364. >>>> Starting back demodulation with 366. >>>> Starting back demodulation with 368. >>>> Starting back demodulation with 370. >>>> Starting back demodulation with 372. >>>> Starting back demodulation with 374. >>>> Starting back demodulation with 376. >>>> Starting back demodulation with 378. >>>> Starting back demodulation with 380. >>>> Starting back demodulation with 382. >>>> Starting back demodulation with 384. given clause #16: (wt=11) 253 [para_into,195.1.1,7.1.1,flip.1] (x*y)* ((y*x)*z)=z. ---> New Demodulator: 397 [new_demod,396] (x* (y*z))* ((x* (z*y))*u)=u. ---> New Demodulator: 399 [new_demod,398] (x* (y*z))* (((z*y)*x)*u)=u. ---> New Demodulator: 401 [new_demod,400] ((x*y)*z)* (((y*x)*z)*u)=u. ---> New Demodulator: 403 [new_demod,402] ((x*y)*z)* (((y*u)* (x* (u*z)))*v)=v. ---> New Demodulator: 405 [new_demod,404] ((x*y)*z)* (((u*y)* (x* (u*z)))*v)=v. ---> New Demodulator: 407 [new_demod,406] ((x* (y*z))*u)* ((y* (x* (z*u)))*v)=v. ---> New Demodulator: 409 [new_demod,408] ((x*y)* (z*u))* (((z*y)* (x*u))*v)=v. ---> New Demodulator: 411 [new_demod,410] ((x*y)*z)* ((z* (y*x))*u)=u. ---> New Demodulator: 413 [new_demod,412] ((x*y)* (z* (y*u)))* (((z*x)*u)*v)=v. ---> New Demodulator: 415 [new_demod,414] ((x*y)* (z* (x*u)))* (((z*y)*u)*v)=v. ---> New Demodulator: 417 [new_demod,416] (x* (y* (z*u)))* (((y* (x*z))*u)*v)=v. ---> New Demodulator: 419 [new_demod,418] ((x*y)*z)* ((z*u)*y)=u*x. ---> New Demodulator: 421 [new_demod,420] (x*y)* ((y*z)* (u*x))=u*z. >>>> Starting back demodulation with 397. >>>> Starting back demodulation with 399. >>>> Starting back demodulation with 401. >>>> Starting back demodulation with 403. >>>> Starting back demodulation with 405. >>>> Starting back demodulation with 407. >>>> Starting back demodulation with 409. >>>> Starting back demodulation with 411. >>>> Starting back demodulation with 413. >>>> Starting back demodulation with 415. >>>> Starting back demodulation with 417. >>>> Starting back demodulation with 419. >>>> Starting back demodulation with 421. given clause #17: (wt=11) 255 [para_into,195.1.1,5.1.1] (x*y)*z= (y*x)*z. given clause #18: (wt=11) 274 [para_from,195.1.1,9.1.1.1] ((x*y)*z)* (y*x)=z. ---> New Demodulator: 443 [new_demod,442] (((x*y)*z)*u)* (z* (y*x))=u. ---> New Demodulator: 445 [new_demod,444] ((x* (y*z))*u)* (x* (z*y))=u. ---> New Demodulator: 447 [new_demod,446] ((x* (y*z))*u)* ((z*y)*x)=u. ---> New Demodulator: 449 [new_demod,448] (((x*y)*z)*u)* ((y*x)*z)=u. ---> New Demodulator: 451 [new_demod,450] (((x*y)*z)*u)* ((y*v)* (x* (v*z)))=u. ---> New Demodulator: 453 [new_demod,452] (((x*y)*z)*u)* ((v*y)* (x* (v*z)))=u. ---> New Demodulator: 455 [new_demod,454] (((x* (y*z))*u)*v)* (y* (x* (z*u)))=v. ---> New Demodulator: 457 [new_demod,456] (((x*y)* (z*u))*v)* ((z*y)* (x*u))=v. ---> New Demodulator: 459 [new_demod,458] ((x*y)*z)* ((u*z)*x)=y*u. ---> New Demodulator: 461 [new_demod,460] ((x*y)* (z*u))* (u*x)=z*y. ---> New Demodulator: 463 [new_demod,462] (((x*y)* (z* (y*u)))*v)* ((z*x)*u)=v. ---> New Demodulator: 465 [new_demod,464] (((x*y)* (z* (x*u)))*v)* ((z*y)*u)=v. ---> New Demodulator: 467 [new_demod,466] ((x* (y* (z*u)))*v)* ((y* (x*z))*u)=v. >>>> Starting back demodulation with 443. >>>> Starting back demodulation with 445. >>>> Starting back demodulation with 447. >>>> Starting back demodulation with 449. >>>> Starting back demodulation with 451. >>>> Starting back demodulation with 453. >>>> Starting back demodulation with 455. >>>> Starting back demodulation with 457. >>>> Starting back demodulation with 459. >>>> Starting back demodulation with 461. >>>> Starting back demodulation with 463. >>>> Starting back demodulation with 465. >>>> Starting back demodulation with 467. ---> New Demodulator: 471 [new_demod,470] (x* (y* ((z*u)*v)))* (u*z)= (x*v)*y. >>>> Starting back demodulation with 471. given clause #19: (wt=11) 295 [para_into,196.1.1,9.1.1,flip.1] (x* (y*z))* (z*y)=x. ---> New Demodulator: 479 [new_demod,478] (x* ((y*z)*u))* (u* (z*y))=x. ---> New Demodulator: 481 [new_demod,480] (x* (y* (z*u)))* (y* (u*z))=x. ---> New Demodulator: 483 [new_demod,482] (x* (y* (z*u)))* ((u*z)*y)=x. ---> New Demodulator: 485 [new_demod,484] (x* ((y*z)*u))* ((z*y)*u)=x. ---> New Demodulator: 487 [new_demod,486] (x* ((y*z)*u))* ((z*v)* (y* (v*u)))=x. ---> New Demodulator: 489 [new_demod,488] (x* ((y*z)*u))* ((v*z)* (y* (v*u)))=x. ---> New Demodulator: 491 [new_demod,490] (x* ((y* (z*u))*v))* (z* (y* (u*v)))=x. ---> New Demodulator: 493 [new_demod,492] (x* ((y*z)* (u*v)))* ((u*z)* (y*v))=x. ---> New Demodulator: 495 [new_demod,494] ((x* ((y*z)*u))*v)* (z*y)=x* (u*v). ---> New Demodulator: 497 [new_demod,496] ((x*y)* (z*u))* (y*z)=x*u. ---> New Demodulator: 500 [new_demod,499] (x* ((y*z)* (u* (z*v))))* ((u*y)*v)=x. ---> New Demodulator: 502 [new_demod,501] (x* ((y*z)* (u* (y*v))))* ((u*z)*v)=x. ---> New Demodulator: 504 [new_demod,503] (x* (y* (z* (u*v))))* ((z* (y*u))*v)=x. >>>> Starting back demodulation with 479. >>>> Starting back demodulation with 481. >>>> Starting back demodulation with 483. >>>> Starting back demodulation with 485. >>>> Starting back demodulation with 487. >>>> Starting back demodulation with 489. >>>> Starting back demodulation with 491. >>>> Starting back demodulation with 493. >>>> Starting back demodulation with 495. >>>> Starting back demodulation with 497. >>>> Starting back demodulation with 500. >>>> Starting back demodulation with 502. >>>> Starting back demodulation with 504. ---> New Demodulator: 509 [new_demod,508] (x* (y* (z* (u*v))))* (v*u)= (x*z)*y. >>>> Starting back demodulation with 509. given clause #20: (wt=15) 24 [para_into,14.1.1.1.2.1,5.1.1] (x* ((y*z)*u))*z= (x*y)*u. ---> New Demodulator: 520 [new_demod,519] (x* (((y* (z*u))*v)*w))*z= (x* (y* (u*v)))*w. ---> New Demodulator: 522 [new_demod,521] (x* (((y*z)* (u*v))*w))* (u*z)= (x* (y*v))*w. ---> New Demodulator: 525 [new_demod,524] (x* ((y*z)*u))* ((z*v)*u)= (x*y)*v. ---> New Demodulator: 529 [new_demod,528] (x* ((y* (z*u))*v))* (u*v)= (x*y)*z. ---> New Demodulator: 531 [new_demod,530] (x* ((y*z)*u))* ((v*z)*u)= (x*y)*v. ---> New Demodulator: 533 [new_demod,532] ((x* ((y* ((z*u)*v))*w))*z)*v= ((x*y)*w)*u. ---> New Demodulator: 536 [new_demod,535] x* (((y*x)*z)*u)= (u*y)*z. ---> New Demodulator: 538 [new_demod,537] (x*y)* (z* ((u* (y*x))*v))= (z*u)*v. ---> New Demodulator: 540 [new_demod,539] x* (y* ((z*x)*u))= (y*z)*u. >>>> Starting back demodulation with 520. >>>> Starting back demodulation with 522. >>>> Starting back demodulation with 525. >> back demodulating 484 with 525. >>>> Starting back demodulation with 529. >>>> Starting back demodulation with 531. >>>> Starting back demodulation with 533. >>>> Starting back demodulation with 536. >>>> Starting back demodulation with 538. >>>> Starting back demodulation with 540. ---> New Demodulator: 550 [new_demod,549] (x* ((y* ((z*u)*v))*w))* ((y*z)*v)= (x*u)*w. ---> New Demodulator: 554 [new_demod,553] ((x* ((y* (z*u))*v))*w)*u= ((x*y)*v)* (w*z). ---> New Demodulator: 558 [new_demod,557] (x* (y* (z* ((u*v)*w))))*v= (x* ((z*u)*w))*y. >>>> Starting back demodulation with 550. >>>> Starting back demodulation with 554. >> back demodulating 532 with 554. >>>> Starting back demodulation with 558. given clause #21: (wt=15) 26 [para_into,14.1.1.1.2.1,3.1.1] (x* (y*z))*u= (x* (y*u))*z. ---> New Demodulator: 576 [new_demod,575] (x* ((y* ((z*u)*v))*w))*u= (x* ((y*z)*v))*w. ---> New Demodulator: 582 [new_demod,581] (x* ((y* ((z*u)*v))*w))*z= (x* ((y*u)*v))*w. ---> New Demodulator: 597 [new_demod,596] (x* (y* (z* (x* (y*u)))))*u=z. >>>> Starting back demodulation with 576. >>>> Starting back demodulation with 582. >>>> Starting back demodulation with 597. ---> New Demodulator: 616 [new_demod,615] (x*y)* ((z* (u* (y*x)))*v)=z* (u*v). ---> New Demodulator: 620 [new_demod,619] ((x* (y* (z*u)))*v)* (u*z)=x* (y*v). ---> New Demodulator: 627 [new_demod,626] (x* ((y* (z*u))*v))* (z*v)= (x*y)*u. ---> New Demodulator: 631 [new_demod,630] (x* ((y* (z*u))*v))* (u* (y* (z*v)))=x. ---> New Demodulator: 636 [new_demod,635] (x* (((y* (z*u))*v)*w))*u= (x* (y* (z*v)))*w. ---> New Demodulator: 638 [new_demod,637] (x* (((y* (z*u))*v)*w))* (y* (z*v))= (x*u)*w. ---> New Demodulator: 641 [new_demod,640] (x* (y* (z* (u*v))))* ((z* (u*y))*v)=x. ---> New Demodulator: 644 [new_demod,643] ((x* (y*z))*u)* ((z* (x* (y*u)))*v)=v. ---> New Demodulator: 646 [new_demod,645] ((x* (y*z))*u)* (v* (z* (x* (y*u))))=v. ---> New Demodulator: 650 [new_demod,649] (((x* (y*z))*u)*v)* (z* (x* (y*u)))=v. ---> New Demodulator: 652 [new_demod,651] ((x* (y* (z*u)))*v)* ((y* (z*x))*u)=v. ---> New Demodulator: 654 [new_demod,653] (x* (y* (z*u)))* (((y* (z*x))*u)*v)=v. ---> New Demodulator: 656 [new_demod,655] (x* (y* (z*u)))* (v* ((y* (z*x))*u))=v. ---> New Demodulator: 658 [new_demod,657] x* ((y* (z*x))*u)=y* (z*u). >>>> Starting back demodulation with 616. >>>> Starting back demodulation with 620. >>>> Starting back demodulation with 627. >>>> Starting back demodulation with 631. >>>> Starting back demodulation with 636. >>>> Starting back demodulation with 638. >>>> Starting back demodulation with 641. >>>> Starting back demodulation with 644. >>>> Starting back demodulation with 646. >>>> Starting back demodulation with 650. >>>> Starting back demodulation with 652. >>>> Starting back demodulation with 654. >>>> Starting back demodulation with 656. >>>> Starting back demodulation with 658. given clause #22: (wt=15) 27 [para_into,14.1.1.1.2,11.1.1] (x*y)*z= (x*u)* ((z*u)*y). ---> New Demodulator: 676 [new_demod,675] ((x* (y*z))*u)* ((v*u)* (z*y))=x*v. ---> New Demodulator: 678 [new_demod,677] (((x*y)*z)*u)* ((v*u)* (y*x))=z*v. ---> New Demodulator: 681 [new_demod,680] ((x*y)*z)* ((u*z)* ((y*x)*v))=v*u. ---> New Demodulator: 683 [new_demod,682] ((x*y)*z)* ((u*z)* (v* (y*x)))=v*u. ---> New Demodulator: 690 [new_demod,689] ((x* ((y*z)*u))*v)* ((w*v)*z)= ((x*y)*u)*w. ---> New Demodulator: 696 [new_demod,695] ((x* ((y*z)*u))*v)* ((w*v)*y)= ((x*z)*u)*w. ---> New Demodulator: 698 [new_demod,697] ((x*y)*z)* ((u*z)*y)=x*u. ---> New Demodulator: 701 [new_demod,700] (x*y)* ((z*y)* (u*x))=u*z. >>>> Starting back demodulation with 676. >>>> Starting back demodulation with 678. >>>> Starting back demodulation with 681. >>>> Starting back demodulation with 683. >>>> Starting back demodulation with 690. >>>> Starting back demodulation with 696. >>>> Starting back demodulation with 698. >>>> Starting back demodulation with 701. ---> New Demodulator: 741 [new_demod,740] (x* ((y*z)* ((u*z)*v)))* (u* (y*v))=x. ---> New Demodulator: 748 [new_demod,747] (x* (y* (z*u)))* ((z*v)* ((y*v)*u))=x. ---> New Demodulator: 751 [new_demod,750] ((x*y)* ((z*y)*u))* ((z* (x*u))*v)=v. ---> New Demodulator: 753 [new_demod,752] ((x*y)* ((z*y)*u))* (v* (z* (x*u)))=v. ---> New Demodulator: 757 [new_demod,756] (((x*y)* ((z*y)*u))*v)* (z* (x*u))=v. ---> New Demodulator: 759 [new_demod,758] ((x* (y*z))*u)* ((y*v)* ((x*v)*z))=u. ---> New Demodulator: 761 [new_demod,760] (x* (y*z))* (((y*u)* ((x*u)*z))*v)=v. ---> New Demodulator: 763 [new_demod,762] (x* (y*z))* (u* ((y*v)* ((x*v)*z)))=u. >>>> Starting back demodulation with 741. >>>> Starting back demodulation with 748. >>>> Starting back demodulation with 751. >>>> Starting back demodulation with 753. >>>> Starting back demodulation with 757. >>>> Starting back demodulation with 759. >>>> Starting back demodulation with 761. >>>> Starting back demodulation with 763. given clause #23: (wt=15) 28 [para_into,14.1.1.1.2,5.1.1] (x* (y* (z*u)))*z= (x*u)*y. ---> New Demodulator: 786 [new_demod,785] (x* (y* ((z*u)* ((v*u)*w))))* (z*w)= (x*v)*y. ---> New Demodulator: 788 [new_demod,787] (x* (y* ((z* (u*v))*w)))* (z* (u*w))= (x*v)*y. ---> New Demodulator: 793 [new_demod,792] (x* (y* ((z* (u*v))*w)))* (z* (v*w))= (x*u)*y. ---> New Demodulator: 795 [new_demod,794] (x* (y* ((z*u)* (v*w))))* (z*w)= (x* (v*u))*y. ---> New Demodulator: 799 [new_demod,798] (x* ((y*z)* (((u*v)*z)*w)))*u= (x*v)* (y*w). ---> New Demodulator: 801 [new_demod,800] (x* ((y* (z* (u*v)))*w))*u= (x*v)* (y* (z*w)). ---> New Demodulator: 806 [new_demod,805] ((x* (y* ((z* (u*v))*w)))*v)*z= ((x*w)*y)*u. ---> New Demodulator: 810 [new_demod,809] ((x* ((y* (z* (u*v)))*w))*v)*z= ((x*y)*w)*u. ---> New Demodulator: 813 [new_demod,812] (x*y)* (z* (u* ((y*x)*v)))= (z*v)*u. ---> New Demodulator: 816 [new_demod,815] x* (y* (z* (x*u)))= (y*u)*z. >>>> Starting back demodulation with 786. >>>> Starting back demodulation with 788. >>>> Starting back demodulation with 793. >>>> Starting back demodulation with 795. >> back demodulating 785 with 795. >>>> Starting back demodulation with 799. >>>> Starting back demodulation with 801. >>>> Starting back demodulation with 806. >>>> Starting back demodulation with 810. >>>> Starting back demodulation with 813. >>>> Starting back demodulation with 816. >> back demodulating 596 with 816. ---> New Demodulator: 833 [new_demod,832] ((x* (y*z))*u)* ((u*z)*x)=y. ---> New Demodulator: 836 [new_demod,835] (x* ((y* (z* (u*v)))*w))* ((y*v)*z)= (x*u)*w. ---> New Demodulator: 840 [new_demod,839] ((x* (y* ((z*u)*v)))* (z*w))*u= ((x*v)*y)*w. ---> New Demodulator: 842 [new_demod,841] ((x* (y* ((z*u)*v)))*w)*u= ((x*v)*y)* (w*z). ---> New Demodulator: 844 [new_demod,843] (x* ((y*z)*u))* (u* (v*z))= (x*y)*v. ---> New Demodulator: 848 [new_demod,847] (x* (y* (z* (u* (v*w)))))*v= (x* ((z*w)*u))*y. ---> New Demodulator: 853 [new_demod,852] ((x*y)*z)* ((z* (u*y))*x)=u. ---> New Demodulator: 855 [new_demod,854] ((x* (y* (z*u)))*v)* ((w*v)*z)= ((x*u)*y)*w. ---> New Demodulator: 858 [new_demod,857] (x* (y* (z*u)))* ((x*u)*y)=z. ---> New Demodulator: 860 [new_demod,859] ((x*y)*z)* (x* (z* (u*y)))=u. >>>> Starting back demodulation with 833. >>>> Starting back demodulation with 836. >>>> Starting back demodulation with 840. >>>> Starting back demodulation with 842. >> back demodulating 839 with 842. >> back demodulating 664 with 842. >> back demodulating 624 with 842. >>>> Starting back demodulation with 844. >>>> Starting back demodulation with 848. >>>> Starting back demodulation with 853. >>>> Starting back demodulation with 855. >>>> Starting back demodulation with 858. >>>> Starting back demodulation with 860. given clause #24: (wt=15) 30 [para_into,14.1.1.1.2,3.1.1] (x*y)*z= (x*u)* (y* (z*u)). ---> New Demodulator: 875 [new_demod,874] ((x* (y*z))*u)* ((z*y)* (v*u))=x*v. ---> New Demodulator: 877 [new_demod,876] (((x*y)*z)*u)* ((y*x)* (v*u))=z*v. ---> New Demodulator: 880 [new_demod,879] ((x*y)*z)* (((y*x)*u)* (v*z))=u*v. ---> New Demodulator: 882 [new_demod,881] ((x*y)*z)* ((u* (y*x))* (v*z))=u*v. ---> New Demodulator: 888 [new_demod,887] ((x* (y* (z*u)))*v)* (z* (w*v))= ((x*u)*y)*w. ---> New Demodulator: 892 [new_demod,891] ((x* ((y*z)*u))*v)* (z* (w*v))= ((x*y)*u)*w. ---> New Demodulator: 898 [new_demod,897] ((x* ((y*z)*u))*v)* (y* (w*v))= ((x*z)*u)*w. ---> New Demodulator: 900 [new_demod,899] ((x*y)*z)* (y* (u*z))=x*u. ---> New Demodulator: 903 [new_demod,902] (x*y)* ((z*x)* (u*y))=z*u. >>>> Starting back demodulation with 875. >>>> Starting back demodulation with 877. >>>> Starting back demodulation with 880. >>>> Starting back demodulation with 882. >>>> Starting back demodulation with 888. >>>> Starting back demodulation with 892. >>>> Starting back demodulation with 898. >>>> Starting back demodulation with 900. >>>> Starting back demodulation with 903. ---> New Demodulator: 940 [new_demod,939] (x*y)* ((y*z)* (x* (u*z)))=u. ---> New Demodulator: 954 [new_demod,953] (x* ((y*z)* (u* (v*z))))* (v* (y*u))=x. ---> New Demodulator: 960 [new_demod,959] (x* (((y*z)* (u* (v*z)))*w))* (y*u)= (x*v)*w. ---> New Demodulator: 962 [new_demod,961] (x* (y* ((z*u)* (v* (w*u)))))* (z*v)= (x*w)*y. ---> New Demodulator: 965 [new_demod,964] (x* (y* (z*u)))* ((z*v)* (u* (y*v)))=x. ---> New Demodulator: 967 [new_demod,966] ((x*y)* (z* (u*y)))* (z*x)=u. ---> New Demodulator: 970 [new_demod,969] ((x*y)* (z* (u*y)))* ((u* (x*z))*v)=v. ---> New Demodulator: 972 [new_demod,971] ((x*y)* (z* (u*y)))* (v* (u* (x*z)))=v. ---> New Demodulator: 977 [new_demod,976] (x*y)* ((x*z)* (y* (u*z)))=u. ---> New Demodulator: 979 [new_demod,978] ((x*y)* (z* (u*y)))* (x*z)=u. ---> New Demodulator: 981 [new_demod,980] (((x*y)* (z* (u*y)))*v)* (u* (x*z))=v. ---> New Demodulator: 983 [new_demod,982] ((x* (y*z))*u)* ((y*v)* (z* (x*v)))=u. ---> New Demodulator: 985 [new_demod,984] (x* (y*z))* (((y*u)* (z* (x*u)))*v)=v. ---> New Demodulator: 987 [new_demod,986] (x* (y*z))* (u* ((y*v)* (z* (x*v))))=u. >>>> Starting back demodulation with 940. >>>> Starting back demodulation with 954. >>>> Starting back demodulation with 960. >>>> Starting back demodulation with 962. >>>> Starting back demodulation with 965. >>>> Starting back demodulation with 967. >>>> Starting back demodulation with 970. >>>> Starting back demodulation with 972. >>>> Starting back demodulation with 977. >>>> Starting back demodulation with 979. >>>> Starting back demodulation with 981. >>>> Starting back demodulation with 983. >>>> Starting back demodulation with 985. >>>> Starting back demodulation with 987. given clause #25: (wt=15) 35 [para_into,14.1.1.1,5.1.1] (((x*y)*z)*u)*x= (u*y)*z. ---> New Demodulator: 1012 [new_demod,1011] ((((x*y)*z)*u)*v)* (y*x)= (v*z)*u. ---> New Demodulator: 1016 [new_demod,1015] (((x* (y*z))*u)*v)* (z*y)= (v*x)*u. ---> New Demodulator: 1019 [new_demod,1018] ((((x*y)* (z* (u*y)))*v)*w)* (x*z)= (w*u)*v. ---> New Demodulator: 1022 [new_demod,1021] ((((x*y)* ((z*y)*u))*v)*w)* (x*u)= (w*z)*v. ---> New Demodulator: 1024 [new_demod,1023] ((((x* (y*z))*u)*v)*w)* (x* (y*u))= (w*z)*v. ---> New Demodulator: 1029 [new_demod,1028] ((((x* (y*z))*u)*v)*w)* (x* (z*u))= (w*y)*v. ---> New Demodulator: 1031 [new_demod,1030] ((((x*y)* (z*u))*v)*w)* (x*u)= (w* (z*y))*v. ---> New Demodulator: 1034 [new_demod,1033] (((x*y)*z)*u)* ((v*y)*z)= (u*x)*v. ---> New Demodulator: 1041 [new_demod,1040] (x*y)* ((((y*x)*z)*u)*v)= (v*z)*u. >>>> Starting back demodulation with 1012. >>>> Starting back demodulation with 1016. >>>> Starting back demodulation with 1019. >>>> Starting back demodulation with 1022. >>>> Starting back demodulation with 1024. >>>> Starting back demodulation with 1029. >>>> Starting back demodulation with 1031. >> back demodulating 1021 with 1031. >>>> Starting back demodulation with 1034. >>>> Starting back demodulation with 1041. ---> New Demodulator: 1075 [new_demod,1074] (((((x* (y*z))*u)*v)*w)*z)*x= ((w*u)*v)*y. ---> New Demodulator: 1078 [new_demod,1077] (x* ((((y*z)*u)*v)*w))* ((v*z)*u)= (x*y)*w. ---> New Demodulator: 1082 [new_demod,1081] (((((x*y)*z)*u)*v)* (x*w))*y= ((v*z)*u)*w. ---> New Demodulator: 1084 [new_demod,1083] (((((x*y)*z)*u)*v)*w)*y= ((v*z)*u)* (w*x). ---> New Demodulator: 1087 [new_demod,1086] (x* ((((y*z)*u)*v)*w))*y= (x* ((v*z)*u))*w. ---> New Demodulator: 1091 [new_demod,1090] (x* (y* (((z*u)*v)*w)))*z= (x* ((w*u)*v))*y. ---> New Demodulator: 1097 [new_demod,1096] ((((x*y)*z)*u)*v)* (x* (w*v))= ((u*y)*z)*w. ---> New Demodulator: 1099 [new_demod,1098] ((((x*y)*z)*u)*v)* ((w*v)*x)= ((u*y)*z)*w. ----> UNIT CONFLICT at 0.06 sec ----> 1102 [binary,1101.1,1.1] $F. Length of proof is 5. Level of proof is 4. ---------------- PROOF ---------------- 1 [] ((A*B)*C)*D!= ((D*B)*C)*A. 3 [] x* (y*x)=y. 5 [] x*y=y*x. 6 [] (x*y)*z!= (x*u)*v| (w*y)*z= (w*u)*v. 7 [para_into,3.1.1.2,3.1.1] (x*y)*x=y. 9 [para_into,5.1.1,3.1.1,flip.1] (x*y)*y=x. 14 [hyper,6,7] (x* ((y*z)*u))*y= (x*z)*u. 35 [para_into,14.1.1.1,5.1.1] (((x*y)*z)*u)*x= (u*y)*z. 1101 [para_from,35.1.1,9.1.1.1] ((x*y)*z)*u= ((u*y)*z)*x. 1102 [binary,1101.1,1.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 25 clauses generated 1669 hyper_res generated 23 para_from generated 753 para_into generated 893 demod & eval rewrites 1050 clauses wt,lit,sk delete 0 tautologies deleted 0 clauses forward subsumed 1477 (subsumed by sos) 642 unit deletions 0 factor simplifications 0 clauses kept 898 new demodulators 202 empty clauses 1 clauses back demodulated 20 clauses back subsumed 1 usable size 26 sos size 851 demodulators size 186 passive size 1 hot size 0 Kbytes malloced 1953 ----------- times (seconds) ----------- user CPU time 0.06 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) That finishes the proof of the theorem. Process 16994 finished Mon Nov 14 15:26:22 2005