%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS132+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:27 AM UTC 2025
% Result : Theorem 0.20s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS132+1 : TPTP v9.0.0. Released v3.1.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n003.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:11:39 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.39 % SZS status Theorem
% 0.20/0.39 % SZS output start Proof
% 0.20/0.39 tff(rr_type, type, (
% 0.20/0.39 rr: ( $i * $i ) > $o)).
% 0.20/0.39 tff(tptp_fun_Y_2_type, type, (
% 0.20/0.39 tptp_fun_Y_2: $i > $i)).
% 0.20/0.39 tff(tptp_fun_X_9_type, type, (
% 0.20/0.39 tptp_fun_X_9: $i)).
% 0.20/0.39 tff(cowlThing_type, type, (
% 0.20/0.39 cowlThing: $i > $o)).
% 0.20/0.39 tff(cB_type, type, (
% 0.20/0.39 cB: $i > $o)).
% 0.20/0.39 tff(cNothing_type, type, (
% 0.20/0.39 cNothing: $i > $o)).
% 0.20/0.39 tff(rp_type, type, (
% 0.20/0.39 rp: ( $i * $i ) > $o)).
% 0.20/0.39 tff(tptp_fun_Y0_3_type, type, (
% 0.20/0.39 tptp_fun_Y0_3: $i > $i)).
% 0.20/0.39 tff(cnotB_type, type, (
% 0.20/0.39 cnotB: $i > $o)).
% 0.20/0.39 tff(cnotA_type, type, (
% 0.20/0.39 cnotA: $i > $o)).
% 0.20/0.39 tff(cnotAorB_type, type, (
% 0.20/0.39 cnotAorB: $i > $o)).
% 0.20/0.39 tff(cA_type, type, (
% 0.20/0.39 cA: $i > $o)).
% 0.20/0.39 tff(cAorB_type, type, (
% 0.20/0.39 cAorB: $i > $o)).
% 0.20/0.39 tff(rs_type, type, (
% 0.20/0.39 rs: ( $i * $i ) > $o)).
% 0.20/0.39 tff(tptp_fun_Y_5_type, type, (
% 0.20/0.39 tptp_fun_Y_5: $i > $i)).
% 0.20/0.39 tff(cowlNothing_type, type, (
% 0.20/0.39 cowlNothing: $i > $o)).
% 0.20/0.39 tff(tptp_fun_Y_1_type, type, (
% 0.20/0.39 tptp_fun_Y_1: $i > $i)).
% 0.20/0.39 tff(tptp_fun_X_7_type, type, (
% 0.20/0.39 tptp_fun_X_7: $i)).
% 0.20/0.39 tff(xsd_string_type, type, (
% 0.20/0.39 xsd_string: $i > $o)).
% 0.20/0.39 tff(tptp_fun_X_8_type, type, (
% 0.20/0.39 tptp_fun_X_8: $i)).
% 0.20/0.39 tff(xsd_integer_type, type, (
% 0.20/0.39 xsd_integer: $i > $o)).
% 0.20/0.39 tff(tptp_fun_Y_6_type, type, (
% 0.20/0.39 tptp_fun_Y_6: $i > $i)).
% 0.20/0.39 tff(rq_type, type, (
% 0.20/0.39 rq: ( $i * $i ) > $o)).
% 0.20/0.39 tff(tptp_fun_Y_4_type, type, (
% 0.20/0.39 tptp_fun_Y_4: $i > $i)).
% 0.20/0.39 tff(tptp_fun_Y_0_type, type, (
% 0.20/0.39 tptp_fun_Y_0: $i > $i)).
% 0.20/0.39 tff(1,assumption,(cNothing(tptp_fun_Y_2(X!9))), introduced(assumption)).
% 0.20/0.39 tff(2,plain,
% 0.20/0.39 (^[X: $i] : refl(((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))) <=> ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(3,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))) <=> ![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[2])).
% 0.20/0.39 tff(4,plain,
% 0.20/0.39 (^[X: $i] : rewrite(((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))) <=> ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(5,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))) <=> ![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[4])).
% 0.20/0.39 tff(6,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y))) <=> ![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))),
% 0.20/0.39 inference(transitivity,[status(thm)],[5, 3])).
% 0.20/0.39 tff(7,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y))) <=> ![X: $i] : ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(8,plain,
% 0.20/0.39 (^[X: $i] : trans(monotonicity(rewrite((~?[Y: $i] : rp(X, Y)) <=> (~?[Y: $i] : rp(X, Y))), ((cNothing(X) => (~?[Y: $i] : rp(X, Y))) <=> (cNothing(X) => (~?[Y: $i] : rp(X, Y))))), rewrite((cNothing(X) => (~?[Y: $i] : rp(X, Y))) <=> ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))), ((cNothing(X) => (~?[Y: $i] : rp(X, Y))) <=> ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(9,plain,
% 0.20/0.39 (![X: $i] : (cNothing(X) => (~?[Y: $i] : rp(X, Y))) <=> ![X: $i] : ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[8])).
% 0.20/0.39 tff(10,axiom,(![X: $i] : (cNothing(X) => (~?[Y: $i] : rp(X, Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_6')).
% 0.20/0.39 tff(11,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.20/0.39 tff(12,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | (~?[Y: $i] : rp(X, Y)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[11, 7])).
% 0.20/0.39 tff(13,plain,(
% 0.20/0.39 ![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))),
% 0.20/0.39 inference(skolemize,[status(sab)],[12])).
% 0.20/0.39 tff(14,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[13, 6])).
% 0.20/0.39 tff(15,plain,
% 0.20/0.39 (((~![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))) | ((~cNothing(tptp_fun_Y_2(X!9))) | ![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y)))) <=> ((~![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))) | (~cNothing(tptp_fun_Y_2(X!9))) | ![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(16,plain,
% 0.20/0.39 ((~![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))) | ((~cNothing(tptp_fun_Y_2(X!9))) | ![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y)))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(17,plain,
% 0.20/0.39 ((~![X: $i] : ((~cNothing(X)) | ![Y: $i] : (~rp(X, Y)))) | (~cNothing(tptp_fun_Y_2(X!9))) | ![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.20/0.39 tff(18,plain,
% 0.20/0.39 (![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[17, 14, 1])).
% 0.20/0.39 tff(19,plain,
% 0.20/0.39 (^[X: $i] : refl(((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X))) <=> ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(20,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X))) <=> ![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[19])).
% 0.20/0.39 tff(21,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0)) <=> ![X: $i] : ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(22,plain,
% 0.20/0.39 (^[X: $i] : rewrite((cNothing(X) => ?[Y0: $i] : rp(X, Y0)) <=> ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0)))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(23,plain,
% 0.20/0.39 (![X: $i] : (cNothing(X) => ?[Y0: $i] : rp(X, Y0)) <=> ![X: $i] : ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[22])).
% 0.20/0.39 tff(24,axiom,(![X: $i] : (cNothing(X) => ?[Y0: $i] : rp(X, Y0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_5')).
% 0.20/0.39 tff(25,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.20/0.39 tff(26,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | ?[Y0: $i] : rp(X, Y0))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[25, 21])).
% 0.20/0.39 tff(27,plain,(
% 0.20/0.39 ![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))),
% 0.20/0.39 inference(skolemize,[status(sab)],[26])).
% 0.20/0.39 tff(28,plain,
% 0.20/0.39 (![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[27, 20])).
% 0.20/0.39 tff(29,plain,
% 0.20/0.39 (((~![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))) | ((~cNothing(tptp_fun_Y_2(X!9))) | rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9))))) <=> ((~![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))) | (~cNothing(tptp_fun_Y_2(X!9))) | rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(30,plain,
% 0.20/0.39 ((~![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))) | ((~cNothing(tptp_fun_Y_2(X!9))) | rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9))))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(31,plain,
% 0.20/0.39 ((~![X: $i] : ((~cNothing(X)) | rp(X, tptp_fun_Y0_3(X)))) | (~cNothing(tptp_fun_Y_2(X!9))) | rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.20/0.39 tff(32,plain,
% 0.20/0.39 (rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9)))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[31, 28, 1])).
% 0.20/0.39 tff(33,plain,
% 0.20/0.39 ((~![Y: $i] : (~rp(tptp_fun_Y_2(X!9), Y))) | (~rp(tptp_fun_Y_2(X!9), tptp_fun_Y0_3(tptp_fun_Y_2(X!9))))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(34,plain,
% 0.20/0.39 ($false),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[33, 32, 18])).
% 0.20/0.39 tff(35,plain,(~cNothing(tptp_fun_Y_2(X!9))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.39 tff(36,plain,
% 0.20/0.39 (^[X: $i] : refl((~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X))) <=> (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(37,plain,
% 0.20/0.39 (![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X))) <=> ![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[36])).
% 0.20/0.39 tff(38,plain,
% 0.20/0.39 (^[X: $i] : trans(trans(monotonicity(rewrite((cnotB(X) & cnotA(X)) <=> (~((~cnotA(X)) | (~cnotB(X))))), ((cnotAorB(X) <=> (cnotB(X) & cnotA(X))) <=> (cnotAorB(X) <=> (~((~cnotA(X)) | (~cnotB(X))))))), rewrite((cnotAorB(X) <=> (~((~cnotA(X)) | (~cnotB(X))))) <=> (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))), ((cnotAorB(X) <=> (cnotB(X) & cnotA(X))) <=> (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X))))), rewrite((~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X))) <=> (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))), ((cnotAorB(X) <=> (cnotB(X) & cnotA(X))) <=> (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(39,plain,
% 0.20/0.39 (![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X))) <=> ![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[38])).
% 0.20/0.39 tff(40,plain,
% 0.20/0.39 (![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X))) <=> ![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(41,axiom,(![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_9')).
% 0.20/0.39 tff(42,plain,
% 0.20/0.39 (![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.20/0.39 tff(43,plain,(
% 0.20/0.39 ![X: $i] : (cnotAorB(X) <=> (cnotB(X) & cnotA(X)))),
% 0.20/0.39 inference(skolemize,[status(sab)],[42])).
% 0.20/0.39 tff(44,plain,
% 0.20/0.39 (![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[43, 39])).
% 0.20/0.39 tff(45,plain,
% 0.20/0.39 (![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[44, 37])).
% 0.20/0.39 tff(46,plain,
% 0.20/0.39 ((~![X: $i] : (~(((~cnotA(X)) | (~cnotB(X))) <=> cnotAorB(X)))) | (~(((~cnotA(X!9)) | (~cnotB(X!9))) <=> cnotAorB(X!9)))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(47,plain,
% 0.20/0.39 (~(((~cnotA(X!9)) | (~cnotB(X!9))) <=> cnotAorB(X!9))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[46, 45])).
% 0.20/0.39 tff(48,plain,
% 0.20/0.39 (^[X: $i] : refl((~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))) <=> (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(49,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[48])).
% 0.20/0.39 tff(50,plain,
% 0.20/0.39 (^[X: $i] : rewrite((~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))) <=> (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(51,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[50])).
% 0.20/0.39 tff(52,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(transitivity,[status(thm)],[51, 49])).
% 0.20/0.39 tff(53,plain,
% 0.20/0.39 (^[X: $i] : trans(monotonicity(rewrite(((~cB(X)) | (rr(X, tptp_fun_Y_2(X)) & cowlThing(tptp_fun_Y_2(X)))) <=> ((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))), rewrite((cB(X) | ![Y: $i] : (~(rr(X, Y) & cowlThing(Y)))) <=> (cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))), ((((~cB(X)) | (rr(X, tptp_fun_Y_2(X)) & cowlThing(tptp_fun_Y_2(X)))) & (cB(X) | ![Y: $i] : (~(rr(X, Y) & cowlThing(Y))))) <=> (((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X)))))) & (cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))))), rewrite((((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X)))))) & (cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y))))) <=> (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))), ((((~cB(X)) | (rr(X, tptp_fun_Y_2(X)) & cowlThing(tptp_fun_Y_2(X)))) & (cB(X) | ![Y: $i] : (~(rr(X, Y) & cowlThing(Y))))) <=> (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(54,plain,
% 0.20/0.39 (![X: $i] : (((~cB(X)) | (rr(X, tptp_fun_Y_2(X)) & cowlThing(tptp_fun_Y_2(X)))) & (cB(X) | ![Y: $i] : (~(rr(X, Y) & cowlThing(Y))))) <=> ![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[53])).
% 0.20/0.39 tff(55,plain,
% 0.20/0.39 (![X: $i] : (cB(X) <=> ?[Y: $i] : (rr(X, Y) & cowlThing(Y))) <=> ![X: $i] : (cB(X) <=> ?[Y: $i] : (rr(X, Y) & cowlThing(Y)))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(56,axiom,(![X: $i] : (cB(X) <=> ?[Y: $i] : (rr(X, Y) & cowlThing(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_4')).
% 0.20/0.39 tff(57,plain,
% 0.20/0.39 (![X: $i] : (cB(X) <=> ?[Y: $i] : (rr(X, Y) & cowlThing(Y)))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.20/0.39 tff(58,plain,(
% 0.20/0.39 ![X: $i] : (((~cB(X)) | (rr(X, tptp_fun_Y_2(X)) & cowlThing(tptp_fun_Y_2(X)))) & (cB(X) | ![Y: $i] : (~(rr(X, Y) & cowlThing(Y)))))),
% 0.20/0.39 inference(skolemize,[status(sab)],[57])).
% 0.20/0.39 tff(59,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[58, 54])).
% 0.20/0.39 tff(60,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[59, 52])).
% 0.20/0.39 tff(61,plain,
% 0.20/0.39 (((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9)))))))))) <=> ((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9))))))))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(62,plain,
% 0.20/0.39 ((~((~((~cB(X!9)) | (~((~rr(X!9, tptp_fun_Y_2(X!9))) | (~cowlThing(tptp_fun_Y_2(X!9))))))) | (~(cB(X!9) | ![Y: $i] : ((~rr(X!9, Y)) | (~cowlThing(Y))))))) <=> (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9)))))))))),
% 0.20/0.39 inference(rewrite,[status(thm)],[])).
% 0.20/0.39 tff(63,plain,
% 0.20/0.39 (((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cB(X!9)) | (~((~rr(X!9, tptp_fun_Y_2(X!9))) | (~cowlThing(tptp_fun_Y_2(X!9))))))) | (~(cB(X!9) | ![Y: $i] : ((~rr(X!9, Y)) | (~cowlThing(Y)))))))) <=> ((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9))))))))))),
% 0.20/0.39 inference(monotonicity,[status(thm)],[62])).
% 0.20/0.39 tff(64,plain,
% 0.20/0.39 (((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cB(X!9)) | (~((~rr(X!9, tptp_fun_Y_2(X!9))) | (~cowlThing(tptp_fun_Y_2(X!9))))))) | (~(cB(X!9) | ![Y: $i] : ((~rr(X!9, Y)) | (~cowlThing(Y)))))))) <=> ((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9))))))))))),
% 0.20/0.39 inference(transitivity,[status(thm)],[63, 61])).
% 0.20/0.39 tff(65,plain,
% 0.20/0.39 ((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cB(X!9)) | (~((~rr(X!9, tptp_fun_Y_2(X!9))) | (~cowlThing(tptp_fun_Y_2(X!9))))))) | (~(cB(X!9) | ![Y: $i] : ((~rr(X!9, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.39 inference(quant_inst,[status(thm)],[])).
% 0.20/0.39 tff(66,plain,
% 0.20/0.39 ((~![X: $i] : (~((~((~cB(X)) | (~((~rr(X, tptp_fun_Y_2(X))) | (~cowlThing(tptp_fun_Y_2(X))))))) | (~(cB(X) | ![Y: $i] : ((~rr(X, Y)) | (~cowlThing(Y)))))))) | (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9)))))))))),
% 0.20/0.39 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.20/0.39 tff(67,plain,
% 0.20/0.39 (~((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9))))))))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[66, 60])).
% 0.20/0.39 tff(68,plain,
% 0.20/0.39 (((~(cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))) | (~((~cB(X!9)) | (~((~cowlThing(tptp_fun_Y_2(X!9))) | (~rr(X!9, tptp_fun_Y_2(X!9)))))))) | (cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y))))),
% 0.20/0.39 inference(tautology,[status(thm)],[])).
% 0.20/0.39 tff(69,plain,
% 0.20/0.39 (cB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rr(X!9, Y)))),
% 0.20/0.39 inference(unit_resolution,[status(thm)],[68, 67])).
% 0.20/0.39 tff(70,assumption,(~cnotAorB(X!9)), introduced(assumption)).
% 0.20/0.39 tff(71,plain,
% 0.20/0.39 (^[X: $i] : refl((~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))) <=> (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(72,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))) <=> ![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[71])).
% 0.20/0.39 tff(73,plain,
% 0.20/0.39 (^[X: $i] : rewrite((~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))) <=> (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))))),
% 0.20/0.39 inference(bind,[status(th)],[])).
% 0.20/0.39 tff(74,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))) <=> ![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.39 inference(quant_intro,[status(thm)],[73])).
% 0.20/0.39 tff(75,plain,
% 0.20/0.39 (![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))) <=> ![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.39 inference(transitivity,[status(thm)],[74, 72])).
% 0.20/0.39 tff(76,plain,
% 0.20/0.39 (^[X: $i] : trans(monotonicity(rewrite(((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) <=> ((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))), ((((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))) <=> (((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))))), rewrite((((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))) <=> (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))), ((((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))) <=> (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(77,plain,
% 0.20/0.40 (![X: $i] : (((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X))))))) <=> ![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[76])).
% 0.20/0.40 tff(78,plain,
% 0.20/0.40 (![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) <=> ![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(79,plain,
% 0.20/0.40 (^[X: $i] : rewrite((cnotAorB(X) <=> ![Y: $i] : (rs(X, Y) => cNothing(Y))) <=> (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(80,plain,
% 0.20/0.40 (![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (rs(X, Y) => cNothing(Y))) <=> ![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[79])).
% 0.20/0.40 tff(81,axiom,(![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (rs(X, Y) => cNothing(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_8')).
% 0.20/0.40 tff(82,plain,
% 0.20/0.40 (![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.20/0.40 tff(83,plain,
% 0.20/0.40 (![X: $i] : (cnotAorB(X) <=> ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[82, 78])).
% 0.20/0.40 tff(84,plain,(
% 0.20/0.40 ![X: $i] : (((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y)))) & (cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))),
% 0.20/0.40 inference(skolemize,[status(sab)],[83])).
% 0.20/0.40 tff(85,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[84, 77])).
% 0.20/0.40 tff(86,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[85, 75])).
% 0.20/0.40 tff(87,plain,
% 0.20/0.40 ((~![X: $i] : (~((~((~cnotAorB(X)) | ![Y: $i] : (cNothing(Y) | (~rs(X, Y))))) | (~(cnotAorB(X) | (~(cNothing(tptp_fun_Y_5(X)) | (~rs(X, tptp_fun_Y_5(X)))))))))) | (~((~((~cnotAorB(X!9)) | ![Y: $i] : (cNothing(Y) | (~rs(X!9, Y))))) | (~(cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))))))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(88,plain,
% 0.20/0.40 (~((~((~cnotAorB(X!9)) | ![Y: $i] : (cNothing(Y) | (~rs(X!9, Y))))) | (~(cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9))))))))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[87, 86])).
% 0.20/0.40 tff(89,plain,
% 0.20/0.40 (((~((~cnotAorB(X!9)) | ![Y: $i] : (cNothing(Y) | (~rs(X!9, Y))))) | (~(cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))))))) | (cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9))))))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(90,plain,
% 0.20/0.40 (cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[89, 88])).
% 0.20/0.40 tff(91,plain,
% 0.20/0.40 ((~(cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9))))))) | cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(92,plain,
% 0.20/0.40 (cnotAorB(X!9) | (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[91, 90])).
% 0.20/0.40 tff(93,plain,
% 0.20/0.40 (~(cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9))))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[92, 70])).
% 0.20/0.40 tff(94,plain,
% 0.20/0.40 ((cNothing(tptp_fun_Y_5(X!9)) | (~rs(X!9, tptp_fun_Y_5(X!9)))) | rs(X!9, tptp_fun_Y_5(X!9))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(95,plain,
% 0.20/0.40 (rs(X!9, tptp_fun_Y_5(X!9))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[94, 93])).
% 0.20/0.40 tff(96,assumption,(cowlNothing(tptp_fun_Y_5(X!9)) | (~cowlThing(tptp_fun_Y_5(X!9)))), introduced(assumption)).
% 0.20/0.40 tff(97,plain,
% 0.20/0.40 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(98,plain,
% 0.20/0.40 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[97])).
% 0.20/0.40 tff(99,plain,
% 0.20/0.40 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(100,plain,
% 0.20/0.40 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[99])).
% 0.20/0.40 tff(101,plain,
% 0.20/0.40 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(102,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_0')).
% 0.20/0.40 tff(103,plain,
% 0.20/0.40 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.20/0.40 tff(104,plain,(
% 0.20/0.40 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.40 inference(skolemize,[status(sab)],[103])).
% 0.20/0.40 tff(105,plain,
% 0.20/0.40 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[104, 100])).
% 0.20/0.40 tff(106,plain,
% 0.20/0.40 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[105, 98])).
% 0.20/0.40 tff(107,plain,
% 0.20/0.40 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(tptp_fun_Y_5(X!9)) | (~cowlThing(tptp_fun_Y_5(X!9)))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(108,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[107, 106, 96])).
% 0.20/0.40 tff(109,plain,(~(cowlNothing(tptp_fun_Y_5(X!9)) | (~cowlThing(tptp_fun_Y_5(X!9))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(110,plain,
% 0.20/0.40 ((cowlNothing(tptp_fun_Y_5(X!9)) | (~cowlThing(tptp_fun_Y_5(X!9)))) | cowlThing(tptp_fun_Y_5(X!9))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(111,plain,
% 0.20/0.40 (cowlThing(tptp_fun_Y_5(X!9))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[110, 109])).
% 0.20/0.40 tff(112,assumption,(rs(X!9, tptp_fun_Y_5(X!9))), introduced(assumption)).
% 0.20/0.40 tff(113,assumption,(![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))), introduced(assumption)).
% 0.20/0.40 tff(114,plain,
% 0.20/0.40 (((~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))) | ((~cowlThing(tptp_fun_Y_5(X!9))) | (~rs(X!9, tptp_fun_Y_5(X!9))))) <=> ((~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))) | (~cowlThing(tptp_fun_Y_5(X!9))) | (~rs(X!9, tptp_fun_Y_5(X!9))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(115,plain,
% 0.20/0.40 ((~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))) | ((~cowlThing(tptp_fun_Y_5(X!9))) | (~rs(X!9, tptp_fun_Y_5(X!9))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(116,plain,
% 0.20/0.40 ((~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))) | (~cowlThing(tptp_fun_Y_5(X!9))) | (~rs(X!9, tptp_fun_Y_5(X!9)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.20/0.40 tff(117,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[116, 113, 112, 111])).
% 0.20/0.40 tff(118,plain,((~rs(X!9, tptp_fun_Y_5(X!9))) | (~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(119,plain,
% 0.20/0.40 (~![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[118, 95])).
% 0.20/0.40 tff(120,plain,
% 0.20/0.40 (^[X: $i] : refl((~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))) <=> (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(121,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[120])).
% 0.20/0.40 tff(122,plain,
% 0.20/0.40 (^[X: $i] : rewrite((~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))) <=> (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(123,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[122])).
% 0.20/0.40 tff(124,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))) <=> ![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(transitivity,[status(thm)],[123, 121])).
% 0.20/0.40 tff(125,plain,
% 0.20/0.40 (^[X: $i] : trans(monotonicity(rewrite(((~cAorB(X)) | (rs(X, tptp_fun_Y_1(X)) & cowlThing(tptp_fun_Y_1(X)))) <=> ((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))), rewrite((cAorB(X) | ![Y: $i] : (~(rs(X, Y) & cowlThing(Y)))) <=> (cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))), ((((~cAorB(X)) | (rs(X, tptp_fun_Y_1(X)) & cowlThing(tptp_fun_Y_1(X)))) & (cAorB(X) | ![Y: $i] : (~(rs(X, Y) & cowlThing(Y))))) <=> (((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X)))))) & (cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))))), rewrite((((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X)))))) & (cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y))))) <=> (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))), ((((~cAorB(X)) | (rs(X, tptp_fun_Y_1(X)) & cowlThing(tptp_fun_Y_1(X)))) & (cAorB(X) | ![Y: $i] : (~(rs(X, Y) & cowlThing(Y))))) <=> (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(126,plain,
% 0.20/0.40 (![X: $i] : (((~cAorB(X)) | (rs(X, tptp_fun_Y_1(X)) & cowlThing(tptp_fun_Y_1(X)))) & (cAorB(X) | ![Y: $i] : (~(rs(X, Y) & cowlThing(Y))))) <=> ![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[125])).
% 0.20/0.40 tff(127,plain,
% 0.20/0.40 (![X: $i] : (cAorB(X) <=> ?[Y: $i] : (rs(X, Y) & cowlThing(Y))) <=> ![X: $i] : (cAorB(X) <=> ?[Y: $i] : (rs(X, Y) & cowlThing(Y)))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(128,axiom,(![X: $i] : (cAorB(X) <=> ?[Y: $i] : (rs(X, Y) & cowlThing(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_3')).
% 0.20/0.40 tff(129,plain,
% 0.20/0.40 (![X: $i] : (cAorB(X) <=> ?[Y: $i] : (rs(X, Y) & cowlThing(Y)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[128, 127])).
% 0.20/0.40 tff(130,plain,(
% 0.20/0.40 ![X: $i] : (((~cAorB(X)) | (rs(X, tptp_fun_Y_1(X)) & cowlThing(tptp_fun_Y_1(X)))) & (cAorB(X) | ![Y: $i] : (~(rs(X, Y) & cowlThing(Y)))))),
% 0.20/0.40 inference(skolemize,[status(sab)],[129])).
% 0.20/0.40 tff(131,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[130, 126])).
% 0.20/0.40 tff(132,plain,
% 0.20/0.40 (![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[131, 124])).
% 0.20/0.40 tff(133,plain,
% 0.20/0.40 (((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))))))) <=> ((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(134,plain,
% 0.20/0.40 ((~((~((~cAorB(X!9)) | (~((~rs(X!9, tptp_fun_Y_1(X!9))) | (~cowlThing(tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~rs(X!9, Y)) | (~cowlThing(Y))))))) <=> (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))))))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(135,plain,
% 0.20/0.40 (((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~rs(X!9, tptp_fun_Y_1(X!9))) | (~cowlThing(tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~rs(X!9, Y)) | (~cowlThing(Y)))))))) <=> ((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))))))),
% 0.20/0.40 inference(monotonicity,[status(thm)],[134])).
% 0.20/0.40 tff(136,plain,
% 0.20/0.40 (((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~rs(X!9, tptp_fun_Y_1(X!9))) | (~cowlThing(tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~rs(X!9, Y)) | (~cowlThing(Y)))))))) <=> ((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))))))),
% 0.20/0.40 inference(transitivity,[status(thm)],[135, 133])).
% 0.20/0.40 tff(137,plain,
% 0.20/0.40 ((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~rs(X!9, tptp_fun_Y_1(X!9))) | (~cowlThing(tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~rs(X!9, Y)) | (~cowlThing(Y)))))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(138,plain,
% 0.20/0.40 ((~![X: $i] : (~((~((~cAorB(X)) | (~((~rs(X, tptp_fun_Y_1(X))) | (~cowlThing(tptp_fun_Y_1(X))))))) | (~(cAorB(X) | ![Y: $i] : ((~rs(X, Y)) | (~cowlThing(Y)))))))) | (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))))))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[137, 136])).
% 0.20/0.40 tff(139,plain,
% 0.20/0.40 (~((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[138, 132])).
% 0.20/0.40 tff(140,plain,
% 0.20/0.40 (((~((~cAorB(X!9)) | (~((~cowlThing(tptp_fun_Y_1(X!9))) | (~rs(X!9, tptp_fun_Y_1(X!9))))))) | (~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))))) | (cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(141,plain,
% 0.20/0.40 (cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[140, 139])).
% 0.20/0.40 tff(142,plain,
% 0.20/0.40 ((~(cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y))))) | cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(143,plain,
% 0.20/0.40 (cAorB(X!9) | ![Y: $i] : ((~cowlThing(Y)) | (~rs(X!9, Y)))),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[142, 141])).
% 0.20/0.40 tff(144,plain,
% 0.20/0.40 (cAorB(X!9)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[143, 119])).
% 0.20/0.40 tff(145,assumption,(cowlNothing(X!7) | (~cowlThing(X!7))), introduced(assumption)).
% 0.20/0.40 tff(146,plain,
% 0.20/0.40 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!7) | (~cowlThing(X!7))))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(147,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[146, 106, 145])).
% 0.20/0.40 tff(148,plain,(~(cowlNothing(X!7) | (~cowlThing(X!7)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(149,plain,
% 0.20/0.40 ((cowlNothing(X!7) | (~cowlThing(X!7))) | cowlThing(X!7)),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(150,plain,
% 0.20/0.40 (cowlThing(X!7)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[149, 148])).
% 0.20/0.40 tff(151,plain,
% 0.20/0.40 ((cowlNothing(X!7) | (~cowlThing(X!7))) | (~cowlNothing(X!7))),
% 0.20/0.40 inference(tautology,[status(thm)],[])).
% 0.20/0.40 tff(152,plain,
% 0.20/0.40 (~cowlNothing(X!7)),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[151, 148])).
% 0.20/0.40 tff(153,assumption,(xsd_integer(X!8) <=> xsd_string(X!8)), introduced(assumption)).
% 0.20/0.40 tff(154,plain,
% 0.20/0.40 (^[X: $i] : refl((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(155,plain,
% 0.20/0.40 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[154])).
% 0.20/0.40 tff(156,plain,
% 0.20/0.40 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.40 tff(157,plain,
% 0.20/0.40 (^[X: $i] : trans(rewrite((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), rewrite((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), ((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))))),
% 0.20/0.40 inference(bind,[status(th)],[])).
% 0.20/0.40 tff(158,plain,
% 0.20/0.40 (![X: $i] : (xsd_string(X) <=> (~xsd_integer(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(quant_intro,[status(thm)],[157])).
% 0.20/0.40 tff(159,axiom,(![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_1')).
% 0.20/0.40 tff(160,plain,
% 0.20/0.40 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.20/0.40 tff(161,plain,
% 0.20/0.40 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[160, 156])).
% 0.20/0.40 tff(162,plain,(
% 0.20/0.40 ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(skolemize,[status(sab)],[161])).
% 0.20/0.40 tff(163,plain,
% 0.20/0.40 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.20/0.40 inference(modus_ponens,[status(thm)],[162, 155])).
% 0.20/0.40 tff(164,plain,
% 0.20/0.40 ((~![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))) | (~(xsd_integer(X!8) <=> xsd_string(X!8)))),
% 0.20/0.40 inference(quant_inst,[status(thm)],[])).
% 0.20/0.40 tff(165,plain,
% 0.20/0.40 ($false),
% 0.20/0.40 inference(unit_resolution,[status(thm)],[164, 163, 153])).
% 0.20/0.40 tff(166,plain,(~(xsd_integer(X!8) <=> xsd_string(X!8))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.40 tff(167,plain,
% 0.20/0.40 (((cowlNothing(X!7) | (~cowlThing(X!7))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> (cowlNothing(X!7) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))) | (~cowlThing(X!7)))),
% 0.20/0.40 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(168,plain,
% 0.20/0.41 ((~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))) <=> (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(169,plain,
% 0.20/0.41 ((~(~(cowlNothing(X!7) | (~cowlThing(X!7))))) <=> (cowlNothing(X!7) | (~cowlThing(X!7)))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(170,plain,
% 0.20/0.41 ((cowlThing(X!7) & (~cowlNothing(X!7))) <=> (~(cowlNothing(X!7) | (~cowlThing(X!7))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(171,plain,
% 0.20/0.41 ((~(cowlThing(X!7) & (~cowlNothing(X!7)))) <=> (~(~(cowlNothing(X!7) | (~cowlThing(X!7)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[170])).
% 0.20/0.41 tff(172,plain,
% 0.20/0.41 ((~(cowlThing(X!7) & (~cowlNothing(X!7)))) <=> (cowlNothing(X!7) | (~cowlThing(X!7)))),
% 0.20/0.41 inference(transitivity,[status(thm)],[171, 169])).
% 0.20/0.41 tff(173,plain,
% 0.20/0.41 (((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> ((cowlNothing(X!7) | (~cowlThing(X!7))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[172, 168])).
% 0.20/0.41 tff(174,plain,
% 0.20/0.41 (((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> (cowlNothing(X!7) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))) | (~cowlThing(X!7)))),
% 0.20/0.41 inference(transitivity,[status(thm)],[173, 167])).
% 0.20/0.41 tff(175,plain,
% 0.20/0.41 (((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> ((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(176,plain,
% 0.20/0.41 (((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> ((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[168])).
% 0.20/0.41 tff(177,plain,
% 0.20/0.41 (((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9))))) <=> ((~(cowlThing(X!7) & (~cowlNothing(X!7)))) | (xsd_integer(X!8) <=> xsd_string(X!8)) | (~(cAorB(X!9) <=> (cA(X!9) | cB(X!9)))))),
% 0.20/0.41 inference(transitivity,[status(thm)],[176, 175])).
% 0.20/0.41 tff(178,plain,
% 0.20/0.41 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X)))) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(179,plain,
% 0.20/0.41 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[178])).
% 0.20/0.41 tff(180,plain,
% 0.20/0.41 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X)))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(181,plain,
% 0.20/0.41 ((~((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i] : (cAorB(X) <=> (cB(X) | cA(X))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X)))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(182,axiom,(~((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i] : (cAorB(X) <=> (cB(X) | cA(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','the_axiom')).
% 0.20/0.41 tff(183,plain,
% 0.20/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[182, 181])).
% 0.20/0.41 tff(184,plain,
% 0.20/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[183, 179])).
% 0.20/0.41 tff(185,plain,
% 0.20/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[184, 180])).
% 0.20/0.41 tff(186,plain,
% 0.20/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : (cAorB(X) <=> (cA(X) | cB(X))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[185, 179])).
% 0.20/0.41 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.20/0.41 (a!2 (not (and (cowlThing X!7) (not (cowlNothing X!7)))))
% 0.20/0.41 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.20/0.41 (a!5 (forall ((X $i)) (= (cAorB X) (or (cA X) (cB X)))))
% 0.20/0.41 (a!6 (not (= (cAorB X!9) (or (cA X!9) (cB X!9))))))
% 0.20/0.41 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!8) (xsd_string X!8)))))
% 0.20/0.41 (a!7 (~ (not (and a!1 a!3 a!5))
% 0.20/0.41 (or a!2 (= (xsd_integer X!8) (xsd_string X!8)) a!6))))
% 0.20/0.41 (nnf-neg (sk (~ (not a!1) a!2)) a!4 (sk (~ (not a!5) a!6)) a!7)))
% 0.20/0.41 Proof display could not be completed: unexpected number of arguments
% 0.20/0.41 % E exiting
%------------------------------------------------------------------------------