%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : ALG194+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 18:06:11 EDT 2022 % Result : Theorem 0.62s 0.81s % Output : Proof 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : ALG194+1 : TPTP v8.1.0. Released v2.7.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n027.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Wed Jun 8 03:46:26 EDT 2022 % 0.14/0.34 % CPUTime : % 0.62/0.81 % SZS status Theorem % 0.62/0.81 (* PROOF-FOUND *) % 0.62/0.81 (* BEGIN-PROOF *) % 0.62/0.81 % SZS output start Proof % 0.62/0.81 1. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 0.62/0.81 2. ((op (e0) (e0)) = (e0)) ((op (e0) (e0)) != (e0)) ### Axiom % 0.62/0.81 3. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e0) (e0)) = (e0)) ### ConjTree 2 % 0.62/0.81 4. ((op (e1) (e1)) != (e1)) ((op (e1) (e1)) = (e1)) ### Axiom % 0.62/0.81 5. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e1) (e1)) != (e1)) ### ConjTree 4 % 0.62/0.81 6. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 5 % 0.62/0.81 7. ((op (e2) (e2)) != (e2)) ((op (e2) (e2)) = (e2)) ### Axiom % 0.62/0.81 8. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e2) (e2)) != (e2)) ### ConjTree 7 % 0.62/0.81 9. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 8 % 0.62/0.81 10. ((op (e3) (e3)) != (e3)) ((op (e3) (e3)) = (e3)) ### Axiom % 0.62/0.81 11. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e3) (e3)) != (e3)) ### ConjTree 10 % 0.62/0.81 12. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 11 % 0.62/0.81 13. ((op (e4) (e4)) != (e4)) ((op (e4) (e4)) = (e4)) ### Axiom % 0.62/0.81 14. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e4) (e4)) != (e4)) ### ConjTree 13 % 0.62/0.81 15. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 14 % 0.62/0.81 16. ((op (e5) (e5)) != (e5)) ((op (e5) (e5)) = (e5)) ### Axiom % 0.62/0.81 17. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e5) (e5)) != (e5)) ### ConjTree 16 % 0.62/0.81 18. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 17 % 0.62/0.81 19. ((op (e6) (e6)) != (e6)) ((op (e6) (e6)) = (e6)) ### Axiom % 0.62/0.81 20. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e6) (e6)) != (e6)) ### ConjTree 19 % 0.62/0.81 21. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e0) (e0)) = (e0)) ### NotAnd 3 20 % 0.62/0.81 22. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) = (e0)) ### DisjTree 1 6 9 12 15 18 21 % 0.62/0.81 23. ((op (e1) (e1)) = (e1)) ((op (e1) (e1)) != (e1)) ### Axiom % 0.62/0.81 24. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e1) (e1)) = (e1)) ### ConjTree 23 % 0.62/0.81 25. ((op (e0) (e0)) != (e0)) ((op (e0) (e0)) = (e0)) ### Axiom % 0.62/0.81 26. (-. (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6))))))))) ((op (e0) (e0)) != (e0)) ### ConjTree 25 % 0.62/0.81 27. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 26 % 0.62/0.81 28. ((op (e1) (e1)) = (e1)) ((op (e1) (e1)) != (e1)) ### Axiom % 0.62/0.81 29. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 8 % 0.62/0.81 30. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 11 % 0.62/0.81 31. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 14 % 0.62/0.82 32. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 17 % 0.62/0.82 33. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e1) (e1)) = (e1)) ### NotAnd 24 20 % 0.62/0.82 34. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e1) (e1)) = (e1)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 27 28 29 30 31 32 33 % 0.62/0.82 35. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 0.62/0.82 36. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e2) (e2)) = (e2)) ### ConjTree 35 % 0.62/0.82 37. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 26 % 0.62/0.82 38. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 5 % 0.62/0.82 39. ((op (e2) (e2)) = (e2)) ((op (e2) (e2)) != (e2)) ### Axiom % 0.62/0.82 40. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 11 % 0.62/0.82 41. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 14 % 0.62/0.82 42. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 17 % 0.62/0.82 43. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e2) (e2)) = (e2)) ### NotAnd 36 20 % 0.62/0.82 44. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e2) (e2)) = (e2)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 37 38 39 40 41 42 43 % 0.62/0.82 45. ((op (e3) (e3)) = (e3)) ((op (e3) (e3)) != (e3)) ### Axiom % 0.62/0.82 46. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e3) (e3)) = (e3)) ### ConjTree 45 % 0.62/0.82 47. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 26 % 0.62/0.82 48. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 5 % 0.62/0.82 49. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 8 % 0.62/0.82 50. ((op (e3) (e3)) = (e3)) ((op (e3) (e3)) != (e3)) ### Axiom % 0.62/0.82 51. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 14 % 0.62/0.82 52. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 17 % 0.62/0.82 53. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e3) (e3)) = (e3)) ### NotAnd 46 20 % 0.62/0.82 54. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e3) (e3)) = (e3)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 47 48 49 50 51 52 53 % 0.62/0.82 55. ((op (e4) (e4)) = (e4)) ((op (e4) (e4)) != (e4)) ### Axiom % 0.62/0.82 56. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e4) (e4)) = (e4)) ### ConjTree 55 % 0.62/0.82 57. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 26 % 0.62/0.82 58. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 5 % 0.62/0.82 59. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 8 % 0.62/0.82 60. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 11 % 0.62/0.82 61. ((op (e4) (e4)) = (e4)) ((op (e4) (e4)) != (e4)) ### Axiom % 0.62/0.82 62. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 17 % 0.62/0.82 63. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e4) (e4)) = (e4)) ### NotAnd 56 20 % 0.62/0.82 64. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e4) (e4)) = (e4)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 57 58 59 60 61 62 63 % 0.62/0.82 65. ((op (e5) (e5)) = (e5)) ((op (e5) (e5)) != (e5)) ### Axiom % 0.62/0.82 66. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e5) (e5)) = (e5)) ### ConjTree 65 % 0.62/0.82 67. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 26 % 0.62/0.82 68. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 5 % 0.62/0.82 69. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 8 % 0.62/0.82 70. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 11 % 0.62/0.82 71. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 14 % 0.62/0.82 72. ((op (e5) (e5)) = (e5)) ((op (e5) (e5)) != (e5)) ### Axiom % 0.62/0.82 73. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e6) (e6)) != (e6)) ((op (e5) (e5)) = (e5)) ### NotAnd 66 20 % 0.62/0.82 74. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e5) (e5)) = (e5)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 67 68 69 70 71 72 73 % 0.62/0.82 75. ((op (e6) (e6)) = (e6)) ((op (e6) (e6)) != (e6)) ### Axiom % 0.62/0.82 76. (-. (((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6))))))))) ((op (e6) (e6)) = (e6)) ### ConjTree 75 % 0.62/0.82 77. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e0) (e0)) != (e0)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 26 % 0.62/0.82 78. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e1) (e1)) != (e1)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 5 % 0.62/0.82 79. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e2) (e2)) != (e2)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 8 % 0.62/0.82 80. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e3) (e3)) != (e3)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 11 % 0.62/0.82 81. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e4) (e4)) != (e4)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 14 % 0.62/0.82 82. (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ((op (e5) (e5)) != (e5)) ((op (e6) (e6)) = (e6)) ### NotAnd 76 17 % 0.62/0.82 83. ((op (e6) (e6)) = (e6)) ((op (e6) (e6)) != (e6)) ### Axiom % 0.62/0.82 84. (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ((op (e6) (e6)) = (e6)) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) ### DisjTree 77 78 79 80 81 82 83 % 0.62/0.82 85. (-. (((op (e0) (e0)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ (((op (e4) (e4)) != (e4)) /\ (((op (e5) (e5)) != (e5)) /\ ((op (e6) (e6)) != (e6))))))))) (-. ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))) (-. (((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6))))))))) ### DisjTree 22 34 44 54 64 74 84 % 0.62/0.82 86. (-. ((((op (e0) (e0)) != (e0)) /\ (((op (e1) (e1)) != (e1)) /\ (((op (e2) (e2)) != (e2)) /\ (((op (e3) (e3)) != (e3)) /\ (((op (e4) (e4)) != (e4)) /\ (((op (e5) (e5)) != (e5)) /\ ((op (e6) (e6)) != (e6)))))))) \/ ((((op (e0) (e0)) = (e0)) /\ (((op (e1) (e1)) = (e1)) /\ (((op (e2) (e2)) = (e2)) /\ (((op (e3) (e3)) = (e3)) /\ (((op (e4) (e4)) = (e4)) /\ (((op (e5) (e5)) = (e5)) /\ ((op (e6) (e6)) = (e6)))))))) \/ ((((op (e0) (e0)) = (e0)) \/ (((op (e1) (e1)) = (e1)) \/ (((op (e2) (e2)) = (e2)) \/ (((op (e3) (e3)) = (e3)) \/ (((op (e4) (e4)) = (e4)) \/ (((op (e5) (e5)) = (e5)) \/ ((op (e6) (e6)) = (e6)))))))) /\ (((op (e0) (e0)) != (e0)) \/ (((op (e1) (e1)) != (e1)) \/ (((op (e2) (e2)) != (e2)) \/ (((op (e3) (e3)) != (e3)) \/ (((op (e4) (e4)) != (e4)) \/ (((op (e5) (e5)) != (e5)) \/ ((op (e6) (e6)) != (e6)))))))))))) ### ConjTree 85 % 0.62/0.82 % SZS output end Proof % 0.62/0.82 (* END-PROOF *) %------------------------------------------------------------------------------