%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYO606+1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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 : 300s
% DateTime : Sat Jun 21 05:41:58 AM UTC 2025
% Result : Theorem 0.21s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SYO606+1 : TPTP v9.0.0. Released v7.0.0.
% 0.11/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n011.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 13:17:12 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.21/0.44 % SZS status Theorem
% 0.21/0.44 % SZS output start Proof
% 0.21/0.44 tff(h_both_type, type, (
% 0.21/0.44 h_both: ( $i * $i ) > $o)).
% 0.21/0.44 tff(tptp_fun_B_5_type, type, (
% 0.21/0.44 tptp_fun_B_5: $i > $i)).
% 0.21/0.44 tff(tptp_fun_A_3_type, type, (
% 0.21/0.44 tptp_fun_A_3: $i)).
% 0.21/0.44 tff(h_false_only_type, type, (
% 0.21/0.44 h_false_only: ( $i * $i ) > $o)).
% 0.21/0.44 tff(g_false_only_type, type, (
% 0.21/0.44 g_false_only: ( $i * $i ) > $o)).
% 0.21/0.44 tff(tptp_fun_B_2_type, type, (
% 0.21/0.44 tptp_fun_B_2: $i)).
% 0.21/0.44 tff(h_true_only_type, type, (
% 0.21/0.44 h_true_only: ( $i * $i ) > $o)).
% 0.21/0.44 tff(tptp_fun_A_0_type, type, (
% 0.21/0.44 tptp_fun_A_0: $i)).
% 0.21/0.44 tff(tptp_fun_B_1_type, type, (
% 0.21/0.44 tptp_fun_B_1: $i)).
% 0.21/0.44 tff(g_true_only_type, type, (
% 0.21/0.44 g_true_only: ( $i * $i ) > $o)).
% 0.21/0.44 tff(tptp_fun_B_4_type, type, (
% 0.21/0.44 tptp_fun_B_4: $i > $i)).
% 0.21/0.44 tff(tptp_fun_B_6_type, type, (
% 0.21/0.44 tptp_fun_B_6: $i > $i)).
% 0.21/0.44 tff(g_both_type, type, (
% 0.21/0.44 g_both: ( $i * $i ) > $o)).
% 0.21/0.44 tff(tptp_fun_C_7_type, type, (
% 0.21/0.44 tptp_fun_C_7: ( $i * $i ) > $i)).
% 0.21/0.44 tff(tptp_fun_A_8_type, type, (
% 0.21/0.44 tptp_fun_A_8: $i)).
% 0.21/0.44 tff(tptp_fun_B_10_type, type, (
% 0.21/0.44 tptp_fun_B_10: $i)).
% 0.21/0.44 tff(tptp_fun_B_9_type, type, (
% 0.21/0.44 tptp_fun_B_9: $i)).
% 0.21/0.44 tff(tptp_fun_A_15_type, type, (
% 0.21/0.44 tptp_fun_A_15: $i)).
% 0.21/0.44 tff(tptp_fun_B_14_type, type, (
% 0.21/0.44 tptp_fun_B_14: $i)).
% 0.21/0.44 tff(tptp_fun_B_13_type, type, (
% 0.21/0.44 tptp_fun_B_13: $i > $i)).
% 0.21/0.44 tff(tptp_fun_C_12_type, type, (
% 0.21/0.44 tptp_fun_C_12: ( $i * $i ) > $i)).
% 0.21/0.44 tff(tptp_fun_B_11_type, type, (
% 0.21/0.44 tptp_fun_B_11: $i)).
% 0.21/0.44 tff(g_false_type, type, (
% 0.21/0.44 g_false: ( $i * $i ) > $o)).
% 0.21/0.44 tff(g_true_type, type, (
% 0.21/0.44 g_true: ( $i * $i ) > $o)).
% 0.21/0.44 tff(h_true_type, type, (
% 0.21/0.44 h_true: ( $i * $i ) > $o)).
% 0.21/0.44 tff(h_false_type, type, (
% 0.21/0.44 h_false: ( $i * $i ) > $o)).
% 0.21/0.44 tff(1,assumption,((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_B_5(A!0))) | g_true_only(A!0, tptp_fun_B_6(A!0)))) | (~((~g_true_only(A!0, B!1)) | (~((~((~h_both(A!0, tptp_fun_B_5(A!0))) | h_true_only(A!0, tptp_fun_B_4(A!0)))) | h_false_only(A!0, tptp_fun_B_5(A!0))))))), introduced(assumption)).
% 0.21/0.44 tff(2,assumption,(![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))), introduced(assumption)).
% 0.21/0.44 tff(3,plain,
% 0.21/0.44 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!8, B!9)) | (~h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))) | (~((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))))))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(4,plain,
% 0.21/0.44 (~((~((~g_both(A!8, B!9)) | (~h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))) | (~((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[3, 2])).
% 0.21/0.44 tff(5,plain,
% 0.21/0.44 (((~((~g_both(A!8, B!9)) | (~h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))) | (~((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))))) | ((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(6,plain,
% 0.21/0.44 ((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[5, 4])).
% 0.21/0.44 tff(7,assumption,(~((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B))))), introduced(assumption)).
% 0.21/0.44 tff(8,plain,
% 0.21/0.44 (((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)))) | g_true_only(A!8, B!9)),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(9,plain,
% 0.21/0.44 (g_true_only(A!8, B!9)),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.21/0.44 tff(10,plain,
% 0.21/0.44 ((~((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))))) | (~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(11,plain,
% 0.21/0.44 ((~((~g_true_only(A!8, B!9)) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))))) | (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[10, 9])).
% 0.21/0.44 tff(12,plain,
% 0.21/0.44 (~(h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[11, 6])).
% 0.21/0.44 tff(13,plain,
% 0.21/0.44 ((h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))) | (~h_false_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(14,plain,
% 0.21/0.44 (~h_false_only(A!8, tptp_fun_C_7(B!9, A!8))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[13, 12])).
% 0.21/0.44 tff(15,plain,
% 0.21/0.44 ((h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))) | (~h_both(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(16,plain,
% 0.21/0.44 (~h_both(A!8, tptp_fun_C_7(B!9, A!8))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[15, 12])).
% 0.21/0.44 tff(17,plain,
% 0.21/0.44 (^[X_2: $i, X_1: $i] : refl((h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1)) <=> (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1)))),
% 0.21/0.44 inference(bind,[status(th)],[])).
% 0.21/0.44 tff(18,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(quant_intro,[status(thm)],[17])).
% 0.21/0.44 tff(19,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(20,plain,
% 0.21/0.44 (^[X_2: $i, X_1: $i] : trans(monotonicity(rewrite((h_true_only(X_2, X_1) | h_both(X_2, X_1)) <=> (h_true_only(X_2, X_1) | h_both(X_2, X_1))), (((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1)) <=> ((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1)))), rewrite(((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1)) <=> (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))), (((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1)) <=> (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))))),
% 0.21/0.44 inference(bind,[status(th)],[])).
% 0.21/0.44 tff(21,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : ((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(quant_intro,[status(thm)],[20])).
% 0.21/0.44 tff(22,axiom,(![X_2: $i, X_1: $i] : ((h_true_only(X_2, X_1) | h_both(X_2, X_1)) | h_false_only(X_2, X_1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','exhaustion_h')).
% 0.21/0.44 tff(23,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.21/0.44 tff(24,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.21/0.44 tff(25,plain,(
% 0.21/0.44 ![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(skolemize,[status(sab)],[24])).
% 0.21/0.44 tff(26,plain,
% 0.21/0.44 (![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[25, 18])).
% 0.21/0.44 tff(27,plain,
% 0.21/0.44 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(28,plain,
% 0.21/0.44 ((h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8))) <=> (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(rewrite,[status(thm)],[])).
% 0.21/0.44 tff(29,plain,
% 0.21/0.44 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8))))),
% 0.21/0.44 inference(monotonicity,[status(thm)],[28])).
% 0.21/0.44 tff(30,plain,
% 0.21/0.44 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(transitivity,[status(thm)],[29, 27])).
% 0.21/0.44 tff(31,plain,
% 0.21/0.44 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(32,plain,
% 0.21/0.44 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8)) | h_both(A!8, tptp_fun_C_7(B!9, A!8)) | h_true_only(A!8, tptp_fun_C_7(B!9, A!8))),
% 0.21/0.44 inference(modus_ponens,[status(thm)],[31, 30])).
% 0.21/0.44 tff(33,plain,
% 0.21/0.44 (h_true_only(A!8, tptp_fun_C_7(B!9, A!8))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[32, 26, 14, 16])).
% 0.21/0.44 tff(34,assumption,(~![B: $i] : h_false_only(A!8, B)), introduced(assumption)).
% 0.21/0.44 tff(35,plain,
% 0.21/0.44 (((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)))) | ((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(36,plain,
% 0.21/0.44 ((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[35, 7])).
% 0.21/0.44 tff(37,plain,
% 0.21/0.44 ((~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B))) | (~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(38,plain,
% 0.21/0.44 (~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[37, 36, 34])).
% 0.21/0.44 tff(39,plain,
% 0.21/0.44 (((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B)))) | ![B: $i] : (~h_true_only(A!8, B))),
% 0.21/0.44 inference(tautology,[status(thm)],[])).
% 0.21/0.44 tff(40,plain,
% 0.21/0.44 (![B: $i] : (~h_true_only(A!8, B))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.21/0.44 tff(41,plain,
% 0.21/0.44 ((~![B: $i] : (~h_true_only(A!8, B))) | (~h_true_only(A!8, tptp_fun_C_7(B!9, A!8)))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(42,plain,
% 0.21/0.44 ($false),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[41, 40, 33])).
% 0.21/0.44 tff(43,plain,(((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | ![B: $i] : h_false_only(A!8, B)), inference(lemma,lemma(discharge,[]))).
% 0.21/0.44 tff(44,plain,
% 0.21/0.44 (![B: $i] : h_false_only(A!8, B)),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[43, 7, 2])).
% 0.21/0.44 tff(45,plain,
% 0.21/0.44 ((~![B: $i] : h_false_only(A!8, B)) | h_false_only(A!8, tptp_fun_C_7(B!9, A!8))),
% 0.21/0.44 inference(quant_inst,[status(thm)],[])).
% 0.21/0.44 tff(46,plain,
% 0.21/0.44 ($false),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[45, 44, 14])).
% 0.21/0.44 tff(47,plain,(((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.44 tff(48,plain,
% 0.21/0.44 ((~g_true_only(A!8, B!9)) | (~((~((~h_both(A!8, B!10)) | (~![B: $i] : (~h_true_only(A!8, B))))) | ![B: $i] : h_false_only(A!8, B)))),
% 0.21/0.44 inference(unit_resolution,[status(thm)],[47, 2])).
% 0.21/0.44 tff(49,assumption,((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))))), introduced(assumption)).
% 0.21/0.45 tff(50,plain,
% 0.21/0.45 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))))))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(51,plain,
% 0.21/0.45 ($false),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[50, 2, 49])).
% 0.21/0.45 tff(52,plain,((~((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.45 tff(53,plain,
% 0.21/0.45 (~((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[52, 2])).
% 0.21/0.45 tff(54,plain,
% 0.21/0.45 (((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))))) | ((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(55,plain,
% 0.21/0.45 ((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[54, 53])).
% 0.21/0.45 tff(56,plain,
% 0.21/0.45 (~((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[50, 2])).
% 0.21/0.45 tff(57,plain,
% 0.21/0.45 (((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))))) | ((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(58,plain,
% 0.21/0.45 ((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[57, 56])).
% 0.21/0.45 tff(59,assumption,((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))), introduced(assumption)).
% 0.21/0.45 tff(60,assumption,(![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))), introduced(assumption)).
% 0.21/0.45 tff(61,plain,
% 0.21/0.45 (((~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))) | ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))) <=> ((~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))) | (~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))),
% 0.21/0.45 inference(rewrite,[status(thm)],[])).
% 0.21/0.45 tff(62,plain,
% 0.21/0.45 ((~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))) | ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15)))))))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(63,plain,
% 0.21/0.45 ((~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))) | (~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, tptp_fun_C_7(B!14, A!15)) | h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))))),
% 0.21/0.45 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.21/0.45 tff(64,plain,
% 0.21/0.45 ($false),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[63, 60, 59, 58])).
% 0.21/0.45 tff(65,plain,((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, tptp_fun_C_7(B!14, A!15))))) | (~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.45 tff(66,plain,
% 0.21/0.45 (~![C: $i] : ((~((~g_both(A!15, B!14)) | (~h_false_only(A!15, C)))) | (~((~g_true_only(A!15, B!14)) | (~(h_both(A!15, C) | h_false_only(A!15, C))))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[65, 55, 2])).
% 0.21/0.45 tff(67,assumption,((~((~g_both(A!3, tptp_fun_B_6(A!3))) | (~h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))) | (~((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))))), introduced(assumption)).
% 0.21/0.45 tff(68,plain,
% 0.21/0.45 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!3, tptp_fun_B_6(A!3))) | (~h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))) | (~((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))))))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(69,plain,
% 0.21/0.45 ($false),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[68, 2, 67])).
% 0.21/0.45 tff(70,plain,((~((~((~g_both(A!3, tptp_fun_B_6(A!3))) | (~h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))) | (~((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)))))))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.45 tff(71,plain,
% 0.21/0.45 (~((~((~g_both(A!3, tptp_fun_B_6(A!3))) | (~h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))) | (~((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)))))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[70, 2])).
% 0.21/0.45 tff(72,plain,
% 0.21/0.45 (((~((~g_both(A!3, tptp_fun_B_6(A!3))) | (~h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))) | (~((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))))) | ((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)))))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(73,plain,
% 0.21/0.45 ((~g_true_only(A!3, tptp_fun_B_6(A!3))) | (~(h_both(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3)) | h_false_only(A!3, tptp_fun_C_7(tptp_fun_B_6(A!3), A!3))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.21/0.45 tff(74,plain,
% 0.21/0.45 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))))))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(75,plain,
% 0.21/0.45 (~((~((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)))))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[74, 2])).
% 0.21/0.45 tff(76,plain,
% 0.21/0.45 (((~((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))))) | ((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)))))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(77,plain,
% 0.21/0.45 ((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[76, 75])).
% 0.21/0.45 tff(78,plain,
% 0.21/0.45 (((~((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_13(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))))) | ((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0))))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(79,plain,
% 0.21/0.45 ((~g_both(A!0, tptp_fun_B_13(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_13(A!0), A!0)))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[78, 75])).
% 0.21/0.45 tff(80,assumption,(~(g_false_only(A!0, B!1) | (~![B: $i] : (~h_true_only(A!0, B))))), introduced(assumption)).
% 0.21/0.45 tff(81,plain,
% 0.21/0.45 ((g_false_only(A!0, B!1) | (~![B: $i] : (~h_true_only(A!0, B)))) | ![B: $i] : (~h_true_only(A!0, B))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(82,plain,
% 0.21/0.45 (![B: $i] : (~h_true_only(A!0, B))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[81, 80])).
% 0.21/0.45 tff(83,assumption,(h_true_only(A!0, tptp_fun_C_7(B!1, A!0))), introduced(assumption)).
% 0.21/0.45 tff(84,assumption,(![B: $i] : (~h_true_only(A!0, B))), introduced(assumption)).
% 0.21/0.45 tff(85,plain,
% 0.21/0.45 ((~![B: $i] : (~h_true_only(A!0, B))) | (~h_true_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(86,plain,
% 0.21/0.45 ($false),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[85, 84, 83])).
% 0.21/0.45 tff(87,plain,((~h_true_only(A!0, tptp_fun_C_7(B!1, A!0))) | (~![B: $i] : (~h_true_only(A!0, B)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.45 tff(88,plain,
% 0.21/0.45 (~h_true_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[87, 82])).
% 0.21/0.45 tff(89,assumption,(~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))), introduced(assumption)).
% 0.21/0.45 tff(90,plain,
% 0.21/0.45 ((h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(91,plain,
% 0.21/0.45 (~h_both(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[90, 89])).
% 0.21/0.45 tff(92,plain,
% 0.21/0.45 ((h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(tautology,[status(thm)],[])).
% 0.21/0.45 tff(93,plain,
% 0.21/0.45 (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[92, 89])).
% 0.21/0.45 tff(94,assumption,(~h_true_only(A!0, tptp_fun_C_7(B!1, A!0))), introduced(assumption)).
% 0.21/0.45 tff(95,plain,
% 0.21/0.45 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(rewrite,[status(thm)],[])).
% 0.21/0.45 tff(96,plain,
% 0.21/0.45 ((h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0))) <=> (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(rewrite,[status(thm)],[])).
% 0.21/0.45 tff(97,plain,
% 0.21/0.45 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.45 inference(monotonicity,[status(thm)],[96])).
% 0.21/0.45 tff(98,plain,
% 0.21/0.45 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(transitivity,[status(thm)],[97, 95])).
% 0.21/0.45 tff(99,plain,
% 0.21/0.45 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.45 inference(quant_inst,[status(thm)],[])).
% 0.21/0.45 tff(100,plain,
% 0.21/0.45 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(modus_ponens,[status(thm)],[99, 98])).
% 0.21/0.45 tff(101,plain,
% 0.21/0.45 (h_false_only(A!0, tptp_fun_C_7(B!1, A!0)) | h_both(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[100, 26, 94])).
% 0.21/0.45 tff(102,plain,
% 0.21/0.45 ($false),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[101, 93, 91])).
% 0.21/0.45 tff(103,plain,((h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))) | h_true_only(A!0, tptp_fun_C_7(B!1, A!0))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.45 tff(104,plain,
% 0.21/0.45 (h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.45 inference(unit_resolution,[status(thm)],[103, 88])).
% 0.21/0.45 tff(105,plain,
% 0.21/0.45 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))) | (~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))))))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(106,plain,
% 0.21/0.46 (~((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))) | (~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))))))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[105, 2])).
% 0.21/0.46 tff(107,plain,
% 0.21/0.46 (((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))) | (~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))))) | ((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(108,plain,
% 0.21/0.46 ((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[107, 106])).
% 0.21/0.46 tff(109,plain,
% 0.21/0.46 (((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))) | (~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))))) | ((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(110,plain,
% 0.21/0.46 ((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[109, 106])).
% 0.21/0.46 tff(111,plain,
% 0.21/0.46 ((~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))))) | (~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(112,plain,
% 0.21/0.46 ((~((~g_true_only(A!0, B!1)) | (~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))))) | (~g_true_only(A!0, B!1))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[111, 104])).
% 0.21/0.46 tff(113,plain,
% 0.21/0.46 (~g_true_only(A!0, B!1)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[112, 110])).
% 0.21/0.46 tff(114,plain,
% 0.21/0.46 (^[X_2: $i, X_1: $i] : refl((g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1)) <=> (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1)))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(115,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[114])).
% 0.21/0.46 tff(116,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(117,plain,
% 0.21/0.46 (^[X_2: $i, X_1: $i] : trans(monotonicity(rewrite((g_true_only(X_2, X_1) | g_both(X_2, X_1)) <=> (g_true_only(X_2, X_1) | g_both(X_2, X_1))), (((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1)) <=> ((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1)))), rewrite(((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1)) <=> (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))), (((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1)) <=> (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))))),
% 0.21/0.46 inference(bind,[status(th)],[])).
% 0.21/0.46 tff(118,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : ((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1)) <=> ![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(quant_intro,[status(thm)],[117])).
% 0.21/0.46 tff(119,axiom,(![X_2: $i, X_1: $i] : ((g_true_only(X_2, X_1) | g_both(X_2, X_1)) | g_false_only(X_2, X_1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','exhaustion_g')).
% 0.21/0.46 tff(120,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.21/0.46 tff(121,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[120, 116])).
% 0.21/0.46 tff(122,plain,(
% 0.21/0.46 ![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(skolemize,[status(sab)],[121])).
% 0.21/0.46 tff(123,plain,
% 0.21/0.46 (![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[122, 115])).
% 0.21/0.46 tff(124,plain,
% 0.21/0.46 ((g_false_only(A!0, B!1) | (~![B: $i] : (~h_true_only(A!0, B)))) | (~g_false_only(A!0, B!1))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(125,plain,
% 0.21/0.46 (~g_false_only(A!0, B!1)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[124, 80])).
% 0.21/0.46 tff(126,plain,
% 0.21/0.46 (((~![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))) | (g_false_only(A!0, B!1) | g_true_only(A!0, B!1) | g_both(A!0, B!1))) <=> ((~![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))) | g_false_only(A!0, B!1) | g_true_only(A!0, B!1) | g_both(A!0, B!1))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(127,plain,
% 0.21/0.46 ((~![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))) | (g_false_only(A!0, B!1) | g_true_only(A!0, B!1) | g_both(A!0, B!1))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(128,plain,
% 0.21/0.46 ((~![X_2: $i, X_1: $i] : (g_false_only(X_2, X_1) | g_true_only(X_2, X_1) | g_both(X_2, X_1))) | g_false_only(A!0, B!1) | g_true_only(A!0, B!1) | g_both(A!0, B!1)),
% 0.21/0.46 inference(modus_ponens,[status(thm)],[127, 126])).
% 0.21/0.46 tff(129,plain,
% 0.21/0.46 (g_true_only(A!0, B!1) | g_both(A!0, B!1)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[128, 125, 123])).
% 0.21/0.46 tff(130,plain,
% 0.21/0.46 (g_both(A!0, B!1)),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[129, 113])).
% 0.21/0.46 tff(131,plain,
% 0.21/0.46 ((~((~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))))) | (~g_both(A!0, B!1)) | (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(132,plain,
% 0.21/0.46 (~h_false_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[131, 130, 108])).
% 0.21/0.46 tff(133,plain,
% 0.21/0.46 ((~(h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0)))) | h_both(A!0, tptp_fun_C_7(B!1, A!0)) | h_false_only(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(134,plain,
% 0.21/0.46 (h_both(A!0, tptp_fun_C_7(B!1, A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[133, 132, 104])).
% 0.21/0.46 tff(135,assumption,(h_true_only(A!0, tptp_fun_C_12(B!1, A!0))), introduced(assumption)).
% 0.21/0.46 tff(136,plain,
% 0.21/0.46 ((~![B: $i] : (~h_true_only(A!0, B))) | (~h_true_only(A!0, tptp_fun_C_12(B!1, A!0)))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(137,plain,
% 0.21/0.46 ($false),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[136, 84, 135])).
% 0.21/0.46 tff(138,plain,((~h_true_only(A!0, tptp_fun_C_12(B!1, A!0))) | (~![B: $i] : (~h_true_only(A!0, B)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.46 tff(139,plain,
% 0.21/0.46 (~h_true_only(A!0, tptp_fun_C_12(B!1, A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[138, 82])).
% 0.21/0.46 tff(140,assumption,((~((~g_both(A!0, tptp_fun_B_6(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))))), introduced(assumption)).
% 0.21/0.46 tff(141,plain,
% 0.21/0.46 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!0, tptp_fun_B_6(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))))))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(142,plain,
% 0.21/0.46 ($false),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[141, 2, 140])).
% 0.21/0.46 tff(143,plain,((~((~((~g_both(A!0, tptp_fun_B_6(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))))))) | (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.46 tff(144,plain,
% 0.21/0.46 (~((~((~g_both(A!0, tptp_fun_B_6(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))))))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[143, 2])).
% 0.21/0.46 tff(145,plain,
% 0.21/0.46 (((~((~g_both(A!0, tptp_fun_B_6(A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))) | (~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))))) | ((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(146,plain,
% 0.21/0.46 ((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[145, 144])).
% 0.21/0.46 tff(147,assumption,(h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))), introduced(assumption)).
% 0.21/0.46 tff(148,plain,
% 0.21/0.46 ((~![B: $i] : (~h_true_only(A!0, B))) | (~h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.46 inference(quant_inst,[status(thm)],[])).
% 0.21/0.46 tff(149,plain,
% 0.21/0.46 ($false),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[148, 84, 147])).
% 0.21/0.46 tff(150,plain,((~h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))) | (~![B: $i] : (~h_true_only(A!0, B)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.46 tff(151,plain,
% 0.21/0.46 (~h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[150, 82])).
% 0.21/0.46 tff(152,assumption,(~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))), introduced(assumption)).
% 0.21/0.46 tff(153,plain,
% 0.21/0.46 ((h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))) | (~h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(154,plain,
% 0.21/0.46 (~h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[153, 152])).
% 0.21/0.46 tff(155,plain,
% 0.21/0.46 ((h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))) | (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.46 inference(tautology,[status(thm)],[])).
% 0.21/0.46 tff(156,plain,
% 0.21/0.46 (~h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.46 inference(unit_resolution,[status(thm)],[155, 152])).
% 0.21/0.46 tff(157,assumption,(~h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))), introduced(assumption)).
% 0.21/0.46 tff(158,plain,
% 0.21/0.46 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(159,plain,
% 0.21/0.46 ((h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))) <=> (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.46 inference(rewrite,[status(thm)],[])).
% 0.21/0.46 tff(160,plain,
% 0.21/0.46 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))),
% 0.21/0.46 inference(monotonicity,[status(thm)],[159])).
% 0.21/0.46 tff(161,plain,
% 0.21/0.46 (((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))) <=> ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.47 inference(transitivity,[status(thm)],[160, 158])).
% 0.21/0.47 tff(162,plain,
% 0.21/0.47 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(163,plain,
% 0.21/0.47 ((~![X_2: $i, X_1: $i] : (h_false_only(X_2, X_1) | h_true_only(X_2, X_1) | h_both(X_2, X_1))) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.21/0.47 tff(164,plain,
% 0.21/0.47 (h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[163, 26, 157])).
% 0.21/0.47 tff(165,plain,
% 0.21/0.47 ($false),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[164, 156, 154])).
% 0.21/0.47 tff(166,plain,((h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))) | h_true_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.47 tff(167,plain,
% 0.21/0.47 (h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[166, 151])).
% 0.21/0.47 tff(168,plain,
% 0.21/0.47 ((~((~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)))))) | (~g_true_only(A!0, tptp_fun_B_6(A!0))) | (~(h_both(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0)) | h_false_only(A!0, tptp_fun_C_7(tptp_fun_B_6(A!0), A!0))))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(169,plain,
% 0.21/0.47 (~g_true_only(A!0, tptp_fun_B_6(A!0))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[168, 167, 146])).
% 0.21/0.47 tff(170,assumption,(h_true_only(A!0, tptp_fun_B_4(A!0))), introduced(assumption)).
% 0.21/0.47 tff(171,plain,
% 0.21/0.47 ((~![B: $i] : (~h_true_only(A!0, B))) | (~h_true_only(A!0, tptp_fun_B_4(A!0)))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(172,plain,
% 0.21/0.47 ($false),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[171, 84, 170])).
% 0.21/0.47 tff(173,plain,((~h_true_only(A!0, tptp_fun_B_4(A!0))) | (~![B: $i] : (~h_true_only(A!0, B)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.47 tff(174,plain,
% 0.21/0.47 (~h_true_only(A!0, tptp_fun_B_4(A!0))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[173, 82])).
% 0.21/0.47 tff(175,assumption,(h_both(A!0, tptp_fun_C_7(B!1, A!0))), introduced(assumption)).
% 0.21/0.47 tff(176,assumption,(~g_true_only(A!0, tptp_fun_B_6(A!0))), introduced(assumption)).
% 0.21/0.47 tff(177,assumption,(g_both(A!0, B!1)), introduced(assumption)).
% 0.21/0.47 tff(178,assumption,(~h_true_only(A!0, tptp_fun_B_4(A!0))), introduced(assumption)).
% 0.21/0.47 tff(179,assumption,(![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))), introduced(assumption)).
% 0.21/0.47 tff(180,plain,
% 0.21/0.47 (((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | ((~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))))) <=> ((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | (~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(181,plain,
% 0.21/0.47 (((~g_both(A!0, B!1)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0))) <=> ((~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(182,plain,
% 0.21/0.47 (((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | ((~g_both(A!0, B!1)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)))) <=> ((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | ((~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0)))))),
% 0.21/0.47 inference(monotonicity,[status(thm)],[181])).
% 0.21/0.47 tff(183,plain,
% 0.21/0.47 (((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | ((~g_both(A!0, B!1)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)))) <=> ((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | (~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))))),
% 0.21/0.47 inference(transitivity,[status(thm)],[182, 180])).
% 0.21/0.47 tff(184,plain,
% 0.21/0.47 ((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | ((~g_both(A!0, B!1)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0))) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(185,plain,
% 0.21/0.47 ((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | (~g_both(A!0, B!1)) | h_true_only(A!0, tptp_fun_B_4(A!0)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0)))),
% 0.21/0.47 inference(modus_ponens,[status(thm)],[184, 183])).
% 0.21/0.47 tff(186,plain,
% 0.21/0.47 ($false),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[185, 179, 178, 177, 176, 175])).
% 0.21/0.47 tff(187,plain,((~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))) | h_true_only(A!0, tptp_fun_B_4(A!0)) | (~g_both(A!0, B!1)) | g_true_only(A!0, tptp_fun_B_6(A!0)) | (~h_both(A!0, tptp_fun_C_7(B!1, A!0)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.47 tff(188,plain,
% 0.21/0.47 (~![A: $i, B_18: $i, B: $i] : ((~g_both(A, B_18)) | (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)) | g_true_only(A, tptp_fun_B_6(A)))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[187, 174, 130, 169, 134])).
% 0.21/0.47 tff(189,assumption,(~((~g_both(A!8, B!11)) | (~![B: $i] : (~g_true_only(A!8, B))) | (~![B: $i] : h_false_only(A!8, B)))), introduced(assumption)).
% 0.21/0.47 tff(190,plain,
% 0.21/0.47 (((~g_both(A!8, B!11)) | (~![B: $i] : (~g_true_only(A!8, B))) | (~![B: $i] : h_false_only(A!8, B))) | ![B: $i] : h_false_only(A!8, B)),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(191,plain,
% 0.21/0.47 (![B: $i] : h_false_only(A!8, B)),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[190, 189])).
% 0.21/0.47 tff(192,assumption,(~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))), introduced(assumption)).
% 0.21/0.47 tff(193,assumption,(![B: $i] : h_false_only(A!8, B)), introduced(assumption)).
% 0.21/0.47 tff(194,plain,
% 0.21/0.47 ((~![B: $i] : h_false_only(A!8, B)) | h_false_only(A!8, tptp_fun_C_7(B!11, A!8))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(195,plain,
% 0.21/0.47 ($false),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[194, 193, 192])).
% 0.21/0.47 tff(196,plain,(h_false_only(A!8, tptp_fun_C_7(B!11, A!8)) | (~![B: $i] : h_false_only(A!8, B))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.47 tff(197,plain,
% 0.21/0.47 (h_false_only(A!8, tptp_fun_C_7(B!11, A!8))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[196, 191])).
% 0.21/0.47 tff(198,plain,
% 0.21/0.47 (((~g_both(A!8, B!11)) | (~![B: $i] : (~g_true_only(A!8, B))) | (~![B: $i] : h_false_only(A!8, B))) | g_both(A!8, B!11)),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(199,plain,
% 0.21/0.47 (g_both(A!8, B!11)),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[198, 189])).
% 0.21/0.47 tff(200,assumption,(h_false_only(A!8, tptp_fun_C_7(B!11, A!8))), introduced(assumption)).
% 0.21/0.47 tff(201,assumption,(g_both(A!8, B!11)), introduced(assumption)).
% 0.21/0.47 tff(202,plain,
% 0.21/0.47 ((~((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))) | (~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8)))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(203,plain,
% 0.21/0.47 (~((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[202, 201, 200])).
% 0.21/0.47 tff(204,plain,
% 0.21/0.47 (((~((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))) | (~((~g_true_only(A!8, B!11)) | (~(h_both(A!8, tptp_fun_C_7(B!11, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))))) | ((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))),
% 0.21/0.47 inference(tautology,[status(thm)],[])).
% 0.21/0.47 tff(205,plain,
% 0.21/0.47 ((~((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))) | (~((~g_true_only(A!8, B!11)) | (~(h_both(A!8, tptp_fun_C_7(B!11, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[204, 203])).
% 0.21/0.47 tff(206,plain,
% 0.21/0.47 ((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~((~((~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))) | (~((~g_true_only(A!8, B!11)) | (~(h_both(A!8, tptp_fun_C_7(B!11, A!8)) | h_false_only(A!8, tptp_fun_C_7(B!11, A!8))))))))),
% 0.21/0.47 inference(quant_inst,[status(thm)],[])).
% 0.21/0.47 tff(207,plain,
% 0.21/0.47 ($false),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[206, 2, 205])).
% 0.21/0.47 tff(208,plain,((~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) | (~g_both(A!8, B!11)) | (~h_false_only(A!8, tptp_fun_C_7(B!11, A!8)))), inference(lemma,lemma(discharge,[]))).
% 0.21/0.47 tff(209,plain,
% 0.21/0.47 (~![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))),
% 0.21/0.47 inference(unit_resolution,[status(thm)],[208, 199, 197])).
% 0.21/0.47 tff(210,plain,
% 0.21/0.47 ((![A: $i, B_17: $i, B_16: $i, B: $i] : (~((~((~g_true_only(A, B)) | (~((~((~h_both(A, B_16)) | h_true_only(A, tptp_fun_B_4(A)))) | h_false_only(A, tptp_fun_B_5(A)))))) | (~((~h_false_only(A, tptp_fun_B_5(A))) | (~g_both(A, B_17)) | g_true_only(A, tptp_fun_B_6(A)))))) | ![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) <=> (![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))) | ![A: $i, B_17: $i, B_16: $i, B: $i] : (~((~((~g_true_only(A, B)) | (~((~((~h_both(A, B_16)) | h_true_only(A, tptp_fun_B_4(A)))) | h_false_only(A, tptp_fun_B_5(A)))))) | (~((~h_false_only(A, tptp_fun_B_5(A))) | (~g_both(A, B_17)) | g_true_only(A, tptp_fun_B_6(A)))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(211,plain,
% 0.21/0.47 ((![A: $i] : (~((~(![B: $i] : (~g_true_only(A, B)) | (~((~(![B: $i] : (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)))) | h_false_only(A, tptp_fun_B_5(A)))))) | (~((~h_false_only(A, tptp_fun_B_5(A))) | ![B: $i] : (~g_both(A, B)) | g_true_only(A, tptp_fun_B_6(A)))))) | ![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))))) <=> (![A: $i, B_17: $i, B_16: $i, B: $i] : (~((~((~g_true_only(A, B)) | (~((~((~h_both(A, B_16)) | h_true_only(A, tptp_fun_B_4(A)))) | h_false_only(A, tptp_fun_B_5(A)))))) | (~((~h_false_only(A, tptp_fun_B_5(A))) | (~g_both(A, B_17)) | g_true_only(A, tptp_fun_B_6(A)))))) | ![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(212,plain,
% 0.21/0.47 ((![A: $i] : ((![B: $i] : (~g_true_only(A, B)) | ((![B: $i] : (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A))) & (~h_false_only(A, tptp_fun_B_5(A))))) & ((~h_false_only(A, tptp_fun_B_5(A))) | ![B: $i] : (~g_both(A, B)) | g_true_only(A, tptp_fun_B_6(A)))) | ![A: $i, B: $i] : (~((g_both(A, B) & h_false_only(A, tptp_fun_C_7(B, A))) | (g_true_only(A, B) & (h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))) <=> (![A: $i] : (~((~(![B: $i] : (~g_true_only(A, B)) | (~((~(![B: $i] : (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A)))) | h_false_only(A, tptp_fun_B_5(A)))))) | (~((~h_false_only(A, tptp_fun_B_5(A))) | ![B: $i] : (~g_both(A, B)) | g_true_only(A, tptp_fun_B_6(A)))))) | ![A: $i, B: $i] : (~((~((~g_both(A, B)) | (~h_false_only(A, tptp_fun_C_7(B, A))))) | (~((~g_true_only(A, B)) | (~(h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(213,plain,
% 0.21/0.47 ((![A: $i] : ((![B: $i] : (~g_true_only(A, B)) | ((![B: $i] : (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A))) & (~h_false_only(A, tptp_fun_B_5(A))))) & (![B: $i] : (~g_both(A, B)) | g_true_only(A, tptp_fun_B_6(A)) | (~h_false_only(A, tptp_fun_B_5(A))))) | ![A: $i, B: $i] : (~((g_both(A, B) & h_false_only(A, tptp_fun_C_7(B, A))) | (g_true_only(A, B) & (h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A))))))) <=> (![A: $i] : ((![B: $i] : (~g_true_only(A, B)) | ((![B: $i] : (~h_both(A, B)) | h_true_only(A, tptp_fun_B_4(A))) & (~h_false_only(A, tptp_fun_B_5(A))))) & ((~h_false_only(A, tptp_fun_B_5(A))) | ![B: $i] : (~g_both(A, B)) | g_true_only(A, tptp_fun_B_6(A)))) | ![A: $i, B: $i] : (~((g_both(A, B) & h_false_only(A, tptp_fun_C_7(B, A))) | (g_true_only(A, B) & (h_both(A, tptp_fun_C_7(B, A)) | h_false_only(A, tptp_fun_C_7(B, A)))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(214,plain,
% 0.21/0.47 ((?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))))) <=> (?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(215,plain,
% 0.21/0.47 ((~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))) <=> (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))))))),
% 0.21/0.47 inference(monotonicity,[status(thm)],[214])).
% 0.21/0.47 tff(216,plain,
% 0.21/0.47 ((~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))) <=> (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(217,plain,
% 0.21/0.47 ((~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | ((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C))))) <=> (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))))))),
% 0.21/0.47 inference(rewrite,[status(thm)],[])).
% 0.21/0.47 tff(218,axiom,(~(((![A: $i] : (![B: $i] : g_false_only(A, B) | ?[B: $i] : h_true_only(A, B)) & ![A: $i, B: $i] : ?[C: $i] : (g_false_only(A, B) | h_true_only(A, C))) | (?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | ((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C))))) | (((?[A: $i] : (((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ?[B: $i] : h_both(A, B)) & (~?[B: $i] : h_true_only(A, B))) & (~?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | ((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ![B: $i] : h_false_only(A, B))))) & ?[A: $i] : (?[B: $i] : (?[C: $i] : (g_both(A, B) & h_both(A, C)) & (~?[C: $i] : (g_false_only(A, B) | h_true_only(A, C)))) & (~?[B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C)))))) & (~?[A: $i, B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','nc5')).
% 0.21/0.47 tff(219,plain,
% 0.21/0.47 (~((![A: $i] : (![B: $i] : g_false_only(A, B) | ?[B: $i] : h_true_only(A, B)) & ![A: $i, B: $i] : ?[C: $i] : (g_false_only(A, B) | h_true_only(A, C))) | (?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | ((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C)))))),
% 0.21/0.48 inference(or_elim,[status(thm)],[218])).
% 0.21/0.48 tff(220,plain,
% 0.21/0.48 (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | ((?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B))) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C))) | (g_both(A, B) & h_false_only(A, C))))),
% 0.21/0.48 inference(or_elim,[status(thm)],[219])).
% 0.21/0.48 tff(221,plain,
% 0.21/0.48 (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))),
% 0.21/0.48 inference(modus_ponens,[status(thm)],[220, 217])).
% 0.21/0.48 tff(222,plain,
% 0.21/0.48 (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))),
% 0.21/0.49 inference(modus_ponens,[status(thm)],[221, 215])).
% 0.21/0.49 tff(223,plain,
% 0.21/0.49 (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))),
% 0.21/0.49 inference(modus_ponens,[status(thm)],[222, 216])).
% 0.21/0.49 tff(224,plain,
% 0.21/0.49 (~(?[A: $i] : ((?[B: $i] : g_true_only(A, B) & ((?[B: $i] : h_both(A, B) & (~?[B: $i] : h_true_only(A, B))) | ![B: $i] : h_false_only(A, B))) | (?[B: $i] : g_both(A, B) & (~?[B: $i] : g_true_only(A, B)) & ![B: $i] : h_false_only(A, B))) & ?[A: $i, B: $i] : ![C: $i] : ((g_both(A, B) & h_false_only(A, C)) | (g_true_only(A, B) & (h_both(A, C) | h_false_only(A, C)))))),
% 0.21/0.49 inference(modus_ponens,[status(thm)],[223, 215])).
% 0.21/0.49 unexpected number of arguments: (let ((a!1 (lambda ((A $i))
% 0.21/0.49 (let ((a!1 (lambda ((B $i))
% 0.21/0.49 (refl (~ (not (g_true_only A B))
% 0.21/0.49 (not (g_true_only A B))))))
% 0.21/0.49 (a!2 (exists ((B $i)) (g_true_only A B)))
% 0.21/0.49 (a!3 (forall ((B $i)) (not (g_true_only A B))))
% 0.21/0.49 (a!4 (lambda ((B $i))
% 0.21/0.49 (refl (~ (not (h_both A B)) (not (h_both A B))))))
% 0.21/0.49 (a!5 (exists ((B $i)) (h_both A B)))
% 0.21/0.49 (a!6 (forall ((B $i)) (not (h_both A B))))
% 0.21/0.49 (a!7 (exists ((B $i)) (h_true_only A B)))
% 0.21/0.49 (a!12 (forall ((B $i)) (h_false_only A B)))
% 0.21/0.49 (a!18 (lambda ((B $i))
% 0.21/0.49 (refl (~ (not (g_both A B)) (not (g_both A B))))))
% 0.21/0.49 (a!19 (exists ((B $i)) (g_both A B)))
% 0.21/0.49 (a!20 (forall ((B $i)) (not (g_both A B)))))
% 0.21/0.49 (let ((a!8 (sk (~ a!7 (h_true_only A (B!4 A)))))
% 0.21/0.49 (a!10 (~ (not (and a!5 (not a!7)))
% 0.21/0.49 (or a!6 (h_true_only A (B!4 A)))))
% 0.21/0.49 (a!13 (~ (not a!12) (not (h_false_only A (B!5 A)))))
% 0.21/0.49 (a!14 (not (or (and a!5 (not a!7)) a!12)))
% 0.21/0.49 (a!15 (and (or a!6 (h_true_only A (B!4 A)))
% 0.21/0.49 (not (h_false_only A (B!5 A)))))
% 0.21/0.49 (a!16 (and a!2 (or (and a!5 (not a!7)) a!12)))
% 0.21/0.49 (a!21 (sk (~ a!2 (g_true_only A (B!6 A)))))
% 0.21/0.49 (a!23 (or a!20
% 0.21/0.49 (g_true_only A (B!6 A))
% 0.21/0.49 (not (h_false_only A (B!5 A))))))
% 0.21/0.49 (let ((a!9 (nnf-neg a!8
% 0.21/0.49 (~ (not (not a!7)) (h_true_only A (B!4 A)))))
% 0.21/0.49 (a!22 (nnf-neg a!21
% 0.21/0.49 (~ (not (not a!2)) (g_true_only A (B!6 A)))))
% 0.21/0.49 (a!24 (~ (not (and a!19 (not a!2) a!12)) a!23))
% 0.21/0.49 (a!26 (not (or a!16 (and a!19 (not a!2) a!12)))))
% 0.21/0.49 (let ((a!11 (nnf-neg (nnf-neg (proof-bind a!4) (~ (not a!5) a!6))
% 0.21/0.49 a!9
% 0.21/0.49 a!10))
% 0.21/0.49 (a!25 (nnf-neg (nnf-neg (proof-bind a!18)
% 0.21/0.49 (~ (not a!19) a!20))
% 0.21/0.49 a!22
% 0.21/0.49 (sk a!13)
% 0.21/0.49 a!24)))
% 0.21/0.49 (let ((a!17 (nnf-neg (nnf-neg (proof-bind a!1) (~ (not a!2) a!3))
% 0.21/0.49 (nnf-neg a!11 (sk a!13) (~ a!14 a!15))
% 0.21/0.49 (~ (not a!16) (or a!3 a!15)))))
% 0.21/0.49 (nnf-neg a!17 a!25 (~ a!26 (and (or a!3 a!15) a!23))))))))))
% 0.21/0.49 (a!2 (exists ((A $i))
% 0.21/0.49 (let ((a!1 (exists ((B $i)) (g_true_only A B)))
% 0.21/0.49 (a!2 (exists ((B $i)) (h_both A B)))
% 0.21/0.49 (a!3 (exists ((B $i)) (h_true_only A B)))
% 0.21/0.49 (a!4 (forall ((B $i)) (h_false_only A B)))
% 0.21/0.49 (a!6 (exists ((B $i)) (g_both A B))))
% 0.21/0.49 (let ((a!5 (and a!1 (or (and a!2 (not a!3)) a!4))))
% 0.21/0.49 (or a!5 (and a!6 (not a!1) a!4))))))
% 0.21/0.49 (a!3 (forall ((A $i))
% 0.21/0.49 (let ((a!1 (forall ((B $i)) (not (g_true_only A B))))
% 0.21/0.49 (a!2 (forall ((B $i)) (not (h_both A B))))
% 0.21/0.49 (a!4 (forall ((B $i)) (not (g_both A B)))))
% 0.21/0.49 (let ((a!3 (and (or a!2 (h_true_only A (B!4 A)))
% 0.21/0.49 (not (h_false_only A (B!5 A)))))
% 0.21/0.49 (a!5 (or a!4
% 0.21/0.49 (g_true_only A (B!6 A))
% 0.21/0.49 (not (h_false_only A (B!5 A))))))
% 0.21/0.49 (and (or a!1 a!3) a!5)))))
% 0.21/0.49 (a!4 (lambda ((A $i) (B $i))
% 0.21/0.49 (let ((a!1 (forall ((C $i))
% 0.21/0.49 (or (and (g_both A B) (h_false_only A C))
% 0.21/0.49 (and (g_true_only A B)
% 0.21/0.49 (or (h_both A C) (h_false_only A C))))))
% 0.21/0.49 (a!2 (and (g_true_only A B)
% 0.21/0.49 (or (h_both A (C!7 B A))
% 0.21/0.49 (h_false_only A (C!7 B A))))))
% 0.21/0.49 (let ((a!3 (or (and (g_both A B) (h_false_only A (C!7 B A))) a!2)))
% 0.21/0.49 (sk (~ (not a!1) (not a!3)))))))
% 0.21/0.49 (a!5 (exists ((A $i) (B $i))
% 0.21/0.49 (forall ((C $i))
% 0.21/0.49 (or (and (g_both A B) (h_false_only A C))
% 0.21/0.49 (and (g_true_only A B) (or (h_both A C) (h_false_only A C)))))))
% 0.21/0.49 (a!6 (forall ((A $i) (B $i))
% 0.21/0.49 (let ((a!1 (and (g_true_only A B)
% 0.21/0.49 (or (h_both A (C!7 B A))
% 0.21/0.49 (h_false_only A (C!7 B A))))))
% 0.21/0.49 (let ((a!2 (or (and (g_both A B) (h_false_only A (C!7 B A))) a!1)))
% 0.21/0.49 (not a!2))))))
% 0.21/0.49 (nnf-neg (nnf-neg (proof-bind a!1) (~ (not a!2) a!3))
% 0.21/0.49 (nnf-neg (proof-bind a!4) (~ (not a!5) a!6))
% 0.21/0.49 (~ (not (and a!2 a!5)) (or a!3 a!6))))
% 0.21/0.49 Proof display could not be completed: unexpected number of arguments
% 0.21/0.49 % E exiting
%------------------------------------------------------------------------------