%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n028.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 : Sun Jul 17 03:31:51 EDT 2022 % Result : Unsatisfiable 21.13s 21.31s % Output : Proof 21.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : KRS081+1 : TPTP v8.1.0. Released v3.1.0. % 0.09/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.32 % Computer : n028.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Tue Jun 7 11:52:45 EDT 2022 % 0.12/0.33 % CPUTime : % 21.13/21.31 % SZS status Theorem % 21.13/21.31 (* PROOF-FOUND *) % 21.13/21.31 (* BEGIN-PROOF *) % 21.13/21.31 % SZS output start Proof % 21.13/21.31 1. (rr (i2003_11_14_17_19_24236) T_0) (-. (rr (i2003_11_14_17_19_24236) T_0)) ### Axiom % 21.13/21.31 2. (rr (i2003_11_14_17_19_24236) T_1) (-. (rr (i2003_11_14_17_19_24236) T_1)) ### Axiom % 21.13/21.31 3. (rr (i2003_11_14_17_19_24236) T_2) (-. (rr (i2003_11_14_17_19_24236) T_2)) ### Axiom % 21.13/21.31 4. (rr (i2003_11_14_17_19_24236) T_3) (-. (rr (i2003_11_14_17_19_24236) T_3)) ### Axiom % 21.13/21.31 5. (rr (i2003_11_14_17_19_24236) T_4) (-. (rr (i2003_11_14_17_19_24236) T_4)) ### Axiom % 21.13/21.31 6. (T_0 != T_1) (T_0 = T_1) ### Axiom % 21.13/21.31 7. (T_0 != T_2) (T_0 = T_2) ### Axiom % 21.13/21.31 8. (T_0 = T_3) (T_3 != T_0) ### Sym(=) % 21.13/21.31 9. (-. (cp1 T_0)) (cp1 T_3) (T_0 = T_3) ### P-NotP 8 % 21.13/21.31 10. (T_0 != T_4) (T_0 = T_4) ### Axiom % 21.13/21.31 11. (T_2 != T_1) (T_1 = T_2) ### Sym(=) % 21.13/21.31 12. (T_3 != T_1) (T_1 = T_3) ### Sym(=) % 21.13/21.31 13. (T_1 != T_4) (T_1 = T_4) ### Axiom % 21.13/21.31 14. (T_3 != T_2) (T_2 = T_3) ### Sym(=) % 21.13/21.31 15. (T_2 != T_4) (T_2 = T_4) ### Axiom % 21.13/21.31 16. (T_3 != T_4) (T_3 = T_4) ### Axiom % 21.13/21.31 17. (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) T_4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = T_4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = T_4) \/ ((T_2 = T_3) \/ ((T_2 = T_4) \/ (T_3 = T_4))))))))))) (T_3 != T_4) (T_2 != T_4) (T_3 != T_2) (T_1 != T_4) (T_3 != T_1) (T_2 != T_1) (T_0 != T_4) (cp1 T_3) (-. (cp1 T_0)) (T_0 != T_2) (T_0 != T_1) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) ### DisjTree 1 2 3 4 5 6 7 9 10 11 12 13 14 15 16 % 21.13/21.31 18. (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (T_0 != T_1) (T_0 != T_2) (-. (cp1 T_0)) (cp1 T_3) (T_0 != T_4) (T_2 != T_1) (T_3 != T_1) (T_1 != T_4) (T_3 != T_2) (T_2 != T_4) (T_3 != T_4) ### All 17 % 21.13/21.31 19. (-. (cp1 T_1)) (T_3 != T_4) (T_2 != T_4) (T_3 != T_2) (T_1 != T_4) (T_2 != T_1) (T_0 != T_4) (cp1 T_3) (-. (cp1 T_0)) (T_0 != T_2) (T_0 != T_1) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) ### P-NotP 18 % 21.13/21.31 20. (-. (cp1 T_4)) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (T_0 != T_1) (T_0 != T_2) (-. (cp1 T_0)) (cp1 T_3) (T_0 != T_4) (T_2 != T_1) (T_1 != T_4) (T_3 != T_2) (T_2 != T_4) (-. (cp1 T_1)) ### P-NotP 19 % 21.13/21.31 21. (-. (cp1 T_2)) (-. (cp1 T_1)) (T_2 != T_4) (T_1 != T_4) (T_2 != T_1) (T_0 != T_4) (cp1 T_3) (-. (cp1 T_0)) (T_0 != T_2) (T_0 != T_1) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (-. (cp1 T_4)) ### P-NotP 20 % 21.13/21.31 22. (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (T_0 != T_1) (-. (cp1 T_0)) (cp1 T_3) (T_0 != T_4) (T_2 != T_1) (T_1 != T_4) (T_2 != T_4) (-. (cp1 T_1)) (-. (cp1 T_2)) ### P-NotP 21 % 21.13/21.31 23. (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (T_2 != T_4) (T_1 != T_4) (T_2 != T_1) (T_0 != T_4) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) ### P-NotP 22 % 21.13/21.31 24. (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (T_0 != T_4) (T_2 != T_1) (T_1 != T_4) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) ### P-NotP 23 % 21.13/21.31 25. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 21.13/21.31 26. (-. (cp2 T_4)) (cp2 T_4) ### Axiom % 21.13/21.31 27. (((T_0 = T_4) /\ (cp2 T_0)) => (cp2 T_4)) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (T_1 != T_4) (T_2 != T_1) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) ### DisjTree 24 25 26 % 21.13/21.31 28. (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (T_2 != T_1) (T_1 != T_4) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) ### All 27 % 21.13/21.33 29. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 21.13/21.33 30. (-. (cp4 T_4)) (cp4 T_4) ### Axiom % 21.13/21.33 31. (((T_1 = T_4) /\ (cp4 T_1)) => (cp4 T_4)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (T_2 != T_1) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) ### DisjTree 28 29 30 % 21.13/21.33 32. (All B, (((T_1 = B) /\ (cp4 T_1)) => (cp4 B))) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) T_3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = T_3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = T_3) \/ ((T_1 = Y4) \/ ((T_2 = T_3) \/ ((T_2 = Y4) \/ (T_3 = Y4)))))))))))) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (T_2 != T_1) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) ### All 31 % 21.13/21.33 33. (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((T_2 = Y3) \/ ((T_2 = Y4) \/ (Y3 = Y4))))))))))))) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (T_2 != T_1) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All B, (((T_0 = B) /\ (cp2 T_0)) => (cp2 B))) (All B, (((T_1 = B) /\ (cp4 T_1)) => (cp4 B))) ### All 32 % 21.13/21.33 34. (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All B, (((T_1 = B) /\ (cp4 T_1)) => (cp4 B))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (T_2 != T_1) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((T_2 = Y3) \/ ((T_2 = Y4) \/ (Y3 = Y4))))))))))))) ### All 33 % 21.13/21.33 35. (cp3 T_2) (-. (cp3 T_2)) ### Axiom % 21.13/21.33 36. (-. (cp3 T_1)) (cp3 T_1) ### Axiom % 21.13/21.33 37. (((T_2 = T_1) /\ (cp3 T_2)) => (cp3 T_1)) (-. (cp3 T_1)) (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((T_2 = Y3) \/ ((T_2 = Y4) \/ (Y3 = Y4))))))))))))) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All B, (((T_1 = B) /\ (cp4 T_1)) => (cp4 B))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### DisjTree 34 35 36 % 21.13/21.33 38. (All B, (((T_2 = B) /\ (cp3 T_2)) => (cp3 B))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All B, (((T_1 = B) /\ (cp4 T_1)) => (cp4 B))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((T_2 = Y3) \/ ((T_2 = Y4) \/ (Y3 = Y4))))))))))))) (-. (cp3 T_1)) ### All 37 % 21.13/21.33 39. (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) T_2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = T_2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = T_2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((T_2 = Y3) \/ ((T_2 = Y4) \/ (Y3 = Y4))))))))))))) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All B, (((T_2 = B) /\ (cp3 T_2)) => (cp3 B))) ### All 38 % 21.13/21.33 40. (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))) (All B, (((T_2 = B) /\ (cp3 T_2)) => (cp3 B))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) ### All 39 % 21.13/21.33 41. (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) T_1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = T_1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((T_1 = Y2) \/ ((T_1 = Y3) \/ ((T_1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))) ### All 40 % 21.13/21.37 42. (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) T_0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((T_0 = Y1) \/ ((T_0 = Y2) \/ ((T_0 = Y3) \/ ((T_0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4))))))))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (-. (cp1 T_0)) (cp1 T_3) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) ### All 41 % 21.13/21.37 43. (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (cp1 T_3) (-. (cp1 T_0)) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 42 % 21.13/21.37 44. (cp2 T_0) (-. (cp2 T_0)) ### Axiom % 21.13/21.37 45. (-. ((cp2 T_0) \/ ((cp4 T_0) \/ ((cp5 T_0) \/ (cp3 T_0))))) (cp2 T_0) ### ConjTree 44 % 21.13/21.37 46. ((cp1 T_0) => (-. ((cp2 T_0) \/ ((cp4 T_0) \/ ((cp5 T_0) \/ (cp3 T_0)))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp1 T_1)) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) ### Imply 43 45 % 21.13/21.37 47. (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (-. (cp1 T_1)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 46 % 21.13/21.37 48. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 21.13/21.37 49. (-. ((cp2 T_1) \/ ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1))))) (cp4 T_1) ### ConjTree 48 % 21.13/21.37 50. ((cp1 T_1) => (-. ((cp2 T_1) \/ ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1)))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (-. (cp1 T_4)) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) ### Imply 47 49 % 21.13/21.37 51. (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (-. (cp1 T_4)) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### All 50 % 21.13/21.37 52. (cp5 T_4) (-. (cp5 T_4)) ### Axiom % 21.13/21.37 53. (-. ((cp2 T_4) \/ ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4))))) (cp5 T_4) ### ConjTree 52 % 21.13/21.37 54. ((cp1 T_4) => (-. ((cp2 T_4) \/ ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4)))))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp1 T_2)) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) ### Imply 51 53 % 21.13/21.37 55. (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (-. (cp1 T_2)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 54 % 21.13/21.38 56. (cp3 T_2) (-. (cp3 T_2)) ### Axiom % 21.13/21.38 57. (-. ((cp2 T_2) \/ ((cp4 T_2) \/ ((cp5 T_2) \/ (cp3 T_2))))) (cp3 T_2) ### ConjTree 56 % 21.13/21.38 58. ((cp1 T_2) => (-. ((cp2 T_2) \/ ((cp4 T_2) \/ ((cp5 T_2) \/ (cp3 T_2)))))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (-. (cp2 T_2)) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) ### Imply 55 57 % 21.13/21.38 59. (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (-. (cp2 T_2)) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 58 % 21.13/21.38 60. (cp3 T_2) (-. (cp3 T_2)) ### Axiom % 21.13/21.38 61. (-. ((cp4 T_2) \/ ((cp5 T_2) \/ (cp3 T_2)))) (cp3 T_2) ### ConjTree 60 % 21.13/21.38 62. ((cp2 T_2) => (-. ((cp4 T_2) \/ ((cp5 T_2) \/ (cp3 T_2))))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp2 T_1)) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) ### Imply 59 61 % 21.13/21.38 63. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (-. (cp2 T_1)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 62 % 21.13/21.38 64. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 21.13/21.38 65. (-. ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1)))) (cp4 T_1) ### ConjTree 64 % 21.13/21.38 66. ((cp2 T_1) => (-. ((cp4 T_1) \/ ((cp5 T_1) \/ (cp3 T_1))))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (-. (cp2 T_4)) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 63 65 % 21.13/21.38 67. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (-. (cp2 T_4)) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 66 % 21.13/21.38 68. (cp5 T_4) (-. (cp5 T_4)) ### Axiom % 21.13/21.38 69. (-. ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4)))) (cp5 T_4) ### ConjTree 68 % 21.13/21.38 70. ((cp2 T_4) => (-. ((cp4 T_4) \/ ((cp5 T_4) \/ (cp3 T_4))))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (-. (cp3 T_4)) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 67 69 % 21.13/21.38 71. (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (-. (cp3 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 70 % 21.13/21.38 72. (cp5 T_4) (-. (cp5 T_4)) ### Axiom % 21.13/21.38 73. (-. ((cp4 T_4) \/ (cp5 T_4))) (cp5 T_4) ### NotOr 72 % 21.13/21.38 74. ((cp3 T_4) => (-. ((cp4 T_4) \/ (cp5 T_4)))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (cp4 T_1) (-. (cp4 T_4)) (-. (cp3 T_1)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) ### Imply 71 73 % 21.13/21.38 75. (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp3 T_1)) (-. (cp4 T_4)) (cp4 T_1) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 74 % 21.13/21.38 76. (cp4 T_1) (-. (cp4 T_1)) ### Axiom % 21.13/21.38 77. (-. ((cp4 T_1) \/ (cp5 T_1))) (cp4 T_1) ### NotOr 76 % 21.13/21.38 78. ((cp3 T_1) => (-. ((cp4 T_1) \/ (cp5 T_1)))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (cp4 T_1) (-. (cp4 T_4)) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) ### Imply 75 77 % 21.13/21.38 79. (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (-. (cp4 T_4)) (cp4 T_1) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 78 % 21.13/21.38 80. (cp5 T_4) (-. (cp5 T_4)) ### Axiom % 21.13/21.38 81. ((cp4 T_4) => (-. (cp5 T_4))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_4) (cp1 T_3) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) ### Imply 79 80 % 21.13/21.38 82. (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (cp4 T_1) (cp1 T_3) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_3) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### All 81 % 21.13/21.38 83. ((rr (i2003_11_14_17_19_24236) T_3) /\ ((cp1 T_3) /\ (cp T_3))) (cp5 T_4) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_4) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) ### ConjTree 82 % 21.13/21.38 84. (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (cp4 T_1) (rr (i2003_11_14_17_19_24236) T_4) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp5 T_4) ### Exists 83 % 21.13/21.39 85. ((rr (i2003_11_14_17_19_24236) T_4) /\ (cp5 T_4)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (cp2 T_0) (rr (i2003_11_14_17_19_24236) T_0) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) ### And 84 % 21.13/21.39 86. (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (cp4 T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_0) (cp2 T_0) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 85 % 21.13/21.39 87. ((rr (i2003_11_14_17_19_24236) T_0) /\ ((cp2 T_0) /\ (cp T_0))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (rr (i2003_11_14_17_19_24236) T_1) (rr (i2003_11_14_17_19_24236) T_2) (cp4 T_1) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) ### ConjTree 86 % 21.13/21.39 88. (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (cp4 T_1) (rr (i2003_11_14_17_19_24236) T_2) (rr (i2003_11_14_17_19_24236) T_1) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 87 % 21.13/21.39 89. ((rr (i2003_11_14_17_19_24236) T_1) /\ ((cp4 T_1) /\ (cp T_1))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (cp3 T_2) (rr (i2003_11_14_17_19_24236) T_2) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) ### ConjTree 88 % 21.13/21.39 90. (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp4 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (rr (i2003_11_14_17_19_24236) T_2) (cp3 T_2) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 89 % 21.13/21.39 91. ((rr (i2003_11_14_17_19_24236) T_2) /\ (cp3 T_2)) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp4 Y) /\ (cp Y)))) ### And 90 % 21.13/21.39 92. (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp3 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp4 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Exists 91 % 21.13/21.39 93. ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp3 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp4 Y) /\ (cp Y)))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp4 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp2 Y) /\ (cp Y)))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp5 Y))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp Y) /\ (cp3 Y)))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp1 Y))) /\ ((All Y0, (All Y1, (All Y2, (All Y3, (All Y4, (((rr (i2003_11_14_17_19_24236) Y0) /\ ((rr (i2003_11_14_17_19_24236) Y1) /\ ((rr (i2003_11_14_17_19_24236) Y2) /\ ((rr (i2003_11_14_17_19_24236) Y3) /\ (rr (i2003_11_14_17_19_24236) Y4))))) => ((Y0 = Y1) \/ ((Y0 = Y2) \/ ((Y0 = Y3) \/ ((Y0 = Y4) \/ ((Y1 = Y2) \/ ((Y1 = Y3) \/ ((Y1 = Y4) \/ ((Y2 = Y3) \/ ((Y2 = Y4) \/ (Y3 = Y4)))))))))))))))) /\ ((Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ ((cp1 Y) /\ (cp Y)))) /\ (Ex Y, ((rr (i2003_11_14_17_19_24236) Y) /\ (cp2 Y)))))))))))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp4 X) => (-. (cp5 X)))) ### ConjTree 92 % 21.13/21.39 94. (cUnsatisfiable (i2003_11_14_17_19_24236)) (All X, ((cp4 X) => (-. (cp5 X)))) (All X, ((cp3 X) => (-. ((cp4 X) \/ (cp5 X))))) (All X, ((cp2 X) => (-. ((cp4 X) \/ ((cp5 X) \/ (cp3 X)))))) (All X, ((cp1 X) => (-. ((cp2 X) \/ ((cp4 X) \/ ((cp5 X) \/ (cp3 X))))))) (All A, (All B, (((A = B) /\ (cp3 A)) => (cp3 B)))) (All A, (All B, (((A = B) /\ (cp4 A)) => (cp4 B)))) (All A, (All B, (((A = B) /\ (cp2 A)) => (cp2 B)))) ### Definition-Pseudo(cUnsatisfiable) 93 % 21.13/21.39 % SZS output end Proof % 21.13/21.39 (* END-PROOF *) %------------------------------------------------------------------------------