%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS265+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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:13:39 AM UTC 2025
% Result : Theorem 41.85s 42.04s
% Output : Proof 41.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS265+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % 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 : Thu Jun 19 19:20:35 EDT 2025
% 0.12/0.33 % CPUTime :
% 41.85/42.04 % SZS status Theorem
% 41.85/42.04 % SZS output start Proof
% 41.85/42.04 tff(model_type, type, (
% 41.85/42.04 model: ( $i * $i ) > $o)).
% 41.85/42.04 tff(tptp_fun_F_32_type, type, (
% 41.85/42.04 tptp_fun_F_32: $i)).
% 41.85/42.04 tff(tptp_fun_I1_3_type, type, (
% 41.85/42.04 tptp_fun_I1_3: ( $i * $i ) > $i)).
% 41.85/42.04 tff(not_type, type, (
% 41.85/42.04 not: $i > $i)).
% 41.85/42.04 tff(tptp_fun_Ax_38_type, type, (
% 41.85/42.04 tptp_fun_Ax_38: $i)).
% 41.85/42.04 tff(status_type, type, (
% 41.85/42.04 status: ( $i * $i * $i ) > $o)).
% 41.85/42.04 tff(thm_type, type, (
% 41.85/42.04 thm: $i)).
% 41.85/42.04 tff(cax_type, type, (
% 41.85/42.04 cax: $i)).
% 41.85/42.04 tff(tptp_fun_I1_0_type, type, (
% 41.85/42.04 tptp_fun_I1_0: $i > $i)).
% 41.85/42.04 tff(mighta_type, type, (
% 41.85/42.04 mighta: ( $i * $i ) > $o)).
% 41.85/42.04 tff(tptp_fun_C_18_type, type, (
% 41.85/42.04 tptp_fun_C_18: ( $i * $i ) > $i)).
% 41.85/42.04 tff(tptp_fun_Ax_19_type, type, (
% 41.85/42.04 tptp_fun_Ax_19: ( $i * $i ) > $i)).
% 41.85/42.04 tff(1,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : rewrite((~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~((~status(Ax, C, thm)) | ![I1: $i] : ((~model(I1, Ax)) | model(I1, C)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(2,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> ![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~((~status(Ax, C, thm)) | ![I1: $i] : ((~model(I1, Ax)) | model(I1, C))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[1])).
% 41.85/42.04 tff(3,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : refl((~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(4,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> ![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[3])).
% 41.85/42.04 tff(5,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : rewrite((~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(6,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> ![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[5])).
% 41.85/42.04 tff(7,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))) <=> ![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(transitivity,[status(thm)],[6, 4])).
% 41.85/42.04 tff(8,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : trans(monotonicity(rewrite((![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))) <=> (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))), ((((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))) <=> (((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))))), rewrite((((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))) <=> (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))), ((((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))) <=> (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(9,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm)))) <=> ![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[8])).
% 41.85/42.04 tff(10,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm)) <=> ![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 41.85/42.04 inference(rewrite,[status(thm)],[])).
% 41.85/42.04 tff(11,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : rewrite((![I1: $i] : (model(I1, Ax) => model(I1, C)) <=> status(Ax, C, thm)) <=> (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm)))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(12,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (![I1: $i] : (model(I1, Ax) => model(I1, C)) <=> status(Ax, C, thm)) <=> ![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[11])).
% 41.85/42.04 tff(13,axiom,(![Ax: $i, C: $i] : (![I1: $i] : (model(I1, Ax) => model(I1, C)) <=> status(Ax, C, thm))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax','thm')).
% 41.85/42.04 tff(14,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 41.85/42.04 inference(modus_ponens,[status(thm)],[13, 12])).
% 41.85/42.04 tff(15,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 41.85/42.04 inference(modus_ponens,[status(thm)],[14, 10])).
% 41.85/42.04 tff(16,plain,(
% 41.85/42.04 ![Ax: $i, C: $i] : (((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm)) & (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))),
% 41.85/42.04 inference(skolemize,[status(sab)],[15])).
% 41.85/42.04 tff(17,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(modus_ponens,[status(thm)],[16, 9])).
% 41.85/42.04 tff(18,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~(![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) | (~status(Ax, C, thm))))))),
% 41.85/42.04 inference(modus_ponens,[status(thm)],[17, 7])).
% 41.85/42.04 tff(19,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~((~status(Ax, C, thm)) | ![I1: $i] : ((~model(I1, Ax)) | model(I1, C))))))),
% 41.85/42.04 inference(modus_ponens,[status(thm)],[18, 2])).
% 41.85/42.04 tff(20,plain,
% 41.85/42.04 ((~![Ax: $i, C: $i] : (~((~((~((~model(tptp_fun_I1_3(C, Ax), Ax)) | model(tptp_fun_I1_3(C, Ax), C))) | status(Ax, C, thm))) | (~((~status(Ax, C, thm)) | ![I1: $i] : ((~model(I1, Ax)) | model(I1, C))))))) | (~((~((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))) | (~((~status(F!32, not(Ax!38), thm)) | ![I1: $i] : ((~model(I1, F!32)) | model(I1, not(Ax!38)))))))),
% 41.85/42.04 inference(quant_inst,[status(thm)],[])).
% 41.85/42.04 tff(21,plain,
% 41.85/42.04 (~((~((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))) | (~((~status(F!32, not(Ax!38), thm)) | ![I1: $i] : ((~model(I1, F!32)) | model(I1, not(Ax!38))))))),
% 41.85/42.04 inference(unit_resolution,[status(thm)],[20, 19])).
% 41.85/42.04 tff(22,plain,
% 41.85/42.04 (((~((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))) | (~((~status(F!32, not(Ax!38), thm)) | ![I1: $i] : ((~model(I1, F!32)) | model(I1, not(Ax!38)))))) | ((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))),
% 41.85/42.04 inference(tautology,[status(thm)],[])).
% 41.85/42.04 tff(23,plain,
% 41.85/42.04 ((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm)),
% 41.85/42.04 inference(unit_resolution,[status(thm)],[22, 21])).
% 41.85/42.04 tff(24,assumption,(status(F!32, not(Ax!38), thm)), introduced(assumption)).
% 41.85/42.04 tff(25,assumption,((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | (~((~status(F!32, not(Ax!38), cax)) | ![I1: $i] : (~model(I1, F!32))))), introduced(assumption)).
% 41.85/42.04 tff(26,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : rewrite((~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~((~status(Ax, C, cax)) | ![I1: $i] : (~model(I1, Ax)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(27,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> ![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~((~status(Ax, C, cax)) | ![I1: $i] : (~model(I1, Ax))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[26])).
% 41.85/42.04 tff(28,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : refl((~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(29,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> ![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[28])).
% 41.85/42.04 tff(30,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : rewrite((~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))))),
% 41.85/42.04 inference(bind,[status(th)],[])).
% 41.85/42.04 tff(31,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> ![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.04 inference(quant_intro,[status(thm)],[30])).
% 41.85/42.04 tff(32,plain,
% 41.85/42.04 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))) <=> ![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.04 inference(transitivity,[status(thm)],[31, 29])).
% 41.85/42.04 tff(33,plain,
% 41.85/42.04 (^[Ax: $i, C: $i] : trans(monotonicity(rewrite((![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))) <=> (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))), (((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))) <=> ((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))))), rewrite(((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))) <=> (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))), (((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))) <=> (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(34,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : ((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax)))) <=> ![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[33])).
% 41.85/42.05 tff(35,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax))) <=> ![Ax: $i, C: $i] : (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(36,plain,
% 41.85/42.05 (^[Ax: $i, C: $i] : trans(trans(monotonicity(rewrite((~?[I1: $i] : model(I1, Ax)) <=> (~?[I1: $i] : model(I1, Ax))), (((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)) <=> ((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)))), rewrite(((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)) <=> (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))), (((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)) <=> (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax))))), rewrite((~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax))) <=> (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))), (((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)) <=> (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(37,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : ((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax)) <=> ![Ax: $i, C: $i] : (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[36])).
% 41.85/42.05 tff(38,axiom,(![Ax: $i, C: $i] : ((~?[I1: $i] : model(I1, Ax)) <=> status(Ax, C, cax))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax','cax')).
% 41.85/42.05 tff(39,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[38, 37])).
% 41.85/42.05 tff(40,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~(?[I1: $i] : model(I1, Ax) <=> status(Ax, C, cax)))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[39, 35])).
% 41.85/42.05 tff(41,plain,(
% 41.85/42.05 ![Ax: $i, C: $i] : ((model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax)) & (![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))),
% 41.85/42.05 inference(skolemize,[status(sab)],[40])).
% 41.85/42.05 tff(42,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[41, 34])).
% 41.85/42.05 tff(43,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~(![I1: $i] : (~model(I1, Ax)) | (~status(Ax, C, cax))))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[42, 32])).
% 41.85/42.05 tff(44,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~((~status(Ax, C, cax)) | ![I1: $i] : (~model(I1, Ax))))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[43, 27])).
% 41.85/42.05 tff(45,plain,
% 41.85/42.05 ((~![Ax: $i, C: $i] : (~((~(model(tptp_fun_I1_0(Ax), Ax) | status(Ax, C, cax))) | (~((~status(Ax, C, cax)) | ![I1: $i] : (~model(I1, Ax))))))) | (~((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | (~((~status(F!32, not(Ax!38), cax)) | ![I1: $i] : (~model(I1, F!32))))))),
% 41.85/42.05 inference(quant_inst,[status(thm)],[])).
% 41.85/42.05 tff(46,plain,
% 41.85/42.05 ($false),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[45, 44, 25])).
% 41.85/42.05 tff(47,plain,(~((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | (~((~status(F!32, not(Ax!38), cax)) | ![I1: $i] : (~model(I1, F!32)))))), inference(lemma,lemma(discharge,[]))).
% 41.85/42.05 tff(48,plain,
% 41.85/42.05 (((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | (~((~status(F!32, not(Ax!38), cax)) | ![I1: $i] : (~model(I1, F!32))))) | (model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))),
% 41.85/42.05 inference(tautology,[status(thm)],[])).
% 41.85/42.05 tff(49,plain,
% 41.85/42.05 (model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax)),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[48, 47])).
% 41.85/42.05 tff(50,assumption,(model(tptp_fun_I1_0(F!32), F!32)), introduced(assumption)).
% 41.85/42.05 tff(51,plain,
% 41.85/42.05 (^[I: $i] : refl((~model(I, F!32)) <=> (~model(I, F!32)))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(52,plain,
% 41.85/42.05 (![I: $i] : (~model(I, F!32)) <=> ![I: $i] : (~model(I, F!32))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[51])).
% 41.85/42.05 tff(53,plain,
% 41.85/42.05 (?[F: $i] : ![I: $i] : (~model(I, F)) <=> ?[F: $i] : ![I: $i] : (~model(I, F))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(54,axiom,(?[F: $i] : ![I: $i] : (~model(I, F))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax','contradiction')).
% 41.85/42.05 tff(55,plain,
% 41.85/42.05 (?[F: $i] : ![I: $i] : (~model(I, F))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[54, 53])).
% 41.85/42.05 tff(56,plain,(
% 41.85/42.05 $oeq(![I: $i] : (~model(I, F!32)), ![I: $i] : (~model(I, F!32)))),
% 41.85/42.05 inference(transitivity,[status(sab)],[55])).
% 41.85/42.05 tff(57,plain,
% 41.85/42.05 (![I: $i] : (~model(I, F!32))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[56, 52])).
% 41.85/42.05 tff(58,plain,
% 41.85/42.05 ((~![I: $i] : (~model(I, F!32))) | (~model(tptp_fun_I1_0(F!32), F!32))),
% 41.85/42.05 inference(quant_inst,[status(thm)],[])).
% 41.85/42.05 tff(59,plain,
% 41.85/42.05 ($false),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[58, 57, 50])).
% 41.85/42.05 tff(60,plain,(~model(tptp_fun_I1_0(F!32), F!32)), inference(lemma,lemma(discharge,[]))).
% 41.85/42.05 tff(61,plain,
% 41.85/42.05 ((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax)),
% 41.85/42.05 inference(tautology,[status(thm)],[])).
% 41.85/42.05 tff(62,plain,
% 41.85/42.05 ((~(model(tptp_fun_I1_0(F!32), F!32) | status(F!32, not(Ax!38), cax))) | status(F!32, not(Ax!38), cax)),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[61, 60])).
% 41.85/42.05 tff(63,plain,
% 41.85/42.05 (status(F!32, not(Ax!38), cax)),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[62, 49])).
% 41.85/42.05 tff(64,plain,
% 41.85/42.05 (^[S1: $i, S2: $i] : refl((~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))) <=> (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(65,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))) <=> ![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[64])).
% 41.85/42.05 tff(66,plain,
% 41.85/42.05 (^[S1: $i, S2: $i] : rewrite((~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))) <=> (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(67,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))) <=> ![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[66])).
% 41.85/42.05 tff(68,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))) <=> ![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(transitivity,[status(thm)],[67, 65])).
% 41.85/42.05 tff(69,plain,
% 41.85/42.05 (^[S1: $i, S2: $i] : trans(monotonicity(rewrite((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) <=> (mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))), trans(monotonicity(rewrite((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) <=> (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))), (((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2))) <=> ((~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))) | (~mighta(S1, S2))))), rewrite(((~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))) | (~mighta(S1, S2))) <=> ((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))), (((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2))) <=> ((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))), (((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))) <=> ((mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))) & ((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))))), rewrite(((mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))) & ((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)))))) <=> (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))), (((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))) <=> (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(70,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : ((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))) <=> ![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[69])).
% 41.85/42.05 tff(71,plain,
% 41.85/42.05 (^[S1: $i, S2: $i] : rewrite(((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2))) | mighta(S1, S2)) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))) <=> ((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))))),
% 41.85/42.05 inference(bind,[status(th)],[])).
% 41.85/42.05 tff(72,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : ((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2))) | mighta(S1, S2)) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2)))) <=> ![S1: $i, S2: $i] : ((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2))))),
% 41.85/42.05 inference(quant_intro,[status(thm)],[71])).
% 41.85/42.05 tff(73,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2)) <=> ![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(74,axiom,(![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax','mighta')).
% 41.85/42.05 tff(75,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[74, 73])).
% 41.85/42.05 tff(76,plain,(
% 41.85/42.05 ![S1: $i, S2: $i] : ((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2))) | mighta(S1, S2)) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2))))),
% 41.85/42.05 inference(skolemize,[status(sab)],[75])).
% 41.85/42.05 tff(77,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : ((mighta(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & status(Ax, C, S2)))) & ((status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1) & status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2)) | (~mighta(S1, S2))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[76, 72])).
% 41.85/42.05 tff(78,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[77, 70])).
% 41.85/42.05 tff(79,plain,
% 41.85/42.05 (![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[78, 68])).
% 41.85/42.05 tff(80,plain,
% 41.85/42.05 ((~![S1: $i, S2: $i] : (~((~(mighta(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))) | (~((~mighta(S1, S2)) | (~((~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S1)) | (~status(tptp_fun_Ax_19(S2, S1), tptp_fun_C_18(S2, S1), S2))))))))) | (~((~(mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))) | (~((~mighta(cax, thm)) | (~((~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), cax)) | (~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), thm))))))))),
% 41.85/42.05 inference(quant_inst,[status(thm)],[])).
% 41.85/42.05 tff(81,plain,
% 41.85/42.05 (~((~(mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))) | (~((~mighta(cax, thm)) | (~((~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), cax)) | (~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), thm)))))))),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[80, 79])).
% 41.85/42.05 tff(82,plain,
% 41.85/42.05 (((~(mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))) | (~((~mighta(cax, thm)) | (~((~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), cax)) | (~status(tptp_fun_Ax_19(thm, cax), tptp_fun_C_18(thm, cax), thm))))))) | (mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))),
% 41.85/42.05 inference(tautology,[status(thm)],[])).
% 41.85/42.05 tff(83,plain,
% 41.85/42.05 (mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[82, 81])).
% 41.85/42.05 tff(84,plain,
% 41.85/42.05 ((~mighta(cax, thm)) <=> (~mighta(cax, thm))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(85,axiom,(~mighta(cax, thm)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mighta_cax_thm')).
% 41.85/42.05 tff(86,plain,
% 41.85/42.05 (~mighta(cax, thm)),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[85, 84])).
% 41.85/42.05 tff(87,plain,
% 41.85/42.05 ((~(mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))) | mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))),
% 41.85/42.05 inference(tautology,[status(thm)],[])).
% 41.85/42.05 tff(88,plain,
% 41.85/42.05 ((~(mighta(cax, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax))))) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[87, 86])).
% 41.85/42.05 tff(89,plain,
% 41.85/42.05 (![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[88, 83])).
% 41.85/42.05 tff(90,plain,
% 41.85/42.05 (((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | ((~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm)))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | (~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm)))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(91,plain,
% 41.85/42.05 (((~status(F!32, not(Ax!38), thm)) | (~status(F!32, not(Ax!38), cax))) <=> ((~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm)))),
% 41.85/42.05 inference(rewrite,[status(thm)],[])).
% 41.85/42.05 tff(92,plain,
% 41.85/42.05 (((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | ((~status(F!32, not(Ax!38), thm)) | (~status(F!32, not(Ax!38), cax)))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | ((~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm))))),
% 41.85/42.05 inference(monotonicity,[status(thm)],[91])).
% 41.85/42.05 tff(93,plain,
% 41.85/42.05 (((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | ((~status(F!32, not(Ax!38), thm)) | (~status(F!32, not(Ax!38), cax)))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | (~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm)))),
% 41.85/42.05 inference(transitivity,[status(thm)],[92, 90])).
% 41.85/42.05 tff(94,plain,
% 41.85/42.05 ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | ((~status(F!32, not(Ax!38), thm)) | (~status(F!32, not(Ax!38), cax)))),
% 41.85/42.05 inference(quant_inst,[status(thm)],[])).
% 41.85/42.05 tff(95,plain,
% 41.85/42.05 ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, cax)))) | (~status(F!32, not(Ax!38), cax)) | (~status(F!32, not(Ax!38), thm))),
% 41.85/42.05 inference(modus_ponens,[status(thm)],[94, 93])).
% 41.85/42.05 tff(96,plain,
% 41.85/42.05 ($false),
% 41.85/42.05 inference(unit_resolution,[status(thm)],[95, 89, 63, 24])).
% 41.85/42.05 tff(97,plain,(~status(F!32, not(Ax!38), thm)), inference(lemma,lemma(discharge,[]))).
% 41.85/42.05 tff(98,plain,
% 41.85/42.05 ((~((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))) | (~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm)),
% 41.85/42.06 inference(tautology,[status(thm)],[])).
% 41.85/42.06 tff(99,plain,
% 41.85/42.06 ((~((~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))) | status(F!32, not(Ax!38), thm))) | (~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38))))),
% 41.85/42.06 inference(unit_resolution,[status(thm)],[98, 97])).
% 41.85/42.06 tff(100,plain,
% 41.85/42.06 (~((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38)))),
% 41.85/42.06 inference(unit_resolution,[status(thm)],[99, 23])).
% 41.85/42.06 tff(101,plain,
% 41.85/42.06 (((~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)) | model(tptp_fun_I1_3(not(Ax!38), F!32), not(Ax!38))) | model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)),
% 41.85/42.06 inference(tautology,[status(thm)],[])).
% 41.85/42.06 tff(102,plain,
% 41.85/42.06 (model(tptp_fun_I1_3(not(Ax!38), F!32), F!32)),
% 41.85/42.06 inference(unit_resolution,[status(thm)],[101, 100])).
% 41.85/42.06 tff(103,plain,
% 41.85/42.06 ((~![I: $i] : (~model(I, F!32))) | (~model(tptp_fun_I1_3(not(Ax!38), F!32), F!32))),
% 41.85/42.06 inference(quant_inst,[status(thm)],[])).
% 41.85/42.06 tff(104,plain,
% 41.85/42.06 ($false),
% 41.85/42.06 inference(unit_resolution,[status(thm)],[103, 57, 102])).
% 41.85/42.06 % SZS output end Proof
% 41.85/42.07 % E exiting
%------------------------------------------------------------------------------