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