%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEV515+1 : TPTP v9.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.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:29:20 AM UTC 2025
% Result : Theorem 0.20s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEV515+1 : TPTP v9.0.0. Released v7.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n001.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 : 300
% 0.12/0.33 % DateTime : Fri Jun 20 07:45:20 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.38 % SZS status Theorem
% 0.20/0.38 % SZS output start Proof
% 0.20/0.38 tff(g_true_only_type, type, (
% 0.20/0.38 g_true_only: ( $i * $i ) > $o)).
% 0.20/0.38 tff(tptp_fun_A_0_type, type, (
% 0.20/0.38 tptp_fun_A_0: $i)).
% 0.20/0.38 tff(g_false_only_type, type, (
% 0.20/0.38 g_false_only: ( $i * $i ) > $o)).
% 0.20/0.38 tff(tptp_fun_A_2_type, type, (
% 0.20/0.38 tptp_fun_A_2: $i)).
% 0.20/0.38 tff(g_both_type, type, (
% 0.20/0.38 g_both: ( $i * $i ) > $o)).
% 0.20/0.38 tff(tptp_fun_B_1_type, type, (
% 0.20/0.38 tptp_fun_B_1: $i > $i)).
% 0.20/0.38 tff(1,assumption,(g_true_only(A!0, A!0)), introduced(assumption)).
% 0.20/0.38 tff(2,plain,
% 0.20/0.38 ((g_both(A!0, A!0) | g_true_only(A!0, A!0)) | (~g_true_only(A!0, A!0))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(3,plain,
% 0.20/0.38 (g_both(A!0, A!0) | g_true_only(A!0, A!0)),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.20/0.38 tff(4,plain,
% 0.20/0.38 (^[B: $i] : refl((~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B))))))) <=> (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B))))))))),
% 0.20/0.38 inference(bind,[status(th)],[])).
% 0.20/0.38 tff(5,plain,
% 0.20/0.38 (![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B))))))) <=> ![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))),
% 0.20/0.38 inference(quant_intro,[status(thm)],[4])).
% 0.20/0.38 tff(6,plain,
% 0.20/0.38 (^[B: $i] : rewrite((~((g_both(B, A!0) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A!0) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A!0) & (g_both(B, B) | g_false_only(B, B))))) <=> (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B))))))))),
% 0.20/0.38 inference(bind,[status(th)],[])).
% 0.20/0.38 tff(7,plain,
% 0.20/0.38 (![B: $i] : (~((g_both(B, A!0) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A!0) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A!0) & (g_both(B, B) | g_false_only(B, B))))) <=> ![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))),
% 0.20/0.38 inference(quant_intro,[status(thm)],[6])).
% 0.20/0.38 tff(8,plain,
% 0.20/0.38 ((~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B))))) <=> (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))),
% 0.20/0.38 inference(rewrite,[status(thm)],[])).
% 0.20/0.38 tff(9,plain,
% 0.20/0.38 ((~![A: $i] : ?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B))))) <=> (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))),
% 0.20/0.38 inference(rewrite,[status(thm)],[])).
% 0.20/0.38 tff(10,axiom,(~(![A: $i] : ?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B)))) | (?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','nc1')).
% 0.20/0.38 tff(11,plain,
% 0.20/0.38 (~![A: $i] : ?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B))))),
% 0.20/0.38 inference(or_elim,[status(thm)],[10])).
% 0.20/0.38 tff(12,plain,
% 0.20/0.38 (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[11, 9])).
% 0.20/0.38 tff(13,plain,
% 0.20/0.38 (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[12, 8])).
% 0.20/0.38 tff(14,plain,
% 0.20/0.38 (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[13, 8])).
% 0.20/0.38 tff(15,plain,
% 0.20/0.38 (~![A: $i] : ?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[14, 8])).
% 0.20/0.38 tff(16,plain,(
% 0.20/0.38 $oeq((~?[B: $i] : ((g_both(B, A!0) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A!0) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A!0) & (g_both(B, B) | g_false_only(B, B))))), ![B: $i] : (~((g_both(B, A!0) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A!0) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A!0) & (g_both(B, B) | g_false_only(B, B))))))),
% 0.20/0.38 inference(transitivity,[status(sab)],[15])).
% 0.20/0.38 tff(17,plain,
% 0.20/0.38 (![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[16, 7])).
% 0.20/0.38 tff(18,plain,
% 0.20/0.38 (![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))),
% 0.20/0.38 inference(modus_ponens,[status(thm)],[17, 5])).
% 0.20/0.38 tff(19,plain,
% 0.20/0.38 ((~![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))) | (~((~((~g_both(A!0, A!0)) | (~(g_false_only(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))))))),
% 0.20/0.38 inference(quant_inst,[status(thm)],[])).
% 0.20/0.38 tff(20,plain,
% 0.20/0.38 (~((~((~g_both(A!0, A!0)) | (~(g_false_only(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0))))))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[19, 18])).
% 0.20/0.38 tff(21,plain,
% 0.20/0.38 (((~((~g_both(A!0, A!0)) | (~(g_false_only(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))))) | ((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(22,plain,
% 0.20/0.38 ((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0)))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[21, 20])).
% 0.20/0.38 tff(23,plain,
% 0.20/0.38 ((~((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))) | (~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0)))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(24,plain,
% 0.20/0.38 ((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0)))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[23, 22])).
% 0.20/0.38 tff(25,plain,
% 0.20/0.38 ($false),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[24, 3, 1])).
% 0.20/0.38 tff(26,plain,(~g_true_only(A!0, A!0)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.38 tff(27,plain,
% 0.20/0.38 (((~g_false_only(A!0, A!2)) | (~g_true_only(A!0, A!0))) | g_true_only(A!0, A!0)),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(28,plain,
% 0.20/0.38 ((~g_false_only(A!0, A!2)) | (~g_true_only(A!0, A!0))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[27, 26])).
% 0.20/0.38 tff(29,assumption,(g_false_only(A!0, A!0)), introduced(assumption)).
% 0.20/0.38 tff(30,plain,
% 0.20/0.38 ((g_both(A!0, A!0) | g_false_only(A!0, A!0)) | (~g_false_only(A!0, A!0))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(31,plain,
% 0.20/0.38 (g_both(A!0, A!0) | g_false_only(A!0, A!0)),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[30, 29])).
% 0.20/0.38 tff(32,plain,
% 0.20/0.38 (((~((~g_both(A!0, A!0)) | (~(g_false_only(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_true_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_true_only(A!0, A!0))))) | (~((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))))) | ((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0))))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(33,plain,
% 0.20/0.38 ((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[32, 20])).
% 0.20/0.38 tff(34,plain,
% 0.20/0.38 ((~((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0))))) | (~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(35,plain,
% 0.20/0.38 ((~g_false_only(A!0, A!0)) | (~(g_both(A!0, A!0) | g_false_only(A!0, A!0)))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[34, 33])).
% 0.20/0.38 tff(36,plain,
% 0.20/0.38 ($false),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[35, 31, 29])).
% 0.20/0.38 tff(37,plain,(~g_false_only(A!0, A!0)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.38 tff(38,plain,
% 0.20/0.38 (((~g_false_only(A!0, A!0)) | (~g_true_only(A!0, A!2))) | g_false_only(A!0, A!0)),
% 0.20/0.38 inference(tautology,[status(thm)],[])).
% 0.20/0.38 tff(39,plain,
% 0.20/0.38 ((~g_false_only(A!0, A!0)) | (~g_true_only(A!0, A!2))),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[38, 37])).
% 0.20/0.38 tff(40,assumption,((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))), introduced(assumption)).
% 0.20/0.38 tff(41,plain,
% 0.20/0.38 ((~![B: $i] : (~((~((~g_both(B, A!0)) | (~(g_false_only(B, B) | g_true_only(B, B))))) | (~((~g_true_only(B, A!0)) | (~(g_both(B, B) | g_true_only(B, B))))) | (~((~g_false_only(B, A!0)) | (~(g_both(B, B) | g_false_only(B, B)))))))) | (~((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))))),
% 0.20/0.38 inference(quant_inst,[status(thm)],[])).
% 0.20/0.38 tff(42,plain,
% 0.20/0.38 ($false),
% 0.20/0.38 inference(unit_resolution,[status(thm)],[41, 18, 40])).
% 0.20/0.38 tff(43,plain,(~((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.39 tff(44,plain,
% 0.20/0.39 (((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))) | ((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(45,plain,
% 0.20/0.39 ((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[44, 43])).
% 0.20/0.39 tff(46,plain,
% 0.20/0.39 (((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))) | ((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(47,plain,
% 0.20/0.39 ((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[46, 43])).
% 0.20/0.39 tff(48,plain,
% 0.20/0.39 (((~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))) | ((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(49,plain,
% 0.20/0.39 ((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[48, 43])).
% 0.20/0.39 tff(50,plain,
% 0.20/0.39 (^[X_2: $i, X_1: $i] : refl((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)))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(51,plain,
% 0.20/0.39 (![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_true_only(X_2, X_1) | g_both(X_2, X_1) | g_false_only(X_2, X_1))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[50])).
% 0.20/0.39 tff(52,plain,
% 0.20/0.39 (![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_true_only(X_2, X_1) | g_both(X_2, X_1) | g_false_only(X_2, X_1))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(53,plain,
% 0.20/0.39 (^[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_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)) <=> (g_true_only(X_2, X_1) | g_both(X_2, X_1) | g_false_only(X_2, X_1))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(54,plain,
% 0.20/0.39 (![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_true_only(X_2, X_1) | g_both(X_2, X_1) | g_false_only(X_2, X_1))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[53])).
% 0.20/0.39 tff(55,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/sandbox/benchmark/theBenchmark.p','exhaustion_g')).
% 0.20/0.39 tff(56,plain,
% 0.20/0.39 (![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))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.20/0.39 tff(57,plain,
% 0.20/0.39 (![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))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[56, 52])).
% 0.20/0.39 tff(58,plain,(
% 0.20/0.39 ![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))),
% 0.20/0.39 inference(skolemize,[status(sab)],[57])).
% 0.20/0.39 tff(59,plain,
% 0.20/0.39 (![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))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[58, 51])).
% 0.20/0.39 tff(60,plain,
% 0.20/0.39 (((~![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))) | (g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0))) <=> ((~![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))) | g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(61,plain,
% 0.20/0.39 ((g_true_only(A!0, A!0) | g_both(A!0, A!0) | g_false_only(A!0, A!0)) <=> (g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(62,plain,
% 0.20/0.39 (((~![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))) | (g_true_only(A!0, A!0) | g_both(A!0, A!0) | g_false_only(A!0, A!0))) <=> ((~![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))) | (g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0)))),
% 0.20/0.39 inference(monotonicity,[status(thm)],[61])).
% 0.20/0.39 tff(63,plain,
% 0.20/0.39 (((~![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))) | (g_true_only(A!0, A!0) | g_both(A!0, A!0) | g_false_only(A!0, A!0))) <=> ((~![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))) | g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0))),
% 0.20/0.39 inference(transitivity,[status(thm)],[62, 60])).
% 0.20/0.39 tff(64,plain,
% 0.20/0.39 ((~![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))) | (g_true_only(A!0, A!0) | g_both(A!0, A!0) | g_false_only(A!0, A!0))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(65,plain,
% 0.20/0.39 ((~![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))) | g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0)),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.20/0.39 tff(66,plain,
% 0.20/0.39 (g_both(A!0, A!0) | g_false_only(A!0, A!0) | g_true_only(A!0, A!0)),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[65, 59])).
% 0.20/0.39 tff(67,plain,
% 0.20/0.39 (g_both(A!0, A!0)),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[66, 26, 37])).
% 0.20/0.39 tff(68,assumption,(![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))), introduced(assumption)).
% 0.20/0.39 tff(69,plain,
% 0.20/0.39 (((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | ((~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))) <=> ((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(70,plain,
% 0.20/0.39 (((~g_both(A!0, A!0)) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))) <=> ((~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(71,plain,
% 0.20/0.39 (((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | ((~g_both(A!0, A!0)) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))) <=> ((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | ((~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))))),
% 0.20/0.39 inference(monotonicity,[status(thm)],[70])).
% 0.20/0.39 tff(72,plain,
% 0.20/0.39 (((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | ((~g_both(A!0, A!0)) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))) <=> ((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))),
% 0.20/0.39 inference(transitivity,[status(thm)],[71, 69])).
% 0.20/0.39 tff(73,plain,
% 0.20/0.39 ((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | ((~g_both(A!0, A!0)) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(74,plain,
% 0.20/0.39 ((~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))) | (~g_both(A!0, A!0)) | (~((~g_both(tptp_fun_B_1(A!0), A!0)) | (~(g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_true_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_true_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)))))) | (~((~g_false_only(tptp_fun_B_1(A!0), A!0)) | (~(g_both(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0)) | g_false_only(tptp_fun_B_1(A!0), tptp_fun_B_1(A!0))))))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.20/0.39 tff(75,plain,
% 0.20/0.39 ($false),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[74, 68, 67, 49, 47, 45])).
% 0.20/0.39 tff(76,plain,(~![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.39 tff(77,plain,
% 0.20/0.39 ((![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B)))))) <=> (![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B))))) | ![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(78,plain,
% 0.20/0.39 (^[A: $i, B: $i] : trans(monotonicity(rewrite(((~g_both(B, A)) | (~g_both(B, B))) <=> ((~g_both(B, A)) | (~g_both(B, B)))), ((((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) <=> (((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))))), rewrite((((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) <=> ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))), ((((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) <=> ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(79,plain,
% 0.20/0.40 (![A: $i, B: $i] : (((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) <=> ![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[78])).
% 0.20/0.40 tff(80,plain,
% 0.20/0.40 ((![A: $i, B: $i] : (((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B)))))) <=> (![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B))))))),
% 0.20/0.40 inference(monotonicity,[status(thm)],[79])).
% 0.20/0.40 tff(81,plain,
% 0.20/0.40 ((![A: $i, B: $i] : (((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B)))))) <=> (![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B))))) | ![A: $i, B: $i] : ((~g_both(B, A)) | (~g_both(B, B)) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))))),
% 0.20/0.40 inference(transitivity,[status(thm)],[80, 77])).
% 0.20/0.40 tff(82,plain,
% 0.20/0.40 ((![A: $i] : (![B: $i] : ((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B)))))) <=> (![A: $i, B: $i] : (((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(83,plain,
% 0.20/0.40 ((![A: $i] : (![B: $i] : (~(g_both(B, A) & g_both(B, B))) | (g_both(tptp_fun_B_1(A), A) & (g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_true_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_false_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))) | ![B: $i] : ((g_true_only(B, A!2) & g_false_only(B, B)) | (g_false_only(B, A!2) & g_true_only(B, B)))) <=> (![A: $i] : (![B: $i] : ((~g_both(B, A)) | (~g_both(B, B))) | (~((~g_both(tptp_fun_B_1(A), A)) | (~(g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_true_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | (~((~g_false_only(tptp_fun_B_1(A), A)) | (~(g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))))) | ![B: $i] : ((~((~g_true_only(B, A!2)) | (~g_false_only(B, B)))) | (~((~g_false_only(B, A!2)) | (~g_true_only(B, B))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(84,plain,
% 0.20/0.40 ((![A: $i] : (![B: $i] : (~(g_both(B, A) & g_both(B, B))) | ((g_both(tptp_fun_B_1(A), A) & (g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_true_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_false_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))))) | ![B: $i] : ((g_true_only(B, A!2) & g_false_only(B, B)) | (g_false_only(B, A!2) & g_true_only(B, B)))) <=> (![A: $i] : (![B: $i] : (~(g_both(B, A) & g_both(B, B))) | (g_both(tptp_fun_B_1(A), A) & (g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_true_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_true_only(tptp_fun_B_1(A), tptp_fun_B_1(A)))) | (g_false_only(tptp_fun_B_1(A), A) & (g_both(tptp_fun_B_1(A), tptp_fun_B_1(A)) | g_false_only(tptp_fun_B_1(A), tptp_fun_B_1(A))))) | ![B: $i] : ((g_true_only(B, A!2) & g_false_only(B, B)) | (g_false_only(B, A!2) & g_true_only(B, B))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(85,plain,
% 0.20/0.40 ((?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B))))) <=> (?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(86,plain,
% 0.20/0.40 ((~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))) <=> (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B))))))),
% 0.20/0.40 inference(monotonicity,[status(thm)],[85])).
% 0.20/0.40 tff(87,plain,
% 0.20/0.40 ((~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))) <=> (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(88,plain,
% 0.20/0.40 ((~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))) <=> (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(89,plain,
% 0.20/0.40 (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : (((g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B)))) | (g_false_only(B, A) & (g_false_only(B, B) | g_both(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.40 inference(or_elim,[status(thm)],[10])).
% 0.20/0.40 tff(90,plain,
% 0.20/0.40 (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[89, 88])).
% 0.20/0.41 tff(91,plain,
% 0.20/0.41 (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[90, 86])).
% 0.20/0.41 tff(92,plain,
% 0.20/0.41 (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[91, 87])).
% 0.20/0.41 tff(93,plain,
% 0.20/0.41 (~(?[A: $i] : (?[B: $i] : (g_both(B, A) & g_both(B, B)) & (~?[B: $i] : ((g_both(B, A) & (g_false_only(B, B) | g_true_only(B, B))) | (g_true_only(B, A) & (g_both(B, B) | g_true_only(B, B))) | (g_false_only(B, A) & (g_both(B, B) | g_false_only(B, B)))))) & (~?[A: $i] : ![B: $i] : ((g_true_only(B, A) & g_false_only(B, B)) | (g_false_only(B, A) & g_true_only(B, B)))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[92, 86])).
% 0.20/0.41 unexpected number of arguments: (let ((a!1 (exists ((A $i))
% 0.20/0.41 (let ((a!1 (exists ((B $i)) (and (g_both B A) (g_both B B))))
% 0.20/0.41 (a!2 (exists ((B $i))
% 0.20/0.41 (or (and (g_both B A)
% 0.20/0.41 (or (g_false_only B B) (g_true_only B B)))
% 0.20/0.41 (and (g_true_only B A)
% 0.20/0.41 (or (g_both B B) (g_true_only B B)))
% 0.20/0.41 (and (g_false_only B A)
% 0.20/0.41 (or (g_both B B) (g_false_only B B)))))))
% 0.20/0.41 (and a!1 (not a!2)))))
% 0.20/0.41 (a!2 (forall ((A $i))
% 0.20/0.41 (let ((a!1 (forall ((B $i)) (not (and (g_both B A) (g_both B B)))))
% 0.20/0.41 (a!2 (and (g_both (B!1 A) A)
% 0.20/0.41 (or (g_false_only (B!1 A) (B!1 A))
% 0.20/0.41 (g_true_only (B!1 A) (B!1 A)))))
% 0.20/0.41 (a!3 (and (g_true_only (B!1 A) A)
% 0.20/0.41 (or (g_both (B!1 A) (B!1 A))
% 0.20/0.41 (g_true_only (B!1 A) (B!1 A)))))
% 0.20/0.41 (a!4 (and (g_false_only (B!1 A) A)
% 0.20/0.41 (or (g_both (B!1 A) (B!1 A))
% 0.20/0.41 (g_false_only (B!1 A) (B!1 A))))))
% 0.20/0.41 (or a!1 (or a!2 a!3 a!4)))))
% 0.20/0.41 (a!4 (exists ((A $i))
% 0.20/0.41 (forall ((B $i))
% 0.20/0.41 (or (and (g_true_only B A) (g_false_only B B))
% 0.20/0.41 (and (g_false_only B A) (g_true_only B B))))))
% 0.20/0.41 (a!5 (forall ((B $i))
% 0.20/0.41 (or (and (g_true_only B A!2) (g_false_only B B))
% 0.20/0.41 (and (g_false_only B A!2) (g_true_only B B)))))
% 0.20/0.41 (a!6 (proof-bind (lambda ((B $i))
% 0.20/0.41 (let ((a!1 (or (and (g_true_only B A!2)
% 0.20/0.41 (g_false_only B B))
% 0.20/0.41 (and (g_false_only B A!2)
% 0.20/0.41 (g_true_only B B)))))
% 0.20/0.41 (refl (~ a!1 a!1)))))))
% 0.20/0.41 (let ((a!3 (nnf-neg (proof-bind (lambda ((A $i))
% 0.20/0.41 (let ((a!1 (exists ((B $i))
% 0.20/0.41 (and (g_both B A) (g_both B B))))
% 0.20/0.41 (a!2 (forall ((B $i))
% 0.20/0.41 (not (and (g_both B A)
% 0.20/0.41 (g_both B B)))))
% 0.20/0.41 (a!4 (exists ((B $i))
% 0.20/0.41 (or (and (g_both B A)
% 0.20/0.41 (or (g_false_only B B)
% 0.20/0.41 (g_true_only B B)))
% 0.20/0.41 (and (g_true_only B A)
% 0.20/0.41 (or (g_both B B)
% 0.20/0.41 (g_true_only B B)))
% 0.20/0.41 (and (g_false_only B A)
% 0.20/0.41 (or (g_both B B)
% 0.20/0.41 (g_false_only B B))))))
% 0.20/0.41 (a!5 (and (g_both (B!1 A) A)
% 0.20/0.41 (or (g_false_only (B!1 A)
% 0.20/0.41 (B!1 A))
% 0.20/0.41 (g_true_only (B!1 A)
% 0.20/0.41 (B!1 A)))))
% 0.20/0.41 (a!6 (and (g_true_only (B!1 A) A)
% 0.20/0.41 (or (g_both (B!1 A) (B!1 A))
% 0.20/0.41 (g_true_only (B!1 A)
% 0.20/0.41 (B!1 A)))))
% 0.20/0.41 (a!7 (and (g_false_only (B!1 A) A)
% 0.20/0.41 (or (g_both (B!1 A) (B!1 A))
% 0.20/0.41 (g_false_only (B!1 A)
% 0.20/0.41 (B!1 A))))))
% 0.20/0.41 (let ((a!3 (nnf-neg (proof-bind (lambda ((B $i))
% 0.20/0.41 (let ((a!1 (~ (not (and (g_both B
% 0.20/0.41 A)
% 0.20/0.41 (g_both B
% 0.20/0.41 B)))
% 0.20/0.41 (not (and (g_both B
% 0.20/0.41 A)
% 0.20/0.41 (g_both B
% 0.20/0.41 B))))))
% 0.20/0.41 (refl a!1))))
% 0.20/0.41 (~ (not a!1) a!2)))
% 0.20/0.41 (a!8 (nnf-neg (sk (~ a!4
% 0.20/0.41 (or a!5 a!6 a!7)))
% 0.20/0.41 (~ (not (not a!4))
% 0.20/0.41 (or a!5 a!6 a!7))))
% 0.20/0.41 (a!9 (~ (not (and a!1 (not a!4)))
% 0.20/0.41 (or a!2 (or a!5 a!6 a!7)))))
% 0.20/0.41 (nnf-neg a!3 a!8 a!9)))))
% 0.20/0.41 (~ (not a!1) a!2)))
% 0.20/0.41 (a!7 (nnf-neg (trans (sk (~ a!4 a!5))
% 0.20/0.41 (nnf-pos a!6 (~ a!5 a!5))
% 0.20/0.41 (~ a!4 a!5))
% 0.20/0.41 (~ (not (not a!4)) a!5)))
% 0.20/0.41 (a!8 (~ (not (and a!1 (not a!4))) (or a!2 a!5))))
% 0.20/0.41 (nnf-neg a!3 a!7 a!8)))
% 0.20/0.41 Proof display could not be completed: unexpected number of arguments
% 0.20/0.41 % E exiting
%------------------------------------------------------------------------------