%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYO607+1 : TPTP v8.1.0. Released v7.0.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 21 20:05:13 EDT 2022 % Result : Theorem 0.87s 1.02s % Output : Proof 0.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : SYO607+1 : TPTP v8.1.0. Released v7.0.0. % 0.07/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.36 % Computer : n027.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Fri Jul 8 20:11:16 EDT 2022 % 0.15/0.36 % CPUTime : % 0.87/1.02 % SZS status Theorem % 0.87/1.02 (* PROOF-FOUND *) % 0.87/1.02 (* BEGIN-PROOF *) % 0.87/1.02 % SZS output start Proof % 0.87/1.02 1. (-. (g_true (a) T_0)) (g_true (a) T_0) ### Axiom % 0.87/1.02 2. (g_true_only (a) T_0) (-. (g_true (a) T_0)) ### Extension/test/true_only_g 1 % 0.87/1.02 3. (-. (g_true (a) T_0)) (g_true (a) T_0) ### Axiom % 0.87/1.02 4. (g_both (a) T_0) (-. (g_true (a) T_0)) ### Extension/test/both_g 3 % 0.87/1.02 5. (g_false_only (a) T_0) (-. (g_false_only (a) T_0)) ### Axiom % 0.87/1.02 6. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.87/1.02 7. (g_true_only T_0 T_1) (-. (g_true T_0 T_1)) ### Extension/test/true_only_g 6 % 0.87/1.02 8. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.87/1.02 9. (-. (Ex B, (g_both T_0 B))) (g_both T_0 T_1) ### NotExists 8 % 0.87/1.02 10. (g_false_only T_0 T_1) (-. (g_false_only T_0 T_1)) ### Axiom % 0.87/1.02 11. (-. (Ex B, (g_false_only T_0 B))) (g_false_only T_0 T_1) ### NotExists 10 % 0.87/1.02 12. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (-. (Ex B, (g_false_only T_0 B))) (-. (Ex B, (g_both T_0 B))) (-. (g_true T_0 T_1)) ### DisjTree 7 9 11 % 0.87/1.02 13. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (g_true T_0 T_1)) (-. (Ex B, (g_both T_0 B))) (-. (Ex B, (g_false_only T_0 B))) ### All 12 % 0.87/1.02 14. (-. ((g_false_only (a) T_0) /\ (Ex B, (g_false_only T_0 B)))) (-. (Ex B, (g_both T_0 B))) (-. (g_true T_0 T_1)) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (g_false_only (a) T_0) ### NotAnd 5 13 % 0.87/1.02 15. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_0) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (g_true T_0 T_1)) (-. (Ex B, (g_both T_0 B))) ### NotExists 14 % 0.87/1.02 16. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.87/1.02 17. (g_true_only T_0 T_1) (g_false T_0 T_1) ### Extension/test/true_only_g 16 % 0.87/1.02 18. (g_false_only (a) T_0) (-. (g_false_only (a) T_0)) ### Axiom % 0.87/1.02 19. (-. ((g_false_only (a) T_0) /\ (Ex B, (g_false_only T_0 B)))) (g_false_only T_0 T_1) (g_false_only (a) T_0) ### NotAnd 18 11 % 0.87/1.02 20. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_0) (g_false_only T_0 T_1) ### NotExists 19 % 0.87/1.02 21. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (g_false_only (a) T_0) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex B, (g_both T_0 B))) (g_false T_0 T_1) ### DisjTree 17 9 20 % 0.87/1.02 22. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (g_false T_0 T_1) (-. (Ex B, (g_both T_0 B))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_0) ### All 21 % 0.87/1.02 23. (-. (g_true_only T_0 T_1)) (-. (Ex B, (g_both T_0 B))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (g_false_only (a) T_0) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### Extension/test/not_true_only_g 15 22 % 0.87/1.02 24. (-. (All B, (g_true_only T_0 B))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_0) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex B, (g_both T_0 B))) ### NotAllEx 23 % 0.87/1.02 25. (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex B, (g_both T_0 B))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (g_false_only (a) T_0) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### NotExists 24 % 0.87/1.02 26. ((g_true_only (a) T_0) \/ ((g_both (a) T_0) \/ (g_false_only (a) T_0))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex B, (g_both T_0 B))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (g_true (a) T_0)) ### DisjTree 2 4 25 % 0.87/1.02 27. (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (g_true (a) T_0)) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex B, (g_both T_0 B))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ((g_true_only (a) T_0) \/ ((g_both (a) T_0) \/ (g_false_only (a) T_0))) ### All 26 % 0.87/1.02 28. (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex B, (g_both T_0 B))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (g_true (a) T_0)) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### All 27 % 0.87/1.02 29. (g_false_only (a) T_0) (-. (g_false_only (a) T_0)) ### Axiom % 0.87/1.02 30. (Ex B, (g_false_only T_0 B)) (-. (Ex B, (g_false_only T_0 B))) ### Axiom % 0.87/1.02 31. (-. ((g_false_only (a) T_0) /\ (Ex B, (g_false_only T_0 B)))) (Ex B, (g_false_only T_0 B)) (g_false_only (a) T_0) ### NotAnd 29 30 % 0.87/1.02 32. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_0) (Ex B, (g_false_only T_0 B)) ### NotExists 31 % 0.87/1.02 33. ((g_true_only (a) T_0) \/ ((g_both (a) T_0) \/ (g_false_only (a) T_0))) (Ex B, (g_false_only T_0 B)) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (g_true (a) T_0)) ### DisjTree 2 4 32 % 0.87/1.02 34. (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (g_true (a) T_0)) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (Ex B, (g_false_only T_0 B)) ### All 33 % 0.87/1.02 35. (-. (-. (Ex B, (g_false_only T_0 B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (g_true (a) T_0)) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) ### NotNot 34 % 0.87/1.02 36. (-. ((Ex B, (g_both T_0 B)) /\ (-. (Ex B, (g_false_only T_0 B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (g_true (a) T_0)) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) ### NotAnd 28 35 % 0.87/1.02 37. (g_false (a) T_0) (-. (g_false (a) T_0)) ### Axiom % 0.87/1.02 38. (-. (g_both (a) T_0)) (g_false (a) T_0) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. ((Ex B, (g_both T_0 B)) /\ (-. (Ex B, (g_false_only T_0 B))))) ### Extension/test/not_both_g 36 37 % 0.87/1.02 39. (-. ((g_both (a) T_0) \/ ((Ex B, (g_both T_0 B)) /\ (-. (Ex B, (g_false_only T_0 B)))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (g_false (a) T_0) ### NotOr 38 % 0.87/1.02 40. (g_false (a) T_0) (-. (g_false (a) T_0)) ### Axiom % 0.87/1.02 41. (g_true_only (a) T_0) (g_false (a) T_0) ### Extension/test/true_only_g 40 % 0.87/1.02 42. (All B, (g_true_only T_0 B)) (-. (All B, (g_true_only T_0 B))) ### Axiom % 0.87/1.02 43. (-. (Ex A, (All B, (g_true_only A B)))) (All B, (g_true_only T_0 B)) ### NotExists 42 % 0.87/1.02 44. (-. (((g_both (a) T_0) \/ ((Ex B, (g_both T_0 B)) /\ (-. (Ex B, (g_false_only T_0 B))))) /\ ((-. (g_true_only (a) T_0)) /\ (-. (All B, (g_true_only T_0 B)))))) (g_false (a) T_0) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### DisjTree 39 41 43 % 0.87/1.02 45. (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (g_false (a) T_0) ### NotExists 44 % 0.87/1.02 46. (g_false_only (a) T_0) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) ### Extension/test/false_only_g 45 % 0.87/1.03 47. ((g_true_only (a) T_0) \/ ((g_both (a) T_0) \/ (g_false_only (a) T_0))) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (g_true (a) T_0)) ### DisjTree 2 4 46 % 0.87/1.03 48. (-. (g_true (a) T_0)) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) ### All 47 % 0.87/1.03 49. (-. (g_true_only (a) T_0)) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) ### Extension/test/not_true_only_g 48 45 % 0.87/1.03 50. (-. (All B, (g_true_only (a) B))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) ### NotAllEx 49 % 0.87/1.03 51. (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) ### NotExists 50 % 0.87/1.03 52. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B))))))) ### All 51 % 0.87/1.03 53. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B)))) ### Axiom % 0.87/1.03 54. (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (g_true (a) T_0)) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex B, (g_both T_0 B))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### All 26 % 0.87/1.03 55. (-. ((Ex B, (g_both T_0 B)) /\ (-. (Ex B, (g_false_only T_0 B))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (g_true (a) T_0)) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) ### NotAnd 54 35 % 0.87/1.03 56. (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (g_true (a) T_0)) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### NotExists 55 % 0.87/1.03 57. (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (g_true (a) T_0)) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### All 56 % 0.87/1.03 58. (g_false (a) T_0) (-. (g_false (a) T_0)) ### Axiom % 0.87/1.03 59. (-. (g_both (a) T_0)) (g_false (a) T_0) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### Extension/test/not_both_g 56 58 % 0.87/1.03 60. (-. (Ex B, (g_both (a) B))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false (a) T_0) ### NotExists 59 % 0.87/1.03 61. (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (g_false (a) T_0) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (-. (Ex B, (g_both (a) B))) ### All 60 % 0.87/1.03 62. (-. (g_true_only (a) T_0)) (-. (Ex B, (g_both (a) B))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### Extension/test/not_true_only_g 57 61 % 0.87/1.03 63. (-. (All B, (g_true_only (a) B))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (-. (Ex B, (g_both (a) B))) ### NotAllEx 62 % 0.87/1.03 64. (-. (Ex B, (g_both (a) B))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### NotExists 63 % 0.87/1.03 65. (g_false_only (a) T_2) (-. (g_false_only (a) T_2)) ### Axiom % 0.87/1.03 66. (-. (g_true T_2 T_3)) (g_true T_2 T_3) ### Axiom % 0.87/1.03 67. (g_true_only T_2 T_3) (-. (g_true T_2 T_3)) ### Extension/test/true_only_g 66 % 0.87/1.03 68. (-. (g_true T_2 T_3)) (g_true T_2 T_3) ### Axiom % 0.87/1.03 69. (g_both T_2 T_3) (-. (g_true T_2 T_3)) ### Extension/test/both_g 68 % 0.87/1.03 70. (g_false T_2 T_3) (-. (g_false T_2 T_3)) ### Axiom % 0.87/1.03 71. (-. (g_true T_2 T_3)) (g_true T_2 T_3) ### Axiom % 0.87/1.03 72. (-. (g_false_only T_2 T_3)) (-. (g_true T_2 T_3)) (g_false T_2 T_3) ### Extension/test/not_false_only_g 70 71 % 0.87/1.03 73. (-. (Ex B, (g_false_only T_2 B))) (g_false T_2 T_3) (-. (g_true T_2 T_3)) ### NotExists 72 % 0.87/1.03 74. (g_false T_2 T_3) (-. (g_false T_2 T_3)) ### Axiom % 0.87/1.03 75. (-. (g_both T_2 T_3)) (g_false T_2 T_3) (-. (Ex B, (g_false_only T_2 B))) ### Extension/test/not_both_g 73 74 % 0.87/1.03 76. (-. (Ex B, (g_both T_2 B))) (-. (Ex B, (g_false_only T_2 B))) (g_false T_2 T_3) ### NotExists 75 % 0.87/1.03 77. (g_false_only T_2 T_3) (-. (Ex B, (g_false_only T_2 B))) (-. (Ex B, (g_both T_2 B))) ### Extension/test/false_only_g 76 % 0.87/1.03 78. ((g_true_only T_2 T_3) \/ ((g_both T_2 T_3) \/ (g_false_only T_2 T_3))) (-. (Ex B, (g_both T_2 B))) (-. (Ex B, (g_false_only T_2 B))) (-. (g_true T_2 T_3)) ### DisjTree 67 69 77 % 0.87/1.03 79. (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (-. (g_true T_2 T_3)) (-. (Ex B, (g_false_only T_2 B))) (-. (Ex B, (g_both T_2 B))) ### All 78 % 0.87/1.03 80. (-. ((g_false_only (a) T_2) /\ (Ex B, (g_false_only T_2 B)))) (-. (Ex B, (g_both T_2 B))) (-. (g_true T_2 T_3)) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (g_false_only (a) T_2) ### NotAnd 65 79 % 0.87/1.03 81. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (-. (g_true T_2 T_3)) (-. (Ex B, (g_both T_2 B))) ### NotExists 80 % 0.87/1.03 82. (g_false_only (a) T_2) (-. (g_false_only (a) T_2)) ### Axiom % 0.87/1.03 83. (-. ((g_false_only (a) T_2) /\ (Ex B, (g_false_only T_2 B)))) (g_false T_2 T_3) (-. (Ex B, (g_both T_2 B))) (g_false_only (a) T_2) ### NotAnd 82 76 % 0.87/1.03 84. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (-. (Ex B, (g_both T_2 B))) (g_false T_2 T_3) ### NotExists 83 % 0.87/1.03 85. (-. (g_true_only T_2 T_3)) (-. (Ex B, (g_both T_2 B))) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (g_false_only (a) T_2) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### Extension/test/not_true_only_g 81 84 % 0.87/1.03 86. (-. (All B, (g_true_only T_2 B))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (-. (Ex B, (g_both T_2 B))) ### NotAllEx 85 % 0.87/1.03 87. (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex B, (g_both T_2 B))) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (g_false_only (a) T_2) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### NotExists 86 % 0.87/1.03 88. (g_false_only (a) T_2) (-. (g_false_only (a) T_2)) ### Axiom % 0.87/1.03 89. (Ex B, (g_false_only T_2 B)) (-. (Ex B, (g_false_only T_2 B))) ### Axiom % 0.87/1.03 90. (-. ((g_false_only (a) T_2) /\ (Ex B, (g_false_only T_2 B)))) (Ex B, (g_false_only T_2 B)) (g_false_only (a) T_2) ### NotAnd 88 89 % 0.87/1.03 91. (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (Ex B, (g_false_only T_2 B)) ### NotExists 90 % 0.87/1.03 92. (-. (-. (Ex B, (g_false_only T_2 B)))) (g_false_only (a) T_2) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### NotNot 91 % 0.87/1.03 93. (-. ((Ex B, (g_both T_2 B)) /\ (-. (Ex B, (g_false_only T_2 B))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) ### NotAnd 87 92 % 0.87/1.03 94. (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only T_2 X_1) \/ ((g_both T_2 X_1) \/ (g_false_only T_2 X_1)))) (g_false_only (a) T_2) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### NotExists 93 % 0.87/1.03 95. (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (g_false_only (a) T_2) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### All 94 % 0.87/1.03 96. (Ex B, (g_false_only (a) B)) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### Exists 95 % 0.87/1.03 97. (-. (-. (Ex B, (g_false_only (a) B)))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### NotNot 96 % 0.87/1.03 98. (-. ((Ex B, (g_both (a) B)) /\ (-. (Ex B, (g_false_only (a) B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### NotAnd 64 97 % 0.87/1.03 99. (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) (All X_1, ((g_true_only (a) X_1) \/ ((g_both (a) X_1) \/ (g_false_only (a) X_1)))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### NotExists 98 % 0.87/1.03 100. (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B)))))) ### All 99 % 0.87/1.03 101. (-. (Ex A, (All B, (g_true_only A B)))) (Ex A, (All B, (g_true_only A B))) ### Axiom % 0.87/1.03 102. (-. ((Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B)))))) /\ ((-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) /\ ((Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ (-. (Ex A, (All B, (g_true_only A B)))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. (Ex A, (All B, (g_true_only A B)))) (-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) ### DisjTree 52 53 100 101 % 0.87/1.03 103. (-. ((Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B)))) \/ ((Ex A, (All B, (g_true_only A B))) \/ ((Ex A, (((g_both (a) A) \/ ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ ((-. (g_true_only (a) A)) /\ (-. (All B, (g_true_only A B)))))) /\ ((-. (Ex A, ((g_false_only (a) A) /\ (Ex B, (g_false_only A B))))) /\ ((Ex A, ((Ex B, (g_both A B)) /\ (-. (Ex B, (g_false_only A B))))) /\ (-. (Ex A, (All B, (g_true_only A B)))))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### ConjTree 102 % 0.87/1.03 % SZS output end Proof % 0.87/1.03 (* END-PROOF *) %------------------------------------------------------------------------------