%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS234+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:13:37 AM UTC 2025
% Result : Theorem 0.63s 0.81s
% Output : Proof 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS234+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 19 19:18:17 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.63/0.81 % SZS status Theorem
% 0.63/0.81 % SZS output start Proof
% 0.63/0.81 tff(model_type, type, (
% 0.63/0.81 model: ( $i * $i ) > $o)).
% 0.63/0.81 tff(tptp_fun_Ax_25_type, type, (
% 0.63/0.81 tptp_fun_Ax_25: ( $i * $i ) > $i)).
% 0.63/0.81 tff(uns_type, type, (
% 0.63/0.81 uns: $i)).
% 0.63/0.81 tff(thm_type, type, (
% 0.63/0.81 thm: $i)).
% 0.63/0.81 tff(tptp_fun_I1_0_type, type, (
% 0.63/0.81 tptp_fun_I1_0: $i > $i)).
% 0.63/0.81 tff(tptp_fun_F_29_type, type, (
% 0.63/0.81 tptp_fun_F_29: $i)).
% 0.63/0.81 tff(tptp_fun_C_24_type, type, (
% 0.63/0.81 tptp_fun_C_24: ( $i * $i ) > $i)).
% 0.63/0.81 tff(not_type, type, (
% 0.63/0.81 not: $i > $i)).
% 0.63/0.81 tff(status_type, type, (
% 0.63/0.81 status: ( $i * $i * $i ) > $o)).
% 0.63/0.81 tff(tptp_fun_I1_15_type, type, (
% 0.63/0.81 tptp_fun_I1_15: $i > $i)).
% 0.63/0.81 tff(tptp_fun_I2_16_type, type, (
% 0.63/0.81 tptp_fun_I2_16: $i > $i)).
% 0.63/0.81 tff(nevera_type, type, (
% 0.63/0.81 nevera: ( $i * $i ) > $o)).
% 0.63/0.81 tff(tptp_fun_I1_3_type, type, (
% 0.63/0.81 tptp_fun_I1_3: ( $i * $i ) > $i)).
% 0.63/0.81 tff(1,plain,
% 0.63/0.81 (^[I: $i, F: $i] : refl((~(model(I, F) <=> model(I, not(F)))) <=> (~(model(I, F) <=> model(I, not(F)))))),
% 0.63/0.81 inference(bind,[status(th)],[])).
% 0.63/0.81 tff(2,plain,
% 0.63/0.81 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F)))) <=> ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 0.63/0.81 inference(quant_intro,[status(thm)],[1])).
% 0.63/0.81 tff(3,plain,
% 0.63/0.81 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F)))) <=> ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 0.63/0.81 inference(rewrite,[status(thm)],[])).
% 0.63/0.81 tff(4,axiom,(![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax','completeness')).
% 0.63/0.81 tff(5,plain,
% 0.63/0.81 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.63/0.81 tff(6,plain,(
% 0.63/0.81 ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 0.63/0.81 inference(skolemize,[status(sab)],[5])).
% 0.63/0.81 tff(7,plain,
% 0.63/0.81 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.63/0.81 tff(8,plain,
% 0.63/0.81 ((~![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))) | (~(model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)) <=> model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns)))))),
% 0.63/0.81 inference(quant_inst,[status(thm)],[])).
% 0.63/0.81 tff(9,plain,
% 0.63/0.81 (~(model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)) <=> model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns))))),
% 0.63/0.81 inference(unit_resolution,[status(thm)],[8, 7])).
% 0.63/0.81 tff(10,plain,
% 0.63/0.81 (^[Ax: $i, C: $i] : refl((~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))) <=> (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))))),
% 0.63/0.81 inference(bind,[status(th)],[])).
% 0.63/0.81 tff(11,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(quant_intro,[status(thm)],[10])).
% 0.63/0.81 tff(12,plain,
% 0.63/0.81 (^[Ax: $i, C: $i] : rewrite((~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))) <=> (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))))),
% 0.63/0.81 inference(bind,[status(th)],[])).
% 0.63/0.81 tff(13,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(quant_intro,[status(thm)],[12])).
% 0.63/0.81 tff(14,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(transitivity,[status(thm)],[13, 11])).
% 0.63/0.81 tff(15,plain,
% 0.63/0.81 (^[Ax: $i, C: $i] : trans(monotonicity(rewrite((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) <=> (status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))), trans(monotonicity(rewrite((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) <=> (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))), (((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns))) <=> ((~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))) | (~status(Ax, C, uns))))), rewrite(((~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))) | (~status(Ax, C, uns))) <=> ((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))), (((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns))) <=> ((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))), (((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))) <=> ((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))))), rewrite(((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C))))))) <=> (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))), (((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))) <=> (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))))),
% 0.63/0.81 inference(bind,[status(th)],[])).
% 0.63/0.81 tff(16,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : ((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(quant_intro,[status(thm)],[15])).
% 0.63/0.81 tff(17,plain,
% 0.63/0.81 (^[Ax: $i, C: $i] : rewrite(((((~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) | status(Ax, C, uns)) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))) <=> ((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))))),
% 0.63/0.81 inference(bind,[status(th)],[])).
% 0.63/0.81 tff(18,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : ((((~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) | status(Ax, C, uns)) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns)))) <=> ![Ax: $i, C: $i] : ((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns))))),
% 0.63/0.81 inference(quant_intro,[status(thm)],[17])).
% 0.63/0.81 tff(19,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) <=> status(Ax, C, uns)) <=> ![Ax: $i, C: $i] : ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) <=> status(Ax, C, uns))),
% 0.63/0.81 inference(rewrite,[status(thm)],[])).
% 0.63/0.81 tff(20,axiom,(![Ax: $i, C: $i] : ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) <=> status(Ax, C, uns))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax','uns')).
% 0.63/0.81 tff(21,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) <=> status(Ax, C, uns))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[20, 19])).
% 0.63/0.81 tff(22,plain,(
% 0.63/0.81 ![Ax: $i, C: $i] : ((((~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) | status(Ax, C, uns)) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns))))),
% 0.63/0.81 inference(skolemize,[status(sab)],[21])).
% 0.63/0.81 tff(23,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : ((status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C)))) & ((![I1: $i] : model(I1, Ax) & ![I2: $i] : model(I2, not(C))) | (~status(Ax, C, uns))))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[22, 18])).
% 0.63/0.81 tff(24,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[23, 16])).
% 0.63/0.81 tff(25,plain,
% 0.63/0.81 (![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))),
% 0.63/0.81 inference(modus_ponens,[status(thm)],[24, 14])).
% 0.63/0.81 tff(26,plain,
% 0.63/0.81 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))))))),
% 0.63/0.81 inference(rewrite,[status(thm)],[])).
% 0.63/0.81 tff(27,plain,
% 0.63/0.81 ((~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))))) <=> (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))),
% 0.63/0.82 inference(rewrite,[status(thm)],[])).
% 0.63/0.82 tff(28,plain,
% 0.63/0.82 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))))))),
% 0.63/0.82 inference(monotonicity,[status(thm)],[27])).
% 0.63/0.82 tff(29,plain,
% 0.63/0.82 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))))))),
% 0.63/0.82 inference(transitivity,[status(thm)],[28, 26])).
% 0.63/0.82 tff(30,plain,
% 0.63/0.82 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))),
% 0.63/0.82 inference(quant_inst,[status(thm)],[])).
% 0.63/0.82 tff(31,plain,
% 0.63/0.82 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, uns) | (~model(tptp_fun_I1_15(Ax), Ax)) | (~model(tptp_fun_I2_16(C), not(C))))) | (~((~status(Ax, C, uns)) | (~((~![I1: $i] : model(I1, Ax)) | (~![I2: $i] : model(I2, not(C)))))))))) | (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.63/0.82 tff(32,plain,
% 0.63/0.82 (~((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[31, 25])).
% 0.63/0.82 tff(33,plain,
% 0.63/0.82 (((~(status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns) | (~model(tptp_fun_I2_16(tptp_fun_C_24(thm, uns)), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_15(tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))))) | ((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(34,plain,
% 0.63/0.82 ((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[33, 32])).
% 0.63/0.82 tff(35,plain,
% 0.63/0.82 (^[S1: $i, S2: $i] : rewrite((~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(36,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> ![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[35])).
% 0.63/0.82 tff(37,plain,
% 0.63/0.82 (^[S1: $i, S2: $i] : refl((~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(38,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> ![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[37])).
% 0.63/0.82 tff(39,plain,
% 0.63/0.82 (^[S1: $i, S2: $i] : rewrite((~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(40,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> ![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[39])).
% 0.63/0.82 tff(41,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))) <=> ![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(transitivity,[status(thm)],[40, 38])).
% 0.63/0.82 tff(42,plain,
% 0.63/0.82 (^[S1: $i, S2: $i] : trans(monotonicity(rewrite((![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))) <=> (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))), ((((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))) <=> (((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))))), rewrite((((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))) <=> (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))), ((((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))) <=> (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(43,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2)))) <=> ![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[42])).
% 0.63/0.82 tff(44,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2)) <=> ![S1: $i, S2: $i] : (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2))),
% 0.63/0.82 inference(rewrite,[status(thm)],[])).
% 0.63/0.82 tff(45,plain,
% 0.63/0.82 (^[S1: $i, S2: $i] : rewrite((![Ax: $i, C: $i] : (status(Ax, C, S1) => (~status(Ax, C, S2))) <=> nevera(S1, S2)) <=> (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2)))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(46,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (![Ax: $i, C: $i] : (status(Ax, C, S1) => (~status(Ax, C, S2))) <=> nevera(S1, S2)) <=> ![S1: $i, S2: $i] : (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[45])).
% 0.63/0.82 tff(47,axiom,(![S1: $i, S2: $i] : (![Ax: $i, C: $i] : (status(Ax, C, S1) => (~status(Ax, C, S2))) <=> nevera(S1, S2))), file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax','nevera')).
% 0.63/0.82 tff(48,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[47, 46])).
% 0.63/0.82 tff(49,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) <=> nevera(S1, S2))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[48, 44])).
% 0.63/0.82 tff(50,plain,(
% 0.63/0.82 ![S1: $i, S2: $i] : (((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2)) & (![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))),
% 0.63/0.82 inference(skolemize,[status(sab)],[49])).
% 0.63/0.82 tff(51,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[50, 43])).
% 0.63/0.82 tff(52,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~(![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1))) | (~nevera(S1, S2))))))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[51, 41])).
% 0.63/0.82 tff(53,plain,
% 0.63/0.82 (![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[52, 36])).
% 0.63/0.82 tff(54,plain,
% 0.63/0.82 (((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)))))) <=> ((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))))))),
% 0.63/0.82 inference(rewrite,[status(thm)],[])).
% 0.63/0.82 tff(55,plain,
% 0.63/0.82 ((~((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))))) <=> (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)))))),
% 0.63/0.82 inference(rewrite,[status(thm)],[])).
% 0.63/0.82 tff(56,plain,
% 0.63/0.82 (((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns)))))))) <=> ((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))))))),
% 0.63/0.82 inference(monotonicity,[status(thm)],[55])).
% 0.63/0.82 tff(57,plain,
% 0.63/0.82 (((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns)))))))) <=> ((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))))))),
% 0.63/0.82 inference(transitivity,[status(thm)],[56, 54])).
% 0.63/0.82 tff(58,plain,
% 0.63/0.82 ((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns)))))))),
% 0.63/0.82 inference(quant_inst,[status(thm)],[])).
% 0.63/0.82 tff(59,plain,
% 0.63/0.82 ((~![S1: $i, S2: $i] : (~((~((~((~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S2)) | (~status(tptp_fun_Ax_25(S2, S1), tptp_fun_C_24(S2, S1), S1)))) | nevera(S1, S2))) | (~((~nevera(S1, S2)) | ![Ax: $i, C: $i] : ((~status(Ax, C, S2)) | (~status(Ax, C, S1)))))))) | (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)))))),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.63/0.82 tff(60,plain,
% 0.63/0.82 (~((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[59, 53])).
% 0.63/0.82 tff(61,plain,
% 0.63/0.82 (((~((~nevera(uns, thm)) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, uns))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)))) | ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(62,plain,
% 0.63/0.82 ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[61, 60])).
% 0.63/0.82 tff(63,plain,
% 0.63/0.82 ((~nevera(uns, thm)) <=> (~nevera(uns, thm))),
% 0.63/0.82 inference(rewrite,[status(thm)],[])).
% 0.63/0.82 tff(64,axiom,(~nevera(uns, thm)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','nevera_uns_thm')).
% 0.63/0.82 tff(65,plain,
% 0.63/0.82 (~nevera(uns, thm)),
% 0.63/0.82 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.63/0.82 tff(66,plain,
% 0.63/0.82 ((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm)),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(67,plain,
% 0.63/0.82 ((~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))) | nevera(uns, thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[66, 65])).
% 0.63/0.82 tff(68,plain,
% 0.63/0.82 (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[67, 62])).
% 0.63/0.82 tff(69,plain,
% 0.63/0.82 (((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(70,plain,
% 0.63/0.82 (status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[69, 68])).
% 0.63/0.82 tff(71,plain,
% 0.63/0.82 ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(72,plain,
% 0.63/0.82 ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns)) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))))) | (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[71, 70])).
% 0.63/0.82 tff(73,plain,
% 0.63/0.82 (~((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[72, 34])).
% 0.63/0.82 tff(74,plain,
% 0.63/0.82 (((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))) | ![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(75,plain,
% 0.63/0.82 (![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.63/0.82 tff(76,plain,
% 0.63/0.82 ((~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns)))) | model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns)))),
% 0.63/0.82 inference(quant_inst,[status(thm)],[])).
% 0.63/0.82 tff(77,plain,
% 0.63/0.82 (model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns)))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[76, 75])).
% 0.63/0.82 tff(78,plain,
% 0.63/0.82 ((model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)) <=> model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns))) | (~model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns))))),
% 0.63/0.82 inference(tautology,[status(thm)],[])).
% 0.63/0.82 tff(79,plain,
% 0.63/0.82 ((model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)) <=> model(tptp_fun_I1_0(F!29), not(tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[78, 77])).
% 0.63/0.82 tff(80,plain,
% 0.63/0.82 (~model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns))),
% 0.63/0.82 inference(unit_resolution,[status(thm)],[79, 9])).
% 0.63/0.82 tff(81,plain,
% 0.63/0.82 (^[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)))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(82,plain,
% 0.63/0.82 (![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))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[81])).
% 0.63/0.82 tff(83,plain,
% 0.63/0.82 (^[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)))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(84,plain,
% 0.63/0.82 (![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))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[83])).
% 0.63/0.82 tff(85,plain,
% 0.63/0.82 (^[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)))))))),
% 0.63/0.82 inference(bind,[status(th)],[])).
% 0.63/0.82 tff(86,plain,
% 0.63/0.82 (![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))))))),
% 0.63/0.82 inference(quant_intro,[status(thm)],[85])).
% 0.63/0.82 tff(87,plain,
% 0.63/0.82 (![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))))))),
% 0.63/0.83 inference(transitivity,[status(thm)],[86, 84])).
% 0.63/0.83 tff(88,plain,
% 0.63/0.83 (^[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))))))))),
% 0.63/0.83 inference(bind,[status(th)],[])).
% 0.63/0.83 tff(89,plain,
% 0.63/0.83 (![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))))))),
% 0.63/0.83 inference(quant_intro,[status(thm)],[88])).
% 0.63/0.83 tff(90,plain,
% 0.63/0.83 (![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))),
% 0.63/0.83 inference(rewrite,[status(thm)],[])).
% 0.63/0.83 tff(91,plain,
% 0.63/0.83 (^[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)))),
% 0.63/0.83 inference(bind,[status(th)],[])).
% 0.63/0.83 tff(92,plain,
% 0.63/0.83 (![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))),
% 0.63/0.83 inference(quant_intro,[status(thm)],[91])).
% 0.63/0.83 tff(93,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')).
% 0.63/0.83 tff(94,plain,
% 0.63/0.83 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.63/0.83 tff(95,plain,
% 0.63/0.83 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[94, 90])).
% 0.63/0.83 tff(96,plain,(
% 0.63/0.83 ![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))))),
% 0.63/0.83 inference(skolemize,[status(sab)],[95])).
% 0.63/0.83 tff(97,plain,
% 0.63/0.83 (![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))))))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[96, 89])).
% 0.63/0.83 tff(98,plain,
% 0.63/0.83 (![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))))))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[97, 87])).
% 0.63/0.83 tff(99,plain,
% 0.63/0.83 (![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))))))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[98, 82])).
% 0.63/0.83 tff(100,plain,
% 0.63/0.83 (((~![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))))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), 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))))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))))))),
% 0.63/0.83 inference(rewrite,[status(thm)],[])).
% 0.63/0.83 tff(101,plain,
% 0.63/0.83 ((~((~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))))) <=> (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)))))),
% 0.63/0.83 inference(rewrite,[status(thm)],[])).
% 0.63/0.83 tff(102,plain,
% 0.63/0.83 (((~![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(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))))))) <=> ((~![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))))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))))))),
% 0.63/0.83 inference(monotonicity,[status(thm)],[101])).
% 0.63/0.83 tff(103,plain,
% 0.63/0.83 (((~![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(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))))))) <=> ((~![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))))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))))))),
% 0.63/0.83 inference(transitivity,[status(thm)],[102, 100])).
% 0.63/0.83 tff(104,plain,
% 0.63/0.83 ((~![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(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))) | (~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))))))),
% 0.63/0.83 inference(quant_inst,[status(thm)],[])).
% 0.63/0.83 tff(105,plain,
% 0.63/0.83 ((~![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))))))) | (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)))))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[104, 103])).
% 0.63/0.83 tff(106,plain,
% 0.63/0.83 (~((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm))))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[105, 99])).
% 0.63/0.83 tff(107,plain,
% 0.63/0.83 (((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_3(tptp_fun_C_24(thm, uns), tptp_fun_Ax_25(thm, uns)), tptp_fun_C_24(thm, uns)))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)))) | ((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))),
% 0.63/0.83 inference(tautology,[status(thm)],[])).
% 0.63/0.83 tff(108,plain,
% 0.63/0.83 ((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[107, 106])).
% 0.63/0.83 tff(109,plain,
% 0.63/0.83 (((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), uns))) | status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)),
% 0.63/0.83 inference(tautology,[status(thm)],[])).
% 0.63/0.83 tff(110,plain,
% 0.63/0.83 (status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[109, 68])).
% 0.63/0.83 tff(111,plain,
% 0.63/0.83 ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | (~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(tautology,[status(thm)],[])).
% 0.63/0.83 tff(112,plain,
% 0.63/0.83 ((~((~status(tptp_fun_Ax_25(thm, uns), tptp_fun_C_24(thm, uns), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns))))) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[111, 110])).
% 0.63/0.83 tff(113,plain,
% 0.63/0.83 (![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[112, 108])).
% 0.63/0.83 tff(114,plain,
% 0.63/0.83 (((~![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))) | ((~model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)))) <=> ((~![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(rewrite,[status(thm)],[])).
% 0.63/0.83 tff(115,plain,
% 0.63/0.83 ((~![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))) | ((~model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns)))),
% 0.63/0.83 inference(quant_inst,[status(thm)],[])).
% 0.63/0.83 tff(116,plain,
% 0.63/0.83 ((~![I1: $i] : ((~model(I1, tptp_fun_Ax_25(thm, uns))) | model(I1, tptp_fun_C_24(thm, uns)))) | (~model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_0(F!29), tptp_fun_C_24(thm, uns))),
% 0.63/0.83 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.63/0.83 tff(117,plain,
% 0.63/0.83 (~model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[116, 113, 80])).
% 0.63/0.83 tff(118,plain,
% 0.63/0.83 (((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | (~![I2: $i] : model(I2, not(tptp_fun_C_24(thm, uns))))) | ![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))),
% 0.63/0.83 inference(tautology,[status(thm)],[])).
% 0.63/0.83 tff(119,plain,
% 0.63/0.83 (![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[118, 73])).
% 0.63/0.83 tff(120,plain,
% 0.63/0.83 ((~![I1: $i] : model(I1, tptp_fun_Ax_25(thm, uns))) | model(tptp_fun_I1_0(F!29), tptp_fun_Ax_25(thm, uns))),
% 0.63/0.83 inference(quant_inst,[status(thm)],[])).
% 0.63/0.83 tff(121,plain,
% 0.63/0.83 ($false),
% 0.63/0.83 inference(unit_resolution,[status(thm)],[120, 119, 117])).
% 0.63/0.83 % SZS output end Proof
% 0.63/0.84 % E exiting
%------------------------------------------------------------------------------