%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS157+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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:29 AM UTC 2025
% Result : Theorem 0.19s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS157+1 : TPTP v9.0.0. Released v3.1.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n005.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:50 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.44 % SZS status Theorem
% 0.19/0.44 % SZS output start Proof
% 0.19/0.44 tff(xsd_string_type, type, (
% 0.19/0.44 xsd_string: $i > $o)).
% 0.19/0.44 tff(tptp_fun_X_135_type, type, (
% 0.19/0.44 tptp_fun_X_135: $i)).
% 0.19/0.44 tff(xsd_integer_type, type, (
% 0.19/0.44 xsd_integer: $i > $o)).
% 0.19/0.44 tff(cowlThing_type, type, (
% 0.19/0.44 cowlThing: $i > $o)).
% 0.19/0.44 tff(tptp_fun_X_134_type, type, (
% 0.19/0.44 tptp_fun_X_134: $i)).
% 0.19/0.44 tff(cowlNothing_type, type, (
% 0.19/0.44 cowlNothing: $i > $o)).
% 0.19/0.44 tff(cC30_type, type, (
% 0.19/0.44 cC30: $i > $o)).
% 0.19/0.44 tff(iV3102_type, type, (
% 0.19/0.44 iV3102: $i)).
% 0.19/0.44 tff(cC28_type, type, (
% 0.19/0.44 cC28: $i > $o)).
% 0.19/0.44 tff(cC14_type, type, (
% 0.19/0.44 cC14: $i > $o)).
% 0.19/0.44 tff(cC26xcomp_type, type, (
% 0.19/0.44 cC26xcomp: $i > $o)).
% 0.19/0.44 tff(cC16xcomp_type, type, (
% 0.19/0.44 cC16xcomp: $i > $o)).
% 0.19/0.44 tff(cC2xcomp_type, type, (
% 0.19/0.44 cC2xcomp: $i > $o)).
% 0.19/0.44 tff(cC12xcomp_type, type, (
% 0.19/0.44 cC12xcomp: $i > $o)).
% 0.19/0.44 tff(cC46_type, type, (
% 0.19/0.44 cC46: $i > $o)).
% 0.19/0.44 tff(cC216_type, type, (
% 0.19/0.44 cC216: $i > $o)).
% 0.19/0.44 tff(cTEST_type, type, (
% 0.19/0.44 cTEST: $i > $o)).
% 0.19/0.44 tff(cC64_type, type, (
% 0.19/0.44 cC64: $i > $o)).
% 0.19/0.44 tff(cTOP_type, type, (
% 0.19/0.44 cTOP: $i > $o)).
% 0.19/0.44 tff(cC62xcomp_type, type, (
% 0.19/0.44 cC62xcomp: $i > $o)).
% 0.19/0.44 tff(cC44_type, type, (
% 0.19/0.44 cC44: $i > $o)).
% 0.19/0.44 tff(cC42xcomp_type, type, (
% 0.19/0.44 cC42xcomp: $i > $o)).
% 0.19/0.44 tff(cC32xcomp_type, type, (
% 0.19/0.44 cC32xcomp: $i > $o)).
% 0.19/0.44 tff(1,assumption,(cowlNothing(X!134) | (~cowlThing(X!134))), introduced(assumption)).
% 0.19/0.44 tff(2,plain,
% 0.19/0.44 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(3,plain,
% 0.19/0.44 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[2])).
% 0.19/0.44 tff(4,plain,
% 0.19/0.44 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(5,plain,
% 0.19/0.44 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[4])).
% 0.19/0.44 tff(6,plain,
% 0.19/0.44 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(7,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_0')).
% 0.19/0.44 tff(8,plain,
% 0.19/0.44 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.19/0.44 tff(9,plain,(
% 0.19/0.44 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.19/0.44 inference(skolemize,[status(sab)],[8])).
% 0.19/0.44 tff(10,plain,
% 0.19/0.44 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.19/0.44 tff(11,plain,
% 0.19/0.44 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[10, 3])).
% 0.19/0.44 tff(12,plain,
% 0.19/0.44 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!134) | (~cowlThing(X!134))))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(13,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[12, 11, 1])).
% 0.19/0.44 tff(14,plain,(~(cowlNothing(X!134) | (~cowlThing(X!134)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(15,plain,
% 0.19/0.44 ((cowlNothing(X!134) | (~cowlThing(X!134))) | cowlThing(X!134)),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(16,plain,
% 0.19/0.44 (cowlThing(X!134)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[15, 14])).
% 0.19/0.44 tff(17,plain,
% 0.19/0.44 ((cowlNothing(X!134) | (~cowlThing(X!134))) | (~cowlNothing(X!134))),
% 0.19/0.44 inference(tautology,[status(thm)],[])).
% 0.19/0.44 tff(18,plain,
% 0.19/0.44 (~cowlNothing(X!134)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[17, 14])).
% 0.19/0.44 tff(19,plain,
% 0.19/0.44 (^[X: $i] : refl((~(((~cC28(X)) | (~cC14(X))) <=> cC30(X))) <=> (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(20,plain,
% 0.19/0.44 (![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[19])).
% 0.19/0.44 tff(21,plain,
% 0.19/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC28(X) & cC14(X)) <=> (~((~cC28(X)) | (~cC14(X))))), ((cC30(X) <=> (cC28(X) & cC14(X))) <=> (cC30(X) <=> (~((~cC28(X)) | (~cC14(X))))))), rewrite((cC30(X) <=> (~((~cC28(X)) | (~cC14(X))))) <=> (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))), ((cC30(X) <=> (cC28(X) & cC14(X))) <=> (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X))))), rewrite((~(((~cC28(X)) | (~cC14(X))) <=> cC30(X))) <=> (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))), ((cC30(X) <=> (cC28(X) & cC14(X))) <=> (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(22,plain,
% 0.19/0.44 (![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[21])).
% 0.19/0.44 tff(23,plain,
% 0.19/0.44 (![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X))) <=> ![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X)))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(24,axiom,(![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_132')).
% 0.19/0.44 tff(25,plain,
% 0.19/0.44 (![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[24, 23])).
% 0.19/0.44 tff(26,plain,(
% 0.19/0.44 ![X: $i] : (cC30(X) <=> (cC28(X) & cC14(X)))),
% 0.19/0.44 inference(skolemize,[status(sab)],[25])).
% 0.19/0.44 tff(27,plain,
% 0.19/0.44 (![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[26, 22])).
% 0.19/0.44 tff(28,plain,
% 0.19/0.44 (![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[27, 20])).
% 0.19/0.44 tff(29,plain,
% 0.19/0.44 (((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(30,plain,
% 0.19/0.44 ((~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))) <=> (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(31,plain,
% 0.19/0.44 ((((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102)) <=> (((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(32,plain,
% 0.19/0.44 ((~(((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102))) <=> (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)))),
% 0.19/0.44 inference(monotonicity,[status(thm)],[31])).
% 0.19/0.44 tff(33,plain,
% 0.19/0.44 ((~(((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102))) <=> (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)))),
% 0.19/0.44 inference(transitivity,[status(thm)],[32, 30])).
% 0.19/0.44 tff(34,plain,
% 0.19/0.44 (((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))))),
% 0.19/0.44 inference(monotonicity,[status(thm)],[33])).
% 0.19/0.44 tff(35,plain,
% 0.19/0.44 (((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))))),
% 0.19/0.44 inference(transitivity,[status(thm)],[34, 29])).
% 0.19/0.44 tff(36,plain,
% 0.19/0.44 ((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC28(iV3102)) | (~cC14(iV3102))) <=> cC30(iV3102)))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(37,plain,
% 0.19/0.44 ((~![X: $i] : (~(((~cC28(X)) | (~cC14(X))) <=> cC30(X)))) | (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[36, 35])).
% 0.19/0.44 tff(38,plain,
% 0.19/0.44 (~(((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102))),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[37, 28])).
% 0.19/0.44 tff(39,plain,
% 0.19/0.44 (^[X: $i] : refl((~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X))) <=> (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(40,plain,
% 0.19/0.44 (![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X))) <=> ![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[39])).
% 0.19/0.44 tff(41,plain,
% 0.19/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC16xcomp(X) & cC26xcomp(X)) <=> (~((~cC16xcomp(X)) | (~cC26xcomp(X))))), ((cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X))) <=> (cC28(X) <=> (~((~cC16xcomp(X)) | (~cC26xcomp(X))))))), rewrite((cC28(X) <=> (~((~cC16xcomp(X)) | (~cC26xcomp(X))))) <=> (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))), ((cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X))) <=> (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X))))), rewrite((~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X))) <=> (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))), ((cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X))) <=> (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(42,plain,
% 0.19/0.45 (![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X))) <=> ![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[41])).
% 0.19/0.45 tff(43,plain,
% 0.19/0.45 (![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X))) <=> ![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(44,axiom,(![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_131')).
% 0.19/0.45 tff(45,plain,
% 0.19/0.45 (![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.19/0.45 tff(46,plain,(
% 0.19/0.45 ![X: $i] : (cC28(X) <=> (cC16xcomp(X) & cC26xcomp(X)))),
% 0.19/0.45 inference(skolemize,[status(sab)],[45])).
% 0.19/0.45 tff(47,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[46, 42])).
% 0.19/0.45 tff(48,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[47, 40])).
% 0.19/0.45 tff(49,plain,
% 0.19/0.45 ((~![X: $i] : (~(((~cC16xcomp(X)) | (~cC26xcomp(X))) <=> cC28(X)))) | (~(((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))) <=> cC28(iV3102)))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(50,plain,
% 0.19/0.45 (~(((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))) <=> cC28(iV3102))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[49, 48])).
% 0.19/0.45 tff(51,plain,
% 0.19/0.45 (cC16xcomp(iV3102) <=> cC16xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(52,axiom,(cC16xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_210')).
% 0.19/0.45 tff(53,plain,
% 0.19/0.45 (cC16xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.19/0.45 tff(54,plain,
% 0.19/0.45 (cC26xcomp(iV3102) <=> cC26xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(55,axiom,(cC26xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_206')).
% 0.19/0.45 tff(56,plain,
% 0.19/0.45 (cC26xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.19/0.45 tff(57,plain,
% 0.19/0.45 ((~((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102)))) | (~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(58,plain,
% 0.19/0.45 (~((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[57, 56, 53])).
% 0.19/0.45 tff(59,plain,
% 0.19/0.45 ((((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))) <=> cC28(iV3102)) | ((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))) | cC28(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(60,plain,
% 0.19/0.45 ((((~cC16xcomp(iV3102)) | (~cC26xcomp(iV3102))) <=> cC28(iV3102)) | cC28(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.19/0.45 tff(61,plain,
% 0.19/0.45 (cC28(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[60, 50])).
% 0.19/0.45 tff(62,plain,
% 0.19/0.45 (^[X: $i] : refl((~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X))) <=> (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(63,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X))) <=> ![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[62])).
% 0.19/0.45 tff(64,plain,
% 0.19/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC2xcomp(X) & cC12xcomp(X)) <=> (~((~cC12xcomp(X)) | (~cC2xcomp(X))))), ((cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X))) <=> (cC14(X) <=> (~((~cC12xcomp(X)) | (~cC2xcomp(X))))))), rewrite((cC14(X) <=> (~((~cC12xcomp(X)) | (~cC2xcomp(X))))) <=> (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))), ((cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X))) <=> (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X))))), rewrite((~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X))) <=> (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))), ((cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X))) <=> (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(65,plain,
% 0.19/0.45 (![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X))) <=> ![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[64])).
% 0.19/0.45 tff(66,plain,
% 0.19/0.45 (![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X))) <=> ![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(67,axiom,(![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_44')).
% 0.19/0.45 tff(68,plain,
% 0.19/0.45 (![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.19/0.45 tff(69,plain,(
% 0.19/0.45 ![X: $i] : (cC14(X) <=> (cC2xcomp(X) & cC12xcomp(X)))),
% 0.19/0.45 inference(skolemize,[status(sab)],[68])).
% 0.19/0.45 tff(70,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[69, 65])).
% 0.19/0.45 tff(71,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[70, 63])).
% 0.19/0.45 tff(72,plain,
% 0.19/0.45 ((~![X: $i] : (~(((~cC12xcomp(X)) | (~cC2xcomp(X))) <=> cC14(X)))) | (~(((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))) <=> cC14(iV3102)))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(73,plain,
% 0.19/0.45 (~(((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))) <=> cC14(iV3102))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.19/0.45 tff(74,plain,
% 0.19/0.45 (cC12xcomp(iV3102) <=> cC12xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(75,axiom,(cC12xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_215')).
% 0.19/0.45 tff(76,plain,
% 0.19/0.45 (cC12xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.19/0.45 tff(77,plain,
% 0.19/0.45 (cC2xcomp(iV3102) <=> cC2xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(78,axiom,(cC2xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_203')).
% 0.19/0.45 tff(79,plain,
% 0.19/0.45 (cC2xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.19/0.45 tff(80,plain,
% 0.19/0.45 ((~((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102)))) | (~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(81,plain,
% 0.19/0.45 (~((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[80, 79, 76])).
% 0.19/0.45 tff(82,plain,
% 0.19/0.45 ((((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))) <=> cC14(iV3102)) | ((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))) | cC14(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(83,plain,
% 0.19/0.45 ((((~cC12xcomp(iV3102)) | (~cC2xcomp(iV3102))) <=> cC14(iV3102)) | cC14(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[82, 81])).
% 0.19/0.45 tff(84,plain,
% 0.19/0.45 (cC14(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[83, 73])).
% 0.19/0.45 tff(85,plain,
% 0.19/0.45 ((~((~cC14(iV3102)) | (~cC28(iV3102)))) | (~cC14(iV3102)) | (~cC28(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(86,plain,
% 0.19/0.45 (~((~cC14(iV3102)) | (~cC28(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[85, 84, 61])).
% 0.19/0.45 tff(87,plain,
% 0.19/0.45 ((((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)) | ((~cC14(iV3102)) | (~cC28(iV3102))) | cC30(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(88,plain,
% 0.19/0.45 ((((~cC14(iV3102)) | (~cC28(iV3102))) <=> cC30(iV3102)) | cC30(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[87, 86])).
% 0.19/0.45 tff(89,plain,
% 0.19/0.45 (cC30(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[88, 38])).
% 0.19/0.45 tff(90,plain,
% 0.19/0.45 (^[X: $i] : refl((~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X))) <=> (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(91,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X))) <=> ![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[90])).
% 0.19/0.45 tff(92,plain,
% 0.19/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC216(X) & cC46(X)) <=> (~((~cC216(X)) | (~cC46(X))))), ((cTEST(X) <=> (cC216(X) & cC46(X))) <=> (cTEST(X) <=> (~((~cC216(X)) | (~cC46(X))))))), rewrite((cTEST(X) <=> (~((~cC216(X)) | (~cC46(X))))) <=> (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))), ((cTEST(X) <=> (cC216(X) & cC46(X))) <=> (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X))))), rewrite((~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X))) <=> (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))), ((cTEST(X) <=> (cC216(X) & cC46(X))) <=> (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(93,plain,
% 0.19/0.45 (![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X))) <=> ![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[92])).
% 0.19/0.45 tff(94,plain,
% 0.19/0.45 (![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X))) <=> ![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(95,axiom,(![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_201')).
% 0.19/0.45 tff(96,plain,
% 0.19/0.45 (![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[95, 94])).
% 0.19/0.45 tff(97,plain,(
% 0.19/0.45 ![X: $i] : (cTEST(X) <=> (cC216(X) & cC46(X)))),
% 0.19/0.45 inference(skolemize,[status(sab)],[96])).
% 0.19/0.45 tff(98,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[97, 93])).
% 0.19/0.45 tff(99,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[98, 91])).
% 0.19/0.45 tff(100,plain,
% 0.19/0.45 ((~![X: $i] : (~(((~cC216(X)) | (~cC46(X))) <=> cTEST(X)))) | (~(((~cC216(iV3102)) | (~cC46(iV3102))) <=> cTEST(iV3102)))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(101,plain,
% 0.19/0.45 (~(((~cC216(iV3102)) | (~cC46(iV3102))) <=> cTEST(iV3102))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[100, 99])).
% 0.19/0.45 tff(102,plain,
% 0.19/0.45 (cTEST(iV3102) <=> cTEST(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(103,axiom,(cTEST(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_202')).
% 0.19/0.45 tff(104,plain,
% 0.19/0.45 (cTEST(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.19/0.45 tff(105,plain,
% 0.19/0.45 ((((~cC216(iV3102)) | (~cC46(iV3102))) <=> cTEST(iV3102)) | (~((~cC216(iV3102)) | (~cC46(iV3102)))) | (~cTEST(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(106,plain,
% 0.19/0.45 ((((~cC216(iV3102)) | (~cC46(iV3102))) <=> cTEST(iV3102)) | (~((~cC216(iV3102)) | (~cC46(iV3102))))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[105, 104])).
% 0.19/0.45 tff(107,plain,
% 0.19/0.45 (~((~cC216(iV3102)) | (~cC46(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[106, 101])).
% 0.19/0.45 tff(108,plain,
% 0.19/0.45 (((~cC216(iV3102)) | (~cC46(iV3102))) | cC46(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(109,plain,
% 0.19/0.45 (cC46(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[108, 107])).
% 0.19/0.45 tff(110,plain,
% 0.19/0.45 (^[X: $i] : refl((~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X))) <=> (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(111,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X))) <=> ![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[110])).
% 0.19/0.45 tff(112,plain,
% 0.19/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC62xcomp(X) & cTOP(X)) <=> (~((~cC62xcomp(X)) | (~cTOP(X))))), ((cC64(X) <=> (cC62xcomp(X) & cTOP(X))) <=> (cC64(X) <=> (~((~cC62xcomp(X)) | (~cTOP(X))))))), rewrite((cC64(X) <=> (~((~cC62xcomp(X)) | (~cTOP(X))))) <=> (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))), ((cC64(X) <=> (cC62xcomp(X) & cTOP(X))) <=> (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X))))), rewrite((~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X))) <=> (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))), ((cC64(X) <=> (cC62xcomp(X) & cTOP(X))) <=> (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(113,plain,
% 0.19/0.45 (![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X))) <=> ![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[112])).
% 0.19/0.45 tff(114,plain,
% 0.19/0.45 (![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X))) <=> ![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(115,axiom,(![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_166')).
% 0.19/0.45 tff(116,plain,
% 0.19/0.45 (![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.19/0.45 tff(117,plain,(
% 0.19/0.45 ![X: $i] : (cC64(X) <=> (cC62xcomp(X) & cTOP(X)))),
% 0.19/0.45 inference(skolemize,[status(sab)],[116])).
% 0.19/0.45 tff(118,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[117, 113])).
% 0.19/0.45 tff(119,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[118, 111])).
% 0.19/0.45 tff(120,plain,
% 0.19/0.45 ((~![X: $i] : (~(((~cC62xcomp(X)) | (~cTOP(X))) <=> cC64(X)))) | (~(((~cC62xcomp(iV3102)) | (~cTOP(iV3102))) <=> cC64(iV3102)))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(121,plain,
% 0.19/0.45 (~(((~cC62xcomp(iV3102)) | (~cTOP(iV3102))) <=> cC64(iV3102))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[120, 119])).
% 0.19/0.45 tff(122,plain,
% 0.19/0.45 (cC62xcomp(iV3102) <=> cC62xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(123,axiom,(cC62xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_212')).
% 0.19/0.45 tff(124,plain,
% 0.19/0.45 (cC62xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[123, 122])).
% 0.19/0.45 tff(125,plain,
% 0.19/0.45 (cTOP(iV3102) <=> cTOP(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(126,axiom,(cTOP(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_205')).
% 0.19/0.45 tff(127,plain,
% 0.19/0.45 (cTOP(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[126, 125])).
% 0.19/0.45 tff(128,plain,
% 0.19/0.45 ((~((~cC62xcomp(iV3102)) | (~cTOP(iV3102)))) | (~cC62xcomp(iV3102)) | (~cTOP(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(129,plain,
% 0.19/0.45 (~((~cC62xcomp(iV3102)) | (~cTOP(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[128, 127, 124])).
% 0.19/0.45 tff(130,plain,
% 0.19/0.45 ((((~cC62xcomp(iV3102)) | (~cTOP(iV3102))) <=> cC64(iV3102)) | ((~cC62xcomp(iV3102)) | (~cTOP(iV3102))) | cC64(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(131,plain,
% 0.19/0.45 ((((~cC62xcomp(iV3102)) | (~cTOP(iV3102))) <=> cC64(iV3102)) | cC64(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[130, 129])).
% 0.19/0.45 tff(132,plain,
% 0.19/0.45 (cC64(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[131, 121])).
% 0.19/0.45 tff(133,plain,
% 0.19/0.45 (((~cC216(iV3102)) | (~cC46(iV3102))) | cC216(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(134,plain,
% 0.19/0.45 (cC216(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[133, 107])).
% 0.19/0.45 tff(135,plain,
% 0.19/0.45 (^[X: $i] : refl((~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X))) <=> (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(136,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X))) <=> ![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[135])).
% 0.19/0.45 tff(137,plain,
% 0.19/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC42xcomp(X) & cC32xcomp(X)) <=> (~((~cC32xcomp(X)) | (~cC42xcomp(X))))), ((cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X))) <=> (cC44(X) <=> (~((~cC32xcomp(X)) | (~cC42xcomp(X))))))), rewrite((cC44(X) <=> (~((~cC32xcomp(X)) | (~cC42xcomp(X))))) <=> (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))), ((cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X))) <=> (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X))))), rewrite((~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X))) <=> (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))), ((cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X))) <=> (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))))),
% 0.19/0.45 inference(bind,[status(th)],[])).
% 0.19/0.45 tff(138,plain,
% 0.19/0.45 (![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X))) <=> ![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))),
% 0.19/0.45 inference(quant_intro,[status(thm)],[137])).
% 0.19/0.45 tff(139,plain,
% 0.19/0.45 (![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X))) <=> ![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(140,axiom,(![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_147')).
% 0.19/0.45 tff(141,plain,
% 0.19/0.45 (![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.19/0.45 tff(142,plain,(
% 0.19/0.45 ![X: $i] : (cC44(X) <=> (cC42xcomp(X) & cC32xcomp(X)))),
% 0.19/0.45 inference(skolemize,[status(sab)],[141])).
% 0.19/0.45 tff(143,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[142, 138])).
% 0.19/0.45 tff(144,plain,
% 0.19/0.45 (![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[143, 136])).
% 0.19/0.45 tff(145,plain,
% 0.19/0.45 ((~![X: $i] : (~(((~cC32xcomp(X)) | (~cC42xcomp(X))) <=> cC44(X)))) | (~(((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))) <=> cC44(iV3102)))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(146,plain,
% 0.19/0.45 (~(((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))) <=> cC44(iV3102))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[145, 144])).
% 0.19/0.45 tff(147,plain,
% 0.19/0.45 (cC42xcomp(iV3102) <=> cC42xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(148,axiom,(cC42xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_211')).
% 0.19/0.45 tff(149,plain,
% 0.19/0.45 (cC42xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[148, 147])).
% 0.19/0.45 tff(150,plain,
% 0.19/0.45 (cC32xcomp(iV3102) <=> cC32xcomp(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(151,axiom,(cC32xcomp(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_207')).
% 0.19/0.45 tff(152,plain,
% 0.19/0.45 (cC32xcomp(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.19/0.45 tff(153,plain,
% 0.19/0.45 ((~((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102)))) | (~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(154,plain,
% 0.19/0.45 (~((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102)))),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[153, 152, 149])).
% 0.19/0.45 tff(155,plain,
% 0.19/0.45 ((((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))) <=> cC44(iV3102)) | ((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))) | cC44(iV3102)),
% 0.19/0.45 inference(tautology,[status(thm)],[])).
% 0.19/0.45 tff(156,plain,
% 0.19/0.45 ((((~cC32xcomp(iV3102)) | (~cC42xcomp(iV3102))) <=> cC44(iV3102)) | cC44(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[155, 154])).
% 0.19/0.45 tff(157,plain,
% 0.19/0.45 (cC44(iV3102)),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[156, 146])).
% 0.19/0.45 tff(158,plain,
% 0.19/0.45 (cowlThing(iV3102) <=> cowlThing(iV3102)),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(159,axiom,(cowlThing(iV3102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_217')).
% 0.19/0.45 tff(160,plain,
% 0.19/0.45 (cowlThing(iV3102)),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.19/0.45 tff(161,plain,
% 0.19/0.45 (((cowlNothing(X!134) | (~cowlThing(X!134))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102))) <=> (cowlNothing(X!134) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102)) | (~cowlThing(X!134)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(162,plain,
% 0.19/0.45 ((~(~(cowlNothing(X!134) | (~cowlThing(X!134))))) <=> (cowlNothing(X!134) | (~cowlThing(X!134)))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(163,plain,
% 0.19/0.45 ((cowlThing(X!134) & (~cowlNothing(X!134))) <=> (~(cowlNothing(X!134) | (~cowlThing(X!134))))),
% 0.19/0.45 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(164,plain,
% 0.19/0.45 ((~(cowlThing(X!134) & (~cowlNothing(X!134)))) <=> (~(~(cowlNothing(X!134) | (~cowlThing(X!134)))))),
% 0.19/0.45 inference(monotonicity,[status(thm)],[163])).
% 0.19/0.45 tff(165,plain,
% 0.19/0.45 ((~(cowlThing(X!134) & (~cowlNothing(X!134)))) <=> (cowlNothing(X!134) | (~cowlThing(X!134)))),
% 0.19/0.45 inference(transitivity,[status(thm)],[164, 162])).
% 0.19/0.45 tff(166,plain,
% 0.19/0.45 (((~(cowlThing(X!134) & (~cowlNothing(X!134)))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102))) <=> ((cowlNothing(X!134) | (~cowlThing(X!134))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102)))),
% 0.19/0.46 inference(monotonicity,[status(thm)],[165])).
% 0.19/0.46 tff(167,plain,
% 0.19/0.46 (((~(cowlThing(X!134) & (~cowlNothing(X!134)))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102))) <=> (cowlNothing(X!134) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102)) | (~cowlThing(X!134)))),
% 0.19/0.46 inference(transitivity,[status(thm)],[166, 161])).
% 0.19/0.46 tff(168,plain,
% 0.19/0.46 (((~(cowlThing(X!134) & (~cowlNothing(X!134)))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102))) <=> ((~(cowlThing(X!134) & (~cowlNothing(X!134)))) | (xsd_integer(X!135) <=> xsd_string(X!135)) | (~cC14(iV3102)) | (~cC44(iV3102)) | (~cC216(iV3102)) | (~cC64(iV3102)) | (~cC46(iV3102)) | (~cC28(iV3102)) | (~cowlThing(iV3102)) | (~cC30(iV3102)))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(169,plain,
% 0.19/0.46 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102)) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(170,plain,
% 0.19/0.46 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102)))),
% 0.19/0.46 inference(monotonicity,[status(thm)],[169])).
% 0.19/0.46 tff(171,plain,
% 0.19/0.46 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102)))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(172,plain,
% 0.19/0.46 ((~(((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC14(iV3102)) & cC44(iV3102)) & cC216(iV3102)) & cC64(iV3102)) & cC46(iV3102)) & cC28(iV3102)) & cowlThing(iV3102)) & cC30(iV3102))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102)))),
% 0.19/0.46 inference(rewrite,[status(thm)],[])).
% 0.19/0.46 tff(173,axiom,(~(((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC14(iV3102)) & cC44(iV3102)) & cC216(iV3102)) & cC64(iV3102)) & cC46(iV3102)) & cC28(iV3102)) & cowlThing(iV3102)) & cC30(iV3102))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','the_axiom')).
% 0.19/0.46 tff(174,plain,
% 0.19/0.46 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))),
% 0.19/0.46 inference(modus_ponens,[status(thm)],[173, 172])).
% 0.19/0.46 tff(175,plain,
% 0.19/0.46 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))),
% 0.19/0.46 inference(modus_ponens,[status(thm)],[174, 170])).
% 0.19/0.46 tff(176,plain,
% 0.19/0.46 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))),
% 0.19/0.46 inference(modus_ponens,[status(thm)],[175, 171])).
% 0.19/0.46 tff(177,plain,
% 0.19/0.46 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC14(iV3102) & cC44(iV3102) & cC216(iV3102) & cC64(iV3102) & cC46(iV3102) & cC28(iV3102) & cowlThing(iV3102) & cC30(iV3102))),
% 0.19/0.46 inference(modus_ponens,[status(thm)],[176, 170])).
% 0.19/0.46 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.19/0.46 (a!2 (not (and (cowlThing X!134) (not (cowlNothing X!134)))))
% 0.19/0.46 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.19/0.46 (a!5 (refl (~ (not (cC14 iV3102)) (not (cC14 iV3102)))))
% 0.19/0.46 (a!6 (refl (~ (not (cC44 iV3102)) (not (cC44 iV3102)))))
% 0.19/0.46 (a!7 (refl (~ (not (cC216 iV3102)) (not (cC216 iV3102)))))
% 0.19/0.46 (a!8 (refl (~ (not (cC64 iV3102)) (not (cC64 iV3102)))))
% 0.19/0.46 (a!9 (refl (~ (not (cC46 iV3102)) (not (cC46 iV3102)))))
% 0.19/0.46 (a!10 (refl (~ (not (cC28 iV3102)) (not (cC28 iV3102)))))
% 0.19/0.46 (a!11 (refl (~ (not (cowlThing iV3102)) (not (cowlThing iV3102)))))
% 0.19/0.46 (a!12 (refl (~ (not (cC30 iV3102)) (not (cC30 iV3102))))))
% 0.19/0.46 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!135) (xsd_string X!135)))))
% 0.19/0.46 (a!13 (~ (not (and a!1
% 0.19/0.46 a!3
% 0.19/0.46 (cC14 iV3102)
% 0.19/0.46 (cC44 iV3102)
% 0.19/0.46 (cC216 iV3102)
% 0.19/0.46 (cC64 iV3102)
% 0.19/0.46 (cC46 iV3102)
% 0.19/0.46 (cC28 iV3102)
% 0.19/0.46 (cowlThing iV3102)
% 0.19/0.46 (cC30 iV3102)))
% 0.19/0.46 (or a!2
% 0.19/0.46 (= (xsd_integer X!135) (xsd_string X!135))
% 0.19/0.46 (not (cC14 iV3102))
% 0.19/0.46 (not (cC44 iV3102))
% 0.19/0.46 (not (cC216 iV3102))
% 0.19/0.46 (not (cC64 iV3102))
% 0.19/0.46 (not (cC46 iV3102))
% 0.19/0.46 (not (cC28 iV3102))
% 0.19/0.46 (not (cowlThing iV3102))
% 0.19/0.46 (not (cC30 iV3102))))))
% 0.19/0.46 (nnf-neg (sk (~ (not a!1) a!2)) a!4 a!5 a!6 a!7 a!8 a!9 a!10 a!11 a!12 a!13)))
% 0.19/0.46 Proof display could not be completed: unexpected number of arguments
% 0.19/0.47 % E exiting
%------------------------------------------------------------------------------