The theorem is that the self-dual equation
(x ^ y) v (z ^ (x v y)) = (x v y) ^ (z v (x ^ y))
can be used to express modularity in quasilattices.
The first known equational proof is reported in W. McCune and R. Padmanabhan, Automated Deduction in Equational Logic and Geometry, submitted for publication, 1995. See the online version of this monograph for additional information.
Previous proofs have been model theoretic.
The proof presented here (obtained October 16, 1995) has length 13.
You may simply take the input and start experimenting.
------------> process usable: ** KEPT (pick-wt=3): 4 [] x=x. Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=5): 5 [] x^x=x. ---> New Demodulator: 6 [new_demod,5] x^x=x. ** KEPT (pick-wt=7): 7 [] x^y=y^x. ** KEPT (pick-wt=11): 8 [] (x^y)^z=x^ (y^z). ---> New Demodulator: 9 [new_demod,8] (x^y)^z=x^ (y^z). ** KEPT (pick-wt=5): 10 [] x v x=x. ---> New Demodulator: 11 [new_demod,10] x v x=x. ** KEPT (pick-wt=7): 12 [] x v y=y v x. ** KEPT (pick-wt=11): 13 [] (x v y) v z=x v (y v z). ---> New Demodulator: 14 [new_demod,13] (x v y) v z=x v (y v z). ** KEPT (pick-wt=2): 15 [] x^ (x v y)=x. ---> New Demodulator: 16 [new_demod,15] x^ (x v y)=x. ** KEPT (pick-wt=2): 17 [] x v (x^y)=x. ---> New Demodulator: 18 [new_demod,17] x v (x^y)=x. ** KEPT (pick-wt=5): 19 [] x*x=x. ---> New Demodulator: 20 [new_demod,19] x*x=x. ** KEPT (pick-wt=7): 21 [] x*y=y*x. ** KEPT (pick-wt=11): 22 [] (x*y)*z=x* (y*z). ---> New Demodulator: 23 [new_demod,22] (x*y)*z=x* (y*z). ** KEPT (pick-wt=2): 24 [] x* (x v y)=x. ---> New Demodulator: 25 [new_demod,24] x* (x v y)=x. ** KEPT (pick-wt=2): 26 [] x v (x*y)=x. ---> New Demodulator: 27 [new_demod,26] x v (x*y)=x. >>>> Starting back demodulation with 6. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x^y=y^x. >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. Following clause subsumed by 12 during input processing: 0 [copy,12,flip.1] x v y=y v x. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 18. >>>> Starting back demodulation with 20. Following clause subsumed by 21 during input processing: 0 [copy,21,flip.1] x*y=y*x. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 27. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=2) 15 [] x^ (x v y)=x. ----> UNIT CONFLICT at 0.72 sec ----> 84 [binary,82.1,1.1] $F. Length of proof is 13. Level of proof is 6. ---------------- PROOF ---------------- 1 [] A^B!=A*B. 7 [] x^y=y^x. 8 [] (x^y)^z=x^ (y^z). 12 [] x v y=y v x. 15 [] x^ (x v y)=x. 17 [] x v (x^y)=x. 21 [] x*y=y*x. 23,22 [] (x*y)*z=x* (y*z). 24 [] x* (x v y)=x. 26 [] x v (x*y)=x. 28 [para_into,7.1.1,15.1.1,flip.1] (x v y)^x=x. 30 [para_from,7.1.1,17.1.1.2] x v (y^x)=x. 34 [para_into,12.1.1,26.1.1,flip.1] (x*y) v x=x. 40 [para_from,12.1.1,24.1.1.2] x* (y v x)=x. 44 [para_from,34.1.1,28.1.1.1] x^ (x*y)=x*y. 46 [para_into,21.1.1,40.1.1,flip.1] (x v y)*y=y. 50 [para_from,21.1.1,44.1.1.2] x^ (y*x)=x*y. 57,56 [para_into,46.1.1.1,30.1.1] x* (y^x)=y^x. 59,58 [para_into,46.1.1.1,17.1.1] x* (x^y)=x^y. 60 [para_from,8.1.1,17.1.1.2] (x^y) v (x^ (y^z))=x^y. 64 [para_into,60.1.1.2.2,50.1.1] (x^y) v (x^ (y*z))=x^y. 74 [para_into,64.1.1.2,50.1.1] (x^y) v (x*y)=x^y. 82 [para_from,74.1.1,40.1.1.2,demod,23,57,59] x^y=x*y. 84 [binary,82.1,1.1] $F. -------------- statistics ------------- clauses given 35 clauses generated 656 (hot clauses generated) 36 para_from generated 238 para_into generated 418 demod & eval rewrites 553 clauses wt,lit,sk delete 241 tautologies deleted 0 clauses forward subsumed 391 cl not subsumed due to ancestor_subsume 0 (subsumed by sos) 3 unit deletions 0 factor simplifications 0 clauses kept 42 (hot clauses kept) 0 new demodulators 38 empty clauses 1 clauses back demodulated 0 clauses back subsumed 0 usable size 36 sos size 6 demodulators size 38 passive size 1 hot size 2 Kbytes malloced 255 ----------- times (seconds) ----------- user CPU time 0.78 (0 hr, 0 min, 0 sec) system CPU time 0.35 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) input time 0.10 clausify time 0.00 process input 0.04 para_into time 0.04 para_from time 0.05 pre_process time 0.40 renumber time 0.00 demod time 0.09 order equalities 0.02 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.02 hints keep time 0.00 sort lits time 0.00 forward subsume 0.07 delete cl time 0.01 keep cl time 0.03 hints time 0.00 print_cl time 0.00 conflict time 0.06 new demod time 0.02 post_process time 0.01 back demod time 0.00 back subsume 0.01 factor time 0.00 hot list time 0.03 unindex time 0.00 The job finished Mon Oct 16 16:46:38 1995