%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYO605+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 : n026.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:12 EDT 2022 % Result : Theorem 0.47s 0.72s % Output : Proof 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYO605+1 : TPTP v8.1.0. Released v7.0.0. % 0.10/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 8 21:44:25 EDT 2022 % 0.13/0.34 % CPUTime : % 0.47/0.72 % SZS status Theorem % 0.47/0.72 (* PROOF-FOUND *) % 0.47/0.72 (* BEGIN-PROOF *) % 0.47/0.72 % SZS output start Proof % 0.47/0.72 1. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.47/0.72 2. (g_true_only T_0 T_1) (-. (g_true T_0 T_1)) ### Extension/test/true_only_g 1 % 0.47/0.72 3. (-. (g_false T_0 T_1)) (g_false T_0 T_1) ### Axiom % 0.47/0.72 4. (g_both T_0 T_1) (-. (g_false T_0 T_1)) ### Extension/test/both_g 3 % 0.47/0.72 5. (-. (g_false T_0 T_1)) (g_false T_0 T_1) ### Axiom % 0.47/0.72 6. (g_false_only T_0 T_1) (-. (g_false T_0 T_1)) ### Extension/test/false_only_g 5 % 0.47/0.72 7. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (-. (g_false T_0 T_1)) (-. (g_true T_0 T_1)) ### DisjTree 2 4 6 % 0.47/0.72 8. (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)) (-. (g_false T_0 T_1)) ### All 7 % 0.47/0.72 9. (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 T_0 T_1)) (-. (g_true T_0 T_1)) ### All 8 % 0.47/0.72 10. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.47/0.72 11. (-. (g_false_only T_0 T_1)) (-. (g_true T_0 T_1)) (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_false_only_g 9 10 % 0.47/0.72 12. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.47/0.72 13. (g_both T_0 T_1) (-. (g_true T_0 T_1)) ### Extension/test/both_g 12 % 0.47/0.72 14. (g_true_only T_0 T_0) (-. (g_true_only T_0 T_0)) ### Axiom % 0.47/0.72 15. (g_true_only T_0 T_1) (-. (g_true_only T_0 T_1)) ### Axiom % 0.47/0.72 16. (-. ((g_both T_0 T_1) \/ (g_true_only T_0 T_1))) (g_true_only T_0 T_1) ### NotOr 15 % 0.47/0.72 17. (-. ((g_true_only T_0 T_0) /\ ((g_both T_0 T_1) \/ (g_true_only T_0 T_1)))) (g_true_only T_0 T_1) (g_true_only T_0 T_0) ### NotAnd 14 16 % 0.47/0.72 18. (-. (((g_true_only T_0 T_0) /\ ((g_both T_0 T_1) \/ (g_true_only T_0 T_1))) \/ (((g_both T_0 T_0) /\ ((g_false_only T_0 T_1) \/ (g_true_only T_0 T_1))) \/ ((g_false_only T_0 T_0) /\ ((g_false_only T_0 T_1) \/ (g_both T_0 T_1)))))) (g_true_only T_0 T_0) (g_true_only T_0 T_1) ### ConjTree 17 % 0.47/0.72 19. (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (g_true_only T_0 T_1) (g_true_only T_0 T_0) ### NotExists 18 % 0.47/0.72 20. (-. (g_false T_0 T_0)) (g_false T_0 T_0) ### Axiom % 0.47/0.72 21. (g_both T_0 T_0) (-. (g_false T_0 T_0)) ### Extension/test/both_g 20 % 0.47/0.72 22. (-. (g_false T_0 T_0)) (g_false T_0 T_0) ### Axiom % 0.47/0.72 23. (g_false_only T_0 T_0) (-. (g_false T_0 T_0)) ### Extension/test/false_only_g 22 % 0.47/0.72 24. ((g_true_only T_0 T_0) \/ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0))) (-. (g_false T_0 T_0)) (g_true_only T_0 T_1) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### DisjTree 19 21 23 % 0.47/0.72 25. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (g_true_only T_0 T_1) (-. (g_false T_0 T_0)) ### All 24 % 0.47/0.72 26. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (-. (g_false T_0 T_1)) (-. (g_false T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C 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)))) ### DisjTree 25 4 6 % 0.47/0.72 27. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false T_0 T_0)) (-. (g_false T_0 T_1)) ### All 26 % 0.47/0.72 28. (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 T_0 T_1)) (-. (g_false T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### All 27 % 0.47/0.72 29. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.47/0.72 30. (-. (g_false_only T_0 T_1)) (-. (g_true T_0 T_1)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false T_0 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))))) ### Extension/test/not_false_only_g 28 29 % 0.47/0.72 31. (-. (g_true T_0 T_0)) (g_true T_0 T_0) ### Axiom % 0.47/0.72 32. (g_true_only T_0 T_0) (-. (g_true T_0 T_0)) ### Extension/test/true_only_g 31 % 0.47/0.72 33. (-. (g_true T_0 T_0)) (g_true T_0 T_0) ### Axiom % 0.47/0.72 34. (g_both T_0 T_0) (-. (g_true T_0 T_0)) ### Extension/test/both_g 33 % 0.47/0.72 35. ((g_true_only T_0 T_0) \/ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0))) (-. (g_false T_0 T_0)) (-. (g_true T_0 T_0)) ### DisjTree 32 34 23 % 0.47/0.72 36. (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_0)) (-. (g_false T_0 T_0)) ### All 35 % 0.47/0.72 37. (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 T_0 T_0)) (-. (g_true T_0 T_0)) ### All 36 % 0.47/0.72 38. (-. (g_false T_0 T_0)) (g_false T_0 T_0) ### Axiom % 0.47/0.72 39. (-. (g_true_only T_0 T_0)) (-. (g_false T_0 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))))) ### Extension/test/not_true_only_g 37 38 % 0.47/0.72 40. (-. ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (g_false T_0 T_0)) ### NotOr 39 % 0.47/0.72 41. (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (g_false T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_1)) ### NotAnd 30 40 % 0.47/0.72 42. (-. (g_both T_0 T_1)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false T_0 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))))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) ### Extension/test/not_both_g 41 28 % 0.47/0.72 43. (-. ((g_true_only T_0 T_0) \/ (g_false_only T_0 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))))) (-. (g_false T_0 T_0)) ### NotOr 39 % 0.47/0.72 44. (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (g_false T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### NotAnd 42 43 % 0.47/0.72 45. (-. (g_true T_0 T_0)) (g_true T_0 T_0) ### Axiom % 0.47/0.72 46. (-. (g_false_only T_0 T_0)) (-. (g_true T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### Extension/test/not_false_only_g 44 45 % 0.57/0.74 47. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.57/0.74 48. (-. (g_true T_0 T_1)) (g_true T_0 T_1) ### Axiom % 0.57/0.74 49. (-. (g_false_only T_0 T_1)) (-. (g_true T_0 T_1)) (g_false T_0 T_1) ### Extension/test/not_false_only_g 47 48 % 0.57/0.74 50. (-. ((g_false_only T_0 T_1) \/ (g_both T_0 T_1))) (g_false T_0 T_1) (-. (g_true T_0 T_1)) ### NotOr 49 % 0.57/0.74 51. (-. ((g_false_only T_0 T_0) /\ ((g_false_only T_0 T_1) \/ (g_both T_0 T_1)))) (-. (g_true T_0 T_1)) (g_false T_0 T_1) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_0)) ### NotAnd 46 50 % 0.57/0.74 52. (-. (((g_true_only T_0 T_0) /\ ((g_both T_0 T_1) \/ (g_true_only T_0 T_1))) \/ (((g_both T_0 T_0) /\ ((g_false_only T_0 T_1) \/ (g_true_only T_0 T_1))) \/ ((g_false_only T_0 T_0) /\ ((g_false_only T_0 T_1) \/ (g_both T_0 T_1)))))) (-. (g_true T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) (-. (g_true T_0 T_1)) ### ConjTree 51 % 0.57/0.74 53. (-. (g_true T_0 T_1)) (g_false T_0 T_1) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_0)) ### NotExists 52 % 0.57/0.74 54. (g_false_only T_0 T_1) (-. (g_true T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (g_true T_0 T_1)) ### Extension/test/false_only_g 53 % 0.57/0.74 55. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_0)) (-. (g_true T_0 T_1)) ### DisjTree 2 13 54 % 0.57/0.74 56. (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)) (-. (g_true T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### All 55 % 0.57/0.74 57. (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_0)) (-. (g_true T_0 T_1)) ### All 56 % 0.57/0.74 58. (g_false T_0 T_0) (-. (g_false T_0 T_0)) ### Axiom % 0.57/0.74 59. (-. (g_both T_0 T_0)) (g_false T_0 T_0) (-. (g_true T_0 T_1)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### Extension/test/not_both_g 57 58 % 0.57/0.74 60. (-. (g_true_only T_0 T_0)) (-. (g_both T_0 T_0)) (-. (g_true T_0 T_1)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### Extension/test/not_true_only_g 57 59 % 0.57/0.74 61. (-. ((g_true_only T_0 T_0) \/ (g_both T_0 T_0))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_true T_0 T_1)) ### NotOr 60 % 0.57/0.74 62. (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 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))))) (-. (g_true T_0 T_1)) ### NotAnd 11 61 % 0.57/0.74 63. (g_false T_0 T_0) (-. (g_false T_0 T_0)) ### Axiom % 0.57/0.74 64. (-. (g_both T_0 T_0)) (g_false T_0 T_0) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) (-. (g_true T_0 T_1)) ### Extension/test/not_both_g 53 63 % 0.57/0.74 65. (-. (g_true_only T_0 T_0)) (-. (g_both T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) (-. (g_true T_0 T_1)) ### Extension/test/not_true_only_g 53 64 % 0.57/0.75 66. (-. ((g_true_only T_0 T_0) \/ (g_both T_0 T_0))) (-. (g_true T_0 T_1)) (g_false T_0 T_1) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### NotOr 65 % 0.57/0.75 67. (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) (-. (g_true T_0 T_1)) ### NotAnd 49 66 % 0.57/0.75 68. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.57/0.75 69. (-. (g_both T_0 T_1)) (g_false T_0 T_1) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### Extension/test/not_both_g 67 68 % 0.57/0.75 70. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.57/0.75 71. (g_true T_0 T_1) (-. (g_true T_0 T_1)) ### Axiom % 0.57/0.75 72. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.57/0.75 73. (-. (g_both T_0 T_1)) (g_false T_0 T_1) (g_true T_0 T_1) ### Extension/test/not_both_g 71 72 % 0.57/0.75 74. (-. (g_both T_0 T_0)) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) ### Extension/test/not_both_g 46 44 % 0.57/0.75 75. (-. ((g_both T_0 T_1) /\ (g_both T_0 T_0))) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_true T_0 T_1) (g_false T_0 T_1) ### NotAnd 73 74 % 0.57/0.75 76. (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) (g_false T_0 T_1) (g_true T_0 T_1) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) ### NotExists 75 % 0.57/0.75 77. (-. (g_false_only T_0 T_1)) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) (g_false T_0 T_1) ### Extension/test/not_false_only_g 70 76 % 0.57/0.75 78. (-. ((g_true_only T_0 T_0) \/ (g_both T_0 T_0))) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### NotOr 74 % 0.57/0.75 79. (g_false T_0 T_1) (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) ### NotAnd 77 78 % 0.57/0.75 80. (-. ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) (g_false T_0 T_1) ### NotOr 79 % 0.57/0.75 81. (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) ### NotAnd 69 80 % 0.57/0.75 82. (-. (g_true_only T_0 T_1)) (-. (Ex B, ((g_both B T_1) /\ (g_both B 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_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### Extension/test/not_true_only_g 62 81 % 0.57/0.75 83. (-. ((g_both T_0 T_0) \/ (g_false_only T_0 T_0))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### NotOr 74 % 0.57/0.75 84. (-. ((g_true_only T_0 T_1) /\ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 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))))) (-. (Ex B, ((g_both B T_1) /\ (g_both B B)))) ### NotAnd 82 83 % 0.57/0.76 85. (-. (((g_true_only T_0 T_1) /\ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0))) \/ (((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0))) \/ ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))))) (-. (Ex B, ((g_both B T_1) /\ (g_both B 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 C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### ConjTree 84 % 0.57/0.76 86. (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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 B T_1) /\ (g_both B B)))) ### NotExists 85 % 0.57/0.76 87. (-. (All A, (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))) (-. (Ex B, ((g_both B T_1) /\ (g_both B 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_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) ### NotAllEx 86 % 0.57/0.76 88. (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B 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 B T_1) /\ (g_both B B)))) ### NotExists 87 % 0.57/0.76 89. (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B)))))) ### Axiom % 0.57/0.76 90. (-. (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B)))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) ### NotNot 89 % 0.57/0.76 91. (-. ((Ex B, ((g_both B T_1) /\ (g_both B B))) /\ (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B 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_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) ### NotAnd 88 90 % 0.57/0.76 92. (-. (Ex A, ((Ex B, ((g_both B A) /\ (g_both B B))) /\ (-. (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B)))))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B 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 91 % 0.57/0.76 93. (g_true_only T_2 T_2) (-. (g_true_only T_2 T_2)) ### Axiom % 0.57/0.76 94. (g_true_only T_2 T_3) (-. (g_true_only T_2 T_3)) ### Axiom % 0.57/0.76 95. (-. ((g_both T_2 T_3) \/ (g_true_only T_2 T_3))) (g_true_only T_2 T_3) ### NotOr 94 % 0.57/0.76 96. (-. ((g_true_only T_2 T_2) /\ ((g_both T_2 T_3) \/ (g_true_only T_2 T_3)))) (g_true_only T_2 T_3) (g_true_only T_2 T_2) ### NotAnd 93 95 % 0.57/0.76 97. (-. (((g_true_only T_2 T_2) /\ ((g_both T_2 T_3) \/ (g_true_only T_2 T_3))) \/ (((g_both T_2 T_2) /\ ((g_false_only T_2 T_3) \/ (g_true_only T_2 T_3))) \/ ((g_false_only T_2 T_2) /\ ((g_false_only T_2 T_3) \/ (g_both T_2 T_3)))))) (g_true_only T_2 T_2) (g_true_only T_2 T_3) ### ConjTree 96 % 0.57/0.76 98. (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) (g_true_only T_2 T_3) (g_true_only T_2 T_2) ### NotExists 97 % 0.57/0.76 99. ((g_true_only T_2 T_3) /\ (g_true_only T_2 T_2)) (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) ### And 98 % 0.57/0.76 100. (g_false_only T_2 T_2) (-. (g_false_only T_2 T_2)) ### Axiom % 0.57/0.76 101. (g_false_only T_2 T_3) (-. (g_false_only T_2 T_3)) ### Axiom % 0.57/0.76 102. (-. ((g_false_only T_2 T_3) \/ (g_both T_2 T_3))) (g_false_only T_2 T_3) ### NotOr 101 % 0.57/0.76 103. (-. ((g_false_only T_2 T_2) /\ ((g_false_only T_2 T_3) \/ (g_both T_2 T_3)))) (g_false_only T_2 T_3) (g_false_only T_2 T_2) ### NotAnd 100 102 % 0.57/0.76 104. (-. (((g_true_only T_2 T_2) /\ ((g_both T_2 T_3) \/ (g_true_only T_2 T_3))) \/ (((g_both T_2 T_2) /\ ((g_false_only T_2 T_3) \/ (g_true_only T_2 T_3))) \/ ((g_false_only T_2 T_2) /\ ((g_false_only T_2 T_3) \/ (g_both T_2 T_3)))))) (g_false_only T_2 T_2) (g_false_only T_2 T_3) ### ConjTree 103 % 0.57/0.76 105. (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) (g_false_only T_2 T_3) (g_false_only T_2 T_2) ### NotExists 104 % 0.57/0.76 106. ((g_false_only T_2 T_3) /\ (g_false_only T_2 T_2)) (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) ### And 105 % 0.57/0.76 107. (((g_true_only T_2 T_3) /\ (g_true_only T_2 T_2)) \/ ((g_false_only T_2 T_3) /\ (g_false_only T_2 T_2))) (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) ### Or 99 106 % 0.57/0.76 108. (All B, (((g_true_only B T_3) /\ (g_true_only B B)) \/ ((g_false_only B T_3) /\ (g_false_only B B)))) (-. (Ex C, (((g_true_only C T_2) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C T_2) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C T_2) /\ ((g_false_only C T_3) \/ (g_both C T_3))))))) ### All 107 % 0.57/0.77 109. (-. (All A, (Ex C, (((g_true_only C A) /\ ((g_both C T_3) \/ (g_true_only C T_3))) \/ (((g_both C A) /\ ((g_false_only C T_3) \/ (g_true_only C T_3))) \/ ((g_false_only C A) /\ ((g_false_only C T_3) \/ (g_both C T_3)))))))) (All B, (((g_true_only B T_3) /\ (g_true_only B B)) \/ ((g_false_only B T_3) /\ (g_false_only B B)))) ### NotAllEx 108 % 0.57/0.77 110. (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (All B, (((g_true_only B T_3) /\ (g_true_only B B)) \/ ((g_false_only B T_3) /\ (g_false_only B B)))) ### NotExists 109 % 0.57/0.77 111. (Ex A, (All B, (((g_true_only B A) /\ (g_true_only B B)) \/ ((g_false_only B A) /\ (g_false_only B B))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) ### Exists 110 % 0.57/0.77 112. (g_false T_0 T_1) (-. (g_false T_0 T_1)) ### Axiom % 0.57/0.77 113. (-. ((g_both T_0 T_0) /\ (g_both T_0 T_1))) (g_true T_0 T_1) (g_false T_0 T_1) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### NotAnd 74 73 % 0.57/0.77 114. (-. (Ex C, ((g_both C T_0) /\ (g_both C T_1)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) (g_false T_0 T_1) (g_true T_0 T_1) ### NotExists 113 % 0.57/0.77 115. (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))) ### Axiom % 0.57/0.77 116. (-. (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### NotNot 115 % 0.57/0.77 117. (-. ((Ex C, ((g_both C T_0) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))))) (g_true T_0 T_1) (g_false T_0 T_1) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) ### NotAnd 114 116 % 0.57/0.77 118. (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) (g_false T_0 T_1) (g_true T_0 T_1) ### NotExists 117 % 0.57/0.77 119. (-. (g_false_only T_0 T_1)) (-. (g_false_only T_0 T_0)) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (g_false T_0 T_1) ### Extension/test/not_false_only_g 112 118 % 0.57/0.77 120. (g_false T_0 T_1) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 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))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. (g_false_only T_0 T_0)) ### NotAnd 119 78 % 0.57/0.77 121. (-. ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (g_false T_0 T_1) ### NotOr 120 % 0.57/0.77 122. (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (g_false T_0 T_1) ### NotAnd 69 121 % 0.57/0.77 123. (-. (g_true_only T_0 T_1)) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (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_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### Extension/test/not_true_only_g 62 122 % 0.57/0.77 124. (-. ((g_true_only T_0 T_1) /\ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0)))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (-. ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))) (-. ((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 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))))) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) ### NotAnd 123 83 % 0.57/0.77 125. (-. (((g_true_only T_0 T_1) /\ ((g_both T_0 T_0) \/ (g_false_only T_0 T_0))) \/ (((g_both T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_false_only T_0 T_0))) \/ ((g_false_only T_0 T_1) /\ ((g_true_only T_0 T_0) \/ (g_both T_0 T_0)))))) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (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 C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) ### ConjTree 124 % 0.57/0.77 126. (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (-. (Ex C, (((g_true_only C T_0) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C T_0) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C T_0) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))) (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, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) ### NotExists 125 % 0.57/0.77 127. (-. (All A, (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))) (-. (Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) (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_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) ### NotAllEx 126 % 0.57/0.77 128. (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B 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, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1)))))))))) ### NotExists 127 % 0.57/0.77 129. (-. (g_false T_4 T_1)) (g_false T_4 T_1) ### Axiom % 0.57/0.77 130. (g_false_only T_4 T_1) (-. (g_false T_4 T_1)) ### Extension/test/false_only_g 129 % 0.57/0.77 131. ((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) (-. (g_false T_4 T_1)) ### And 130 % 0.57/0.77 132. (-. (g_true T_4 T_1)) (g_true T_4 T_1) ### Axiom % 0.57/0.77 133. (g_true_only T_4 T_1) (-. (g_true T_4 T_1)) ### Extension/test/true_only_g 132 % 0.57/0.77 134. ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1)) (-. (g_true T_4 T_1)) ### And 133 % 0.57/0.77 135. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (-. (g_true T_4 T_1)) (-. (g_false T_4 T_1)) ### Or 131 134 % 0.57/0.77 136. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_1)) (-. (g_true T_4 T_1)) ### All 135 % 0.57/0.77 137. (-. (g_true T_4 T_1)) (g_true T_4 T_1) ### Axiom % 0.57/0.77 138. (-. (g_false_only T_4 T_1)) (-. (g_true T_4 T_1)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_false_only_g 136 137 % 0.57/0.77 139. (-. (g_true T_4 T_4)) (g_true T_4 T_4) ### Axiom % 0.57/0.77 140. (g_true_only T_4 T_4) (-. (g_true T_4 T_4)) ### Extension/test/true_only_g 139 % 0.57/0.77 141. ((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) (-. (g_true T_4 T_4)) ### And 140 % 0.57/0.77 142. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (-. (g_true T_4 T_1)) (-. (g_true T_4 T_4)) ### Or 141 134 % 0.57/0.77 143. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_true T_4 T_4)) (-. (g_true T_4 T_1)) ### All 142 % 0.57/0.77 144. (g_false T_4 T_4) (-. (g_false T_4 T_4)) ### Axiom % 0.57/0.77 145. (-. (g_both T_4 T_4)) (g_false T_4 T_4) (-. (g_true T_4 T_1)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_both_g 143 144 % 0.57/0.77 146. (-. (g_true_only T_4 T_4)) (-. (g_both T_4 T_4)) (-. (g_true T_4 T_1)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_true_only_g 143 145 % 0.57/0.77 147. (-. ((g_true_only T_4 T_4) \/ (g_both T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_true T_4 T_1)) ### NotOr 146 % 0.57/0.77 148. (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_true T_4 T_1)) ### NotAnd 138 147 % 0.57/0.77 149. (g_false T_4 T_1) (-. (g_false T_4 T_1)) ### Axiom % 0.57/0.77 150. (-. (g_true T_4 T_1)) (g_true T_4 T_1) ### Axiom % 0.57/0.77 151. (-. (g_false_only T_4 T_1)) (-. (g_true T_4 T_1)) (g_false T_4 T_1) ### Extension/test/not_false_only_g 149 150 % 0.57/0.77 152. (g_false T_4 T_1) (-. (g_false T_4 T_1)) ### Axiom % 0.57/0.77 153. (g_true_only T_4 T_1) (g_false T_4 T_1) ### Extension/test/true_only_g 152 % 0.57/0.79 154. ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1)) (g_false T_4 T_1) ### And 153 % 0.57/0.79 155. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (g_false T_4 T_1) (-. (g_true T_4 T_4)) ### Or 141 154 % 0.57/0.79 156. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_true T_4 T_4)) (g_false T_4 T_1) ### All 155 % 0.57/0.79 157. (g_false T_4 T_4) (-. (g_false T_4 T_4)) ### Axiom % 0.57/0.79 158. (g_true_only T_4 T_4) (g_false T_4 T_4) ### Extension/test/true_only_g 157 % 0.57/0.79 159. ((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) (g_false T_4 T_4) ### And 158 % 0.57/0.79 160. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (g_false T_4 T_1) (g_false T_4 T_4) ### Or 159 154 % 0.57/0.79 161. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_4) (g_false T_4 T_1) ### All 160 % 0.57/0.79 162. (-. (g_true_only T_4 T_4)) (g_false T_4 T_1) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_true_only_g 156 161 % 0.57/0.79 163. (-. ((g_true_only T_4 T_4) \/ (g_both T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_1) ### NotOr 162 % 0.57/0.79 164. (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_1) (-. (g_true T_4 T_1)) ### NotAnd 151 163 % 0.57/0.79 165. (g_false T_4 T_1) (-. (g_false T_4 T_1)) ### Axiom % 0.57/0.79 166. (-. (g_both T_4 T_1)) (g_false T_4 T_1) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) ### Extension/test/not_both_g 164 165 % 0.57/0.79 167. (-. (g_false T_4 T_4)) (g_false T_4 T_4) ### Axiom % 0.57/0.79 168. (g_false_only T_4 T_4) (-. (g_false T_4 T_4)) ### Extension/test/false_only_g 167 % 0.57/0.79 169. ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1)) (-. (g_false T_4 T_4)) ### And 168 % 0.57/0.79 170. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (-. (g_false T_4 T_4)) (-. (g_false T_4 T_1)) ### Or 131 169 % 0.57/0.79 171. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_1)) (-. (g_false T_4 T_4)) ### All 170 % 0.57/0.79 172. (-. (g_true T_4 T_1)) (g_true T_4 T_1) ### Axiom % 0.57/0.79 173. (-. (g_false_only T_4 T_1)) (-. (g_true T_4 T_1)) (-. (g_false T_4 T_4)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_false_only_g 171 172 % 0.57/0.79 174. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (-. (g_false T_4 T_4)) (-. (g_true T_4 T_4)) ### Or 141 169 % 0.57/0.79 175. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_true T_4 T_4)) (-. (g_false T_4 T_4)) ### All 174 % 0.57/0.79 176. (-. (g_false T_4 T_4)) (g_false T_4 T_4) ### Axiom % 0.57/0.79 177. (-. (g_true_only T_4 T_4)) (-. (g_false T_4 T_4)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### Extension/test/not_true_only_g 175 176 % 0.57/0.79 178. (-. ((g_true_only T_4 T_4) \/ (g_both T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_4)) ### NotOr 177 % 0.57/0.79 179. (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_4)) (-. (g_true T_4 T_1)) ### NotAnd 173 178 % 0.57/0.79 180. (-. (g_both T_4 T_1)) (-. (g_false T_4 T_4)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) ### Extension/test/not_both_g 179 171 % 0.57/0.79 181. (-. ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_4)) ### NotOr 177 % 0.57/0.79 182. (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false T_4 T_4)) ### NotAnd 180 181 % 0.57/0.79 183. (-. (g_true T_4 T_4)) (g_true T_4 T_4) ### Axiom % 0.57/0.79 184. (-. (g_false_only T_4 T_4)) (-. (g_true T_4 T_4)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) ### Extension/test/not_false_only_g 182 183 % 0.57/0.79 185. (g_false T_4 T_4) (-. (g_false T_4 T_4)) ### Axiom % 0.57/0.79 186. (g_true T_4 T_4) (-. (g_true T_4 T_4)) ### Axiom % 0.57/0.79 187. (g_false_only T_4 T_4) (g_true T_4 T_4) ### Extension/test/false_only_g 186 % 0.57/0.79 188. ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1)) (g_true T_4 T_4) ### And 187 % 0.57/0.79 189. (((g_true_only T_4 T_4) /\ (g_false_only T_4 T_1)) \/ ((g_false_only T_4 T_4) /\ (g_true_only T_4 T_1))) (g_true T_4 T_4) (g_false T_4 T_4) ### Or 159 188 % 0.57/0.79 190. (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_4) (g_true T_4 T_4) ### All 189 % 0.57/0.79 191. (-. (g_false_only T_4 T_4)) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_4) ### Extension/test/not_false_only_g 185 190 % 0.57/0.79 192. (-. (g_true_only T_4 T_4)) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false_only T_4 T_4)) ### Extension/test/not_true_only_g 184 191 % 0.57/0.79 193. (-. ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) ### NotOr 192 % 0.57/0.79 194. (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (g_false T_4 T_1) ### NotAnd 166 193 % 0.57/0.79 195. (-. (g_true_only T_4 T_1)) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) ### Extension/test/not_true_only_g 148 194 % 0.57/0.79 196. (-. (g_both T_4 T_4)) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. (g_false_only T_4 T_4)) ### Extension/test/not_both_g 184 182 % 0.57/0.79 197. (-. ((g_both T_4 T_4) \/ (g_false_only T_4 T_4))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) ### NotOr 196 % 0.57/0.79 198. (-. ((g_true_only T_4 T_1) /\ ((g_both T_4 T_4) \/ (g_false_only T_4 T_4)))) (-. ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) (-. ((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4)))) ### NotAnd 195 197 % 0.57/0.79 199. (-. (((g_true_only T_4 T_1) /\ ((g_both T_4 T_4) \/ (g_false_only T_4 T_4))) \/ (((g_both T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_false_only T_4 T_4))) \/ ((g_false_only T_4 T_1) /\ ((g_true_only T_4 T_4) \/ (g_both T_4 T_4)))))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### ConjTree 198 % 0.57/0.79 200. (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (All C, (((g_true_only C T_4) /\ (g_false_only C T_1)) \/ ((g_false_only C T_4) /\ (g_true_only C T_1)))) ### NotExists 199 % 0.57/0.79 201. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C T_1)) \/ ((g_false_only C A) /\ (g_true_only C T_1))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) ### Exists 200 % 0.57/0.79 202. (-. (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C T_1)) \/ ((g_false_only C A) /\ (g_true_only C T_1))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) ### NotNot 201 % 0.57/0.79 203. (-. ((Ex A, ((Ex C, ((g_both C A) /\ (g_both C T_1))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C T_1) \/ (g_true_only C T_1))) \/ (((g_both C A) /\ ((g_false_only C T_1) \/ (g_true_only C T_1))) \/ ((g_false_only C A) /\ ((g_false_only C T_1) \/ (g_both C T_1))))))))) /\ (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C T_1)) \/ ((g_false_only C A) /\ (g_true_only C T_1)))))))) (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_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) ### NotAnd 128 202 % 0.57/0.79 204. (-. (Ex B, ((Ex A, ((Ex C, ((g_both C A) /\ (g_both C B))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) /\ (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C B)) \/ ((g_false_only C A) /\ (g_true_only C B))))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (-. (Ex B, (((g_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B 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 203 % 0.57/0.79 205. (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B)))))))) ### Axiom % 0.57/0.79 206. (-. ((Ex A, ((Ex B, ((g_both B A) /\ (g_both B B))) /\ (-. (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B))))))))) /\ ((-. (Ex A, (All B, (((g_true_only B A) /\ (g_true_only B B)) \/ ((g_false_only B A) /\ (g_false_only B B)))))) /\ ((Ex B, ((Ex A, ((Ex C, ((g_both C A) /\ (g_both C B))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) /\ (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C B)) \/ ((g_false_only C A) /\ (g_true_only C B)))))))) /\ (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C 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_true_only B T_1) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B T_1) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B T_1) /\ ((g_true_only B B) \/ (g_both B B))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) ### DisjTree 92 111 204 205 % 0.57/0.79 207. (-. (All A, (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B)))))))) (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C 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, ((Ex B, ((g_both B A) /\ (g_both B B))) /\ (-. (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B))))))))) /\ ((-. (Ex A, (All B, (((g_true_only B A) /\ (g_true_only B B)) \/ ((g_false_only B A) /\ (g_false_only B B)))))) /\ ((Ex B, ((Ex A, ((Ex C, ((g_both C A) /\ (g_both C B))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) /\ (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C B)) \/ ((g_false_only C A) /\ (g_true_only C B)))))))) /\ (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))))))) ### NotAllEx 206 % 0.57/0.79 208. (-. ((All A, (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B))))))) \/ ((Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B)))))))) \/ ((Ex A, ((Ex B, ((g_both B A) /\ (g_both B B))) /\ (-. (Ex B, (((g_true_only B A) /\ ((g_both B B) \/ (g_false_only B B))) \/ (((g_both B A) /\ ((g_true_only B B) \/ (g_false_only B B))) \/ ((g_false_only B A) /\ ((g_true_only B B) \/ (g_both B B))))))))) /\ ((-. (Ex A, (All B, (((g_true_only B A) /\ (g_true_only B B)) \/ ((g_false_only B A) /\ (g_false_only B B)))))) /\ ((Ex B, ((Ex A, ((Ex C, ((g_both C A) /\ (g_both C B))) /\ (-. (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C B))))))))) /\ (-. (Ex A, (All C, (((g_true_only C A) /\ (g_false_only C B)) \/ ((g_false_only C A) /\ (g_true_only C B)))))))) /\ (-. (Ex B, (All A, (Ex C, (((g_true_only C A) /\ ((g_both C B) \/ (g_true_only C B))) \/ (((g_both C A) /\ ((g_false_only C B) \/ (g_true_only C B))) \/ ((g_false_only C A) /\ ((g_false_only C B) \/ (g_both C 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 207 % 0.57/0.79 % SZS output end Proof % 0.57/0.79 (* END-PROOF *) %------------------------------------------------------------------------------