%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS264+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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 4.16s 4.32s
% Output : Proof 4.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS264+1 : TPTP v9.0.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 19:21:03 EDT 2025
% 0.12/0.33 % CPUTime :
% 4.16/4.32 % SZS status Theorem
% 4.16/4.32 % SZS output start Proof
% 4.16/4.32 tff(model_type, type, (
% 4.16/4.32 model: ( $i * $i ) > $o)).
% 4.16/4.32 tff(not_type, type, (
% 4.16/4.32 not: $i > $i)).
% 4.16/4.32 tff(tptp_fun_C_37_type, type, (
% 4.16/4.32 tptp_fun_C_37: $i)).
% 4.16/4.32 tff(tptp_fun_I1_14_type, type, (
% 4.16/4.32 tptp_fun_I1_14: ( $i * $i ) > $i)).
% 4.16/4.32 tff(tptp_fun_Ax_38_type, type, (
% 4.16/4.32 tptp_fun_Ax_38: $i)).
% 4.16/4.32 tff(status_type, type, (
% 4.16/4.32 status: ( $i * $i * $i ) > $o)).
% 4.16/4.32 tff(csa_type, type, (
% 4.16/4.32 csa: $i)).
% 4.16/4.32 tff(wth_type, type, (
% 4.16/4.32 wth: $i)).
% 4.16/4.32 tff(tptp_fun_I2_7_type, type, (
% 4.16/4.32 tptp_fun_I2_7: ( $i * $i ) > $i)).
% 4.16/4.32 tff(tptp_fun_I3_6_type, type, (
% 4.16/4.32 tptp_fun_I3_6: ( $i * $i ) > $i)).
% 4.16/4.32 tff(tptp_fun_I1_0_type, type, (
% 4.16/4.32 tptp_fun_I1_0: $i > $i)).
% 4.16/4.32 tff(tptp_fun_I4_12_type, type, (
% 4.16/4.32 tptp_fun_I4_12: $i > $i)).
% 4.16/4.32 tff(tptp_fun_I3_40_type, type, (
% 4.16/4.32 tptp_fun_I3_40: $i)).
% 4.16/4.32 tff(tptp_fun_I4_41_type, type, (
% 4.16/4.32 tptp_fun_I4_41: $i)).
% 4.16/4.32 tff(tptp_fun_I1_39_type, type, (
% 4.16/4.32 tptp_fun_I1_39: $i)).
% 4.16/4.32 tff(nota_type, type, (
% 4.16/4.32 nota: ( $i * $i ) > $o)).
% 4.16/4.32 tff(tptp_fun_C_22_type, type, (
% 4.16/4.32 tptp_fun_C_22: ( $i * $i ) > $i)).
% 4.16/4.32 tff(tptp_fun_Ax_23_type, type, (
% 4.16/4.32 tptp_fun_Ax_23: ( $i * $i ) > $i)).
% 4.16/4.32 tff(thm_type, type, (
% 4.16/4.32 thm: $i)).
% 4.16/4.32 tff(tptp_fun_I1_3_type, type, (
% 4.16/4.32 tptp_fun_I1_3: ( $i * $i ) > $i)).
% 4.16/4.32 tff(mighta_type, type, (
% 4.16/4.32 mighta: ( $i * $i ) > $o)).
% 4.16/4.32 tff(tptp_fun_C_18_type, type, (
% 4.16/4.32 tptp_fun_C_18: ( $i * $i ) > $i)).
% 4.16/4.32 tff(tptp_fun_Ax_19_type, type, (
% 4.16/4.32 tptp_fun_Ax_19: ( $i * $i ) > $i)).
% 4.16/4.32 tff(1,plain,
% 4.16/4.32 (^[I: $i, F: $i] : refl((~(model(I, F) <=> model(I, not(F)))) <=> (~(model(I, F) <=> model(I, not(F)))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(2,plain,
% 4.16/4.32 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F)))) <=> ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[1])).
% 4.16/4.32 tff(3,plain,
% 4.16/4.32 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F)))) <=> ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 4.16/4.32 inference(rewrite,[status(thm)],[])).
% 4.16/4.32 tff(4,axiom,(![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax','completeness')).
% 4.16/4.32 tff(5,plain,
% 4.16/4.32 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[4, 3])).
% 4.16/4.32 tff(6,plain,(
% 4.16/4.32 ![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 4.16/4.32 inference(skolemize,[status(sab)],[5])).
% 4.16/4.32 tff(7,plain,
% 4.16/4.32 (![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[6, 2])).
% 4.16/4.32 tff(8,plain,
% 4.16/4.32 ((~![I: $i, F: $i] : (~(model(I, F) <=> model(I, not(F))))) | (~(model(tptp_fun_I1_14(C!37, Ax!38), C!37) <=> model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))),
% 4.16/4.32 inference(quant_inst,[status(thm)],[])).
% 4.16/4.32 tff(9,plain,
% 4.16/4.32 (~(model(tptp_fun_I1_14(C!37, Ax!38), C!37) <=> model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))),
% 4.16/4.32 inference(unit_resolution,[status(thm)],[8, 7])).
% 4.16/4.32 tff(10,assumption,((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37))))))), introduced(assumption)).
% 4.16/4.32 tff(11,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : rewrite((~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))))))))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(12,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[11])).
% 4.16/4.32 tff(13,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : refl((~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(14,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[13])).
% 4.16/4.32 tff(15,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : rewrite((~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(16,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[15])).
% 4.16/4.32 tff(17,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(transitivity,[status(thm)],[16, 14])).
% 4.16/4.32 tff(18,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : trans(monotonicity(trans(monotonicity(quant_intro(proof_bind(^[I3: $i] : trans(monotonicity(rewrite((model(I3, C) & (~model(I3, Ax))) <=> (~((~model(I3, C)) | model(I3, Ax)))), ((~(model(I3, C) & (~model(I3, Ax)))) <=> (~(~((~model(I3, C)) | model(I3, Ax)))))), rewrite((~(~((~model(I3, C)) | model(I3, Ax)))) <=> ((~model(I3, C)) | model(I3, Ax))), ((~(model(I3, C) & (~model(I3, Ax)))) <=> ((~model(I3, C)) | model(I3, Ax))))), (![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) <=> ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))), ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) <=> (status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C)))), rewrite((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C)) <=> (status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))), ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) <=> (status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax))))), rewrite(((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C)))) <=> ((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))), (((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C))))) <=> ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax))) & ((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))))), rewrite(((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax))) & ((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)))))) <=> (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))), (((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C))))) <=> (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(19,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[18])).
% 4.16/4.32 tff(20,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : rewrite((((![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) | status(Ax, C, wth)) & ((model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & (model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax))) & (~model(tptp_fun_I4_12(C), C))) | (~status(Ax, C, wth)))) <=> ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C))))))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(21,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (((![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) | status(Ax, C, wth)) & ((model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & (model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax))) & (~model(tptp_fun_I4_12(C), C))) | (~status(Ax, C, wth)))) <=> ![Ax: $i, C: $i] : ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C)))))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[20])).
% 4.16/4.32 tff(22,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth)) <=> ![Ax: $i, C: $i] : ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth))),
% 4.16/4.32 inference(rewrite,[status(thm)],[])).
% 4.16/4.32 tff(23,plain,
% 4.16/4.32 (^[Ax: $i, C: $i] : rewrite(((((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax)))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth)) <=> ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth)))),
% 4.16/4.32 inference(bind,[status(th)],[])).
% 4.16/4.32 tff(24,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax)))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth)) <=> ![Ax: $i, C: $i] : ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth))),
% 4.16/4.32 inference(quant_intro,[status(thm)],[23])).
% 4.16/4.32 tff(25,axiom,(![Ax: $i, C: $i] : ((((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax)))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax','wth')).
% 4.16/4.32 tff(26,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[25, 24])).
% 4.16/4.32 tff(27,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : (model(I3, C) & (~model(I3, Ax))) & ?[I4: $i] : (~model(I4, C))) <=> status(Ax, C, wth))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[26, 22])).
% 4.16/4.32 tff(28,plain,(
% 4.16/4.32 ![Ax: $i, C: $i] : (((![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) | status(Ax, C, wth)) & ((model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & (model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax))) & (~model(tptp_fun_I4_12(C), C))) | (~status(Ax, C, wth))))),
% 4.16/4.32 inference(skolemize,[status(sab)],[27])).
% 4.16/4.32 tff(29,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : ((status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I3: $i] : (~(model(I3, C) & (~model(I3, Ax)))) | ![I4: $i] : model(I4, C)) & ((~status(Ax, C, wth)) | (model(tptp_fun_I1_0(Ax), Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & model(tptp_fun_I3_6(C, Ax), C) & (~model(tptp_fun_I3_6(C, Ax), Ax)) & (~model(tptp_fun_I4_12(C), C)))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[28, 21])).
% 4.16/4.32 tff(30,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[29, 19])).
% 4.16/4.32 tff(31,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | ![I1: $i] : (~model(I1, Ax)) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I4: $i] : model(I4, C) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C))))))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[30, 17])).
% 4.16/4.32 tff(32,plain,
% 4.16/4.32 (![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))),
% 4.16/4.32 inference(modus_ponens,[status(thm)],[31, 12])).
% 4.16/4.32 tff(33,plain,
% 4.16/4.32 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)))))))))),
% 4.16/4.32 inference(rewrite,[status(thm)],[])).
% 4.16/4.32 tff(34,plain,
% 4.16/4.32 ((~((~(status(Ax!38, C!37, wth) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I1: $i] : (~model(I1, Ax!38)) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | ![I4: $i] : model(I4, C!37))) | (~((~status(Ax!38, C!37, wth)) | (~(model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)) | (~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))))))))) <=> (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37))))))))),
% 4.16/4.32 inference(rewrite,[status(thm)],[])).
% 4.16/4.32 tff(35,plain,
% 4.16/4.32 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(Ax!38, C!37, wth) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I1: $i] : (~model(I1, Ax!38)) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | ![I4: $i] : model(I4, C!37))) | (~((~status(Ax!38, C!37, wth)) | (~(model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)) | (~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)))))))))),
% 4.16/4.32 inference(monotonicity,[status(thm)],[34])).
% 4.16/4.32 tff(36,plain,
% 4.16/4.32 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(Ax!38, C!37, wth) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I1: $i] : (~model(I1, Ax!38)) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | ![I4: $i] : model(I4, C!37))) | (~((~status(Ax!38, C!37, wth)) | (~(model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)) | (~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)))))))))),
% 4.16/4.33 inference(transitivity,[status(thm)],[35, 33])).
% 4.16/4.33 tff(37,plain,
% 4.16/4.33 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(Ax!38, C!37, wth) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I1: $i] : (~model(I1, Ax!38)) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | ![I4: $i] : model(I4, C!37))) | (~((~status(Ax!38, C!37, wth)) | (~(model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)) | (~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)))))))))),
% 4.16/4.33 inference(quant_inst,[status(thm)],[])).
% 4.16/4.33 tff(38,plain,
% 4.16/4.33 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37))))))))),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[37, 36])).
% 4.16/4.33 tff(39,plain,
% 4.16/4.33 ($false),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[38, 32, 10])).
% 4.16/4.33 tff(40,plain,(~((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37)))))))), inference(lemma,lemma(discharge,[]))).
% 4.16/4.33 tff(41,plain,
% 4.16/4.33 (((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | (~((~status(Ax!38, C!37, wth)) | (~((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | model(tptp_fun_I4_12(C!37), C!37) | (~model(tptp_fun_I1_0(Ax!38), Ax!38)) | model(tptp_fun_I3_6(C!37, Ax!38), Ax!38) | (~model(tptp_fun_I3_6(C!37, Ax!38), C!37))))))) | (![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))),
% 4.16/4.33 inference(tautology,[status(thm)],[])).
% 4.16/4.33 tff(42,plain,
% 4.16/4.33 (![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth)),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[41, 40])).
% 4.16/4.33 tff(43,assumption,(![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))), introduced(assumption)).
% 4.16/4.33 tff(44,plain,
% 4.16/4.33 ((model(I1!39, Ax!38) & ![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)) & ((~model(I3!40, Ax!38)) & model(I3!40, C!37)) & (~model(I4!41, C!37))) <=> (model(I1!39, Ax!38) & ![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)) & (~model(I3!40, Ax!38)) & model(I3!40, C!37) & (~model(I4!41, C!37)))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(45,plain,
% 4.16/4.33 (?[Ax: $i, C: $i] : (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C))) <=> ?[Ax: $i, C: $i] : (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(46,plain,
% 4.16/4.33 (^[Ax: $i, C: $i] : trans(monotonicity(trans(monotonicity(rewrite((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) <=> (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))), (((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) <=> ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))))), rewrite(((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) <=> (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)))), (((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) <=> (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))))), ((((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C))) <=> ((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C))))), rewrite(((?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C))) <=> (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))), ((((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C))) <=> (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))))),
% 4.16/4.33 inference(bind,[status(th)],[])).
% 4.16/4.33 tff(47,plain,
% 4.16/4.33 (?[Ax: $i, C: $i] : (((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C))) <=> ?[Ax: $i, C: $i] : (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))),
% 4.16/4.33 inference(quant_intro,[status(thm)],[46])).
% 4.16/4.33 tff(48,axiom,(?[Ax: $i, C: $i] : (((?[I1: $i] : model(I1, Ax) & ![I2: $i] : (model(I2, Ax) => model(I2, C))) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C))) & ?[I4: $i] : (~model(I4, C)))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax','mixed_pair')).
% 4.16/4.33 tff(49,plain,
% 4.16/4.33 (?[Ax: $i, C: $i] : (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[48, 47])).
% 4.16/4.33 tff(50,plain,
% 4.16/4.33 (?[Ax: $i, C: $i] : (?[I1: $i] : model(I1, Ax) & ![I2: $i] : ((~model(I2, Ax)) | model(I2, C)) & ?[I3: $i] : ((~model(I3, Ax)) & model(I3, C)) & ?[I4: $i] : (~model(I4, C)))),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[49, 45])).
% 4.16/4.33 tff(51,plain,
% 4.16/4.33 (model(I1!39, Ax!38) & ![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)) & (~model(I3!40, Ax!38)) & model(I3!40, C!37) & (~model(I4!41, C!37))),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[50, 44])).
% 4.16/4.33 tff(52,plain,
% 4.16/4.33 (model(I3!40, C!37)),
% 4.16/4.33 inference(and_elim,[status(thm)],[51])).
% 4.16/4.33 tff(53,plain,
% 4.16/4.33 (~model(I3!40, Ax!38)),
% 4.16/4.33 inference(and_elim,[status(thm)],[51])).
% 4.16/4.33 tff(54,plain,
% 4.16/4.33 (((~![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))) | ((~model(I3!40, C!37)) | model(I3!40, Ax!38))) <=> ((~![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))) | (~model(I3!40, C!37)) | model(I3!40, Ax!38))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(55,plain,
% 4.16/4.33 ((~![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))) | ((~model(I3!40, C!37)) | model(I3!40, Ax!38))),
% 4.16/4.33 inference(quant_inst,[status(thm)],[])).
% 4.16/4.33 tff(56,plain,
% 4.16/4.33 ((~![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))) | (~model(I3!40, C!37)) | model(I3!40, Ax!38)),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[55, 54])).
% 4.16/4.33 tff(57,plain,
% 4.16/4.33 ($false),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[56, 53, 52, 43])).
% 4.16/4.33 tff(58,plain,(~![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38))), inference(lemma,lemma(discharge,[]))).
% 4.16/4.33 tff(59,assumption,(~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))), introduced(assumption)).
% 4.16/4.33 tff(60,plain,
% 4.16/4.33 (((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37)) | (~model(tptp_fun_I2_7(C!37, Ax!38), C!37))),
% 4.16/4.33 inference(tautology,[status(thm)],[])).
% 4.16/4.33 tff(61,plain,
% 4.16/4.33 (~model(tptp_fun_I2_7(C!37, Ax!38), C!37)),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[60, 59])).
% 4.16/4.33 tff(62,plain,
% 4.16/4.33 (((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37)) | model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)),
% 4.16/4.33 inference(tautology,[status(thm)],[])).
% 4.16/4.33 tff(63,plain,
% 4.16/4.33 (model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[62, 59])).
% 4.16/4.33 tff(64,plain,
% 4.16/4.33 (^[I2: $i] : refl(((~model(I2, Ax!38)) | model(I2, C!37)) <=> ((~model(I2, Ax!38)) | model(I2, C!37)))),
% 4.16/4.33 inference(bind,[status(th)],[])).
% 4.16/4.33 tff(65,plain,
% 4.16/4.33 (![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37)) <=> ![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))),
% 4.16/4.33 inference(quant_intro,[status(thm)],[64])).
% 4.16/4.33 tff(66,plain,
% 4.16/4.33 (![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))),
% 4.16/4.33 inference(and_elim,[status(thm)],[51])).
% 4.16/4.33 tff(67,plain,
% 4.16/4.33 (![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[66, 65])).
% 4.16/4.33 tff(68,plain,
% 4.16/4.33 (((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | ((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) <=> ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | (~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(69,plain,
% 4.16/4.33 ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | ((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))),
% 4.16/4.33 inference(quant_inst,[status(thm)],[])).
% 4.16/4.33 tff(70,plain,
% 4.16/4.33 ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | (~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37)),
% 4.16/4.33 inference(modus_ponens,[status(thm)],[69, 68])).
% 4.16/4.33 tff(71,plain,
% 4.16/4.33 ($false),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[70, 67, 63, 61])).
% 4.16/4.33 tff(72,plain,((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37)), inference(lemma,lemma(discharge,[]))).
% 4.16/4.33 tff(73,assumption,(![I4: $i] : model(I4, C!37)), introduced(assumption)).
% 4.16/4.33 tff(74,plain,
% 4.16/4.33 (~model(I4!41, C!37)),
% 4.16/4.33 inference(and_elim,[status(thm)],[51])).
% 4.16/4.33 tff(75,plain,
% 4.16/4.33 ((~![I4: $i] : model(I4, C!37)) | model(I4!41, C!37)),
% 4.16/4.33 inference(quant_inst,[status(thm)],[])).
% 4.16/4.33 tff(76,plain,
% 4.16/4.33 ($false),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[75, 74, 73])).
% 4.16/4.33 tff(77,plain,(~![I4: $i] : model(I4, C!37)), inference(lemma,lemma(discharge,[]))).
% 4.16/4.33 tff(78,assumption,(![I1: $i] : (~model(I1, Ax!38))), introduced(assumption)).
% 4.16/4.33 tff(79,plain,
% 4.16/4.33 (model(I1!39, Ax!38)),
% 4.16/4.33 inference(and_elim,[status(thm)],[51])).
% 4.16/4.33 tff(80,plain,
% 4.16/4.33 ((~![I1: $i] : (~model(I1, Ax!38))) | (~model(I1!39, Ax!38))),
% 4.16/4.33 inference(quant_inst,[status(thm)],[])).
% 4.16/4.33 tff(81,plain,
% 4.16/4.33 ($false),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[80, 79, 78])).
% 4.16/4.33 tff(82,plain,(~![I1: $i] : (~model(I1, Ax!38))), inference(lemma,lemma(discharge,[]))).
% 4.16/4.33 tff(83,plain,
% 4.16/4.33 ((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | ![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth)),
% 4.16/4.33 inference(tautology,[status(thm)],[])).
% 4.16/4.33 tff(84,plain,
% 4.16/4.33 ((~(![I1: $i] : (~model(I1, Ax!38)) | ![I4: $i] : model(I4, C!37) | (~((~model(tptp_fun_I2_7(C!37, Ax!38), Ax!38)) | model(tptp_fun_I2_7(C!37, Ax!38), C!37))) | ![I3: $i] : ((~model(I3, C!37)) | model(I3, Ax!38)) | status(Ax!38, C!37, wth))) | status(Ax!38, C!37, wth)),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[83, 82, 77, 72, 58])).
% 4.16/4.33 tff(85,plain,
% 4.16/4.33 (status(Ax!38, C!37, wth)),
% 4.16/4.33 inference(unit_resolution,[status(thm)],[84, 42])).
% 4.16/4.33 tff(86,assumption,(status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)), introduced(assumption)).
% 4.16/4.33 tff(87,plain,
% 4.16/4.33 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))))))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(88,plain,
% 4.16/4.33 ((~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~(model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))))))))) <=> (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))))))),
% 4.16/4.33 inference(rewrite,[status(thm)],[])).
% 4.16/4.33 tff(89,plain,
% 4.16/4.33 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~(model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth))))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))))))),
% 4.16/4.33 inference(monotonicity,[status(thm)],[88])).
% 4.16/4.33 tff(90,plain,
% 4.16/4.33 (((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~(model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth))))))))))) <=> ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))))))),
% 4.16/4.34 inference(transitivity,[status(thm)],[89, 87])).
% 4.16/4.34 tff(91,plain,
% 4.16/4.34 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~(model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth))))))))))),
% 4.16/4.34 inference(quant_inst,[status(thm)],[])).
% 4.16/4.34 tff(92,plain,
% 4.16/4.34 ((~![Ax: $i, C: $i] : (~((~(status(Ax, C, wth) | (~((~model(tptp_fun_I2_7(C, Ax), Ax)) | model(tptp_fun_I2_7(C, Ax), C))) | ![I1: $i] : (~model(I1, Ax)) | ![I3: $i] : ((~model(I3, C)) | model(I3, Ax)) | ![I4: $i] : model(I4, C))) | (~((~status(Ax, C, wth)) | (~(model(tptp_fun_I3_6(C, Ax), Ax) | model(tptp_fun_I4_12(C), C) | (~model(tptp_fun_I1_0(Ax), Ax)) | (~model(tptp_fun_I3_6(C, Ax), C)) | (~![I2: $i] : ((~model(I2, Ax)) | model(I2, C)))))))))) | (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))))))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[91, 90])).
% 4.16/4.34 tff(93,plain,
% 4.16/4.34 (~((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[92, 32])).
% 4.16/4.34 tff(94,plain,
% 4.16/4.34 (((~(status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth) | ![I4: $i] : model(I4, tptp_fun_C_22(thm, wth)) | ![I3: $i] : ((~model(I3, tptp_fun_C_22(thm, wth))) | model(I3, tptp_fun_Ax_23(thm, wth))) | ![I1: $i] : (~model(I1, tptp_fun_Ax_23(thm, wth))) | (~((~model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I2_7(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))))) | ((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(95,plain,
% 4.16/4.34 ((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[94, 93])).
% 4.16/4.34 tff(96,assumption,(~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))), introduced(assumption)).
% 4.16/4.34 tff(97,plain,
% 4.16/4.34 (((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(98,plain,
% 4.16/4.34 (status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[97, 96])).
% 4.16/4.34 tff(99,plain,
% 4.16/4.34 ((~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))) | (~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(100,plain,
% 4.16/4.34 ((~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))))) | (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[99, 98])).
% 4.16/4.34 tff(101,plain,
% 4.16/4.34 (~((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth)))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[100, 95])).
% 4.16/4.34 tff(102,plain,
% 4.16/4.34 (((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_0(tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I4_12(tptp_fun_C_22(thm, wth)), tptp_fun_C_22(thm, wth)) | model(tptp_fun_I3_6(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | ![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(103,plain,
% 4.16/4.34 (![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[102, 101])).
% 4.16/4.34 tff(104,plain,
% 4.16/4.34 (^[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)))))))),
% 4.16/4.34 inference(bind,[status(th)],[])).
% 4.16/4.34 tff(105,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(quant_intro,[status(thm)],[104])).
% 4.16/4.34 tff(106,plain,
% 4.16/4.34 (^[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)))))))),
% 4.16/4.34 inference(bind,[status(th)],[])).
% 4.16/4.34 tff(107,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(quant_intro,[status(thm)],[106])).
% 4.16/4.34 tff(108,plain,
% 4.16/4.34 (^[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)))))))),
% 4.16/4.34 inference(bind,[status(th)],[])).
% 4.16/4.34 tff(109,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(quant_intro,[status(thm)],[108])).
% 4.16/4.34 tff(110,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(transitivity,[status(thm)],[109, 107])).
% 4.16/4.34 tff(111,plain,
% 4.16/4.34 (^[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))))))))),
% 4.16/4.34 inference(bind,[status(th)],[])).
% 4.16/4.34 tff(112,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(quant_intro,[status(thm)],[111])).
% 4.16/4.34 tff(113,plain,
% 4.16/4.34 (![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))),
% 4.16/4.34 inference(rewrite,[status(thm)],[])).
% 4.16/4.34 tff(114,plain,
% 4.16/4.34 (^[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)))),
% 4.16/4.34 inference(bind,[status(th)],[])).
% 4.16/4.34 tff(115,plain,
% 4.16/4.34 (![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))),
% 4.16/4.34 inference(quant_intro,[status(thm)],[114])).
% 4.16/4.34 tff(116,axiom,(![Ax: $i, C: $i] : (![I1: $i] : (model(I1, Ax) => model(I1, C)) <=> status(Ax, C, thm))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax','thm')).
% 4.16/4.34 tff(117,plain,
% 4.16/4.34 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[116, 115])).
% 4.16/4.34 tff(118,plain,
% 4.16/4.34 (![Ax: $i, C: $i] : (![I1: $i] : ((~model(I1, Ax)) | model(I1, C)) <=> status(Ax, C, thm))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[117, 113])).
% 4.16/4.34 tff(119,plain,(
% 4.16/4.34 ![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))))),
% 4.16/4.34 inference(skolemize,[status(sab)],[118])).
% 4.16/4.34 tff(120,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[119, 112])).
% 4.16/4.34 tff(121,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[120, 110])).
% 4.16/4.34 tff(122,plain,
% 4.16/4.34 (![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))))))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[121, 105])).
% 4.16/4.34 tff(123,plain,
% 4.16/4.34 (((~![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_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), 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_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))))),
% 4.16/4.34 inference(rewrite,[status(thm)],[])).
% 4.16/4.34 tff(124,plain,
% 4.16/4.34 ((~((~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))))) <=> (~((~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))))),
% 4.16/4.34 inference(rewrite,[status(thm)],[])).
% 4.16/4.34 tff(125,plain,
% 4.16/4.34 (((~![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_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth)))))))) <=> ((~![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_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))))),
% 4.16/4.34 inference(monotonicity,[status(thm)],[124])).
% 4.16/4.34 tff(126,plain,
% 4.16/4.34 (((~![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_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth)))))))) <=> ((~![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_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))))),
% 4.16/4.34 inference(transitivity,[status(thm)],[125, 123])).
% 4.16/4.34 tff(127,plain,
% 4.16/4.34 ((~![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_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth)))))))),
% 4.16/4.34 inference(quant_inst,[status(thm)],[])).
% 4.16/4.34 tff(128,plain,
% 4.16/4.34 ((~![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_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[127, 126])).
% 4.16/4.34 tff(129,plain,
% 4.16/4.34 (~((~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[128, 122])).
% 4.16/4.34 tff(130,plain,
% 4.16/4.34 (((~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | ![I1: $i] : ((~model(I1, tptp_fun_Ax_23(thm, wth))) | model(I1, tptp_fun_C_22(thm, wth))))) | (~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))) | ((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(131,plain,
% 4.16/4.34 ((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[130, 129])).
% 4.16/4.34 tff(132,plain,
% 4.16/4.34 (((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)) | (~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(133,plain,
% 4.16/4.34 (~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[132, 96])).
% 4.16/4.34 tff(134,plain,
% 4.16/4.34 ((~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(135,plain,
% 4.16/4.34 ((~((~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))) | (~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[134, 133])).
% 4.16/4.34 tff(136,plain,
% 4.16/4.34 (~((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[135, 131])).
% 4.16/4.34 tff(137,plain,
% 4.16/4.34 (((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | (~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(138,plain,
% 4.16/4.34 (~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[137, 136])).
% 4.16/4.34 tff(139,plain,
% 4.16/4.34 (((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))),
% 4.16/4.34 inference(tautology,[status(thm)],[])).
% 4.16/4.34 tff(140,plain,
% 4.16/4.34 (model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[139, 136])).
% 4.16/4.34 tff(141,plain,
% 4.16/4.34 (((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | ((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))) <=> ((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(rewrite,[status(thm)],[])).
% 4.16/4.34 tff(142,plain,
% 4.16/4.34 ((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | ((~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth)))),
% 4.16/4.34 inference(quant_inst,[status(thm)],[])).
% 4.16/4.34 tff(143,plain,
% 4.16/4.34 ((~![I2: $i] : ((~model(I2, tptp_fun_Ax_23(thm, wth))) | model(I2, tptp_fun_C_22(thm, wth)))) | (~model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_Ax_23(thm, wth))) | model(tptp_fun_I1_3(tptp_fun_C_22(thm, wth), tptp_fun_Ax_23(thm, wth)), tptp_fun_C_22(thm, wth))),
% 4.16/4.34 inference(modus_ponens,[status(thm)],[142, 141])).
% 4.16/4.34 tff(144,plain,
% 4.16/4.34 ($false),
% 4.16/4.34 inference(unit_resolution,[status(thm)],[143, 140, 138, 103])).
% 4.16/4.34 tff(145,plain,((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)), inference(lemma,lemma(discharge,[]))).
% 4.16/4.34 tff(146,plain,
% 4.16/4.34 (^[S1: $i, S2: $i] : refl((~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))) <=> (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(147,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))) <=> ![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[146])).
% 4.16/4.35 tff(148,plain,
% 4.16/4.35 (^[S1: $i, S2: $i] : rewrite((~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))) <=> (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(149,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))) <=> ![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[148])).
% 4.16/4.35 tff(150,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))) <=> ![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(transitivity,[status(thm)],[149, 147])).
% 4.16/4.35 tff(151,plain,
% 4.16/4.35 (^[S1: $i, S2: $i] : trans(monotonicity(rewrite((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) <=> (nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))), trans(monotonicity(rewrite((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) <=> (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))), (((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))) <=> ((~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))))), rewrite(((~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))) <=> ((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))), (((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))) <=> ((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))), (((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))) <=> ((nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2))) & ((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))))), rewrite(((nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2))) & ((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))))) <=> (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))), (((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))) <=> (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(152,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : ((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))) <=> ![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[151])).
% 4.16/4.35 tff(153,plain,
% 4.16/4.35 (^[S1: $i, S2: $i] : rewrite(((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2)))) | nota(S1, S2)) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))) <=> ((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(154,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : ((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2)))) | nota(S1, S2)) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2)))) <=> ![S1: $i, S2: $i] : ((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[153])).
% 4.16/4.35 tff(155,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & (~status(Ax, C, S2))) <=> nota(S1, S2)) <=> ![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & (~status(Ax, C, S2))) <=> nota(S1, S2))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(156,axiom,(![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & (~status(Ax, C, S2))) <=> nota(S1, S2))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax','nota')).
% 4.16/4.35 tff(157,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & (~status(Ax, C, S2))) <=> nota(S1, S2))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[156, 155])).
% 4.16/4.35 tff(158,plain,(
% 4.16/4.35 ![S1: $i, S2: $i] : ((![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2)))) | nota(S1, S2)) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))))),
% 4.16/4.35 inference(skolemize,[status(sab)],[157])).
% 4.16/4.35 tff(159,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : ((nota(S1, S2) | ![Ax: $i, C: $i] : (~(status(Ax, C, S1) & (~status(Ax, C, S2))))) & ((status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1) & (~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2))) | (~nota(S1, S2))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[158, 154])).
% 4.16/4.35 tff(160,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[159, 152])).
% 4.16/4.35 tff(161,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[160, 150])).
% 4.16/4.35 tff(162,plain,
% 4.16/4.35 ((~![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))) | (~((~(nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))) | (~((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))))))),
% 4.16/4.35 inference(quant_inst,[status(thm)],[])).
% 4.16/4.35 tff(163,plain,
% 4.16/4.35 (~((~(nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))) | (~((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[162, 161])).
% 4.16/4.35 tff(164,plain,
% 4.16/4.35 (((~(nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))) | (~((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))))) | ((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(165,plain,
% 4.16/4.35 ((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[164, 163])).
% 4.16/4.35 tff(166,plain,
% 4.16/4.35 ((~((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm))))) | (~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(167,plain,
% 4.16/4.35 ((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[166, 165])).
% 4.16/4.35 tff(168,plain,
% 4.16/4.35 (~nota(wth, thm)),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[167, 145])).
% 4.16/4.35 tff(169,plain,
% 4.16/4.35 (((~(nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))) | (~((~nota(wth, thm)) | (~((~status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), wth)) | status(tptp_fun_Ax_23(thm, wth), tptp_fun_C_22(thm, wth), thm)))))) | (nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(170,plain,
% 4.16/4.35 (nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[169, 163])).
% 4.16/4.35 tff(171,plain,
% 4.16/4.35 ((~(nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm)))) | nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(172,plain,
% 4.16/4.35 (nota(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[171, 170])).
% 4.16/4.35 tff(173,plain,
% 4.16/4.35 (![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[172, 168])).
% 4.16/4.35 tff(174,plain,
% 4.16/4.35 (((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))) | ((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(175,plain,
% 4.16/4.35 ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))) | ((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm))),
% 4.16/4.35 inference(quant_inst,[status(thm)],[])).
% 4.16/4.35 tff(176,plain,
% 4.16/4.35 ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, thm))) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[175, 174])).
% 4.16/4.35 tff(177,plain,
% 4.16/4.35 (status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[176, 173, 86])).
% 4.16/4.35 tff(178,plain,
% 4.16/4.35 (^[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)))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(179,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[178])).
% 4.16/4.35 tff(180,plain,
% 4.16/4.35 (^[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)))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(181,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[180])).
% 4.16/4.35 tff(182,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(transitivity,[status(thm)],[181, 179])).
% 4.16/4.35 tff(183,plain,
% 4.16/4.35 (^[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))))))))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(184,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[183])).
% 4.16/4.35 tff(185,plain,
% 4.16/4.35 (^[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)))))),
% 4.16/4.35 inference(bind,[status(th)],[])).
% 4.16/4.35 tff(186,plain,
% 4.16/4.35 (![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))))),
% 4.16/4.35 inference(quant_intro,[status(thm)],[185])).
% 4.16/4.35 tff(187,plain,
% 4.16/4.35 (![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))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(188,axiom,(![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax','mighta')).
% 4.16/4.35 tff(189,plain,
% 4.16/4.35 (![S1: $i, S2: $i] : (?[Ax: $i, C: $i] : (status(Ax, C, S1) & status(Ax, C, S2)) <=> mighta(S1, S2))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[188, 187])).
% 4.16/4.35 tff(190,plain,(
% 4.16/4.35 ![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))))),
% 4.16/4.35 inference(skolemize,[status(sab)],[189])).
% 4.16/4.35 tff(191,plain,
% 4.16/4.35 (![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))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[190, 186])).
% 4.16/4.35 tff(192,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[191, 184])).
% 4.16/4.35 tff(193,plain,
% 4.16/4.35 (![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))))))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[192, 182])).
% 4.16/4.35 tff(194,plain,
% 4.16/4.35 (((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth))))))))) <=> ((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)))))))))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(195,plain,
% 4.16/4.35 ((~((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)))))))) <=> (~((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth))))))))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(196,plain,
% 4.16/4.35 (((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm))))))))) <=> ((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)))))))))),
% 4.16/4.35 inference(monotonicity,[status(thm)],[195])).
% 4.16/4.35 tff(197,plain,
% 4.16/4.35 (((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm))))))))) <=> ((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)))))))))),
% 4.16/4.35 inference(transitivity,[status(thm)],[196, 194])).
% 4.16/4.35 tff(198,plain,
% 4.16/4.35 ((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm))))))))),
% 4.16/4.35 inference(quant_inst,[status(thm)],[])).
% 4.16/4.35 tff(199,plain,
% 4.16/4.35 ((~![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(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth))))))))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[198, 197])).
% 4.16/4.35 tff(200,plain,
% 4.16/4.35 (~((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth)))))))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[199, 193])).
% 4.16/4.35 tff(201,plain,
% 4.16/4.35 (((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | (~((~mighta(wth, thm)) | (~((~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), thm)) | (~status(tptp_fun_Ax_19(thm, wth), tptp_fun_C_18(thm, wth), wth))))))) | (mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(202,plain,
% 4.16/4.35 (mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[201, 200])).
% 4.16/4.35 tff(203,plain,
% 4.16/4.35 ((~mighta(wth, thm)) <=> (~mighta(wth, thm))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(204,axiom,(~mighta(wth, thm)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mighta_wth_thm')).
% 4.16/4.35 tff(205,plain,
% 4.16/4.35 (~mighta(wth, thm)),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[204, 203])).
% 4.16/4.35 tff(206,plain,
% 4.16/4.35 ((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(207,plain,
% 4.16/4.35 ((~(mighta(wth, thm) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth))))) | ![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[206, 205])).
% 4.16/4.35 tff(208,plain,
% 4.16/4.35 (![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[207, 202])).
% 4.16/4.35 tff(209,plain,
% 4.16/4.35 (((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))) | ((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)))),
% 4.16/4.35 inference(rewrite,[status(thm)],[])).
% 4.16/4.35 tff(210,plain,
% 4.16/4.35 ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))) | ((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)))),
% 4.16/4.35 inference(quant_inst,[status(thm)],[])).
% 4.16/4.35 tff(211,plain,
% 4.16/4.35 ((~![Ax: $i, C: $i] : ((~status(Ax, C, thm)) | (~status(Ax, C, wth)))) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), thm)) | (~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth))),
% 4.16/4.35 inference(modus_ponens,[status(thm)],[210, 209])).
% 4.16/4.35 tff(212,plain,
% 4.16/4.35 ($false),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[211, 208, 86, 177])).
% 4.16/4.35 tff(213,plain,(~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)), inference(lemma,lemma(discharge,[]))).
% 4.16/4.35 tff(214,plain,
% 4.16/4.35 (((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(215,plain,
% 4.16/4.35 ((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[214, 213])).
% 4.16/4.35 tff(216,plain,
% 4.16/4.35 ((~![S1: $i, S2: $i] : (~((~(nota(S1, S2) | ![Ax: $i, C: $i] : ((~status(Ax, C, S1)) | status(Ax, C, S2)))) | (~((~nota(S1, S2)) | (~((~status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S1)) | status(tptp_fun_Ax_23(S2, S1), tptp_fun_C_22(S2, S1), S2)))))))) | (~((~(nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))) | (~((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))))))),
% 4.16/4.35 inference(quant_inst,[status(thm)],[])).
% 4.16/4.35 tff(217,plain,
% 4.16/4.35 (~((~(nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))) | (~((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa))))))),
% 4.16/4.35 inference(unit_resolution,[status(thm)],[216, 161])).
% 4.16/4.35 tff(218,plain,
% 4.16/4.35 (((~(nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))) | (~((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))))) | ((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa))))),
% 4.16/4.35 inference(tautology,[status(thm)],[])).
% 4.16/4.35 tff(219,plain,
% 4.16/4.35 ((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[218, 217])).
% 4.16/4.36 tff(220,plain,
% 4.16/4.36 ((~((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa))))) | (~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(221,plain,
% 4.16/4.36 ((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[220, 219])).
% 4.16/4.36 tff(222,plain,
% 4.16/4.36 (~nota(wth, csa)),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[221, 215])).
% 4.16/4.36 tff(223,plain,
% 4.16/4.36 (((~(nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))) | (~((~nota(wth, csa)) | (~((~status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), wth)) | status(tptp_fun_Ax_23(csa, wth), tptp_fun_C_22(csa, wth), csa)))))) | (nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(224,plain,
% 4.16/4.36 (nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[223, 217])).
% 4.16/4.36 tff(225,plain,
% 4.16/4.36 ((~(nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa)))) | nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(226,plain,
% 4.16/4.36 (nota(wth, csa) | ![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[225, 224])).
% 4.16/4.36 tff(227,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[226, 222])).
% 4.16/4.36 tff(228,assumption,(~status(Ax!38, C!37, csa)), introduced(assumption)).
% 4.16/4.36 tff(229,plain,
% 4.16/4.36 (((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))) | ((~status(Ax!38, C!37, wth)) | status(Ax!38, C!37, csa))) <=> ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))) | (~status(Ax!38, C!37, wth)) | status(Ax!38, C!37, csa))),
% 4.16/4.36 inference(rewrite,[status(thm)],[])).
% 4.16/4.36 tff(230,plain,
% 4.16/4.36 ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))) | ((~status(Ax!38, C!37, wth)) | status(Ax!38, C!37, csa))),
% 4.16/4.36 inference(quant_inst,[status(thm)],[])).
% 4.16/4.36 tff(231,plain,
% 4.16/4.36 ((~![Ax: $i, C: $i] : ((~status(Ax, C, wth)) | status(Ax, C, csa))) | (~status(Ax!38, C!37, wth)) | status(Ax!38, C!37, csa)),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[230, 229])).
% 4.16/4.36 tff(232,plain,
% 4.16/4.36 ($false),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[231, 228, 227, 85])).
% 4.16/4.36 tff(233,plain,(status(Ax!38, C!37, csa)), inference(lemma,lemma(discharge,[]))).
% 4.16/4.36 tff(234,plain,
% 4.16/4.36 (^[Ax: $i, C: $i] : rewrite((~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> (~((~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))) | (~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))))))),
% 4.16/4.36 inference(bind,[status(th)],[])).
% 4.16/4.36 tff(235,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))) | (~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C))))))))),
% 4.16/4.36 inference(quant_intro,[status(thm)],[234])).
% 4.16/4.36 tff(236,plain,
% 4.16/4.36 (^[Ax: $i, C: $i] : refl((~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))))),
% 4.16/4.36 inference(bind,[status(th)],[])).
% 4.16/4.36 tff(237,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(quant_intro,[status(thm)],[236])).
% 4.16/4.36 tff(238,plain,
% 4.16/4.36 (^[Ax: $i, C: $i] : rewrite((~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))))),
% 4.16/4.36 inference(bind,[status(th)],[])).
% 4.16/4.36 tff(239,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(quant_intro,[status(thm)],[238])).
% 4.16/4.36 tff(240,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(transitivity,[status(thm)],[239, 237])).
% 4.16/4.36 tff(241,plain,
% 4.16/4.36 (^[Ax: $i, C: $i] : trans(monotonicity(rewrite((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) <=> (status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))), trans(monotonicity(rewrite((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) <=> (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))), (((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa))) <=> ((~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))) | (~status(Ax, C, csa))))), rewrite(((~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))) | (~status(Ax, C, csa))) <=> ((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))), (((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa))) <=> ((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))), (((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))) <=> ((status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C))))) & ((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))))), rewrite(((status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C))))) & ((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))) <=> (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))), (((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))) <=> (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))))),
% 4.16/4.36 inference(bind,[status(th)],[])).
% 4.16/4.36 tff(242,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : ((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))) <=> ![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(quant_intro,[status(thm)],[241])).
% 4.16/4.36 tff(243,plain,
% 4.16/4.36 (^[Ax: $i, C: $i] : rewrite(((![I1: $i] : (~(model(I1, Ax) & model(I1, not(C)))) | status(Ax, C, csa)) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))) <=> ((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))))),
% 4.16/4.36 inference(bind,[status(th)],[])).
% 4.16/4.36 tff(244,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : ((![I1: $i] : (~(model(I1, Ax) & model(I1, not(C)))) | status(Ax, C, csa)) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa)))) <=> ![Ax: $i, C: $i] : ((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa))))),
% 4.16/4.36 inference(quant_intro,[status(thm)],[243])).
% 4.16/4.36 tff(245,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (?[I1: $i] : (model(I1, Ax) & model(I1, not(C))) <=> status(Ax, C, csa)) <=> ![Ax: $i, C: $i] : (?[I1: $i] : (model(I1, Ax) & model(I1, not(C))) <=> status(Ax, C, csa))),
% 4.16/4.36 inference(rewrite,[status(thm)],[])).
% 4.16/4.36 tff(246,axiom,(![Ax: $i, C: $i] : (?[I1: $i] : (model(I1, Ax) & model(I1, not(C))) <=> status(Ax, C, csa))), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax','csa')).
% 4.16/4.36 tff(247,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (?[I1: $i] : (model(I1, Ax) & model(I1, not(C))) <=> status(Ax, C, csa))),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[246, 245])).
% 4.16/4.36 tff(248,plain,(
% 4.16/4.36 ![Ax: $i, C: $i] : ((![I1: $i] : (~(model(I1, Ax) & model(I1, not(C)))) | status(Ax, C, csa)) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa))))),
% 4.16/4.36 inference(skolemize,[status(sab)],[247])).
% 4.16/4.36 tff(249,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : ((status(Ax, C, csa) | ![I1: $i] : (~(model(I1, Ax) & model(I1, not(C))))) & ((model(tptp_fun_I1_14(C, Ax), Ax) & model(tptp_fun_I1_14(C, Ax), not(C))) | (~status(Ax, C, csa))))),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[248, 244])).
% 4.16/4.36 tff(250,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[249, 242])).
% 4.16/4.36 tff(251,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C)))))) | (~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C)))))))))),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[250, 240])).
% 4.16/4.36 tff(252,plain,
% 4.16/4.36 (![Ax: $i, C: $i] : (~((~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))) | (~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C))))))))),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[251, 235])).
% 4.16/4.36 tff(253,plain,
% 4.16/4.36 ((~![Ax: $i, C: $i] : (~((~((~status(Ax, C, csa)) | (~((~model(tptp_fun_I1_14(C, Ax), Ax)) | (~model(tptp_fun_I1_14(C, Ax), not(C))))))) | (~(status(Ax, C, csa) | ![I1: $i] : ((~model(I1, Ax)) | (~model(I1, not(C))))))))) | (~((~((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))))) | (~(status(Ax!38, C!37, csa) | ![I1: $i] : ((~model(I1, Ax!38)) | (~model(I1, not(C!37))))))))),
% 4.16/4.36 inference(quant_inst,[status(thm)],[])).
% 4.16/4.36 tff(254,plain,
% 4.16/4.36 (~((~((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))))) | (~(status(Ax!38, C!37, csa) | ![I1: $i] : ((~model(I1, Ax!38)) | (~model(I1, not(C!37)))))))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[253, 252])).
% 4.16/4.36 tff(255,plain,
% 4.16/4.36 (((~((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))))) | (~(status(Ax!38, C!37, csa) | ![I1: $i] : ((~model(I1, Ax!38)) | (~model(I1, not(C!37))))))) | ((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(256,plain,
% 4.16/4.36 ((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[255, 254])).
% 4.16/4.36 tff(257,plain,
% 4.16/4.36 ((~((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))))) | (~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(258,plain,
% 4.16/4.36 ((~status(Ax!38, C!37, csa)) | (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[257, 256])).
% 4.16/4.36 tff(259,plain,
% 4.16/4.36 (~((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[258, 233])).
% 4.16/4.36 tff(260,plain,
% 4.16/4.36 (((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))) | model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(261,plain,
% 4.16/4.36 (model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[260, 259])).
% 4.16/4.36 tff(262,plain,
% 4.16/4.36 (((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | ((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | model(tptp_fun_I1_14(C!37, Ax!38), C!37))) <=> ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | (~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | model(tptp_fun_I1_14(C!37, Ax!38), C!37))),
% 4.16/4.36 inference(rewrite,[status(thm)],[])).
% 4.16/4.36 tff(263,plain,
% 4.16/4.36 ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | ((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | model(tptp_fun_I1_14(C!37, Ax!38), C!37))),
% 4.16/4.36 inference(quant_inst,[status(thm)],[])).
% 4.16/4.36 tff(264,plain,
% 4.16/4.36 ((~![I2: $i] : ((~model(I2, Ax!38)) | model(I2, C!37))) | (~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | model(tptp_fun_I1_14(C!37, Ax!38), C!37)),
% 4.16/4.36 inference(modus_ponens,[status(thm)],[263, 262])).
% 4.16/4.36 tff(265,plain,
% 4.16/4.36 (model(tptp_fun_I1_14(C!37, Ax!38), C!37)),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[264, 67, 261])).
% 4.16/4.36 tff(266,plain,
% 4.16/4.36 (((~model(tptp_fun_I1_14(C!37, Ax!38), Ax!38)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))) | model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(267,plain,
% 4.16/4.36 (model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[266, 259])).
% 4.16/4.36 tff(268,plain,
% 4.16/4.36 ((model(tptp_fun_I1_14(C!37, Ax!38), C!37) <=> model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))) | (~model(tptp_fun_I1_14(C!37, Ax!38), C!37)) | (~model(tptp_fun_I1_14(C!37, Ax!38), not(C!37)))),
% 4.16/4.36 inference(tautology,[status(thm)],[])).
% 4.16/4.36 tff(269,plain,
% 4.16/4.36 ((model(tptp_fun_I1_14(C!37, Ax!38), C!37) <=> model(tptp_fun_I1_14(C!37, Ax!38), not(C!37))) | (~model(tptp_fun_I1_14(C!37, Ax!38), C!37))),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[268, 267])).
% 4.16/4.36 tff(270,plain,
% 4.16/4.36 ($false),
% 4.16/4.36 inference(unit_resolution,[status(thm)],[269, 265, 9])).
% 4.16/4.36 % SZS output end Proof
% 4.16/4.37 % E exiting
%------------------------------------------------------------------------------