%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYO606+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 : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 20:05:13 EDT 2022 % Result : Theorem 0.18s 0.47s % Output : Proof 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYO606+1 : TPTP v8.1.0. Released v7.0.0. % 0.00/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n010.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 8 21:39:31 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.47 % SZS status Theorem % 0.18/0.47 (* PROOF-FOUND *) % 0.18/0.47 (* BEGIN-PROOF *) % 0.18/0.47 % SZS output start Proof % 0.18/0.47 1. (g_true_only T_0 T_1) (-. (g_true_only T_0 T_1)) ### Axiom % 0.18/0.47 2. (-. (Ex B, (g_true_only T_0 B))) (g_true_only T_0 T_1) ### NotExists 1 % 0.18/0.47 3. (h_true T_0 T_2) (-. (h_true T_0 T_2)) ### Axiom % 0.18/0.47 4. (h_true T_0 T_2) (-. (h_true T_0 T_2)) ### Axiom % 0.18/0.47 5. (-. (h_false T_0 T_2)) (h_false T_0 T_2) ### Axiom % 0.18/0.47 6. (-. (h_true_only T_0 T_2)) (-. (h_false T_0 T_2)) (h_true T_0 T_2) ### Extension/test/not_true_only_h 4 5 % 0.18/0.47 7. (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) (-. (h_false T_0 T_2)) ### NotExists 6 % 0.18/0.47 8. (-. (h_both T_0 T_2)) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) ### Extension/test/not_both_h 3 7 % 0.18/0.47 9. (-. (Ex B, (h_both T_0 B))) (h_true T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) ### NotExists 8 % 0.18/0.47 10. (h_true_only T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (h_both T_0 B))) ### Extension/test/true_only_h 9 % 0.18/0.47 11. (-. (h_false T_0 T_2)) (h_false T_0 T_2) ### Axiom % 0.18/0.47 12. (h_both T_0 T_2) (-. (h_false T_0 T_2)) ### Extension/test/both_h 11 % 0.18/0.47 13. (-. (h_false T_0 T_2)) (h_false T_0 T_2) ### Axiom % 0.18/0.47 14. (h_false_only T_0 T_2) (-. (h_false T_0 T_2)) ### Extension/test/false_only_h 13 % 0.18/0.47 15. ((h_true_only T_0 T_2) \/ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) (-. (h_false T_0 T_2)) (-. (Ex B, (h_both T_0 B))) (-. (Ex B, (h_true_only T_0 B))) ### DisjTree 10 12 14 % 0.18/0.47 16. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (h_both T_0 B))) (-. (h_false T_0 T_2)) ### All 15 % 0.18/0.47 17. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (h_false T_0 T_2)) (-. (Ex B, (h_both T_0 B))) (-. (Ex B, (h_true_only T_0 B))) ### All 16 % 0.18/0.47 18. (-. (Ex B, (h_true_only T_0 B))) (Ex B, (h_true_only T_0 B)) ### Axiom % 0.18/0.47 19. (-. (-. (Ex B, (h_true_only T_0 B)))) (-. (Ex B, (h_true_only T_0 B))) ### NotNot 18 % 0.18/0.47 20. (-. ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false T_0 T_2)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 17 19 % 0.18/0.47 21. (-. ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) ### NotAnd 9 19 % 0.18/0.47 22. (-. (h_false_only T_0 T_2)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))) ### Extension/test/not_false_only_h 20 21 % 0.18/0.47 23. (-. (All B, (h_false_only T_0 B))) (-. ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAllEx 22 % 0.18/0.47 24. (-. (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) ### NotOr 23 % 0.18/0.47 25. (-. ((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_0 T_1) ### NotAnd 2 24 % 0.18/0.47 26. (-. (((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B)))) \/ ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B)))))) (g_true_only T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) ### NotOr 25 % 0.18/0.47 27. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_0 T_1) ### NotExists 26 % 0.18/0.47 28. (-. (g_false T_0 T_1)) (g_false T_0 T_1) ### Axiom % 0.18/0.47 29. (g_both T_0 T_1) (-. (g_false T_0 T_1)) ### Extension/test/both_g 28 % 0.18/0.47 30. (-. (g_false T_0 T_1)) (g_false T_0 T_1) ### Axiom % 0.18/0.47 31. (g_false_only T_0 T_1) (-. (g_false T_0 T_1)) ### Extension/test/false_only_g 30 % 0.18/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)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 27 29 31 % 0.18/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)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (g_false T_0 T_1)) ### All 32 % 0.18/0.47 34. (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)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 33 % 0.18/0.47 35. (g_true_only T_0 T_1) (-. (g_true_only T_0 T_1)) ### Axiom % 0.18/0.47 36. (h_true_only T_0 T_3) (-. (h_true_only T_0 T_3)) ### Axiom % 0.18/0.47 37. (-. (Ex B, (h_true_only T_0 B))) (h_true_only T_0 T_3) ### NotExists 36 % 0.18/0.47 38. (-. (h_false T_0 T_3)) (h_false T_0 T_3) ### Axiom % 0.18/0.47 39. (h_both T_0 T_3) (-. (h_false T_0 T_3)) ### Extension/test/both_h 38 % 0.18/0.47 40. (-. (h_false T_0 T_3)) (h_false T_0 T_3) ### Axiom % 0.18/0.47 41. (h_false_only T_0 T_3) (-. (h_false T_0 T_3)) ### Extension/test/false_only_h 40 % 0.18/0.47 42. ((h_true_only T_0 T_3) \/ ((h_both T_0 T_3) \/ (h_false_only T_0 T_3))) (-. (h_false T_0 T_3)) (-. (Ex B, (h_true_only T_0 B))) ### DisjTree 37 39 41 % 0.18/0.47 43. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false T_0 T_3)) ### All 42 % 0.18/0.47 44. (-. (h_true T_0 T_3)) (h_true T_0 T_3) ### Axiom % 0.18/0.47 45. (-. (h_false_only T_0 T_3)) (-. (h_true T_0 T_3)) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### Extension/test/not_false_only_h 43 44 % 0.18/0.47 46. (-. (h_both T_0 T_3)) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false_only T_0 T_3)) ### Extension/test/not_both_h 45 43 % 0.18/0.47 47. (-. ((h_both T_0 T_3) \/ (h_false_only T_0 T_3))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotOr 46 % 0.18/0.47 48. (-. ((g_true_only T_0 T_1) /\ ((h_both T_0 T_3) \/ (h_false_only T_0 T_3)))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_1) ### NotAnd 35 47 % 0.18/0.47 49. (-. (((g_true_only T_0 T_1) /\ ((h_both T_0 T_3) \/ (h_false_only T_0 T_3))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 T_3)))) (g_true_only T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotOr 48 % 0.18/0.47 50. (-. (All C, (((g_true_only T_0 T_1) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 C))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_1) ### NotAllEx 49 % 0.18/0.47 51. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))) (g_true_only T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotExists 50 % 0.18/0.48 52. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_1) ### NotExists 51 % 0.18/0.48 53. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 52 % 0.18/0.48 54. ((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)) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 53 29 31 % 0.18/0.48 55. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (g_false T_0 T_1)) ### All 54 % 0.18/0.48 56. (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 A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 55 % 0.18/0.48 57. (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_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))))) ### NotAnd 34 56 % 0.18/0.48 58. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.18/0.48 59. (-. (Ex B, (g_both T_0 B))) (g_both T_0 T_1) ### NotExists 58 % 0.18/0.48 60. (-. (Ex B, (g_true_only T_0 B))) (Ex B, (g_true_only T_0 B)) ### Axiom % 0.18/0.48 61. (-. (Ex B, (g_true_only T_0 B))) (Ex B, (g_true_only T_0 B)) ### Axiom % 0.18/0.48 62. (-. (Ex B, (h_true_only T_0 B))) (Ex B, (h_true_only T_0 B)) ### Axiom % 0.18/0.48 63. (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))))) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) ### DisjTree 59 61 9 62 % 0.18/0.48 64. (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) (h_true T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) ### NotExists 63 % 0.18/0.48 65. (h_true_only T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) ### Extension/test/true_only_h 64 % 0.18/0.48 66. ((h_true_only T_0 T_2) \/ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) (-. (h_false T_0 T_2)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) (-. (Ex B, (h_true_only T_0 B))) ### DisjTree 65 12 14 % 0.18/0.48 67. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (h_false T_0 T_2)) ### All 66 % 0.18/0.48 68. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (h_false T_0 T_2)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) (-. (Ex B, (h_true_only T_0 B))) ### All 67 % 0.18/0.48 69. (-. (h_false_only T_0 T_2)) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Extension/test/not_false_only_h 68 64 % 0.18/0.48 70. (-. (All B, (h_false_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) (-. (Ex B, (h_true_only T_0 B))) ### NotAllEx 69 % 0.18/0.48 71. (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) ### DisjTree 59 60 70 % 0.18/0.48 72. (-. ((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B))))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex B, (h_true_only T_0 B))) (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B))))) ### NotAnd 71 24 % 0.18/0.48 73. (-. (((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B)))) \/ ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B)))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) ### NotOr 72 % 0.18/0.48 74. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex B, (h_true_only T_0 B))) ### NotExists 73 % 0.18/0.48 75. (g_true T_0 T_1) (-. (g_true T_0 T_1)) ### Axiom % 0.18/0.48 76. (g_false_only T_0 T_1) (g_true T_0 T_1) ### Extension/test/false_only_g 75 % 0.18/0.48 77. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 27 74 76 % 0.18/0.49 78. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_true T_0 T_1) ### All 77 % 0.18/0.49 79. (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 A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 78 % 0.18/0.49 80. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) ### Axiom % 0.18/0.49 81. (-. (Ex B, (g_true_only T_0 B))) (Ex B, (g_true_only T_0 B)) ### Axiom % 0.18/0.49 82. (h_true_only T_0 T_2) (-. (h_false T_0 T_2)) (-. (Ex B, (h_true_only T_0 B))) ### Extension/test/true_only_h 7 % 0.18/0.49 83. ((h_true_only T_0 T_2) \/ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false T_0 T_2)) ### DisjTree 82 12 14 % 0.18/0.49 84. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (h_false T_0 T_2)) (-. (Ex B, (h_true_only T_0 B))) ### All 83 % 0.18/0.49 85. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false T_0 T_2)) ### All 84 % 0.18/0.49 86. (h_true T_0 T_2) (-. (h_true T_0 T_2)) ### Axiom % 0.18/0.49 87. (h_false T_0 T_2) (-. (h_false T_0 T_2)) ### Axiom % 0.18/0.49 88. (h_true_only T_0 T_2) (h_false T_0 T_2) ### Extension/test/true_only_h 87 % 0.18/0.49 89. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.18/0.49 90. (h_both T_0 T_2) (-. (h_both T_0 T_2)) ### Axiom % 0.18/0.49 91. (-. ((g_both T_0 T_1) /\ (h_both T_0 T_2))) (h_both T_0 T_2) (g_both T_0 T_1) ### NotAnd 89 90 % 0.18/0.49 92. (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) (h_both T_0 T_2) ### NotExists 91 % 0.18/0.49 93. (h_true T_0 T_2) (-. (h_true T_0 T_2)) ### Axiom % 0.18/0.49 94. (h_false_only T_0 T_2) (h_true T_0 T_2) ### Extension/test/false_only_h 93 % 0.18/0.49 95. ((h_true_only T_0 T_2) \/ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) (h_true T_0 T_2) (g_both T_0 T_1) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (h_false T_0 T_2) ### DisjTree 88 92 94 % 0.18/0.49 96. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (h_false T_0 T_2) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) (h_true T_0 T_2) ### All 95 % 0.18/0.49 97. (h_true_only T_0 T_4) (-. (h_true_only T_0 T_4)) ### Axiom % 0.18/0.49 98. (-. (Ex B, (h_true_only T_0 B))) (h_true_only T_0 T_4) ### NotExists 97 % 0.18/0.49 99. ((g_false_only T_0 T_1) \/ (h_true_only T_0 T_4)) (-. (Ex B, (h_true_only T_0 B))) (g_true T_0 T_1) ### Or 76 98 % 0.18/0.49 100. (Ex C, ((g_false_only T_0 T_1) \/ (h_true_only T_0 C))) (g_true T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) ### Exists 99 % 0.18/0.49 101. (-. (-. (Ex C, ((g_false_only T_0 T_1) \/ (h_true_only T_0 C))))) (-. (Ex B, (h_true_only T_0 B))) (g_true T_0 T_1) ### NotNot 100 % 0.18/0.49 102. (-. ((Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 T_1) \/ (h_true_only T_0 C)))))) (g_true T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) (g_both T_0 T_1) (h_false T_0 T_2) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotAnd 96 101 % 0.18/0.49 103. (-. (Ex B, ((Ex C, ((g_both T_0 B) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 B) \/ (h_true_only T_0 C))))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (h_false T_0 T_2) (g_both T_0 T_1) (h_true T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) (g_true T_0 T_1) ### NotExists 102 % 0.18/0.49 104. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) (g_both T_0 T_1) (h_false T_0 T_2) (-. (Ex B, ((Ex C, ((g_both T_0 B) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 B) \/ (h_true_only T_0 C))))))) ### All 103 % 0.18/0.49 105. (g_true_only T_0 T_5) (-. (g_true_only T_0 T_5)) ### Axiom % 0.18/0.49 106. (-. (Ex B, (g_true_only T_0 B))) (g_true_only T_0 T_5) ### NotExists 105 % 0.18/0.49 107. ((g_true_only T_0 T_5) /\ ((h_both T_0 zenon_X6) \/ (h_false_only T_0 zenon_X6))) (-. (Ex B, (g_true_only T_0 B))) ### And 106 % 0.18/0.49 108. (g_false T_0 T_5) (-. (g_false T_0 T_5)) ### Axiom % 0.18/0.49 109. (g_true_only T_0 T_5) (g_false T_0 T_5) ### Extension/test/true_only_g 108 % 0.18/0.49 110. ((g_true_only T_0 T_5) /\ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) (g_false T_0 T_5) ### And 109 % 0.18/0.49 111. ((g_both T_0 T_5) /\ (h_false_only T_0 T_2)) (h_true T_0 T_2) ### And 94 % 0.18/0.49 112. (((g_true_only T_0 T_5) /\ ((h_both T_0 T_2) \/ (h_false_only T_0 T_2))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 T_2))) (h_true T_0 T_2) (g_false T_0 T_5) ### Or 110 111 % 0.18/0.49 113. (All C, (((g_true_only T_0 T_5) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 C)))) (g_false T_0 T_5) (h_true T_0 T_2) ### All 112 % 0.18/0.49 114. (g_both T_0 T_5) (h_true T_0 T_2) (All C, (((g_true_only T_0 T_5) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 C)))) ### Extension/test/both_g 113 % 0.18/0.49 115. ((g_both T_0 T_5) /\ (h_false_only T_0 zenon_X6)) (All C, (((g_true_only T_0 T_5) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 C)))) (h_true T_0 T_2) ### And 114 % 0.18/0.49 116. (((g_true_only T_0 T_5) /\ ((h_both T_0 zenon_X6) \/ (h_false_only T_0 zenon_X6))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 zenon_X6))) (h_true T_0 T_2) (All C, (((g_true_only T_0 T_5) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 C)))) (-. (Ex B, (g_true_only T_0 B))) ### Or 107 115 % 0.18/0.49 117. (-. (Ex B, (g_true_only T_0 B))) (All C, (((g_true_only T_0 T_5) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_5) /\ (h_false_only T_0 C)))) (h_true T_0 T_2) ### All 116 % 0.18/0.49 118. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C))))) (h_true T_0 T_2) (-. (Ex B, (g_true_only T_0 B))) ### Exists 117 % 0.18/0.49 119. (-. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C))))))) (-. (Ex B, (g_true_only T_0 B))) (h_true T_0 T_2) ### NotNot 118 % 0.18/0.49 120. (-. ((Ex B, ((Ex C, ((g_both T_0 B) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 B) \/ (h_true_only T_0 C)))))) /\ (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))))) (-. (Ex B, (g_true_only T_0 B))) (h_false T_0 T_2) (g_both T_0 T_1) (h_true T_0 T_2) (-. (Ex B, (h_true_only T_0 B))) (g_true T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 104 119 % 0.18/0.49 121. (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (h_true T_0 T_2) (g_both T_0 T_1) (h_false T_0 T_2) (-. (Ex B, (g_true_only T_0 B))) ### NotExists 120 % 0.18/0.49 122. (-. (h_true_only T_0 T_2)) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (g_true T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (h_true T_0 T_2) ### Extension/test/not_true_only_h 86 121 % 0.18/0.49 123. (h_true T_0 T_2) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) ### NotExists 122 % 0.18/0.49 124. (-. (h_false_only T_0 T_2)) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) (g_true T_0 T_1) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Extension/test/not_false_only_h 85 123 % 0.18/0.49 125. (-. (All B, (h_false_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_0 T_1) (g_both T_0 T_1) (-. (Ex B, (g_true_only T_0 B))) ### NotAllEx 124 % 0.18/0.49 126. (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B))))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (g_true_only T_0 B))) (g_both T_0 T_1) ### DisjTree 59 81 125 % 0.18/0.49 127. (-. ((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B))))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_0 T_1) (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B))))) ### NotAnd 126 24 % 0.18/0.49 128. (-. (((Ex B, (g_true_only T_0 B)) /\ (((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B)))) \/ (All B, (h_false_only T_0 B)))) \/ ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ (All B, (h_false_only T_0 B)))))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) ### NotOr 127 % 0.18/0.49 129. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_0 T_1) ### NotExists 128 % 0.18/0.49 130. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 27 129 76 % 0.18/0.49 131. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_0 T_1) ### All 130 % 0.18/0.49 132. (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 A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 131 % 0.18/0.49 133. (g_true_only T_7 T_8) (-. (g_true_only T_7 T_8)) ### Axiom % 0.18/0.49 134. (-. (Ex B, (g_true_only T_7 B))) (g_true_only T_7 T_8) ### NotExists 133 % 0.18/0.49 135. (h_both T_7 T_9) (-. (h_both T_7 T_9)) ### Axiom % 0.18/0.49 136. (-. (Ex B, (h_both T_7 B))) (h_both T_7 T_9) ### NotExists 135 % 0.18/0.49 137. (-. (h_false T_7 T_9)) (h_false T_7 T_9) ### Axiom % 0.18/0.49 138. (h_false_only T_7 T_9) (-. (h_false T_7 T_9)) ### Extension/test/false_only_h 137 % 0.18/0.49 139. ((h_both T_7 T_9) \/ (h_false_only T_7 T_9)) (-. (h_false T_7 T_9)) (-. (Ex B, (h_both T_7 B))) ### Or 136 138 % 0.18/0.49 140. ((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) (-. (Ex B, (h_both T_7 B))) (-. (h_false T_7 T_9)) ### And 139 % 0.18/0.49 141. ((g_both T_7 T_8) /\ (h_false_only T_7 T_9)) (-. (h_false T_7 T_9)) ### And 138 % 0.18/0.49 142. (((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 T_9))) (-. (h_false T_7 T_9)) (-. (Ex B, (h_both T_7 B))) ### Or 140 141 % 0.18/0.49 143. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (Ex B, (h_both T_7 B))) (-. (h_false T_7 T_9)) ### All 142 % 0.18/0.49 144. (-. (h_false T_7 T_10)) (h_false T_7 T_10) ### Axiom % 0.18/0.50 145. (h_both T_7 T_10) (-. (h_false T_7 T_10)) ### Extension/test/both_h 144 % 0.18/0.50 146. (h_true T_7 T_10) (-. (h_true T_7 T_10)) ### Axiom % 0.18/0.50 147. (h_false_only T_7 T_10) (h_true T_7 T_10) ### Extension/test/false_only_h 146 % 0.18/0.50 148. ((h_both T_7 T_10) \/ (h_false_only T_7 T_10)) (h_true T_7 T_10) (-. (h_false T_7 T_10)) ### Or 145 147 % 0.18/0.50 149. ((g_true_only T_7 T_8) /\ ((h_both T_7 T_10) \/ (h_false_only T_7 T_10))) (-. (h_false T_7 T_10)) (h_true T_7 T_10) ### And 148 % 0.18/0.50 150. ((g_both T_7 T_8) /\ (h_false_only T_7 T_10)) (h_true T_7 T_10) ### And 147 % 0.18/0.50 151. (((g_true_only T_7 T_8) /\ ((h_both T_7 T_10) \/ (h_false_only T_7 T_10))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 T_10))) (h_true T_7 T_10) (-. (h_false T_7 T_10)) ### Or 149 150 % 0.18/0.50 152. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (h_false T_7 T_10)) (h_true T_7 T_10) ### All 151 % 0.18/0.50 153. (h_true_only T_7 T_10) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### Extension/test/true_only_h 152 % 0.18/0.50 154. (Ex B, (h_true_only T_7 B)) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### Exists 153 % 0.18/0.50 155. (-. (-. (Ex B, (h_true_only T_7 B)))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotNot 154 % 0.18/0.50 156. (-. ((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B))))) (-. (h_false T_7 T_9)) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotAnd 143 155 % 0.18/0.50 157. (h_true T_7 T_9) (-. (h_true T_7 T_9)) ### Axiom % 0.18/0.50 158. (h_false_only T_7 T_9) (h_true T_7 T_9) ### Extension/test/false_only_h 157 % 0.18/0.50 159. ((h_both T_7 T_9) \/ (h_false_only T_7 T_9)) (h_true T_7 T_9) (-. (Ex B, (h_both T_7 B))) ### Or 136 158 % 0.18/0.50 160. ((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) (-. (Ex B, (h_both T_7 B))) (h_true T_7 T_9) ### And 159 % 0.18/0.50 161. ((g_both T_7 T_8) /\ (h_false_only T_7 T_9)) (h_true T_7 T_9) ### And 158 % 0.18/0.50 162. (((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 T_9))) (h_true T_7 T_9) (-. (Ex B, (h_both T_7 B))) ### Or 160 161 % 0.18/0.50 163. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (Ex B, (h_both T_7 B))) (h_true T_7 T_9) ### All 162 % 0.18/0.50 164. (-. ((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B))))) (h_true T_7 T_9) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotAnd 163 155 % 0.18/0.50 165. (-. (h_false_only T_7 T_9)) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. ((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B))))) ### Extension/test/not_false_only_h 156 164 % 0.18/0.50 166. (-. (All B, (h_false_only T_7 B))) (-. ((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B))))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotAllEx 165 % 0.18/0.50 167. (-. (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B)))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotOr 166 % 0.18/0.50 168. (-. ((Ex B, (g_true_only T_7 B)) /\ (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B))))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_true_only T_7 T_8) ### NotAnd 134 167 % 0.18/0.50 169. (-. (((Ex B, (g_true_only T_7 B)) /\ (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B)))) \/ ((Ex B, (g_both T_7 B)) /\ ((-. (Ex B, (g_true_only T_7 B))) /\ (All B, (h_false_only T_7 B)))))) (g_true_only T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotOr 168 % 0.18/0.50 170. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_true_only T_7 T_8) ### NotExists 169 % 0.18/0.50 171. ((g_true_only T_7 T_8) /\ ((h_both T_7 zenon_X11) \/ (h_false_only T_7 zenon_X11))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### And 170 % 0.18/0.50 172. (g_both T_7 T_8) (-. (g_both T_7 T_8)) ### Axiom % 0.18/0.50 173. (-. (Ex B, (g_both T_7 B))) (g_both T_7 T_8) ### NotExists 172 % 0.18/0.50 174. (-. (Ex B, (g_true_only T_7 B))) (Ex B, (g_true_only T_7 B)) ### Axiom % 0.18/0.50 175. (g_false T_7 T_8) (-. (g_false T_7 T_8)) ### Axiom % 0.18/0.50 176. (g_true_only T_7 T_8) (g_false T_7 T_8) ### Extension/test/true_only_g 175 % 0.18/0.50 177. ((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) (g_false T_7 T_8) ### And 176 % 0.18/0.50 178. (((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 T_9))) (-. (h_false T_7 T_9)) (g_false T_7 T_8) ### Or 177 141 % 0.18/0.50 179. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_false T_7 T_8) (-. (h_false T_7 T_9)) ### All 178 % 0.18/0.50 180. (((g_true_only T_7 T_8) /\ ((h_both T_7 T_9) \/ (h_false_only T_7 T_9))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 T_9))) (h_true T_7 T_9) (g_false T_7 T_8) ### Or 177 161 % 0.18/0.50 181. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_false T_7 T_8) (h_true T_7 T_9) ### All 180 % 0.18/0.50 182. (-. (h_false_only T_7 T_9)) (g_false T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### Extension/test/not_false_only_h 179 181 % 0.18/0.50 183. (-. (All B, (h_false_only T_7 B))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_false T_7 T_8) ### NotAllEx 182 % 0.18/0.50 184. (-. ((Ex B, (g_both T_7 B)) /\ ((-. (Ex B, (g_true_only T_7 B))) /\ (All B, (h_false_only T_7 B))))) (g_false T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (Ex B, (g_true_only T_7 B))) (g_both T_7 T_8) ### DisjTree 173 174 183 % 0.18/0.50 185. (-. (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B)))) (g_false T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### NotOr 183 % 0.18/0.50 186. (-. ((Ex B, (g_true_only T_7 B)) /\ (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B))))) (g_both T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_false T_7 T_8) (-. ((Ex B, (g_both T_7 B)) /\ ((-. (Ex B, (g_true_only T_7 B))) /\ (All B, (h_false_only T_7 B))))) ### NotAnd 184 185 % 0.18/0.50 187. (-. (((Ex B, (g_true_only T_7 B)) /\ (((Ex B, (h_both T_7 B)) /\ (-. (Ex B, (h_true_only T_7 B)))) \/ (All B, (h_false_only T_7 B)))) \/ ((Ex B, (g_both T_7 B)) /\ ((-. (Ex B, (g_true_only T_7 B))) /\ (All B, (h_false_only T_7 B)))))) (g_false T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_both T_7 T_8) ### NotOr 186 % 0.18/0.51 188. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (g_both T_7 T_8) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_false T_7 T_8) ### NotExists 187 % 0.18/0.51 189. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (g_both T_7 T_8) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### Extension/test/both_g 188 % 0.18/0.51 190. ((g_both T_7 T_8) /\ (h_false_only T_7 zenon_X11)) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### And 189 % 0.18/0.51 191. (((g_true_only T_7 T_8) /\ ((h_both T_7 zenon_X11) \/ (h_false_only T_7 zenon_X11))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 zenon_X11))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) ### Or 171 190 % 0.18/0.51 192. (All C, (((g_true_only T_7 T_8) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 T_8) /\ (h_false_only T_7 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 191 % 0.18/0.51 193. (Ex B, (All C, (((g_true_only T_7 B) /\ ((h_both T_7 C) \/ (h_false_only T_7 C))) \/ ((g_both T_7 B) /\ (h_false_only T_7 C))))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### Exists 192 % 0.18/0.51 194. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### Exists 193 % 0.18/0.51 195. (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_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))))) ### DisjTree 79 80 132 194 % 0.18/0.51 196. (g_true_only T_0 T_12) (-. (g_true_only T_0 T_12)) ### Axiom % 0.18/0.51 197. (h_true_only T_0 T_13) (-. (h_true_only T_0 T_13)) ### Axiom % 0.18/0.51 198. (-. (Ex B, (h_true_only T_0 B))) (h_true_only T_0 T_13) ### NotExists 197 % 0.18/0.51 199. (-. (h_false T_0 T_13)) (h_false T_0 T_13) ### Axiom % 0.18/0.51 200. (h_both T_0 T_13) (-. (h_false T_0 T_13)) ### Extension/test/both_h 199 % 0.18/0.51 201. (-. (h_false T_0 T_13)) (h_false T_0 T_13) ### Axiom % 0.18/0.51 202. (h_false_only T_0 T_13) (-. (h_false T_0 T_13)) ### Extension/test/false_only_h 201 % 0.18/0.51 203. ((h_true_only T_0 T_13) \/ ((h_both T_0 T_13) \/ (h_false_only T_0 T_13))) (-. (h_false T_0 T_13)) (-. (Ex B, (h_true_only T_0 B))) ### DisjTree 198 200 202 % 0.18/0.51 204. (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false T_0 T_13)) ### All 203 % 0.18/0.51 205. (-. (h_true T_0 T_13)) (h_true T_0 T_13) ### Axiom % 0.18/0.51 206. (-. (h_false_only T_0 T_13)) (-. (h_true T_0 T_13)) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### Extension/test/not_false_only_h 204 205 % 0.18/0.51 207. (-. (h_both T_0 T_13)) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false_only T_0 T_13)) ### Extension/test/not_both_h 206 204 % 0.18/0.51 208. (-. ((h_both T_0 T_13) \/ (h_false_only T_0 T_13))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotOr 207 % 0.18/0.51 209. (-. ((g_true_only T_0 T_12) /\ ((h_both T_0 T_13) \/ (h_false_only T_0 T_13)))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_12) ### NotAnd 196 208 % 0.18/0.51 210. (-. (((g_true_only T_0 T_12) /\ ((h_both T_0 T_13) \/ (h_false_only T_0 T_13))) \/ ((g_both T_0 T_12) /\ (h_false_only T_0 T_13)))) (g_true_only T_0 T_12) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotOr 209 % 0.18/0.51 211. (-. (All C, (((g_true_only T_0 T_12) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_12) /\ (h_false_only T_0 C))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_12) ### NotAllEx 210 % 0.18/0.51 212. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))) (g_true_only T_0 T_12) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotExists 211 % 0.18/0.51 213. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (g_true_only T_0 T_12) ### NotExists 212 % 0.18/0.51 214. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_0 T_12) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 213 % 0.18/0.51 215. (Ex B, (g_true_only T_0 B)) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Exists 214 % 0.18/0.51 216. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.18/0.51 217. (-. (Ex B, (h_both T_0 B))) (-. (h_false_only T_0 T_3)) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotExists 46 % 0.18/0.51 218. (-. ((g_both T_0 T_1) /\ (h_false_only T_0 T_3))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (h_both T_0 B))) (g_both T_0 T_1) ### NotAnd 216 217 % 0.18/0.51 219. (-. (((g_true_only T_0 T_1) /\ ((h_both T_0 T_3) \/ (h_false_only T_0 T_3))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 T_3)))) (g_both T_0 T_1) (-. (Ex B, (h_both T_0 B))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotOr 218 % 0.18/0.51 220. (-. (All C, (((g_true_only T_0 T_1) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 C))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (h_both T_0 B))) (g_both T_0 T_1) ### NotAllEx 219 % 0.18/0.51 221. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))) (g_both T_0 T_1) (-. (Ex B, (h_both T_0 B))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) ### NotExists 220 % 0.18/0.51 222. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex B, (h_both T_0 B))) (g_both T_0 T_1) ### NotExists 221 % 0.18/0.51 223. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) (-. (Ex B, (h_both T_0 B))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 222 % 0.18/0.51 224. (-. (Ex B, (h_true_only T_0 B))) (Ex B, (h_true_only T_0 B)) ### Axiom % 0.18/0.51 225. (-. ((Ex B, (g_both T_0 B)) /\ ((-. (Ex B, (g_true_only T_0 B))) /\ ((Ex B, (h_both T_0 B)) /\ (-. (Ex B, (h_true_only T_0 B))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (g_both T_0 T_1) ### DisjTree 59 215 223 224 % 0.18/0.51 226. (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_0 T_1) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotExists 225 % 0.18/0.51 227. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 53 226 76 % 0.18/0.51 228. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_true T_0 T_1) ### All 227 % 0.18/0.51 229. (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 A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 228 % 0.18/0.51 230. (g_true_only T_14 T_15) (-. (g_true_only T_14 T_15)) ### Axiom % 0.18/0.51 231. (h_true_only T_14 T_16) (-. (h_true_only T_14 T_16)) ### Axiom % 0.18/0.51 232. (-. (Ex B, (h_true_only T_14 B))) (h_true_only T_14 T_16) ### NotExists 231 % 0.18/0.51 233. (-. (h_false T_14 T_16)) (h_false T_14 T_16) ### Axiom % 0.18/0.51 234. (h_both T_14 T_16) (-. (h_false T_14 T_16)) ### Extension/test/both_h 233 % 0.18/0.51 235. (-. (h_false T_14 T_16)) (h_false T_14 T_16) ### Axiom % 0.18/0.51 236. (h_false_only T_14 T_16) (-. (h_false T_14 T_16)) ### Extension/test/false_only_h 235 % 0.18/0.51 237. ((h_true_only T_14 T_16) \/ ((h_both T_14 T_16) \/ (h_false_only T_14 T_16))) (-. (h_false T_14 T_16)) (-. (Ex B, (h_true_only T_14 B))) ### DisjTree 232 234 236 % 0.18/0.51 238. (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) (-. (Ex B, (h_true_only T_14 B))) (-. (h_false T_14 T_16)) ### All 237 % 0.18/0.51 239. (-. (h_true T_14 T_16)) (h_true T_14 T_16) ### Axiom % 0.18/0.51 240. (-. (h_false_only T_14 T_16)) (-. (h_true T_14 T_16)) (-. (Ex B, (h_true_only T_14 B))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) ### Extension/test/not_false_only_h 238 239 % 0.18/0.51 241. (-. (h_both T_14 T_16)) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) (-. (Ex B, (h_true_only T_14 B))) (-. (h_false_only T_14 T_16)) ### Extension/test/not_both_h 240 238 % 0.18/0.51 242. (-. ((h_both T_14 T_16) \/ (h_false_only T_14 T_16))) (-. (Ex B, (h_true_only T_14 B))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) ### NotOr 241 % 0.18/0.51 243. (-. ((g_true_only T_14 T_15) /\ ((h_both T_14 T_16) \/ (h_false_only T_14 T_16)))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) (-. (Ex B, (h_true_only T_14 B))) (g_true_only T_14 T_15) ### NotAnd 230 242 % 0.18/0.51 244. (-. (((g_true_only T_14 T_15) /\ ((h_both T_14 T_16) \/ (h_false_only T_14 T_16))) \/ ((g_both T_14 T_15) /\ (h_false_only T_14 T_16)))) (g_true_only T_14 T_15) (-. (Ex B, (h_true_only T_14 B))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) ### NotOr 243 % 0.18/0.51 245. (-. (All C, (((g_true_only T_14 T_15) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 T_15) /\ (h_false_only T_14 C))))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) (-. (Ex B, (h_true_only T_14 B))) (g_true_only T_14 T_15) ### NotAllEx 244 % 0.18/0.51 246. (-. (Ex B, (All C, (((g_true_only T_14 B) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 B) /\ (h_false_only T_14 C)))))) (g_true_only T_14 T_15) (-. (Ex B, (h_true_only T_14 B))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) ### NotExists 245 % 0.18/0.51 247. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_14 X_1) \/ ((h_both T_14 X_1) \/ (h_false_only T_14 X_1)))) (-. (Ex B, (h_true_only T_14 B))) (g_true_only T_14 T_15) ### NotExists 246 % 0.18/0.51 248. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_14 T_15) (-. (Ex B, (h_true_only T_14 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 247 % 0.18/0.51 249. ((Ex B, (h_both T_14 B)) /\ (-. (Ex B, (h_true_only T_14 B)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (g_true_only T_14 T_15) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### And 248 % 0.18/0.51 250. (g_true_only T_14 T_15) (-. (g_true_only T_14 T_15)) ### Axiom % 0.18/0.51 251. (All B, (h_false_only T_14 B)) (-. (h_false T_14 T_16)) ### All 236 % 0.18/0.51 252. (-. (h_true T_14 T_16)) (h_true T_14 T_16) ### Axiom % 0.18/0.51 253. (-. (h_false_only T_14 T_16)) (-. (h_true T_14 T_16)) (All B, (h_false_only T_14 B)) ### Extension/test/not_false_only_h 251 252 % 0.18/0.51 254. (-. (h_both T_14 T_16)) (All B, (h_false_only T_14 B)) (-. (h_false_only T_14 T_16)) ### Extension/test/not_both_h 253 251 % 0.18/0.52 255. (-. ((h_both T_14 T_16) \/ (h_false_only T_14 T_16))) (All B, (h_false_only T_14 B)) ### NotOr 254 % 0.18/0.52 256. (-. ((g_true_only T_14 T_15) /\ ((h_both T_14 T_16) \/ (h_false_only T_14 T_16)))) (All B, (h_false_only T_14 B)) (g_true_only T_14 T_15) ### NotAnd 250 255 % 0.18/0.52 257. (-. (((g_true_only T_14 T_15) /\ ((h_both T_14 T_16) \/ (h_false_only T_14 T_16))) \/ ((g_both T_14 T_15) /\ (h_false_only T_14 T_16)))) (g_true_only T_14 T_15) (All B, (h_false_only T_14 B)) ### NotOr 256 % 0.18/0.52 258. (-. (All C, (((g_true_only T_14 T_15) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 T_15) /\ (h_false_only T_14 C))))) (All B, (h_false_only T_14 B)) (g_true_only T_14 T_15) ### NotAllEx 257 % 0.18/0.52 259. (-. (Ex B, (All C, (((g_true_only T_14 B) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 B) /\ (h_false_only T_14 C)))))) (g_true_only T_14 T_15) (All B, (h_false_only T_14 B)) ### NotExists 258 % 0.18/0.52 260. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All B, (h_false_only T_14 B)) (g_true_only T_14 T_15) ### NotExists 259 % 0.18/0.52 261. (((Ex B, (h_both T_14 B)) /\ (-. (Ex B, (h_true_only T_14 B)))) \/ (All B, (h_false_only T_14 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_14 T_15) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### Or 249 260 % 0.18/0.52 262. (Ex B, (g_true_only T_14 B)) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (((Ex B, (h_both T_14 B)) /\ (-. (Ex B, (h_true_only T_14 B)))) \/ (All B, (h_false_only T_14 B))) ### Exists 261 % 0.18/0.52 263. ((Ex B, (g_true_only T_14 B)) /\ (((Ex B, (h_both T_14 B)) /\ (-. (Ex B, (h_true_only T_14 B)))) \/ (All B, (h_false_only T_14 B)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### And 262 % 0.18/0.52 264. (g_both T_14 T_17) (-. (g_both T_14 T_17)) ### Axiom % 0.18/0.52 265. (-. (h_false T_14 T_18)) (h_false T_14 T_18) ### Axiom % 0.18/0.52 266. (h_false_only T_14 T_18) (-. (h_false T_14 T_18)) ### Extension/test/false_only_h 265 % 0.18/0.52 267. (All B, (h_false_only T_14 B)) (-. (h_false T_14 T_18)) ### All 266 % 0.18/0.52 268. (h_true T_14 T_18) (-. (h_true T_14 T_18)) ### Axiom % 0.18/0.52 269. (h_false_only T_14 T_18) (h_true T_14 T_18) ### Extension/test/false_only_h 268 % 0.18/0.52 270. (All B, (h_false_only T_14 B)) (h_true T_14 T_18) ### All 269 % 0.18/0.52 271. (-. (h_false_only T_14 T_18)) (All B, (h_false_only T_14 B)) ### Extension/test/not_false_only_h 267 270 % 0.18/0.52 272. (-. ((g_both T_14 T_17) /\ (h_false_only T_14 T_18))) (All B, (h_false_only T_14 B)) (g_both T_14 T_17) ### NotAnd 264 271 % 0.18/0.52 273. (-. (((g_true_only T_14 T_17) /\ ((h_both T_14 T_18) \/ (h_false_only T_14 T_18))) \/ ((g_both T_14 T_17) /\ (h_false_only T_14 T_18)))) (g_both T_14 T_17) (All B, (h_false_only T_14 B)) ### NotOr 272 % 0.18/0.52 274. (-. (All C, (((g_true_only T_14 T_17) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 T_17) /\ (h_false_only T_14 C))))) (All B, (h_false_only T_14 B)) (g_both T_14 T_17) ### NotAllEx 273 % 0.18/0.52 275. (-. (Ex B, (All C, (((g_true_only T_14 B) /\ ((h_both T_14 C) \/ (h_false_only T_14 C))) \/ ((g_both T_14 B) /\ (h_false_only T_14 C)))))) (g_both T_14 T_17) (All B, (h_false_only T_14 B)) ### NotExists 274 % 0.18/0.52 276. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All B, (h_false_only T_14 B)) (g_both T_14 T_17) ### NotExists 275 % 0.18/0.52 277. (Ex B, (g_both T_14 B)) (All B, (h_false_only T_14 B)) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### Exists 276 % 0.18/0.52 278. ((Ex B, (g_both T_14 B)) /\ ((-. (Ex B, (g_true_only T_14 B))) /\ (All B, (h_false_only T_14 B)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### ConjTree 277 % 0.18/0.52 279. (((Ex B, (g_true_only T_14 B)) /\ (((Ex B, (h_both T_14 B)) /\ (-. (Ex B, (h_true_only T_14 B)))) \/ (All B, (h_false_only T_14 B)))) \/ ((Ex B, (g_both T_14 B)) /\ ((-. (Ex B, (g_true_only T_14 B))) /\ (All B, (h_false_only T_14 B))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Or 263 278 % 0.18/0.52 280. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### Exists 279 % 0.18/0.52 281. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.18/0.52 282. (g_both T_0 T_1) (-. (g_both T_0 T_1)) ### Axiom % 0.18/0.52 283. (-. ((g_both T_0 T_1) /\ (h_both T_0 T_3))) (-. (h_false_only T_0 T_3)) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (g_both T_0 T_1) ### NotAnd 282 46 % 0.18/0.52 284. (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) (-. (h_false_only T_0 T_3)) ### NotExists 283 % 0.18/0.52 285. (-. ((g_both T_0 T_1) /\ (h_false_only T_0 T_3))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) ### NotAnd 281 284 % 0.18/0.52 286. (-. (((g_true_only T_0 T_1) /\ ((h_both T_0 T_3) \/ (h_false_only T_0 T_3))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 T_3)))) (g_both T_0 T_1) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) ### NotOr 285 % 0.18/0.52 287. (-. (All C, (((g_true_only T_0 T_1) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 T_1) /\ (h_false_only T_0 C))))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) ### NotAllEx 286 % 0.18/0.52 288. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))) (g_both T_0 T_1) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex B, (h_true_only T_0 B))) ### NotExists 287 % 0.18/0.52 289. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_1, ((h_true_only T_0 X_1) \/ ((h_both T_0 X_1) \/ (h_false_only T_0 X_1)))) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (g_both T_0 T_1) ### NotExists 288 % 0.18/0.52 290. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) (-. (Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C)))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 289 % 0.18/0.52 291. (-. ((Ex C, ((g_both T_0 T_1) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 T_1) \/ (h_true_only T_0 C)))))) (g_true T_0 T_1) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 290 101 % 0.18/0.52 292. (-. (Ex B, ((Ex C, ((g_both T_0 B) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 B) \/ (h_true_only T_0 C))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (g_true T_0 T_1) ### NotExists 291 % 0.18/0.52 293. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C))))) (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))) ### Axiom % 0.18/0.52 294. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C))))) ### NotExists 293 % 0.18/0.52 295. (-. (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### NotNot 294 % 0.18/0.52 296. (-. ((Ex B, ((Ex C, ((g_both T_0 B) /\ (h_both T_0 C))) /\ (-. (Ex C, ((g_false_only T_0 B) \/ (h_true_only T_0 C)))))) /\ (-. (Ex B, (All C, (((g_true_only T_0 B) /\ ((h_both T_0 C) \/ (h_false_only T_0 C))) \/ ((g_both T_0 B) /\ (h_false_only T_0 C)))))))) (g_true T_0 T_1) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (g_both T_0 T_1) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 292 295 % 0.18/0.52 297. (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_0 T_1) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (g_true T_0 T_1) ### NotExists 296 % 0.18/0.52 298. ((g_true_only T_0 T_1) \/ ((g_both T_0 T_1) \/ (g_false_only T_0 T_1))) (g_true T_0 T_1) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 53 297 76 % 0.18/0.52 299. (All X_1, ((g_true_only T_0 X_1) \/ ((g_both T_0 X_1) \/ (g_false_only T_0 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_0 T_1) ### All 298 % 0.18/0.52 300. (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 A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 299 % 0.18/0.52 301. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))) ### Axiom % 0.18/0.52 302. (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (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))))) ### DisjTree 229 280 300 301 % 0.18/0.52 303. (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (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) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) ### NotAnd 195 302 % 0.18/0.52 304. (-. (g_false_only T_0 T_1)) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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 X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (h_true_only T_0 B))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) ### Extension/test/not_false_only_g 57 303 % 0.18/0.53 305. (-. (All B, (g_false_only T_0 B))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (-. (Ex B, (h_true_only T_0 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) ### NotAllEx 304 % 0.18/0.53 306. (-. ((All B, (g_false_only T_0 B)) \/ (Ex B, (h_true_only T_0 B)))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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 X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) ### NotOr 305 % 0.18/0.53 307. (-. (All A, ((All B, (g_false_only A B)) \/ (Ex B, (h_true_only A B))))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) ### NotAllEx 306 % 0.18/0.53 308. (g_true_only T_19 T_20) (-. (g_true_only T_19 T_20)) ### Axiom % 0.18/0.53 309. (-. (Ex B, (g_true_only T_19 B))) (g_true_only T_19 T_20) ### NotExists 308 % 0.18/0.53 310. (h_true T_19 T_21) (-. (h_true T_19 T_21)) ### Axiom % 0.18/0.53 311. (h_true T_19 T_21) (-. (h_true T_19 T_21)) ### Axiom % 0.18/0.53 312. (-. (h_false T_19 T_21)) (h_false T_19 T_21) ### Axiom % 0.18/0.53 313. (-. (h_true_only T_19 T_21)) (-. (h_false T_19 T_21)) (h_true T_19 T_21) ### Extension/test/not_true_only_h 311 312 % 0.18/0.53 314. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 T_21))) (h_true T_19 T_21) (-. (h_false T_19 T_21)) ### NotOr 313 % 0.18/0.53 315. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_21)) (h_true T_19 T_21) ### NotExists 314 % 0.18/0.53 316. (-. (h_both T_19 T_21)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) ### Extension/test/not_both_h 310 315 % 0.18/0.53 317. (-. (Ex B, (h_both T_19 B))) (h_true T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotExists 316 % 0.18/0.53 318. (h_true_only T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (h_both T_19 B))) ### Extension/test/true_only_h 317 % 0.18/0.53 319. (-. (h_false T_19 T_21)) (h_false T_19 T_21) ### Axiom % 0.18/0.53 320. (h_both T_19 T_21) (-. (h_false T_19 T_21)) ### Extension/test/both_h 319 % 0.18/0.53 321. (-. (h_false T_19 T_21)) (h_false T_19 T_21) ### Axiom % 0.18/0.53 322. (h_false_only T_19 T_21) (-. (h_false T_19 T_21)) ### Extension/test/false_only_h 321 % 0.18/0.53 323. ((h_true_only T_19 T_21) \/ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) (-. (h_false T_19 T_21)) (-. (Ex B, (h_both T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### DisjTree 318 320 322 % 0.18/0.53 324. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (h_both T_19 B))) (-. (h_false T_19 T_21)) ### All 323 % 0.18/0.53 325. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (h_false T_19 T_21)) (-. (Ex B, (h_both T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### All 324 % 0.18/0.53 326. (h_true_only T_19 T_22) (-. (h_true_only T_19 T_22)) ### Axiom % 0.18/0.53 327. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 T_22))) (h_true_only T_19 T_22) ### NotOr 326 % 0.18/0.53 328. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true_only T_19 T_22) ### NotExists 327 % 0.18/0.53 329. (Ex B, (h_true_only T_19 B)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### Exists 328 % 0.18/0.53 330. (-. (-. (Ex B, (h_true_only T_19 B)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotNot 329 % 0.18/0.53 331. (-. ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_21)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 325 330 % 0.18/0.53 332. (-. ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) ### NotAnd 317 330 % 0.18/0.53 333. (-. (h_false_only T_19 T_21)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))) ### Extension/test/not_false_only_h 331 332 % 0.18/0.53 334. (-. (All B, (h_false_only T_19 B))) (-. ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAllEx 333 % 0.18/0.53 335. (-. (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotOr 334 % 0.18/0.53 336. (-. ((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_19 T_20) ### NotAnd 309 335 % 0.18/0.53 337. (-. (((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B)))) \/ ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B)))))) (g_true_only T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotOr 336 % 0.18/0.53 338. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_19 T_20) ### NotExists 337 % 0.18/0.53 339. (g_both T_19 T_20) (-. (g_both T_19 T_20)) ### Axiom % 0.18/0.53 340. (-. (Ex B, (g_both T_19 B))) (g_both T_19 T_20) ### NotExists 339 % 0.18/0.53 341. (-. (Ex B, (g_true_only T_19 B))) (Ex B, (g_true_only T_19 B)) ### Axiom % 0.18/0.53 342. (-. (Ex B, (g_true_only T_19 B))) (Ex B, (g_true_only T_19 B)) ### Axiom % 0.18/0.53 343. (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) ### DisjTree 340 342 317 329 % 0.18/0.53 344. (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) (h_true T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotExists 343 % 0.18/0.53 345. (h_true_only T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) ### Extension/test/true_only_h 344 % 0.18/0.53 346. ((h_true_only T_19 T_21) \/ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) (-. (h_false T_19 T_21)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### DisjTree 345 320 322 % 0.18/0.53 347. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (h_false T_19 T_21)) ### All 346 % 0.18/0.53 348. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (h_false T_19 T_21)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### All 347 % 0.18/0.53 349. (-. (h_false_only T_19 T_21)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Extension/test/not_false_only_h 348 344 % 0.18/0.53 350. (-. (All B, (h_false_only T_19 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotAllEx 349 % 0.18/0.53 351. (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) ### DisjTree 340 341 350 % 0.18/0.53 352. (-. ((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B))))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B))))) ### NotAnd 351 335 % 0.18/0.53 353. (-. (((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B)))) \/ ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B)))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) ### NotOr 352 % 0.18/0.53 354. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotExists 353 % 0.18/0.53 355. (-. (g_false T_19 T_20)) (g_false T_19 T_20) ### Axiom % 0.18/0.53 356. (g_false_only T_19 T_20) (-. (g_false T_19 T_20)) ### Extension/test/false_only_g 355 % 0.18/0.53 357. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (-. (g_false T_19 T_20)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 338 354 356 % 0.18/0.53 358. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (g_false T_19 T_20)) ### All 357 % 0.18/0.53 359. (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_19 T_20)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 358 % 0.18/0.53 360. (g_true T_19 T_20) (-. (g_true T_19 T_20)) ### Axiom % 0.18/0.53 361. (g_false_only T_19 T_20) (g_true T_19 T_20) ### Extension/test/false_only_g 360 % 0.18/0.53 362. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (g_true T_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 338 354 361 % 0.18/0.53 363. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_true T_19 T_20) ### All 362 % 0.18/0.53 364. (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_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 363 % 0.18/0.53 365. (-. (g_false_only T_19 T_20)) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### Extension/test/not_false_only_g 359 364 % 0.18/0.53 366. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 zenon_X23))) (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 A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### NotOr 365 % 0.18/0.53 367. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### NotExists 366 % 0.18/0.53 368. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) ### Axiom % 0.18/0.53 369. (-. (Ex B, (g_true_only T_19 B))) (Ex B, (g_true_only T_19 B)) ### Axiom % 0.18/0.53 370. (h_true_only T_19 T_21) (-. (h_false T_19 T_21)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### Extension/test/true_only_h 315 % 0.18/0.53 371. ((h_true_only T_19 T_21) \/ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_21)) ### DisjTree 370 320 322 % 0.18/0.53 372. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (h_false T_19 T_21)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### All 371 % 0.18/0.53 373. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_21)) ### All 372 % 0.18/0.53 374. (h_true T_19 T_21) (-. (h_true T_19 T_21)) ### Axiom % 0.18/0.53 375. (h_false T_19 T_21) (-. (h_false T_19 T_21)) ### Axiom % 0.18/0.53 376. (h_true_only T_19 T_21) (h_false T_19 T_21) ### Extension/test/true_only_h 375 % 0.18/0.53 377. (g_both T_19 T_20) (-. (g_both T_19 T_20)) ### Axiom % 0.18/0.53 378. (h_both T_19 T_21) (-. (h_both T_19 T_21)) ### Axiom % 0.18/0.53 379. (-. ((g_both T_19 T_20) /\ (h_both T_19 T_21))) (h_both T_19 T_21) (g_both T_19 T_20) ### NotAnd 377 378 % 0.18/0.53 380. (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) (h_both T_19 T_21) ### NotExists 379 % 0.18/0.53 381. (h_true T_19 T_21) (-. (h_true T_19 T_21)) ### Axiom % 0.18/0.53 382. (h_false_only T_19 T_21) (h_true T_19 T_21) ### Extension/test/false_only_h 381 % 0.18/0.53 383. ((h_true_only T_19 T_21) \/ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) (h_true T_19 T_21) (g_both T_19 T_20) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (h_false T_19 T_21) ### DisjTree 376 380 382 % 0.18/0.54 384. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (h_false T_19 T_21) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) (h_true T_19 T_21) ### All 383 % 0.18/0.54 385. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C))) ### Axiom % 0.18/0.54 386. (-. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotNot 385 % 0.18/0.54 387. (-. ((Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) (g_both T_19 T_20) (h_false T_19 T_21) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotAnd 384 386 % 0.18/0.54 388. (-. (Ex B, ((Ex C, ((g_both T_19 B) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C))))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (h_false T_19 T_21) (g_both T_19 T_20) (h_true T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotExists 387 % 0.18/0.54 389. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) (g_both T_19 T_20) (h_false T_19 T_21) (-. (Ex B, ((Ex C, ((g_both T_19 B) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C))))))) ### All 388 % 0.18/0.54 390. (g_true_only T_19 T_24) (-. (g_true_only T_19 T_24)) ### Axiom % 0.18/0.54 391. (-. (Ex B, (g_true_only T_19 B))) (g_true_only T_19 T_24) ### NotExists 390 % 0.18/0.54 392. ((g_true_only T_19 T_24) /\ ((h_both T_19 zenon_X25) \/ (h_false_only T_19 zenon_X25))) (-. (Ex B, (g_true_only T_19 B))) ### And 391 % 0.18/0.54 393. (g_false T_19 T_24) (-. (g_false T_19 T_24)) ### Axiom % 0.18/0.54 394. (g_true_only T_19 T_24) (g_false T_19 T_24) ### Extension/test/true_only_g 393 % 0.18/0.54 395. ((g_true_only T_19 T_24) /\ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) (g_false T_19 T_24) ### And 394 % 0.18/0.54 396. ((g_both T_19 T_24) /\ (h_false_only T_19 T_21)) (h_true T_19 T_21) ### And 382 % 0.18/0.54 397. (((g_true_only T_19 T_24) /\ ((h_both T_19 T_21) \/ (h_false_only T_19 T_21))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 T_21))) (h_true T_19 T_21) (g_false T_19 T_24) ### Or 395 396 % 0.18/0.54 398. (All C, (((g_true_only T_19 T_24) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 C)))) (g_false T_19 T_24) (h_true T_19 T_21) ### All 397 % 0.18/0.54 399. (g_both T_19 T_24) (h_true T_19 T_21) (All C, (((g_true_only T_19 T_24) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 C)))) ### Extension/test/both_g 398 % 0.18/0.54 400. ((g_both T_19 T_24) /\ (h_false_only T_19 zenon_X25)) (All C, (((g_true_only T_19 T_24) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 C)))) (h_true T_19 T_21) ### And 399 % 0.18/0.54 401. (((g_true_only T_19 T_24) /\ ((h_both T_19 zenon_X25) \/ (h_false_only T_19 zenon_X25))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 zenon_X25))) (h_true T_19 T_21) (All C, (((g_true_only T_19 T_24) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 C)))) (-. (Ex B, (g_true_only T_19 B))) ### Or 392 400 % 0.18/0.54 402. (-. (Ex B, (g_true_only T_19 B))) (All C, (((g_true_only T_19 T_24) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_24) /\ (h_false_only T_19 C)))) (h_true T_19 T_21) ### All 401 % 0.18/0.54 403. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C))))) (h_true T_19 T_21) (-. (Ex B, (g_true_only T_19 B))) ### Exists 402 % 0.18/0.54 404. (-. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C))))))) (-. (Ex B, (g_true_only T_19 B))) (h_true T_19 T_21) ### NotNot 403 % 0.18/0.54 405. (-. ((Ex B, ((Ex C, ((g_both T_19 B) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C)))))) /\ (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))))) (-. (Ex B, (g_true_only T_19 B))) (h_false T_19 T_21) (g_both T_19 T_20) (h_true T_19 T_21) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 389 404 % 0.18/0.54 406. (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true T_19 T_21) (g_both T_19 T_20) (h_false T_19 T_21) (-. (Ex B, (g_true_only T_19 B))) ### NotExists 405 % 0.18/0.54 407. (-. (h_true_only T_19 T_21)) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (h_true T_19 T_21) ### Extension/test/not_true_only_h 374 406 % 0.18/0.54 408. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 T_21))) (h_true T_19 T_21) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) ### NotOr 407 % 0.18/0.54 409. (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (h_true T_19 T_21) ### NotExists 408 % 0.18/0.54 410. (-. (h_false_only T_19 T_21)) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_both T_19 T_20) (-. (Ex B, (g_true_only T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Extension/test/not_false_only_h 373 409 % 0.18/0.54 411. (-. (All B, (h_false_only T_19 B))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) ### NotAllEx 410 % 0.18/0.54 412. (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex B, (g_true_only T_19 B))) (g_both T_19 T_20) ### DisjTree 340 369 411 % 0.18/0.54 413. (-. ((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B))))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B))))) ### NotAnd 412 335 % 0.18/0.54 414. (-. (((Ex B, (g_true_only T_19 B)) /\ (((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B)))) \/ (All B, (h_false_only T_19 B)))) \/ ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ (All B, (h_false_only T_19 B)))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) ### NotOr 413 % 0.18/0.54 415. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) ### NotExists 414 % 0.18/0.54 416. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (-. (g_false T_19 T_20)) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 338 415 356 % 0.18/0.54 417. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (g_false T_19 T_20)) ### All 416 % 0.18/0.54 418. (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_19 T_20)) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 417 % 0.18/0.54 419. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (g_true T_19 T_20) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 338 415 361 % 0.18/0.54 420. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_19 T_20) ### All 419 % 0.18/0.54 421. (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_19 T_20) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### All 420 % 0.18/0.54 422. (-. (g_false_only T_19 T_20)) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (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 418 421 % 0.18/0.54 423. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 zenon_X23))) (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, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### NotOr 422 % 0.18/0.54 424. (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (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 423 % 0.18/0.55 425. (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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 X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) ### DisjTree 367 368 424 194 % 0.18/0.55 426. (g_true_only T_19 T_20) (-. (g_true_only T_19 T_20)) ### Axiom % 0.18/0.55 427. (h_true_only T_19 T_26) (-. (h_true_only T_19 T_26)) ### Axiom % 0.18/0.55 428. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 T_26))) (h_true_only T_19 T_26) ### NotOr 427 % 0.18/0.55 429. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true_only T_19 T_26) ### NotExists 428 % 0.18/0.55 430. (-. (h_false T_19 T_26)) (h_false T_19 T_26) ### Axiom % 0.18/0.55 431. (h_both T_19 T_26) (-. (h_false T_19 T_26)) ### Extension/test/both_h 430 % 0.18/0.55 432. (-. (h_false T_19 T_26)) (h_false T_19 T_26) ### Axiom % 0.18/0.55 433. (h_false_only T_19 T_26) (-. (h_false T_19 T_26)) ### Extension/test/false_only_h 432 % 0.18/0.55 434. ((h_true_only T_19 T_26) \/ ((h_both T_19 T_26) \/ (h_false_only T_19 T_26))) (-. (h_false T_19 T_26)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### DisjTree 429 431 433 % 0.18/0.55 435. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_26)) ### All 434 % 0.18/0.55 436. (-. (h_true T_19 T_26)) (h_true T_19 T_26) ### Axiom % 0.18/0.55 437. (-. (h_false_only T_19 T_26)) (-. (h_true T_19 T_26)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### Extension/test/not_false_only_h 435 436 % 0.18/0.55 438. (-. (h_both T_19 T_26)) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false_only T_19 T_26)) ### Extension/test/not_both_h 437 435 % 0.18/0.55 439. (-. ((h_both T_19 T_26) \/ (h_false_only T_19 T_26))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotOr 438 % 0.18/0.55 440. (-. ((g_true_only T_19 T_20) /\ ((h_both T_19 T_26) \/ (h_false_only T_19 T_26)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_20) ### NotAnd 426 439 % 0.18/0.55 441. (-. (((g_true_only T_19 T_20) /\ ((h_both T_19 T_26) \/ (h_false_only T_19 T_26))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 T_26)))) (g_true_only T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotOr 440 % 0.18/0.55 442. (-. (All C, (((g_true_only T_19 T_20) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 C))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_20) ### NotAllEx 441 % 0.18/0.55 443. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))) (g_true_only T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotExists 442 % 0.18/0.55 444. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_20) ### NotExists 443 % 0.18/0.55 445. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 444 % 0.18/0.55 446. (g_true_only T_19 T_27) (-. (g_true_only T_19 T_27)) ### Axiom % 0.18/0.55 447. (h_true_only T_19 T_28) (-. (h_true_only T_19 T_28)) ### Axiom % 0.18/0.55 448. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 T_28))) (h_true_only T_19 T_28) ### NotOr 447 % 0.18/0.55 449. (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (h_true_only T_19 T_28) ### NotExists 448 % 0.18/0.55 450. (-. (h_false T_19 T_28)) (h_false T_19 T_28) ### Axiom % 0.18/0.55 451. (h_both T_19 T_28) (-. (h_false T_19 T_28)) ### Extension/test/both_h 450 % 0.18/0.55 452. (-. (h_false T_19 T_28)) (h_false T_19 T_28) ### Axiom % 0.18/0.55 453. (h_false_only T_19 T_28) (-. (h_false T_19 T_28)) ### Extension/test/false_only_h 452 % 0.18/0.55 454. ((h_true_only T_19 T_28) \/ ((h_both T_19 T_28) \/ (h_false_only T_19 T_28))) (-. (h_false T_19 T_28)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### DisjTree 449 451 453 % 0.18/0.55 455. (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false T_19 T_28)) ### All 454 % 0.18/0.55 456. (-. (h_true T_19 T_28)) (h_true T_19 T_28) ### Axiom % 0.18/0.55 457. (-. (h_false_only T_19 T_28)) (-. (h_true T_19 T_28)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### Extension/test/not_false_only_h 455 456 % 0.18/0.55 458. (-. (h_both T_19 T_28)) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false_only T_19 T_28)) ### Extension/test/not_both_h 457 455 % 0.18/0.55 459. (-. ((h_both T_19 T_28) \/ (h_false_only T_19 T_28))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotOr 458 % 0.18/0.55 460. (-. ((g_true_only T_19 T_27) /\ ((h_both T_19 T_28) \/ (h_false_only T_19 T_28)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_27) ### NotAnd 446 459 % 0.18/0.55 461. (-. (((g_true_only T_19 T_27) /\ ((h_both T_19 T_28) \/ (h_false_only T_19 T_28))) \/ ((g_both T_19 T_27) /\ (h_false_only T_19 T_28)))) (g_true_only T_19 T_27) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotOr 460 % 0.18/0.55 462. (-. (All C, (((g_true_only T_19 T_27) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_27) /\ (h_false_only T_19 C))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_27) ### NotAllEx 461 % 0.18/0.55 463. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))) (g_true_only T_19 T_27) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotExists 462 % 0.18/0.56 464. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_true_only T_19 T_27) ### NotExists 463 % 0.18/0.56 465. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_true_only T_19 T_27) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 464 % 0.18/0.56 466. (Ex B, (g_true_only T_19 B)) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### Exists 465 % 0.18/0.56 467. (g_both T_19 T_20) (-. (g_both T_19 T_20)) ### Axiom % 0.18/0.56 468. (-. (Ex B, (h_both T_19 B))) (-. (h_false_only T_19 T_26)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotExists 438 % 0.18/0.56 469. (-. ((g_both T_19 T_20) /\ (h_false_only T_19 T_26))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (h_both T_19 B))) (g_both T_19 T_20) ### NotAnd 467 468 % 0.18/0.56 470. (-. (((g_true_only T_19 T_20) /\ ((h_both T_19 T_26) \/ (h_false_only T_19 T_26))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 T_26)))) (g_both T_19 T_20) (-. (Ex B, (h_both T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotOr 469 % 0.18/0.56 471. (-. (All C, (((g_true_only T_19 T_20) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 C))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (h_both T_19 B))) (g_both T_19 T_20) ### NotAllEx 470 % 0.18/0.56 472. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))) (g_both T_19 T_20) (-. (Ex B, (h_both T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) ### NotExists 471 % 0.18/0.56 473. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex B, (h_both T_19 B))) (g_both T_19 T_20) ### NotExists 472 % 0.18/0.56 474. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) (-. (Ex B, (h_both T_19 B))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 473 % 0.18/0.56 475. (-. ((Ex B, (g_both T_19 B)) /\ ((-. (Ex B, (g_true_only T_19 B))) /\ ((Ex B, (h_both T_19 B)) /\ (-. (Ex B, (h_true_only T_19 B))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (g_both T_19 T_20) ### DisjTree 340 466 474 329 % 0.18/0.56 476. (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_both T_19 T_20) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotExists 475 % 0.18/0.56 477. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (-. (g_false T_19 T_20)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 445 476 356 % 0.18/0.56 478. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (g_false T_19 T_20)) ### All 477 % 0.18/0.56 479. (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_19 T_20)) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 478 % 0.18/0.56 480. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (g_true T_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 445 476 361 % 0.18/0.56 481. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (g_true T_19 T_20) ### All 480 % 0.18/0.56 482. (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_19 T_20) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 481 % 0.18/0.56 483. (-. (g_false_only T_19 T_20)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### Extension/test/not_false_only_g 479 482 % 0.18/0.56 484. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 zenon_X23))) (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 A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotOr 483 % 0.18/0.56 485. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) ### NotExists 484 % 0.18/0.56 486. (g_both T_19 T_20) (-. (g_both T_19 T_20)) ### Axiom % 0.18/0.56 487. (g_both T_19 T_20) (-. (g_both T_19 T_20)) ### Axiom % 0.18/0.56 488. (-. ((g_both T_19 T_20) /\ (h_both T_19 T_26))) (-. (h_false_only T_19 T_26)) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (g_both T_19 T_20) ### NotAnd 487 438 % 0.18/0.56 489. (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (h_false_only T_19 T_26)) ### NotExists 488 % 0.18/0.56 490. (-. ((g_both T_19 T_20) /\ (h_false_only T_19 T_26))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) ### NotAnd 486 489 % 0.18/0.56 491. (-. (((g_true_only T_19 T_20) /\ ((h_both T_19 T_26) \/ (h_false_only T_19 T_26))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 T_26)))) (g_both T_19 T_20) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotOr 490 % 0.18/0.56 492. (-. (All C, (((g_true_only T_19 T_20) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 T_20) /\ (h_false_only T_19 C))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) ### NotAllEx 491 % 0.18/0.56 493. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))) (g_both T_19 T_20) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) ### NotExists 492 % 0.18/0.56 494. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_1, ((h_true_only T_19 X_1) \/ ((h_both T_19 X_1) \/ (h_false_only T_19 X_1)))) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (g_both T_19 T_20) ### NotExists 493 % 0.18/0.56 495. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) (-. (Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C)))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### All 494 % 0.18/0.56 496. (-. ((Ex C, ((g_both T_19 T_20) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 495 386 % 0.18/0.56 497. (-. (Ex B, ((Ex C, ((g_both T_19 B) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### NotExists 496 % 0.18/0.56 498. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C))))) (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))) ### Axiom % 0.18/0.56 499. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C))))) ### NotExists 498 % 0.18/0.56 500. (-. (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### NotNot 499 % 0.18/0.56 501. (-. ((Ex B, ((Ex C, ((g_both T_19 B) /\ (h_both T_19 C))) /\ (-. (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C)))))) /\ (-. (Ex B, (All C, (((g_true_only T_19 B) /\ ((h_both T_19 C) \/ (h_false_only T_19 C))) \/ ((g_both T_19 B) /\ (h_false_only T_19 C)))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (g_both T_19 T_20) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotAnd 497 500 % 0.18/0.56 502. (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (g_both T_19 T_20) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) ### NotExists 501 % 0.18/0.56 503. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (-. (g_false T_19 T_20)) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 445 502 356 % 0.18/0.56 504. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (g_false T_19 T_20)) ### All 503 % 0.18/0.57 505. (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_19 T_20)) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 504 % 0.18/0.57 506. ((g_true_only T_19 T_20) \/ ((g_both T_19 T_20) \/ (g_false_only T_19 T_20))) (g_true T_19 T_20) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 445 502 361 % 0.18/0.57 507. (All X_1, ((g_true_only T_19 X_1) \/ ((g_both T_19 X_1) \/ (g_false_only T_19 X_1)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (g_true T_19 T_20) ### All 506 % 0.18/0.57 508. (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_19 T_20) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### All 507 % 0.18/0.57 509. (-. (g_false_only T_19 T_20)) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (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 505 508 % 0.18/0.57 510. (-. ((g_false_only T_19 T_20) \/ (h_true_only T_19 zenon_X23))) (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, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### NotOr 509 % 0.18/0.57 511. (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))) (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 510 % 0.18/0.57 512. (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))) ### Axiom % 0.18/0.57 513. (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) ### DisjTree 485 280 511 512 % 0.18/0.57 514. (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (-. (Ex C, ((g_false_only T_19 T_20) \/ (h_true_only T_19 C)))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) ### NotAnd 425 513 % 0.18/0.57 515. (-. (All B, (Ex C, ((g_false_only T_19 B) \/ (h_true_only T_19 C))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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 X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) ### NotAllEx 514 % 0.41/0.57 516. (-. (All A, (All B, (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (All X_2, (All X_1, ((g_true_only X_2 X_1) \/ ((g_both X_2 X_1) \/ (g_false_only X_2 X_1))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) ### NotAllEx 515 % 0.41/0.57 517. (-. ((All A, ((All B, (g_false_only A B)) \/ (Ex B, (h_true_only A B)))) /\ (All A, (All B, (Ex C, ((g_false_only A B) \/ (h_true_only A C))))))) (-. ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))) (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 X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_1))))) (-. ((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) ### NotAnd 307 516 % 0.41/0.57 518. (-. (((All A, ((All B, (g_false_only A B)) \/ (Ex B, (h_true_only A B)))) /\ (All A, (All B, (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) \/ (((Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B)))))) /\ (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))) \/ ((Ex A, ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ ((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B))))))) /\ ((-. (Ex A, (((Ex B, (g_true_only A B)) /\ (((Ex B, (h_both A B)) /\ (-. (Ex B, (h_true_only A B)))) \/ (All B, (h_false_only A B)))) \/ ((Ex B, (g_both A B)) /\ ((-. (Ex B, (g_true_only A B))) /\ (All B, (h_false_only A B))))))) /\ ((Ex A, ((Ex B, ((Ex C, ((g_both A B) /\ (h_both A C))) /\ (-. (Ex C, ((g_false_only A B) \/ (h_true_only A C)))))) /\ (-. (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C)))))))) /\ (-. (Ex A, (Ex B, (All C, (((g_true_only A B) /\ ((h_both A C) \/ (h_false_only A C))) \/ ((g_both A B) /\ (h_false_only A C))))))))))))) (All X_2, (All X_1, ((h_true_only X_2 X_1) \/ ((h_both X_2 X_1) \/ (h_false_only X_2 X_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 517 % 0.41/0.57 % SZS output end Proof % 0.41/0.57 (* END-PROOF *) %------------------------------------------------------------------------------