%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS161+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.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:30 AM UTC 2025
% Result : Theorem 0.17s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : KRS161+1 : TPTP v9.0.0. Released v3.1.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.11/0.31 % Computer : n014.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu Jun 19 19:11:54 EDT 2025
% 0.11/0.31 % CPUTime :
% 0.17/0.43 % SZS status Theorem
% 0.17/0.43 % SZS output start Proof
% 0.17/0.43 tff(xsd_string_type, type, (
% 0.17/0.43 xsd_string: $i > $o)).
% 0.17/0.43 tff(tptp_fun_X_115_type, type, (
% 0.17/0.43 tptp_fun_X_115: $i)).
% 0.17/0.43 tff(xsd_integer_type, type, (
% 0.17/0.43 xsd_integer: $i > $o)).
% 0.17/0.43 tff(cowlThing_type, type, (
% 0.17/0.43 cowlThing: $i > $o)).
% 0.17/0.43 tff(tptp_fun_X_114_type, type, (
% 0.17/0.43 tptp_fun_X_114: $i)).
% 0.17/0.43 tff(cowlNothing_type, type, (
% 0.17/0.43 cowlNothing: $i > $o)).
% 0.17/0.43 tff(cC42_type, type, (
% 0.17/0.43 cC42: $i > $o)).
% 0.17/0.43 tff(iV16455_type, type, (
% 0.17/0.43 iV16455: $i)).
% 0.17/0.43 tff(rR1_type, type, (
% 0.17/0.43 rR1: ( $i * $i ) > $o)).
% 0.17/0.43 tff(cC8xcomp_type, type, (
% 0.17/0.43 cC8xcomp: $i > $o)).
% 0.17/0.43 tff(tptp_fun_Y_50_type, type, (
% 0.17/0.43 tptp_fun_Y_50: $i > $i)).
% 0.17/0.43 tff(iV16460_type, type, (
% 0.17/0.43 iV16460: $i)).
% 0.17/0.43 tff(cC44_type, type, (
% 0.17/0.43 cC44: $i > $o)).
% 0.17/0.43 tff(cC40xcomp_type, type, (
% 0.17/0.43 cC40xcomp: $i > $o)).
% 0.17/0.43 tff(cC56_type, type, (
% 0.17/0.43 cC56: $i > $o)).
% 0.17/0.43 tff(cC54xcomp_type, type, (
% 0.17/0.43 cC54xcomp: $i > $o)).
% 0.17/0.43 tff(cC60_type, type, (
% 0.17/0.43 cC60: $i > $o)).
% 0.17/0.43 tff(iV16453_type, type, (
% 0.17/0.43 iV16453: $i)).
% 0.17/0.43 tff(cC12xcomp_type, type, (
% 0.17/0.43 cC12xcomp: $i > $o)).
% 0.17/0.43 tff(tptp_fun_Y_70_type, type, (
% 0.17/0.43 tptp_fun_Y_70: $i > $i)).
% 0.17/0.43 tff(iV16461_type, type, (
% 0.17/0.43 iV16461: $i)).
% 0.17/0.43 tff(cC62_type, type, (
% 0.17/0.43 cC62: $i > $o)).
% 0.17/0.43 tff(cC58xcomp_type, type, (
% 0.17/0.43 cC58xcomp: $i > $o)).
% 0.17/0.43 tff(cC76_type, type, (
% 0.17/0.43 cC76: $i > $o)).
% 0.17/0.43 tff(cC74xcomp_type, type, (
% 0.17/0.43 cC74xcomp: $i > $o)).
% 0.17/0.43 tff(cC38_type, type, (
% 0.17/0.43 cC38: $i > $o)).
% 0.17/0.43 tff(iV16465_type, type, (
% 0.17/0.43 iV16465: $i)).
% 0.17/0.43 tff(iV16464_type, type, (
% 0.17/0.43 iV16464: $i)).
% 0.17/0.43 tff(iV16463_type, type, (
% 0.17/0.43 iV16463: $i)).
% 0.17/0.43 tff(iV16440_type, type, (
% 0.17/0.43 iV16440: $i)).
% 0.17/0.43 tff(iV16462_type, type, (
% 0.17/0.43 iV16462: $i)).
% 0.17/0.43 tff(cC68_type, type, (
% 0.17/0.43 cC68: $i > $o)).
% 0.17/0.43 tff(iV16459_type, type, (
% 0.17/0.43 iV16459: $i)).
% 0.17/0.43 tff(cC66xcomp_type, type, (
% 0.17/0.43 cC66xcomp: $i > $o)).
% 0.17/0.43 tff(cC64xcomp_type, type, (
% 0.17/0.43 cC64xcomp: $i > $o)).
% 0.17/0.43 tff(cC34_type, type, (
% 0.17/0.43 cC34: $i > $o)).
% 0.17/0.43 tff(cC32xcomp_type, type, (
% 0.17/0.43 cC32xcomp: $i > $o)).
% 0.17/0.43 tff(cC30xcomp_type, type, (
% 0.17/0.43 cC30xcomp: $i > $o)).
% 0.17/0.43 tff(cC88_type, type, (
% 0.17/0.43 cC88: $i > $o)).
% 0.17/0.43 tff(cC86xcomp_type, type, (
% 0.17/0.43 cC86xcomp: $i > $o)).
% 0.17/0.43 tff(cC84xcomp_type, type, (
% 0.17/0.43 cC84xcomp: $i > $o)).
% 0.17/0.43 tff(cC50_type, type, (
% 0.17/0.43 cC50: $i > $o)).
% 0.17/0.43 tff(cC48xcomp_type, type, (
% 0.17/0.43 cC48xcomp: $i > $o)).
% 0.17/0.43 tff(cC46xcomp_type, type, (
% 0.17/0.43 cC46xcomp: $i > $o)).
% 0.17/0.43 tff(iV16457_type, type, (
% 0.17/0.43 iV16457: $i)).
% 0.17/0.43 tff(cTOP_type, type, (
% 0.17/0.43 cTOP: $i > $o)).
% 0.17/0.43 tff(cC36xcomp_type, type, (
% 0.17/0.43 cC36xcomp: $i > $o)).
% 0.17/0.43 tff(iV16448_type, type, (
% 0.17/0.43 iV16448: $i)).
% 0.17/0.43 tff(cC82_type, type, (
% 0.17/0.43 cC82: $i > $o)).
% 0.17/0.43 tff(cC96xcomp_type, type, (
% 0.17/0.43 cC96xcomp: $i > $o)).
% 0.17/0.43 tff(cC98_type, type, (
% 0.17/0.43 cC98: $i > $o)).
% 0.17/0.43 tff(iV16439_type, type, (
% 0.17/0.43 iV16439: $i)).
% 0.17/0.43 tff(cC80_type, type, (
% 0.17/0.43 cC80: $i > $o)).
% 0.17/0.43 tff(cC78xcomp_type, type, (
% 0.17/0.43 cC78xcomp: $i > $o)).
% 0.17/0.43 tff(cC28_type, type, (
% 0.17/0.43 cC28: $i > $o)).
% 0.17/0.43 tff(cC106_type, type, (
% 0.17/0.43 cC106: $i > $o)).
% 0.17/0.43 tff(cC108_type, type, (
% 0.17/0.43 cC108: $i > $o)).
% 0.17/0.43 tff(cC130_type, type, (
% 0.17/0.43 cC130: $i > $o)).
% 0.17/0.43 tff(cTEST_type, type, (
% 0.17/0.43 cTEST: $i > $o)).
% 0.17/0.43 tff(cC104_type, type, (
% 0.17/0.43 cC104: $i > $o)).
% 0.17/0.43 tff(cC100xcomp_type, type, (
% 0.17/0.43 cC100xcomp: $i > $o)).
% 0.17/0.43 tff(1,assumption,(cowlNothing(X!114) | (~cowlThing(X!114))), introduced(assumption)).
% 0.17/0.43 tff(2,plain,
% 0.17/0.43 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.17/0.43 inference(bind,[status(th)],[])).
% 0.17/0.43 tff(3,plain,
% 0.17/0.43 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.17/0.43 inference(quant_intro,[status(thm)],[2])).
% 0.17/0.43 tff(4,plain,
% 0.17/0.43 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.17/0.43 inference(bind,[status(th)],[])).
% 0.17/0.43 tff(5,plain,
% 0.17/0.43 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.17/0.43 inference(quant_intro,[status(thm)],[4])).
% 0.17/0.43 tff(6,plain,
% 0.17/0.43 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.17/0.43 inference(rewrite,[status(thm)],[])).
% 0.17/0.43 tff(7,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_0')).
% 0.17/0.43 tff(8,plain,
% 0.17/0.43 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.17/0.43 tff(9,plain,(
% 0.17/0.43 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.17/0.43 inference(skolemize,[status(sab)],[8])).
% 0.17/0.43 tff(10,plain,
% 0.17/0.43 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.17/0.43 tff(11,plain,
% 0.17/0.43 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[10, 3])).
% 0.17/0.43 tff(12,plain,
% 0.17/0.43 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!114) | (~cowlThing(X!114))))),
% 0.17/0.43 inference(quant_inst,[status(thm)],[])).
% 0.17/0.43 tff(13,plain,
% 0.17/0.43 ($false),
% 0.17/0.43 inference(unit_resolution,[status(thm)],[12, 11, 1])).
% 0.17/0.43 tff(14,plain,(~(cowlNothing(X!114) | (~cowlThing(X!114)))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.43 tff(15,plain,
% 0.17/0.43 ((cowlNothing(X!114) | (~cowlThing(X!114))) | cowlThing(X!114)),
% 0.17/0.43 inference(tautology,[status(thm)],[])).
% 0.17/0.43 tff(16,plain,
% 0.17/0.43 (cowlThing(X!114)),
% 0.17/0.43 inference(unit_resolution,[status(thm)],[15, 14])).
% 0.17/0.43 tff(17,assumption,((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455)))))))), introduced(assumption)).
% 0.17/0.43 tff(18,plain,
% 0.17/0.43 (^[X: $i] : refl((~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))) <=> (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))))),
% 0.17/0.43 inference(bind,[status(th)],[])).
% 0.17/0.43 tff(19,plain,
% 0.17/0.43 (![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(quant_intro,[status(thm)],[18])).
% 0.17/0.43 tff(20,plain,
% 0.17/0.43 (^[X: $i] : rewrite((~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))) <=> (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))))),
% 0.17/0.43 inference(bind,[status(th)],[])).
% 0.17/0.43 tff(21,plain,
% 0.17/0.43 (![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(quant_intro,[status(thm)],[20])).
% 0.17/0.43 tff(22,plain,
% 0.17/0.43 (![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(transitivity,[status(thm)],[21, 19])).
% 0.17/0.43 tff(23,plain,
% 0.17/0.43 (^[X: $i] : trans(monotonicity(rewrite(((~cC42(X)) | (rR1(X, tptp_fun_Y_50(X)) & cC8xcomp(tptp_fun_Y_50(X)))) <=> ((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))), rewrite((cC42(X) | ![Y: $i] : (~(rR1(X, Y) & cC8xcomp(Y)))) <=> (cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))), ((((~cC42(X)) | (rR1(X, tptp_fun_Y_50(X)) & cC8xcomp(tptp_fun_Y_50(X)))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & cC8xcomp(Y))))) <=> (((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X)))))) & (cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))))), rewrite((((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X)))))) & (cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y))))) <=> (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))), ((((~cC42(X)) | (rR1(X, tptp_fun_Y_50(X)) & cC8xcomp(tptp_fun_Y_50(X)))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & cC8xcomp(Y))))) <=> (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))))),
% 0.17/0.43 inference(bind,[status(th)],[])).
% 0.17/0.43 tff(24,plain,
% 0.17/0.43 (![X: $i] : (((~cC42(X)) | (rR1(X, tptp_fun_Y_50(X)) & cC8xcomp(tptp_fun_Y_50(X)))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & cC8xcomp(Y))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(quant_intro,[status(thm)],[23])).
% 0.17/0.43 tff(25,plain,
% 0.17/0.43 (![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & cC8xcomp(Y))) <=> ![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & cC8xcomp(Y)))),
% 0.17/0.43 inference(rewrite,[status(thm)],[])).
% 0.17/0.43 tff(26,axiom,(![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & cC8xcomp(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_65')).
% 0.17/0.43 tff(27,plain,
% 0.17/0.43 (![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & cC8xcomp(Y)))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.17/0.43 tff(28,plain,(
% 0.17/0.43 ![X: $i] : (((~cC42(X)) | (rR1(X, tptp_fun_Y_50(X)) & cC8xcomp(tptp_fun_Y_50(X)))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & cC8xcomp(Y)))))),
% 0.17/0.43 inference(skolemize,[status(sab)],[27])).
% 0.17/0.43 tff(29,plain,
% 0.17/0.43 (![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[28, 24])).
% 0.17/0.43 tff(30,plain,
% 0.17/0.43 (![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.17/0.43 tff(31,plain,
% 0.17/0.43 (((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455)))))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455))))))))))),
% 0.17/0.43 inference(rewrite,[status(thm)],[])).
% 0.17/0.43 tff(32,plain,
% 0.17/0.43 ((~((~((~cC42(iV16455)) | (~((~rR1(iV16455, tptp_fun_Y_50(iV16455))) | (~cC8xcomp(tptp_fun_Y_50(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))))) <=> (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455)))))))))),
% 0.17/0.43 inference(rewrite,[status(thm)],[])).
% 0.17/0.43 tff(33,plain,
% 0.17/0.43 (((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~((~rR1(iV16455, tptp_fun_Y_50(iV16455))) | (~cC8xcomp(tptp_fun_Y_50(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455))))))))))),
% 0.17/0.43 inference(monotonicity,[status(thm)],[32])).
% 0.17/0.43 tff(34,plain,
% 0.17/0.43 (((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~((~rR1(iV16455, tptp_fun_Y_50(iV16455))) | (~cC8xcomp(tptp_fun_Y_50(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455))))))))))),
% 0.17/0.44 inference(transitivity,[status(thm)],[33, 31])).
% 0.17/0.44 tff(35,plain,
% 0.17/0.44 ((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~((~rR1(iV16455, tptp_fun_Y_50(iV16455))) | (~cC8xcomp(tptp_fun_Y_50(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))))))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(36,plain,
% 0.17/0.44 ((~![X: $i] : (~((~((~cC42(X)) | (~((~rR1(X, tptp_fun_Y_50(X))) | (~cC8xcomp(tptp_fun_Y_50(X))))))) | (~(cC42(X) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455)))))))))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.17/0.44 tff(37,plain,
% 0.17/0.44 ($false),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[36, 30, 17])).
% 0.17/0.44 tff(38,plain,(~((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455))))))))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.44 tff(39,plain,
% 0.17/0.44 (((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~((~cC8xcomp(tptp_fun_Y_50(iV16455))) | (~rR1(iV16455, tptp_fun_Y_50(iV16455)))))))) | (cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(40,plain,
% 0.17/0.44 (cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.17/0.44 tff(41,assumption,(![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))), introduced(assumption)).
% 0.17/0.44 tff(42,plain,
% 0.17/0.44 (cC8xcomp(iV16460) <=> cC8xcomp(iV16460)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(43,axiom,(cC8xcomp(iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_227')).
% 0.17/0.44 tff(44,plain,
% 0.17/0.44 (cC8xcomp(iV16460)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.17/0.44 tff(45,plain,
% 0.17/0.44 (rR1(iV16455, iV16460) <=> rR1(iV16455, iV16460)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(46,axiom,(rR1(iV16455, iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_193')).
% 0.17/0.44 tff(47,plain,
% 0.17/0.44 (rR1(iV16455, iV16460)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.17/0.44 tff(48,plain,
% 0.17/0.44 (((~![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))) | ((~cC8xcomp(iV16460)) | (~rR1(iV16455, iV16460)))) <=> ((~![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))) | (~cC8xcomp(iV16460)) | (~rR1(iV16455, iV16460)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(49,plain,
% 0.17/0.44 ((~![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))) | ((~cC8xcomp(iV16460)) | (~rR1(iV16455, iV16460)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(50,plain,
% 0.17/0.44 ((~![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))) | (~cC8xcomp(iV16460)) | (~rR1(iV16455, iV16460))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.17/0.44 tff(51,plain,
% 0.17/0.44 ($false),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[50, 47, 44, 41])).
% 0.17/0.44 tff(52,plain,(~![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.44 tff(53,plain,
% 0.17/0.44 ((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y)))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(54,plain,
% 0.17/0.44 ((~(cC42(iV16455) | ![Y: $i] : ((~cC8xcomp(Y)) | (~rR1(iV16455, Y))))) | cC42(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[53, 52])).
% 0.17/0.44 tff(55,plain,
% 0.17/0.44 (cC42(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[54, 40])).
% 0.17/0.44 tff(56,plain,
% 0.17/0.44 (cC40xcomp(iV16455) <=> cC40xcomp(iV16455)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(57,axiom,(cC40xcomp(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_185')).
% 0.17/0.44 tff(58,plain,
% 0.17/0.44 (cC40xcomp(iV16455)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.17/0.44 tff(59,plain,
% 0.17/0.44 ((~((~cC40xcomp(iV16455)) | (~cC42(iV16455)))) | (~cC40xcomp(iV16455)) | (~cC42(iV16455))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(60,plain,
% 0.17/0.44 ((~((~cC40xcomp(iV16455)) | (~cC42(iV16455)))) | (~cC42(iV16455))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.17/0.44 tff(61,plain,
% 0.17/0.44 (~((~cC40xcomp(iV16455)) | (~cC42(iV16455)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[60, 55])).
% 0.17/0.44 tff(62,plain,
% 0.17/0.44 (^[X: $i] : refl((~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X))) <=> (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(63,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X))) <=> ![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[62])).
% 0.17/0.44 tff(64,plain,
% 0.17/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC40xcomp(X) & cC42(X)) <=> (~((~cC40xcomp(X)) | (~cC42(X))))), ((cC44(X) <=> (cC40xcomp(X) & cC42(X))) <=> (cC44(X) <=> (~((~cC40xcomp(X)) | (~cC42(X))))))), rewrite((cC44(X) <=> (~((~cC40xcomp(X)) | (~cC42(X))))) <=> (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))), ((cC44(X) <=> (cC40xcomp(X) & cC42(X))) <=> (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X))))), rewrite((~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X))) <=> (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))), ((cC44(X) <=> (cC40xcomp(X) & cC42(X))) <=> (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(65,plain,
% 0.17/0.44 (![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X))) <=> ![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[64])).
% 0.17/0.44 tff(66,plain,
% 0.17/0.44 (![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X))) <=> ![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(67,axiom,(![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_66')).
% 0.17/0.44 tff(68,plain,
% 0.17/0.44 (![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.17/0.44 tff(69,plain,(
% 0.17/0.44 ![X: $i] : (cC44(X) <=> (cC40xcomp(X) & cC42(X)))),
% 0.17/0.44 inference(skolemize,[status(sab)],[68])).
% 0.17/0.44 tff(70,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[69, 65])).
% 0.17/0.44 tff(71,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[70, 63])).
% 0.17/0.44 tff(72,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))) | (~(((~cC40xcomp(iV16455)) | (~cC42(iV16455))) <=> cC44(iV16455)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(73,plain,
% 0.17/0.44 (~(((~cC40xcomp(iV16455)) | (~cC42(iV16455))) <=> cC44(iV16455))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.17/0.44 tff(74,plain,
% 0.17/0.44 ((((~cC40xcomp(iV16455)) | (~cC42(iV16455))) <=> cC44(iV16455)) | ((~cC40xcomp(iV16455)) | (~cC42(iV16455))) | cC44(iV16455)),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(75,plain,
% 0.17/0.44 (((~cC40xcomp(iV16455)) | (~cC42(iV16455))) | cC44(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.17/0.44 tff(76,plain,
% 0.17/0.44 (cC44(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[75, 61])).
% 0.17/0.44 tff(77,plain,
% 0.17/0.44 (cC54xcomp(iV16455) <=> cC54xcomp(iV16455)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(78,axiom,(cC54xcomp(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_190')).
% 0.17/0.44 tff(79,plain,
% 0.17/0.44 (cC54xcomp(iV16455)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.17/0.44 tff(80,plain,
% 0.17/0.44 ((~((~cC44(iV16455)) | (~cC54xcomp(iV16455)))) | (~cC44(iV16455)) | (~cC54xcomp(iV16455))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(81,plain,
% 0.17/0.44 ((~((~cC44(iV16455)) | (~cC54xcomp(iV16455)))) | (~cC44(iV16455))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[80, 79])).
% 0.17/0.44 tff(82,plain,
% 0.17/0.44 (~((~cC44(iV16455)) | (~cC54xcomp(iV16455)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[81, 76])).
% 0.17/0.44 tff(83,plain,
% 0.17/0.44 (^[X: $i] : refl((~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X))) <=> (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(84,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X))) <=> ![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[83])).
% 0.17/0.44 tff(85,plain,
% 0.17/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC54xcomp(X) & cC44(X)) <=> (~((~cC54xcomp(X)) | (~cC44(X))))), ((cC56(X) <=> (cC54xcomp(X) & cC44(X))) <=> (cC56(X) <=> (~((~cC54xcomp(X)) | (~cC44(X))))))), rewrite((cC56(X) <=> (~((~cC54xcomp(X)) | (~cC44(X))))) <=> (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))), ((cC56(X) <=> (cC54xcomp(X) & cC44(X))) <=> (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X))))), rewrite((~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X))) <=> (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))), ((cC56(X) <=> (cC54xcomp(X) & cC44(X))) <=> (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(86,plain,
% 0.17/0.44 (![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X))) <=> ![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[85])).
% 0.17/0.44 tff(87,plain,
% 0.17/0.44 (![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X))) <=> ![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(88,axiom,(![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_82')).
% 0.17/0.44 tff(89,plain,
% 0.17/0.44 (![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.17/0.44 tff(90,plain,(
% 0.17/0.44 ![X: $i] : (cC56(X) <=> (cC54xcomp(X) & cC44(X)))),
% 0.17/0.44 inference(skolemize,[status(sab)],[89])).
% 0.17/0.44 tff(91,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[90, 86])).
% 0.17/0.44 tff(92,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[91, 84])).
% 0.17/0.44 tff(93,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(94,plain,
% 0.17/0.44 ((~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))) <=> (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(95,plain,
% 0.17/0.44 ((((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455)) <=> (((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(96,plain,
% 0.17/0.44 ((~(((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455))) <=> (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)))),
% 0.17/0.44 inference(monotonicity,[status(thm)],[95])).
% 0.17/0.44 tff(97,plain,
% 0.17/0.44 ((~(((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455))) <=> (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)))),
% 0.17/0.44 inference(transitivity,[status(thm)],[96, 94])).
% 0.17/0.44 tff(98,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))))),
% 0.17/0.44 inference(monotonicity,[status(thm)],[97])).
% 0.17/0.44 tff(99,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))))),
% 0.17/0.44 inference(transitivity,[status(thm)],[98, 93])).
% 0.17/0.44 tff(100,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16455)) | (~cC44(iV16455))) <=> cC56(iV16455)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(101,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.17/0.44 tff(102,plain,
% 0.17/0.44 (~(((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[101, 92])).
% 0.17/0.44 tff(103,plain,
% 0.17/0.44 ((((~cC44(iV16455)) | (~cC54xcomp(iV16455))) <=> cC56(iV16455)) | ((~cC44(iV16455)) | (~cC54xcomp(iV16455))) | cC56(iV16455)),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(104,plain,
% 0.17/0.44 (((~cC44(iV16455)) | (~cC54xcomp(iV16455))) | cC56(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[103, 102])).
% 0.17/0.44 tff(105,plain,
% 0.17/0.44 (cC56(iV16455)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[104, 82])).
% 0.17/0.44 tff(106,assumption,((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453)))))))), introduced(assumption)).
% 0.17/0.44 tff(107,plain,
% 0.17/0.44 (^[X: $i] : refl((~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))) <=> (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(108,plain,
% 0.17/0.44 (![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[107])).
% 0.17/0.44 tff(109,plain,
% 0.17/0.44 (^[X: $i] : rewrite((~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))) <=> (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(110,plain,
% 0.17/0.44 (![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[109])).
% 0.17/0.44 tff(111,plain,
% 0.17/0.44 (![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(transitivity,[status(thm)],[110, 108])).
% 0.17/0.44 tff(112,plain,
% 0.17/0.44 (^[X: $i] : trans(monotonicity(rewrite(((~cC60(X)) | (rR1(X, tptp_fun_Y_70(X)) & cC12xcomp(tptp_fun_Y_70(X)))) <=> ((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))), rewrite((cC60(X) | ![Y: $i] : (~(rR1(X, Y) & cC12xcomp(Y)))) <=> (cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))), ((((~cC60(X)) | (rR1(X, tptp_fun_Y_70(X)) & cC12xcomp(tptp_fun_Y_70(X)))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & cC12xcomp(Y))))) <=> (((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X)))))) & (cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))))), rewrite((((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X)))))) & (cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y))))) <=> (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))), ((((~cC60(X)) | (rR1(X, tptp_fun_Y_70(X)) & cC12xcomp(tptp_fun_Y_70(X)))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & cC12xcomp(Y))))) <=> (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(113,plain,
% 0.17/0.44 (![X: $i] : (((~cC60(X)) | (rR1(X, tptp_fun_Y_70(X)) & cC12xcomp(tptp_fun_Y_70(X)))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & cC12xcomp(Y))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[112])).
% 0.17/0.44 tff(114,plain,
% 0.17/0.44 (![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & cC12xcomp(Y))) <=> ![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & cC12xcomp(Y)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(115,axiom,(![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & cC12xcomp(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_91')).
% 0.17/0.44 tff(116,plain,
% 0.17/0.44 (![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & cC12xcomp(Y)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[115, 114])).
% 0.17/0.44 tff(117,plain,(
% 0.17/0.44 ![X: $i] : (((~cC60(X)) | (rR1(X, tptp_fun_Y_70(X)) & cC12xcomp(tptp_fun_Y_70(X)))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & cC12xcomp(Y)))))),
% 0.17/0.44 inference(skolemize,[status(sab)],[116])).
% 0.17/0.44 tff(118,plain,
% 0.17/0.44 (![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[117, 113])).
% 0.17/0.44 tff(119,plain,
% 0.17/0.44 (![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[118, 111])).
% 0.17/0.44 tff(120,plain,
% 0.17/0.44 (((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453)))))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453))))))))))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(121,plain,
% 0.17/0.44 ((~((~((~cC60(iV16453)) | (~((~rR1(iV16453, tptp_fun_Y_70(iV16453))) | (~cC12xcomp(tptp_fun_Y_70(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))))) <=> (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453)))))))))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(122,plain,
% 0.17/0.44 (((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~((~rR1(iV16453, tptp_fun_Y_70(iV16453))) | (~cC12xcomp(tptp_fun_Y_70(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453))))))))))),
% 0.17/0.44 inference(monotonicity,[status(thm)],[121])).
% 0.17/0.44 tff(123,plain,
% 0.17/0.44 (((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~((~rR1(iV16453, tptp_fun_Y_70(iV16453))) | (~cC12xcomp(tptp_fun_Y_70(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453))))))))))),
% 0.17/0.44 inference(transitivity,[status(thm)],[122, 120])).
% 0.17/0.44 tff(124,plain,
% 0.17/0.44 ((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~((~rR1(iV16453, tptp_fun_Y_70(iV16453))) | (~cC12xcomp(tptp_fun_Y_70(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))))))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(125,plain,
% 0.17/0.44 ((~![X: $i] : (~((~((~cC60(X)) | (~((~rR1(X, tptp_fun_Y_70(X))) | (~cC12xcomp(tptp_fun_Y_70(X))))))) | (~(cC60(X) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453)))))))))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.17/0.44 tff(126,plain,
% 0.17/0.44 ($false),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[125, 119, 106])).
% 0.17/0.44 tff(127,plain,(~((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453))))))))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.44 tff(128,plain,
% 0.17/0.44 (((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~((~cC12xcomp(tptp_fun_Y_70(iV16453))) | (~rR1(iV16453, tptp_fun_Y_70(iV16453)))))))) | (cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(129,plain,
% 0.17/0.44 (cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[128, 127])).
% 0.17/0.44 tff(130,assumption,(![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))), introduced(assumption)).
% 0.17/0.44 tff(131,plain,
% 0.17/0.44 (cC12xcomp(iV16461) <=> cC12xcomp(iV16461)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(132,axiom,(cC12xcomp(iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_237')).
% 0.17/0.44 tff(133,plain,
% 0.17/0.44 (cC12xcomp(iV16461)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.17/0.44 tff(134,plain,
% 0.17/0.44 (rR1(iV16453, iV16461) <=> rR1(iV16453, iV16461)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(135,axiom,(rR1(iV16453, iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_182')).
% 0.17/0.44 tff(136,plain,
% 0.17/0.44 (rR1(iV16453, iV16461)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[135, 134])).
% 0.17/0.44 tff(137,plain,
% 0.17/0.44 (((~![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))) | ((~cC12xcomp(iV16461)) | (~rR1(iV16453, iV16461)))) <=> ((~![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))) | (~cC12xcomp(iV16461)) | (~rR1(iV16453, iV16461)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(138,plain,
% 0.17/0.44 ((~![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))) | ((~cC12xcomp(iV16461)) | (~rR1(iV16453, iV16461)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(139,plain,
% 0.17/0.44 ((~![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))) | (~cC12xcomp(iV16461)) | (~rR1(iV16453, iV16461))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.17/0.44 tff(140,plain,
% 0.17/0.44 ($false),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[139, 136, 133, 130])).
% 0.17/0.44 tff(141,plain,(~![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.44 tff(142,plain,
% 0.17/0.44 ((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y)))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(143,plain,
% 0.17/0.44 ((~(cC60(iV16453) | ![Y: $i] : ((~cC12xcomp(Y)) | (~rR1(iV16453, Y))))) | cC60(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[142, 141])).
% 0.17/0.44 tff(144,plain,
% 0.17/0.44 (cC60(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[143, 129])).
% 0.17/0.44 tff(145,plain,
% 0.17/0.44 (cC58xcomp(iV16453) <=> cC58xcomp(iV16453)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(146,axiom,(cC58xcomp(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_181')).
% 0.17/0.44 tff(147,plain,
% 0.17/0.44 (cC58xcomp(iV16453)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.17/0.44 tff(148,plain,
% 0.17/0.44 ((~((~cC58xcomp(iV16453)) | (~cC60(iV16453)))) | (~cC58xcomp(iV16453)) | (~cC60(iV16453))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(149,plain,
% 0.17/0.44 ((~((~cC58xcomp(iV16453)) | (~cC60(iV16453)))) | (~cC60(iV16453))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[148, 147])).
% 0.17/0.44 tff(150,plain,
% 0.17/0.44 (~((~cC58xcomp(iV16453)) | (~cC60(iV16453)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[149, 144])).
% 0.17/0.44 tff(151,plain,
% 0.17/0.44 (^[X: $i] : refl((~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X))) <=> (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(152,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X))) <=> ![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[151])).
% 0.17/0.44 tff(153,plain,
% 0.17/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC60(X) & cC58xcomp(X)) <=> (~((~cC58xcomp(X)) | (~cC60(X))))), ((cC62(X) <=> (cC60(X) & cC58xcomp(X))) <=> (cC62(X) <=> (~((~cC58xcomp(X)) | (~cC60(X))))))), rewrite((cC62(X) <=> (~((~cC58xcomp(X)) | (~cC60(X))))) <=> (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))), ((cC62(X) <=> (cC60(X) & cC58xcomp(X))) <=> (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X))))), rewrite((~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X))) <=> (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))), ((cC62(X) <=> (cC60(X) & cC58xcomp(X))) <=> (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(154,plain,
% 0.17/0.44 (![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X))) <=> ![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[153])).
% 0.17/0.44 tff(155,plain,
% 0.17/0.44 (![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X))) <=> ![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(156,axiom,(![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_92')).
% 0.17/0.44 tff(157,plain,
% 0.17/0.44 (![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[156, 155])).
% 0.17/0.44 tff(158,plain,(
% 0.17/0.44 ![X: $i] : (cC62(X) <=> (cC60(X) & cC58xcomp(X)))),
% 0.17/0.44 inference(skolemize,[status(sab)],[157])).
% 0.17/0.44 tff(159,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[158, 154])).
% 0.17/0.44 tff(160,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[159, 152])).
% 0.17/0.44 tff(161,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))) | (~(((~cC58xcomp(iV16453)) | (~cC60(iV16453))) <=> cC62(iV16453)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(162,plain,
% 0.17/0.44 (~(((~cC58xcomp(iV16453)) | (~cC60(iV16453))) <=> cC62(iV16453))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[161, 160])).
% 0.17/0.44 tff(163,plain,
% 0.17/0.44 ((((~cC58xcomp(iV16453)) | (~cC60(iV16453))) <=> cC62(iV16453)) | ((~cC58xcomp(iV16453)) | (~cC60(iV16453))) | cC62(iV16453)),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(164,plain,
% 0.17/0.44 (((~cC58xcomp(iV16453)) | (~cC60(iV16453))) | cC62(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[163, 162])).
% 0.17/0.44 tff(165,plain,
% 0.17/0.44 (cC62(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[164, 150])).
% 0.17/0.44 tff(166,plain,
% 0.17/0.44 ((cowlNothing(X!114) | (~cowlThing(X!114))) | (~cowlNothing(X!114))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(167,plain,
% 0.17/0.44 (~cowlNothing(X!114)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[166, 14])).
% 0.17/0.44 tff(168,plain,
% 0.17/0.44 (cC74xcomp(iV16453) <=> cC74xcomp(iV16453)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(169,axiom,(cC74xcomp(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_174')).
% 0.17/0.44 tff(170,plain,
% 0.17/0.44 (cC74xcomp(iV16453)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.17/0.44 tff(171,plain,
% 0.17/0.44 ((~((~cC62(iV16453)) | (~cC74xcomp(iV16453)))) | (~cC62(iV16453)) | (~cC74xcomp(iV16453))),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(172,plain,
% 0.17/0.44 ((~((~cC62(iV16453)) | (~cC74xcomp(iV16453)))) | (~cC62(iV16453))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[171, 170])).
% 0.17/0.44 tff(173,plain,
% 0.17/0.44 (~((~cC62(iV16453)) | (~cC74xcomp(iV16453)))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[172, 165])).
% 0.17/0.44 tff(174,plain,
% 0.17/0.44 (^[X: $i] : refl((~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X))) <=> (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(175,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X))) <=> ![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[174])).
% 0.17/0.44 tff(176,plain,
% 0.17/0.44 (^[X: $i] : trans(trans(monotonicity(rewrite((cC74xcomp(X) & cC62(X)) <=> (~((~cC74xcomp(X)) | (~cC62(X))))), ((cC76(X) <=> (cC74xcomp(X) & cC62(X))) <=> (cC76(X) <=> (~((~cC74xcomp(X)) | (~cC62(X))))))), rewrite((cC76(X) <=> (~((~cC74xcomp(X)) | (~cC62(X))))) <=> (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))), ((cC76(X) <=> (cC74xcomp(X) & cC62(X))) <=> (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X))))), rewrite((~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X))) <=> (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))), ((cC76(X) <=> (cC74xcomp(X) & cC62(X))) <=> (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(177,plain,
% 0.17/0.44 (![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X))) <=> ![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[176])).
% 0.17/0.44 tff(178,plain,
% 0.17/0.44 (![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X))) <=> ![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(179,axiom,(![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_112')).
% 0.17/0.44 tff(180,plain,
% 0.17/0.44 (![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[179, 178])).
% 0.17/0.44 tff(181,plain,(
% 0.17/0.44 ![X: $i] : (cC76(X) <=> (cC74xcomp(X) & cC62(X)))),
% 0.17/0.44 inference(skolemize,[status(sab)],[180])).
% 0.17/0.44 tff(182,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[181, 177])).
% 0.17/0.44 tff(183,plain,
% 0.17/0.44 (![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[182, 175])).
% 0.17/0.44 tff(184,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(185,plain,
% 0.17/0.44 ((~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))) <=> (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(186,plain,
% 0.17/0.44 ((((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453)) <=> (((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(187,plain,
% 0.17/0.44 ((~(((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453))) <=> (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)))),
% 0.17/0.44 inference(monotonicity,[status(thm)],[186])).
% 0.17/0.44 tff(188,plain,
% 0.17/0.44 ((~(((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453))) <=> (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)))),
% 0.17/0.44 inference(transitivity,[status(thm)],[187, 185])).
% 0.17/0.44 tff(189,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))))),
% 0.17/0.44 inference(monotonicity,[status(thm)],[188])).
% 0.17/0.44 tff(190,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))))),
% 0.17/0.44 inference(transitivity,[status(thm)],[189, 184])).
% 0.17/0.44 tff(191,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16453)) | (~cC62(iV16453))) <=> cC76(iV16453)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(192,plain,
% 0.17/0.44 ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[191, 190])).
% 0.17/0.44 tff(193,plain,
% 0.17/0.44 (~(((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453))),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[192, 183])).
% 0.17/0.44 tff(194,plain,
% 0.17/0.44 ((((~cC62(iV16453)) | (~cC74xcomp(iV16453))) <=> cC76(iV16453)) | ((~cC62(iV16453)) | (~cC74xcomp(iV16453))) | cC76(iV16453)),
% 0.17/0.44 inference(tautology,[status(thm)],[])).
% 0.17/0.44 tff(195,plain,
% 0.17/0.44 (((~cC62(iV16453)) | (~cC74xcomp(iV16453))) | cC76(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[194, 193])).
% 0.17/0.44 tff(196,plain,
% 0.17/0.44 (cC76(iV16453)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[195, 173])).
% 0.17/0.44 tff(197,plain,
% 0.17/0.44 (rR1(iV16464, iV16465) <=> rR1(iV16464, iV16465)),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(198,axiom,(rR1(iV16464, iV16465)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_274')).
% 0.17/0.44 tff(199,plain,
% 0.17/0.44 (rR1(iV16464, iV16465)),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[198, 197])).
% 0.17/0.44 tff(200,plain,
% 0.17/0.44 (^[X: $i] : refl((cC38(X) | (~rR1(iV16464, X))) <=> (cC38(X) | (~rR1(iV16464, X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(201,plain,
% 0.17/0.44 (![X: $i] : (cC38(X) | (~rR1(iV16464, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[200])).
% 0.17/0.44 tff(202,plain,
% 0.17/0.44 (![X: $i] : (cC38(X) | (~rR1(iV16464, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(203,plain,
% 0.17/0.44 (^[X: $i] : rewrite((rR1(iV16464, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16464, X))))),
% 0.17/0.44 inference(bind,[status(th)],[])).
% 0.17/0.44 tff(204,plain,
% 0.17/0.44 (![X: $i] : (rR1(iV16464, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(quant_intro,[status(thm)],[203])).
% 0.17/0.44 tff(205,axiom,(![X: $i] : (rR1(iV16464, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_265')).
% 0.17/0.44 tff(206,plain,
% 0.17/0.44 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[205, 204])).
% 0.17/0.44 tff(207,plain,
% 0.17/0.44 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[206, 202])).
% 0.17/0.44 tff(208,plain,(
% 0.17/0.44 ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(skolemize,[status(sab)],[207])).
% 0.17/0.44 tff(209,plain,
% 0.17/0.44 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[208, 201])).
% 0.17/0.44 tff(210,plain,
% 0.17/0.44 (((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | (cC38(iV16465) | (~rR1(iV16464, iV16465)))) <=> ((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | cC38(iV16465) | (~rR1(iV16464, iV16465)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(211,plain,
% 0.17/0.44 ((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | (cC38(iV16465) | (~rR1(iV16464, iV16465)))),
% 0.17/0.44 inference(quant_inst,[status(thm)],[])).
% 0.17/0.44 tff(212,plain,
% 0.17/0.44 ((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | cC38(iV16465) | (~rR1(iV16464, iV16465))),
% 0.17/0.44 inference(modus_ponens,[status(thm)],[211, 210])).
% 0.17/0.44 tff(213,plain,
% 0.17/0.44 (cC38(iV16465)),
% 0.17/0.44 inference(unit_resolution,[status(thm)],[212, 209, 199])).
% 0.17/0.44 tff(214,plain,
% 0.17/0.44 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(215,plain,
% 0.17/0.44 ((~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))) <=> (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)))),
% 0.17/0.44 inference(rewrite,[status(thm)],[])).
% 0.17/0.44 tff(216,plain,
% 0.17/0.44 ((((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464)) <=> (((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(217,plain,
% 0.17/0.45 ((~(((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464))) <=> (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[216])).
% 0.17/0.45 tff(218,plain,
% 0.17/0.45 ((~(((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464))) <=> (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)))),
% 0.17/0.45 inference(transitivity,[status(thm)],[217, 215])).
% 0.17/0.45 tff(219,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[218])).
% 0.17/0.45 tff(220,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))))),
% 0.17/0.45 inference(transitivity,[status(thm)],[219, 214])).
% 0.17/0.45 tff(221,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16464)) | (~cC44(iV16464))) <=> cC56(iV16464)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(222,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[221, 220])).
% 0.17/0.45 tff(223,plain,
% 0.17/0.45 (~(((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[222, 92])).
% 0.17/0.45 tff(224,plain,
% 0.17/0.45 (rR1(iV16463, iV16464) <=> rR1(iV16463, iV16464)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(225,axiom,(rR1(iV16463, iV16464)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_263')).
% 0.17/0.45 tff(226,plain,
% 0.17/0.45 (rR1(iV16463, iV16464)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[225, 224])).
% 0.17/0.45 tff(227,plain,
% 0.17/0.45 (^[X: $i] : refl((cC56(X) | (~rR1(iV16463, X))) <=> (cC56(X) | (~rR1(iV16463, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(228,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16463, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[227])).
% 0.17/0.45 tff(229,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16463, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(230,plain,
% 0.17/0.45 (^[X: $i] : rewrite((rR1(iV16463, X) => cC56(X)) <=> (cC56(X) | (~rR1(iV16463, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(231,plain,
% 0.17/0.45 (![X: $i] : (rR1(iV16463, X) => cC56(X)) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[230])).
% 0.17/0.45 tff(232,axiom,(![X: $i] : (rR1(iV16463, X) => cC56(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_261')).
% 0.17/0.45 tff(233,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[232, 231])).
% 0.17/0.45 tff(234,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[233, 229])).
% 0.17/0.45 tff(235,plain,(
% 0.17/0.45 ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[234])).
% 0.17/0.45 tff(236,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[235, 228])).
% 0.17/0.45 tff(237,plain,
% 0.17/0.45 (((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | (cC56(iV16464) | (~rR1(iV16463, iV16464)))) <=> ((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | cC56(iV16464) | (~rR1(iV16463, iV16464)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(238,plain,
% 0.17/0.45 ((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | (cC56(iV16464) | (~rR1(iV16463, iV16464)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(239,plain,
% 0.17/0.45 ((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | cC56(iV16464) | (~rR1(iV16463, iV16464))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[238, 237])).
% 0.17/0.45 tff(240,plain,
% 0.17/0.45 (cC56(iV16464)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[239, 236, 226])).
% 0.17/0.45 tff(241,plain,
% 0.17/0.45 ((((~cC44(iV16464)) | (~cC54xcomp(iV16464))) <=> cC56(iV16464)) | (~((~cC44(iV16464)) | (~cC54xcomp(iV16464)))) | (~cC56(iV16464))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(242,plain,
% 0.17/0.45 (~((~cC44(iV16464)) | (~cC54xcomp(iV16464)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[241, 240, 223])).
% 0.17/0.45 tff(243,plain,
% 0.17/0.45 (((~cC44(iV16464)) | (~cC54xcomp(iV16464))) | cC44(iV16464)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(244,plain,
% 0.17/0.45 (cC44(iV16464)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[243, 242])).
% 0.17/0.45 tff(245,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))) | (~(((~cC40xcomp(iV16464)) | (~cC42(iV16464))) <=> cC44(iV16464)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(246,plain,
% 0.17/0.45 (~(((~cC40xcomp(iV16464)) | (~cC42(iV16464))) <=> cC44(iV16464))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[245, 71])).
% 0.17/0.45 tff(247,plain,
% 0.17/0.45 ((((~cC40xcomp(iV16464)) | (~cC42(iV16464))) <=> cC44(iV16464)) | (~((~cC40xcomp(iV16464)) | (~cC42(iV16464)))) | (~cC44(iV16464))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(248,plain,
% 0.17/0.45 (~((~cC40xcomp(iV16464)) | (~cC42(iV16464)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[247, 244, 246])).
% 0.17/0.45 tff(249,plain,
% 0.17/0.45 (((~cC40xcomp(iV16464)) | (~cC42(iV16464))) | cC42(iV16464)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(250,plain,
% 0.17/0.45 (cC42(iV16464)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[249, 248])).
% 0.17/0.45 tff(251,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC58xcomp(X)) | (~cC60(X))) <=> cC62(X)))) | (~(((~cC58xcomp(iV16463)) | (~cC60(iV16463))) <=> cC62(iV16463)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(252,plain,
% 0.17/0.45 (~(((~cC58xcomp(iV16463)) | (~cC60(iV16463))) <=> cC62(iV16463))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[251, 160])).
% 0.17/0.45 tff(253,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(254,plain,
% 0.17/0.45 ((~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))) <=> (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(255,plain,
% 0.17/0.45 ((((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463)) <=> (((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(256,plain,
% 0.17/0.45 ((~(((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463))) <=> (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[255])).
% 0.17/0.45 tff(257,plain,
% 0.17/0.45 ((~(((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463))) <=> (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)))),
% 0.17/0.45 inference(transitivity,[status(thm)],[256, 254])).
% 0.17/0.45 tff(258,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[257])).
% 0.17/0.45 tff(259,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463)))) <=> ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))))),
% 0.17/0.45 inference(transitivity,[status(thm)],[258, 253])).
% 0.17/0.45 tff(260,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC74xcomp(iV16463)) | (~cC62(iV16463))) <=> cC76(iV16463)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(261,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC74xcomp(X)) | (~cC62(X))) <=> cC76(X)))) | (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[260, 259])).
% 0.17/0.45 tff(262,plain,
% 0.17/0.45 (~(((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[261, 183])).
% 0.17/0.45 tff(263,plain,
% 0.17/0.45 (rR1(iV16440, iV16463) <=> rR1(iV16440, iV16463)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(264,axiom,(rR1(iV16440, iV16463)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_159')).
% 0.17/0.45 tff(265,plain,
% 0.17/0.45 (rR1(iV16440, iV16463)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[264, 263])).
% 0.17/0.45 tff(266,plain,
% 0.17/0.45 (^[X: $i] : refl((cC76(X) | (~rR1(iV16440, X))) <=> (cC76(X) | (~rR1(iV16440, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(267,plain,
% 0.17/0.45 (![X: $i] : (cC76(X) | (~rR1(iV16440, X))) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[266])).
% 0.17/0.45 tff(268,plain,
% 0.17/0.45 (![X: $i] : (cC76(X) | (~rR1(iV16440, X))) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(269,plain,
% 0.17/0.45 (^[X: $i] : rewrite((rR1(iV16440, X) => cC76(X)) <=> (cC76(X) | (~rR1(iV16440, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(270,plain,
% 0.17/0.45 (![X: $i] : (rR1(iV16440, X) => cC76(X)) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[269])).
% 0.17/0.45 tff(271,axiom,(![X: $i] : (rR1(iV16440, X) => cC76(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_156')).
% 0.17/0.45 tff(272,plain,
% 0.17/0.45 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[271, 270])).
% 0.17/0.45 tff(273,plain,
% 0.17/0.45 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[272, 268])).
% 0.17/0.45 tff(274,plain,(
% 0.17/0.45 ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[273])).
% 0.17/0.45 tff(275,plain,
% 0.17/0.45 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[274, 267])).
% 0.17/0.45 tff(276,plain,
% 0.17/0.45 (((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | (cC76(iV16463) | (~rR1(iV16440, iV16463)))) <=> ((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | cC76(iV16463) | (~rR1(iV16440, iV16463)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(277,plain,
% 0.17/0.45 ((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | (cC76(iV16463) | (~rR1(iV16440, iV16463)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(278,plain,
% 0.17/0.45 ((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | cC76(iV16463) | (~rR1(iV16440, iV16463))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[277, 276])).
% 0.17/0.45 tff(279,plain,
% 0.17/0.45 (cC76(iV16463)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[278, 275, 265])).
% 0.17/0.45 tff(280,plain,
% 0.17/0.45 ((((~cC62(iV16463)) | (~cC74xcomp(iV16463))) <=> cC76(iV16463)) | (~((~cC62(iV16463)) | (~cC74xcomp(iV16463)))) | (~cC76(iV16463))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(281,plain,
% 0.17/0.45 (~((~cC62(iV16463)) | (~cC74xcomp(iV16463)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[280, 279, 262])).
% 0.17/0.45 tff(282,plain,
% 0.17/0.45 (((~cC62(iV16463)) | (~cC74xcomp(iV16463))) | cC62(iV16463)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(283,plain,
% 0.17/0.45 (cC62(iV16463)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[282, 281])).
% 0.17/0.45 tff(284,plain,
% 0.17/0.45 ((((~cC58xcomp(iV16463)) | (~cC60(iV16463))) <=> cC62(iV16463)) | (~((~cC58xcomp(iV16463)) | (~cC60(iV16463)))) | (~cC62(iV16463))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(285,plain,
% 0.17/0.45 (~((~cC58xcomp(iV16463)) | (~cC60(iV16463)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[284, 283, 252])).
% 0.17/0.45 tff(286,plain,
% 0.17/0.45 (((~cC58xcomp(iV16463)) | (~cC60(iV16463))) | cC60(iV16463)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(287,plain,
% 0.17/0.45 (cC60(iV16463)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[286, 285])).
% 0.17/0.45 tff(288,plain,
% 0.17/0.45 (rR1(iV16461, iV16462) <=> rR1(iV16461, iV16462)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(289,axiom,(rR1(iV16461, iV16462)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_243')).
% 0.17/0.45 tff(290,plain,
% 0.17/0.45 (rR1(iV16461, iV16462)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[289, 288])).
% 0.17/0.45 tff(291,plain,
% 0.17/0.45 (^[X: $i] : refl((cC38(X) | (~rR1(iV16461, X))) <=> (cC38(X) | (~rR1(iV16461, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(292,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16461, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[291])).
% 0.17/0.45 tff(293,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16461, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(294,plain,
% 0.17/0.45 (^[X: $i] : rewrite((rR1(iV16461, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16461, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(295,plain,
% 0.17/0.45 (![X: $i] : (rR1(iV16461, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[294])).
% 0.17/0.45 tff(296,axiom,(![X: $i] : (rR1(iV16461, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_241')).
% 0.17/0.45 tff(297,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[296, 295])).
% 0.17/0.45 tff(298,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[297, 293])).
% 0.17/0.45 tff(299,plain,(
% 0.17/0.45 ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[298])).
% 0.17/0.45 tff(300,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[299, 292])).
% 0.17/0.45 tff(301,plain,
% 0.17/0.45 (((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | (cC38(iV16462) | (~rR1(iV16461, iV16462)))) <=> ((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | cC38(iV16462) | (~rR1(iV16461, iV16462)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(302,plain,
% 0.17/0.45 ((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | (cC38(iV16462) | (~rR1(iV16461, iV16462)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(303,plain,
% 0.17/0.45 ((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | cC38(iV16462) | (~rR1(iV16461, iV16462))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[302, 301])).
% 0.17/0.45 tff(304,plain,
% 0.17/0.45 (cC38(iV16462)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[303, 300, 290])).
% 0.17/0.45 tff(305,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(306,plain,
% 0.17/0.45 ((~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))) <=> (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(307,plain,
% 0.17/0.45 ((((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461)) <=> (((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(308,plain,
% 0.17/0.45 ((~(((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461))) <=> (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[307])).
% 0.17/0.45 tff(309,plain,
% 0.17/0.45 ((~(((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461))) <=> (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)))),
% 0.17/0.45 inference(transitivity,[status(thm)],[308, 306])).
% 0.17/0.45 tff(310,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))))),
% 0.17/0.45 inference(monotonicity,[status(thm)],[309])).
% 0.17/0.45 tff(311,plain,
% 0.17/0.45 (((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461)))) <=> ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))))),
% 0.17/0.45 inference(transitivity,[status(thm)],[310, 305])).
% 0.17/0.45 tff(312,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC54xcomp(iV16461)) | (~cC44(iV16461))) <=> cC56(iV16461)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(313,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC54xcomp(X)) | (~cC44(X))) <=> cC56(X)))) | (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[312, 311])).
% 0.17/0.45 tff(314,plain,
% 0.17/0.45 (~(((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[313, 92])).
% 0.17/0.45 tff(315,plain,
% 0.17/0.45 (^[X: $i] : refl((cC56(X) | (~rR1(iV16453, X))) <=> (cC56(X) | (~rR1(iV16453, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(316,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16453, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[315])).
% 0.17/0.45 tff(317,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16453, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(318,plain,
% 0.17/0.45 (^[X: $i] : rewrite((rR1(iV16453, X) => cC56(X)) <=> (cC56(X) | (~rR1(iV16453, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(319,plain,
% 0.17/0.45 (![X: $i] : (rR1(iV16453, X) => cC56(X)) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[318])).
% 0.17/0.45 tff(320,axiom,(![X: $i] : (rR1(iV16453, X) => cC56(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_178')).
% 0.17/0.45 tff(321,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[320, 319])).
% 0.17/0.45 tff(322,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[321, 317])).
% 0.17/0.45 tff(323,plain,(
% 0.17/0.45 ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[322])).
% 0.17/0.45 tff(324,plain,
% 0.17/0.45 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[323, 316])).
% 0.17/0.45 tff(325,plain,
% 0.17/0.45 (((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | (cC56(iV16461) | (~rR1(iV16453, iV16461)))) <=> ((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | cC56(iV16461) | (~rR1(iV16453, iV16461)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(326,plain,
% 0.17/0.45 ((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | (cC56(iV16461) | (~rR1(iV16453, iV16461)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(327,plain,
% 0.17/0.45 ((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | cC56(iV16461) | (~rR1(iV16453, iV16461))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[326, 325])).
% 0.17/0.45 tff(328,plain,
% 0.17/0.45 (cC56(iV16461)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[327, 324, 136])).
% 0.17/0.45 tff(329,plain,
% 0.17/0.45 ((((~cC44(iV16461)) | (~cC54xcomp(iV16461))) <=> cC56(iV16461)) | (~((~cC44(iV16461)) | (~cC54xcomp(iV16461)))) | (~cC56(iV16461))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(330,plain,
% 0.17/0.45 (~((~cC44(iV16461)) | (~cC54xcomp(iV16461)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[329, 328, 314])).
% 0.17/0.45 tff(331,plain,
% 0.17/0.45 (((~cC44(iV16461)) | (~cC54xcomp(iV16461))) | cC44(iV16461)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(332,plain,
% 0.17/0.45 (cC44(iV16461)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[331, 330])).
% 0.17/0.45 tff(333,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC40xcomp(X)) | (~cC42(X))) <=> cC44(X)))) | (~(((~cC40xcomp(iV16461)) | (~cC42(iV16461))) <=> cC44(iV16461)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(334,plain,
% 0.17/0.45 (~(((~cC40xcomp(iV16461)) | (~cC42(iV16461))) <=> cC44(iV16461))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[333, 71])).
% 0.17/0.45 tff(335,plain,
% 0.17/0.45 ((((~cC40xcomp(iV16461)) | (~cC42(iV16461))) <=> cC44(iV16461)) | (~((~cC40xcomp(iV16461)) | (~cC42(iV16461)))) | (~cC44(iV16461))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(336,plain,
% 0.17/0.45 (~((~cC40xcomp(iV16461)) | (~cC42(iV16461)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[335, 332, 334])).
% 0.17/0.45 tff(337,plain,
% 0.17/0.45 (((~cC40xcomp(iV16461)) | (~cC42(iV16461))) | cC42(iV16461)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(338,plain,
% 0.17/0.45 (cC42(iV16461)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[337, 336])).
% 0.17/0.45 tff(339,plain,
% 0.17/0.45 (^[X: $i] : refl((cC38(X) | (~rR1(iV16455, X))) <=> (cC38(X) | (~rR1(iV16455, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(340,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16455, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[339])).
% 0.17/0.45 tff(341,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16455, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(342,plain,
% 0.17/0.45 (^[X: $i] : rewrite((rR1(iV16455, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16455, X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(343,plain,
% 0.17/0.45 (![X: $i] : (rR1(iV16455, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[342])).
% 0.17/0.45 tff(344,axiom,(![X: $i] : (rR1(iV16455, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_188')).
% 0.17/0.45 tff(345,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[344, 343])).
% 0.17/0.45 tff(346,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[345, 341])).
% 0.17/0.45 tff(347,plain,(
% 0.17/0.45 ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[346])).
% 0.17/0.45 tff(348,plain,
% 0.17/0.45 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[347, 340])).
% 0.17/0.45 tff(349,plain,
% 0.17/0.45 (((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | (cC38(iV16460) | (~rR1(iV16455, iV16460)))) <=> ((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | cC38(iV16460) | (~rR1(iV16455, iV16460)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(350,plain,
% 0.17/0.45 ((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | (cC38(iV16460) | (~rR1(iV16455, iV16460)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(351,plain,
% 0.17/0.45 ((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | cC38(iV16460) | (~rR1(iV16455, iV16460))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[350, 349])).
% 0.17/0.45 tff(352,plain,
% 0.17/0.45 (cC38(iV16460)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[351, 348, 47])).
% 0.17/0.45 tff(353,plain,
% 0.17/0.45 (^[X: $i] : refl((~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X))) <=> (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(354,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X))) <=> ![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[353])).
% 0.17/0.45 tff(355,plain,
% 0.17/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC64xcomp(X) & cC66xcomp(X)) <=> (~((~cC64xcomp(X)) | (~cC66xcomp(X))))), ((cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X))) <=> (cC68(X) <=> (~((~cC64xcomp(X)) | (~cC66xcomp(X))))))), rewrite((cC68(X) <=> (~((~cC64xcomp(X)) | (~cC66xcomp(X))))) <=> (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))), ((cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X))) <=> (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X))))), rewrite((~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X))) <=> (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))), ((cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X))) <=> (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(356,plain,
% 0.17/0.45 (![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X))) <=> ![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[355])).
% 0.17/0.45 tff(357,plain,
% 0.17/0.45 (![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X))) <=> ![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(358,axiom,(![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_100')).
% 0.17/0.45 tff(359,plain,
% 0.17/0.45 (![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[358, 357])).
% 0.17/0.45 tff(360,plain,(
% 0.17/0.45 ![X: $i] : (cC68(X) <=> (cC64xcomp(X) & cC66xcomp(X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[359])).
% 0.17/0.45 tff(361,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[360, 356])).
% 0.17/0.45 tff(362,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[361, 354])).
% 0.17/0.45 tff(363,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC64xcomp(X)) | (~cC66xcomp(X))) <=> cC68(X)))) | (~(((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))) <=> cC68(iV16459)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(364,plain,
% 0.17/0.45 (~(((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))) <=> cC68(iV16459))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[363, 362])).
% 0.17/0.45 tff(365,plain,
% 0.17/0.45 (cC66xcomp(iV16459) <=> cC66xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(366,axiom,(cC66xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_221')).
% 0.17/0.45 tff(367,plain,
% 0.17/0.45 (cC66xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[366, 365])).
% 0.17/0.45 tff(368,plain,
% 0.17/0.45 (cC64xcomp(iV16459) <=> cC64xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(369,axiom,(cC64xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_213')).
% 0.17/0.45 tff(370,plain,
% 0.17/0.45 (cC64xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[369, 368])).
% 0.17/0.45 tff(371,plain,
% 0.17/0.45 ((~((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459)))) | (~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(372,plain,
% 0.17/0.45 (~((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[371, 370, 367])).
% 0.17/0.45 tff(373,plain,
% 0.17/0.45 ((((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))) <=> cC68(iV16459)) | ((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))) | cC68(iV16459)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(374,plain,
% 0.17/0.45 ((((~cC64xcomp(iV16459)) | (~cC66xcomp(iV16459))) <=> cC68(iV16459)) | cC68(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[373, 372])).
% 0.17/0.45 tff(375,plain,
% 0.17/0.45 (cC68(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[374, 364])).
% 0.17/0.45 tff(376,plain,
% 0.17/0.45 (^[X: $i] : refl((~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X))) <=> (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(377,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X))) <=> ![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[376])).
% 0.17/0.45 tff(378,plain,
% 0.17/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC30xcomp(X) & cC32xcomp(X)) <=> (~((~cC30xcomp(X)) | (~cC32xcomp(X))))), ((cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X))) <=> (cC34(X) <=> (~((~cC30xcomp(X)) | (~cC32xcomp(X))))))), rewrite((cC34(X) <=> (~((~cC30xcomp(X)) | (~cC32xcomp(X))))) <=> (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))), ((cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X))) <=> (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X))))), rewrite((~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X))) <=> (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))), ((cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X))) <=> (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(379,plain,
% 0.17/0.45 (![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X))) <=> ![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[378])).
% 0.17/0.45 tff(380,plain,
% 0.17/0.45 (![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X))) <=> ![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(381,axiom,(![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_52')).
% 0.17/0.45 tff(382,plain,
% 0.17/0.45 (![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[381, 380])).
% 0.17/0.45 tff(383,plain,(
% 0.17/0.45 ![X: $i] : (cC34(X) <=> (cC30xcomp(X) & cC32xcomp(X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[382])).
% 0.17/0.45 tff(384,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[383, 379])).
% 0.17/0.45 tff(385,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[384, 377])).
% 0.17/0.45 tff(386,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC30xcomp(X)) | (~cC32xcomp(X))) <=> cC34(X)))) | (~(((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))) <=> cC34(iV16459)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(387,plain,
% 0.17/0.45 (~(((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))) <=> cC34(iV16459))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[386, 385])).
% 0.17/0.45 tff(388,plain,
% 0.17/0.45 (cC32xcomp(iV16459) <=> cC32xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(389,axiom,(cC32xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_216')).
% 0.17/0.45 tff(390,plain,
% 0.17/0.45 (cC32xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[389, 388])).
% 0.17/0.45 tff(391,plain,
% 0.17/0.45 (cC30xcomp(iV16459) <=> cC30xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(392,axiom,(cC30xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_209')).
% 0.17/0.45 tff(393,plain,
% 0.17/0.45 (cC30xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[392, 391])).
% 0.17/0.45 tff(394,plain,
% 0.17/0.45 ((~((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459)))) | (~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(395,plain,
% 0.17/0.45 (~((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[394, 393, 390])).
% 0.17/0.45 tff(396,plain,
% 0.17/0.45 ((((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))) <=> cC34(iV16459)) | ((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))) | cC34(iV16459)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(397,plain,
% 0.17/0.45 ((((~cC30xcomp(iV16459)) | (~cC32xcomp(iV16459))) <=> cC34(iV16459)) | cC34(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[396, 395])).
% 0.17/0.45 tff(398,plain,
% 0.17/0.45 (cC34(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[397, 387])).
% 0.17/0.45 tff(399,plain,
% 0.17/0.45 (^[X: $i] : refl((~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X))) <=> (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(400,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X))) <=> ![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[399])).
% 0.17/0.45 tff(401,plain,
% 0.17/0.45 (^[X: $i] : trans(trans(monotonicity(rewrite((cC84xcomp(X) & cC86xcomp(X)) <=> (~((~cC84xcomp(X)) | (~cC86xcomp(X))))), ((cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X))) <=> (cC88(X) <=> (~((~cC84xcomp(X)) | (~cC86xcomp(X))))))), rewrite((cC88(X) <=> (~((~cC84xcomp(X)) | (~cC86xcomp(X))))) <=> (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))), ((cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X))) <=> (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X))))), rewrite((~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X))) <=> (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))), ((cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X))) <=> (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))))),
% 0.17/0.45 inference(bind,[status(th)],[])).
% 0.17/0.45 tff(402,plain,
% 0.17/0.45 (![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X))) <=> ![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))),
% 0.17/0.45 inference(quant_intro,[status(thm)],[401])).
% 0.17/0.45 tff(403,plain,
% 0.17/0.45 (![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X))) <=> ![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X)))),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(404,axiom,(![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_128')).
% 0.17/0.45 tff(405,plain,
% 0.17/0.45 (![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[404, 403])).
% 0.17/0.45 tff(406,plain,(
% 0.17/0.45 ![X: $i] : (cC88(X) <=> (cC84xcomp(X) & cC86xcomp(X)))),
% 0.17/0.45 inference(skolemize,[status(sab)],[405])).
% 0.17/0.45 tff(407,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[406, 402])).
% 0.17/0.45 tff(408,plain,
% 0.17/0.45 (![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[407, 400])).
% 0.17/0.45 tff(409,plain,
% 0.17/0.45 ((~![X: $i] : (~(((~cC84xcomp(X)) | (~cC86xcomp(X))) <=> cC88(X)))) | (~(((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))) <=> cC88(iV16459)))),
% 0.17/0.45 inference(quant_inst,[status(thm)],[])).
% 0.17/0.45 tff(410,plain,
% 0.17/0.45 (~(((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))) <=> cC88(iV16459))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[409, 408])).
% 0.17/0.45 tff(411,plain,
% 0.17/0.45 (cC86xcomp(iV16459) <=> cC86xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(412,axiom,(cC86xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_215')).
% 0.17/0.45 tff(413,plain,
% 0.17/0.45 (cC86xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[412, 411])).
% 0.17/0.45 tff(414,plain,
% 0.17/0.45 (cC84xcomp(iV16459) <=> cC84xcomp(iV16459)),
% 0.17/0.45 inference(rewrite,[status(thm)],[])).
% 0.17/0.45 tff(415,axiom,(cC84xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_210')).
% 0.17/0.45 tff(416,plain,
% 0.17/0.45 (cC84xcomp(iV16459)),
% 0.17/0.45 inference(modus_ponens,[status(thm)],[415, 414])).
% 0.17/0.45 tff(417,plain,
% 0.17/0.45 ((~((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459)))) | (~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(418,plain,
% 0.17/0.45 (~((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459)))),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[417, 416, 413])).
% 0.17/0.45 tff(419,plain,
% 0.17/0.45 ((((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))) <=> cC88(iV16459)) | ((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))) | cC88(iV16459)),
% 0.17/0.45 inference(tautology,[status(thm)],[])).
% 0.17/0.45 tff(420,plain,
% 0.17/0.45 ((((~cC84xcomp(iV16459)) | (~cC86xcomp(iV16459))) <=> cC88(iV16459)) | cC88(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[419, 418])).
% 0.17/0.45 tff(421,plain,
% 0.17/0.45 (cC88(iV16459)),
% 0.17/0.45 inference(unit_resolution,[status(thm)],[420, 410])).
% 0.17/0.45 tff(422,plain,
% 0.17/0.45 (^[X: $i] : refl((~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X))) <=> (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(423,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X))) <=> ![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[422])).
% 0.17/0.46 tff(424,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC46xcomp(X) & cC48xcomp(X)) <=> (~((~cC46xcomp(X)) | (~cC48xcomp(X))))), ((cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X))) <=> (cC50(X) <=> (~((~cC46xcomp(X)) | (~cC48xcomp(X))))))), rewrite((cC50(X) <=> (~((~cC46xcomp(X)) | (~cC48xcomp(X))))) <=> (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))), ((cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X))) <=> (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X))))), rewrite((~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X))) <=> (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))), ((cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X))) <=> (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(425,plain,
% 0.17/0.46 (![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X))) <=> ![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[424])).
% 0.17/0.46 tff(426,plain,
% 0.17/0.46 (![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X))) <=> ![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(427,axiom,(![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_73')).
% 0.17/0.46 tff(428,plain,
% 0.17/0.46 (![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[427, 426])).
% 0.17/0.46 tff(429,plain,(
% 0.17/0.46 ![X: $i] : (cC50(X) <=> (cC46xcomp(X) & cC48xcomp(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[428])).
% 0.17/0.46 tff(430,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[429, 425])).
% 0.17/0.46 tff(431,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[430, 423])).
% 0.17/0.46 tff(432,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC46xcomp(X)) | (~cC48xcomp(X))) <=> cC50(X)))) | (~(((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))) <=> cC50(iV16459)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(433,plain,
% 0.17/0.46 (~(((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))) <=> cC50(iV16459))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[432, 431])).
% 0.17/0.46 tff(434,plain,
% 0.17/0.46 (cC48xcomp(iV16459) <=> cC48xcomp(iV16459)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(435,axiom,(cC48xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_217')).
% 0.17/0.46 tff(436,plain,
% 0.17/0.46 (cC48xcomp(iV16459)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[435, 434])).
% 0.17/0.46 tff(437,plain,
% 0.17/0.46 (cC46xcomp(iV16459) <=> cC46xcomp(iV16459)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(438,axiom,(cC46xcomp(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_212')).
% 0.17/0.46 tff(439,plain,
% 0.17/0.46 (cC46xcomp(iV16459)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[438, 437])).
% 0.17/0.46 tff(440,plain,
% 0.17/0.46 ((~((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459)))) | (~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(441,plain,
% 0.17/0.46 (~((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[440, 439, 436])).
% 0.17/0.46 tff(442,plain,
% 0.17/0.46 ((((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))) <=> cC50(iV16459)) | ((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))) | cC50(iV16459)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(443,plain,
% 0.17/0.46 ((((~cC46xcomp(iV16459)) | (~cC48xcomp(iV16459))) <=> cC50(iV16459)) | cC50(iV16459)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[442, 441])).
% 0.17/0.46 tff(444,plain,
% 0.17/0.46 (cC50(iV16459)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[443, 433])).
% 0.17/0.46 tff(445,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X))) <=> (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(446,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X))) <=> ![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[445])).
% 0.17/0.46 tff(447,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cTOP(X) & cC36xcomp(X)) <=> (~((~cC36xcomp(X)) | (~cTOP(X))))), ((cC38(X) <=> (cTOP(X) & cC36xcomp(X))) <=> (cC38(X) <=> (~((~cC36xcomp(X)) | (~cTOP(X))))))), rewrite((cC38(X) <=> (~((~cC36xcomp(X)) | (~cTOP(X))))) <=> (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))), ((cC38(X) <=> (cTOP(X) & cC36xcomp(X))) <=> (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X))))), rewrite((~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X))) <=> (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))), ((cC38(X) <=> (cTOP(X) & cC36xcomp(X))) <=> (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(448,plain,
% 0.17/0.46 (![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X))) <=> ![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[447])).
% 0.17/0.46 tff(449,plain,
% 0.17/0.46 (![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X))) <=> ![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(450,axiom,(![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_57')).
% 0.17/0.46 tff(451,plain,
% 0.17/0.46 (![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[450, 449])).
% 0.17/0.46 tff(452,plain,(
% 0.17/0.46 ![X: $i] : (cC38(X) <=> (cTOP(X) & cC36xcomp(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[451])).
% 0.17/0.46 tff(453,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[452, 448])).
% 0.17/0.46 tff(454,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[453, 446])).
% 0.17/0.46 tff(455,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))) | (~(((~cC36xcomp(iV16457)) | (~cTOP(iV16457))) <=> cC38(iV16457)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(456,plain,
% 0.17/0.46 (~(((~cC36xcomp(iV16457)) | (~cTOP(iV16457))) <=> cC38(iV16457))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[455, 454])).
% 0.17/0.46 tff(457,plain,
% 0.17/0.46 (cC36xcomp(iV16457) <=> cC36xcomp(iV16457)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(458,axiom,(cC36xcomp(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_201')).
% 0.17/0.46 tff(459,plain,
% 0.17/0.46 (cC36xcomp(iV16457)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[458, 457])).
% 0.17/0.46 tff(460,plain,
% 0.17/0.46 (cTOP(iV16457) <=> cTOP(iV16457)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(461,axiom,(cTOP(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_197')).
% 0.17/0.46 tff(462,plain,
% 0.17/0.46 (cTOP(iV16457)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[461, 460])).
% 0.17/0.46 tff(463,plain,
% 0.17/0.46 ((~((~cC36xcomp(iV16457)) | (~cTOP(iV16457)))) | (~cC36xcomp(iV16457)) | (~cTOP(iV16457))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(464,plain,
% 0.17/0.46 (~((~cC36xcomp(iV16457)) | (~cTOP(iV16457)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[463, 462, 459])).
% 0.17/0.46 tff(465,plain,
% 0.17/0.46 ((((~cC36xcomp(iV16457)) | (~cTOP(iV16457))) <=> cC38(iV16457)) | ((~cC36xcomp(iV16457)) | (~cTOP(iV16457))) | cC38(iV16457)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(466,plain,
% 0.17/0.46 ((((~cC36xcomp(iV16457)) | (~cTOP(iV16457))) <=> cC38(iV16457)) | cC38(iV16457)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[465, 464])).
% 0.17/0.46 tff(467,plain,
% 0.17/0.46 (cC38(iV16457)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[466, 456])).
% 0.17/0.46 tff(468,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC36xcomp(X)) | (~cTOP(X))) <=> cC38(X)))) | (~(((~cC36xcomp(iV16448)) | (~cTOP(iV16448))) <=> cC38(iV16448)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(469,plain,
% 0.17/0.46 (~(((~cC36xcomp(iV16448)) | (~cTOP(iV16448))) <=> cC38(iV16448))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[468, 454])).
% 0.17/0.46 tff(470,plain,
% 0.17/0.46 (cC36xcomp(iV16448) <=> cC36xcomp(iV16448)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(471,axiom,(cC36xcomp(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_168')).
% 0.17/0.46 tff(472,plain,
% 0.17/0.46 (cC36xcomp(iV16448)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[471, 470])).
% 0.17/0.46 tff(473,plain,
% 0.17/0.46 (cTOP(iV16448) <=> cTOP(iV16448)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(474,axiom,(cTOP(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_163')).
% 0.17/0.46 tff(475,plain,
% 0.17/0.46 (cTOP(iV16448)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[474, 473])).
% 0.17/0.46 tff(476,plain,
% 0.17/0.46 ((~((~cC36xcomp(iV16448)) | (~cTOP(iV16448)))) | (~cC36xcomp(iV16448)) | (~cTOP(iV16448))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(477,plain,
% 0.17/0.46 (~((~cC36xcomp(iV16448)) | (~cTOP(iV16448)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[476, 475, 472])).
% 0.17/0.46 tff(478,plain,
% 0.17/0.46 ((((~cC36xcomp(iV16448)) | (~cTOP(iV16448))) <=> cC38(iV16448)) | ((~cC36xcomp(iV16448)) | (~cTOP(iV16448))) | cC38(iV16448)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(479,plain,
% 0.17/0.46 ((((~cC36xcomp(iV16448)) | (~cTOP(iV16448))) <=> cC38(iV16448)) | cC38(iV16448)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[478, 477])).
% 0.17/0.46 tff(480,plain,
% 0.17/0.46 (cC38(iV16448)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[479, 469])).
% 0.17/0.46 tff(481,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X))) <=> (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(482,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X))) <=> ![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[481])).
% 0.17/0.46 tff(483,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC96xcomp(X) & cC82(X)) <=> (~((~cC96xcomp(X)) | (~cC82(X))))), ((cC98(X) <=> (cC96xcomp(X) & cC82(X))) <=> (cC98(X) <=> (~((~cC96xcomp(X)) | (~cC82(X))))))), rewrite((cC98(X) <=> (~((~cC96xcomp(X)) | (~cC82(X))))) <=> (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))), ((cC98(X) <=> (cC96xcomp(X) & cC82(X))) <=> (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X))))), rewrite((~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X))) <=> (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))), ((cC98(X) <=> (cC96xcomp(X) & cC82(X))) <=> (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(484,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X))) <=> ![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[483])).
% 0.17/0.46 tff(485,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X))) <=> ![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(486,axiom,(![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_143')).
% 0.17/0.46 tff(487,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[486, 485])).
% 0.17/0.46 tff(488,plain,(
% 0.17/0.46 ![X: $i] : (cC98(X) <=> (cC96xcomp(X) & cC82(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[487])).
% 0.17/0.46 tff(489,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[488, 484])).
% 0.17/0.46 tff(490,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[489, 482])).
% 0.17/0.46 tff(491,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)))) <=> ((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(492,plain,
% 0.17/0.46 ((~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))) <=> (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(493,plain,
% 0.17/0.46 ((((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440)) <=> (((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(494,plain,
% 0.17/0.46 ((~(((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440))) <=> (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)))),
% 0.17/0.46 inference(monotonicity,[status(thm)],[493])).
% 0.17/0.46 tff(495,plain,
% 0.17/0.46 ((~(((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440))) <=> (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)))),
% 0.17/0.46 inference(transitivity,[status(thm)],[494, 492])).
% 0.17/0.46 tff(496,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440)))) <=> ((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))))),
% 0.17/0.46 inference(monotonicity,[status(thm)],[495])).
% 0.17/0.46 tff(497,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440)))) <=> ((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))))),
% 0.17/0.46 inference(transitivity,[status(thm)],[496, 491])).
% 0.17/0.46 tff(498,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC96xcomp(iV16440)) | (~cC82(iV16440))) <=> cC98(iV16440)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(499,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC96xcomp(X)) | (~cC82(X))) <=> cC98(X)))) | (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[498, 497])).
% 0.17/0.46 tff(500,plain,
% 0.17/0.46 (~(((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[499, 490])).
% 0.17/0.46 tff(501,plain,
% 0.17/0.46 (rR1(iV16439, iV16440) <=> rR1(iV16439, iV16440)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(502,axiom,(rR1(iV16439, iV16440)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_150')).
% 0.17/0.46 tff(503,plain,
% 0.17/0.46 (rR1(iV16439, iV16440)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[502, 501])).
% 0.17/0.46 tff(504,plain,
% 0.17/0.46 (^[X: $i] : refl((cC98(X) | (~rR1(iV16439, X))) <=> (cC98(X) | (~rR1(iV16439, X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(505,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) | (~rR1(iV16439, X))) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[504])).
% 0.17/0.46 tff(506,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) | (~rR1(iV16439, X))) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(507,plain,
% 0.17/0.46 (^[X: $i] : rewrite((rR1(iV16439, X) => cC98(X)) <=> (cC98(X) | (~rR1(iV16439, X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(508,plain,
% 0.17/0.46 (![X: $i] : (rR1(iV16439, X) => cC98(X)) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[507])).
% 0.17/0.46 tff(509,axiom,(![X: $i] : (rR1(iV16439, X) => cC98(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_146')).
% 0.17/0.46 tff(510,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[509, 508])).
% 0.17/0.46 tff(511,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[510, 506])).
% 0.17/0.46 tff(512,plain,(
% 0.17/0.46 ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[511])).
% 0.17/0.46 tff(513,plain,
% 0.17/0.46 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[512, 505])).
% 0.17/0.46 tff(514,plain,
% 0.17/0.46 (((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | (cC98(iV16440) | (~rR1(iV16439, iV16440)))) <=> ((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | cC98(iV16440) | (~rR1(iV16439, iV16440)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(515,plain,
% 0.17/0.46 ((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | (cC98(iV16440) | (~rR1(iV16439, iV16440)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(516,plain,
% 0.17/0.46 ((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | cC98(iV16440) | (~rR1(iV16439, iV16440))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[515, 514])).
% 0.17/0.46 tff(517,plain,
% 0.17/0.46 (cC98(iV16440)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[516, 513, 503])).
% 0.17/0.46 tff(518,plain,
% 0.17/0.46 ((((~cC82(iV16440)) | (~cC96xcomp(iV16440))) <=> cC98(iV16440)) | (~((~cC82(iV16440)) | (~cC96xcomp(iV16440)))) | (~cC98(iV16440))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(519,plain,
% 0.17/0.46 (~((~cC82(iV16440)) | (~cC96xcomp(iV16440)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[518, 517, 500])).
% 0.17/0.46 tff(520,plain,
% 0.17/0.46 (((~cC82(iV16440)) | (~cC96xcomp(iV16440))) | cC82(iV16440)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(521,plain,
% 0.17/0.46 (cC82(iV16440)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[520, 519])).
% 0.17/0.46 tff(522,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X))) <=> (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(523,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X))) <=> ![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[522])).
% 0.17/0.46 tff(524,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC80(X) & cC78xcomp(X)) <=> (~((~cC78xcomp(X)) | (~cC80(X))))), ((cC82(X) <=> (cC80(X) & cC78xcomp(X))) <=> (cC82(X) <=> (~((~cC78xcomp(X)) | (~cC80(X))))))), rewrite((cC82(X) <=> (~((~cC78xcomp(X)) | (~cC80(X))))) <=> (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))), ((cC82(X) <=> (cC80(X) & cC78xcomp(X))) <=> (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X))))), rewrite((~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X))) <=> (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))), ((cC82(X) <=> (cC80(X) & cC78xcomp(X))) <=> (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(525,plain,
% 0.17/0.46 (![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X))) <=> ![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[524])).
% 0.17/0.46 tff(526,plain,
% 0.17/0.46 (![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X))) <=> ![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(527,axiom,(![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_120')).
% 0.17/0.46 tff(528,plain,
% 0.17/0.46 (![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[527, 526])).
% 0.17/0.46 tff(529,plain,(
% 0.17/0.46 ![X: $i] : (cC82(X) <=> (cC80(X) & cC78xcomp(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[528])).
% 0.17/0.46 tff(530,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[529, 525])).
% 0.17/0.46 tff(531,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[530, 523])).
% 0.17/0.46 tff(532,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC78xcomp(X)) | (~cC80(X))) <=> cC82(X)))) | (~(((~cC78xcomp(iV16440)) | (~cC80(iV16440))) <=> cC82(iV16440)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(533,plain,
% 0.17/0.46 (~(((~cC78xcomp(iV16440)) | (~cC80(iV16440))) <=> cC82(iV16440))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[532, 531])).
% 0.17/0.46 tff(534,plain,
% 0.17/0.46 ((((~cC78xcomp(iV16440)) | (~cC80(iV16440))) <=> cC82(iV16440)) | (~((~cC78xcomp(iV16440)) | (~cC80(iV16440)))) | (~cC82(iV16440))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(535,plain,
% 0.17/0.46 (~((~cC78xcomp(iV16440)) | (~cC80(iV16440)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[534, 521, 533])).
% 0.17/0.46 tff(536,plain,
% 0.17/0.46 (((~cC78xcomp(iV16440)) | (~cC80(iV16440))) | cC80(iV16440)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(537,plain,
% 0.17/0.46 (cC80(iV16440)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[536, 535])).
% 0.17/0.46 tff(538,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(539,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[538])).
% 0.17/0.46 tff(540,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC28(X) & cC106(X)) <=> (~((~cC28(X)) | (~cC106(X))))), ((cC108(X) <=> (cC28(X) & cC106(X))) <=> (cC108(X) <=> (~((~cC28(X)) | (~cC106(X))))))), rewrite((cC108(X) <=> (~((~cC28(X)) | (~cC106(X))))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))), ((cC108(X) <=> (cC28(X) & cC106(X))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))))), rewrite((~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))), ((cC108(X) <=> (cC28(X) & cC106(X))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(541,plain,
% 0.17/0.46 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[540])).
% 0.17/0.46 tff(542,plain,
% 0.17/0.46 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X))) <=> ![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(543,axiom,(![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_12')).
% 0.17/0.46 tff(544,plain,
% 0.17/0.46 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[543, 542])).
% 0.17/0.46 tff(545,plain,(
% 0.17/0.46 ![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[544])).
% 0.17/0.46 tff(546,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[545, 541])).
% 0.17/0.46 tff(547,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[546, 539])).
% 0.17/0.46 tff(548,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(549,plain,
% 0.17/0.46 ((~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(550,plain,
% 0.17/0.46 ((((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)) <=> (((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(551,plain,
% 0.17/0.46 ((~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.17/0.46 inference(monotonicity,[status(thm)],[550])).
% 0.17/0.46 tff(552,plain,
% 0.17/0.46 ((~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.17/0.46 inference(transitivity,[status(thm)],[551, 549])).
% 0.17/0.46 tff(553,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))))),
% 0.17/0.46 inference(monotonicity,[status(thm)],[552])).
% 0.17/0.46 tff(554,plain,
% 0.17/0.46 (((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)))) <=> ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))))),
% 0.17/0.46 inference(transitivity,[status(thm)],[553, 548])).
% 0.17/0.46 tff(555,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(556,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[555, 554])).
% 0.17/0.46 tff(557,plain,
% 0.17/0.46 (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[556, 547])).
% 0.17/0.46 tff(558,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(559,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))) <=> ![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[558])).
% 0.17/0.46 tff(560,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC108(X) & cC130(X)) <=> (~((~cC108(X)) | (~cC130(X))))), ((cTEST(X) <=> (cC108(X) & cC130(X))) <=> (cTEST(X) <=> (~((~cC108(X)) | (~cC130(X))))))), rewrite((cTEST(X) <=> (~((~cC108(X)) | (~cC130(X))))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))), ((cTEST(X) <=> (cC108(X) & cC130(X))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))))), rewrite((~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))), ((cTEST(X) <=> (cC108(X) & cC130(X))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(561,plain,
% 0.17/0.46 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X))) <=> ![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[560])).
% 0.17/0.46 tff(562,plain,
% 0.17/0.46 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X))) <=> ![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(563,axiom,(![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_145')).
% 0.17/0.46 tff(564,plain,
% 0.17/0.46 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[563, 562])).
% 0.17/0.46 tff(565,plain,(
% 0.17/0.46 ![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[564])).
% 0.17/0.46 tff(566,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[565, 561])).
% 0.17/0.46 tff(567,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[566, 559])).
% 0.17/0.46 tff(568,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))) | (~(((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(569,plain,
% 0.17/0.46 (~(((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[568, 567])).
% 0.17/0.46 tff(570,plain,
% 0.17/0.46 (cTEST(iV16439) <=> cTEST(iV16439)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(571,axiom,(cTEST(iV16439)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_149')).
% 0.17/0.46 tff(572,plain,
% 0.17/0.46 (cTEST(iV16439)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[571, 570])).
% 0.17/0.46 tff(573,plain,
% 0.17/0.46 ((((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)) | (~((~cC108(iV16439)) | (~cC130(iV16439)))) | (~cTEST(iV16439))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(574,plain,
% 0.17/0.46 ((((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)) | (~((~cC108(iV16439)) | (~cC130(iV16439))))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[573, 572])).
% 0.17/0.46 tff(575,plain,
% 0.17/0.46 (~((~cC108(iV16439)) | (~cC130(iV16439)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[574, 569])).
% 0.17/0.46 tff(576,plain,
% 0.17/0.46 (((~cC108(iV16439)) | (~cC130(iV16439))) | cC108(iV16439)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(577,plain,
% 0.17/0.46 (cC108(iV16439)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[576, 575])).
% 0.17/0.46 tff(578,plain,
% 0.17/0.46 ((((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)) | (~((~cC106(iV16439)) | (~cC28(iV16439)))) | (~cC108(iV16439))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(579,plain,
% 0.17/0.46 ((((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)) | (~((~cC106(iV16439)) | (~cC28(iV16439))))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[578, 577])).
% 0.17/0.46 tff(580,plain,
% 0.17/0.46 (~((~cC106(iV16439)) | (~cC28(iV16439)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[579, 557])).
% 0.17/0.46 tff(581,plain,
% 0.17/0.46 (((~cC106(iV16439)) | (~cC28(iV16439))) | cC28(iV16439)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(582,plain,
% 0.17/0.46 (cC28(iV16439)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[581, 580])).
% 0.17/0.46 tff(583,plain,
% 0.17/0.46 (((~cC106(iV16439)) | (~cC28(iV16439))) | cC106(iV16439)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(584,plain,
% 0.17/0.46 (cC106(iV16439)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[583, 580])).
% 0.17/0.46 tff(585,plain,
% 0.17/0.46 (^[X: $i] : refl((~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X))) <=> (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(586,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X))) <=> ![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[585])).
% 0.17/0.46 tff(587,plain,
% 0.17/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC104(X) & cC100xcomp(X)) <=> (~((~cC100xcomp(X)) | (~cC104(X))))), ((cC106(X) <=> (cC104(X) & cC100xcomp(X))) <=> (cC106(X) <=> (~((~cC100xcomp(X)) | (~cC104(X))))))), rewrite((cC106(X) <=> (~((~cC100xcomp(X)) | (~cC104(X))))) <=> (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))), ((cC106(X) <=> (cC104(X) & cC100xcomp(X))) <=> (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X))))), rewrite((~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X))) <=> (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))), ((cC106(X) <=> (cC104(X) & cC100xcomp(X))) <=> (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))))),
% 0.17/0.46 inference(bind,[status(th)],[])).
% 0.17/0.46 tff(588,plain,
% 0.17/0.46 (![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X))) <=> ![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))),
% 0.17/0.46 inference(quant_intro,[status(thm)],[587])).
% 0.17/0.46 tff(589,plain,
% 0.17/0.46 (![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X))) <=> ![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X)))),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(590,axiom,(![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_11')).
% 0.17/0.46 tff(591,plain,
% 0.17/0.46 (![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[590, 589])).
% 0.17/0.46 tff(592,plain,(
% 0.17/0.46 ![X: $i] : (cC106(X) <=> (cC104(X) & cC100xcomp(X)))),
% 0.17/0.46 inference(skolemize,[status(sab)],[591])).
% 0.17/0.46 tff(593,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[592, 588])).
% 0.17/0.46 tff(594,plain,
% 0.17/0.46 (![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[593, 586])).
% 0.17/0.46 tff(595,plain,
% 0.17/0.46 ((~![X: $i] : (~(((~cC100xcomp(X)) | (~cC104(X))) <=> cC106(X)))) | (~(((~cC100xcomp(iV16439)) | (~cC104(iV16439))) <=> cC106(iV16439)))),
% 0.17/0.46 inference(quant_inst,[status(thm)],[])).
% 0.17/0.46 tff(596,plain,
% 0.17/0.46 (~(((~cC100xcomp(iV16439)) | (~cC104(iV16439))) <=> cC106(iV16439))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[595, 594])).
% 0.17/0.46 tff(597,plain,
% 0.17/0.46 ((((~cC100xcomp(iV16439)) | (~cC104(iV16439))) <=> cC106(iV16439)) | (~((~cC100xcomp(iV16439)) | (~cC104(iV16439)))) | (~cC106(iV16439))),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(598,plain,
% 0.17/0.46 (~((~cC100xcomp(iV16439)) | (~cC104(iV16439)))),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[597, 584, 596])).
% 0.17/0.46 tff(599,plain,
% 0.17/0.46 (((~cC100xcomp(iV16439)) | (~cC104(iV16439))) | cC104(iV16439)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(600,plain,
% 0.17/0.46 (cC104(iV16439)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[599, 598])).
% 0.17/0.46 tff(601,plain,
% 0.17/0.46 (((~cC108(iV16439)) | (~cC130(iV16439))) | cC130(iV16439)),
% 0.17/0.46 inference(tautology,[status(thm)],[])).
% 0.17/0.46 tff(602,plain,
% 0.17/0.46 (cC130(iV16439)),
% 0.17/0.46 inference(unit_resolution,[status(thm)],[601, 575])).
% 0.17/0.46 tff(603,plain,
% 0.17/0.46 (cowlThing(iV16465) <=> cowlThing(iV16465)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(604,axiom,(cowlThing(iV16465)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_276')).
% 0.17/0.46 tff(605,plain,
% 0.17/0.46 (cowlThing(iV16465)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[604, 603])).
% 0.17/0.46 tff(606,plain,
% 0.17/0.46 (cowlThing(iV16464) <=> cowlThing(iV16464)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(607,axiom,(cowlThing(iV16464)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_264')).
% 0.17/0.46 tff(608,plain,
% 0.17/0.46 (cowlThing(iV16464)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[607, 606])).
% 0.17/0.46 tff(609,plain,
% 0.17/0.46 (cowlThing(iV16463) <=> cowlThing(iV16463)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(610,axiom,(cowlThing(iV16463)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_256')).
% 0.17/0.46 tff(611,plain,
% 0.17/0.46 (cowlThing(iV16463)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[610, 609])).
% 0.17/0.46 tff(612,plain,
% 0.17/0.46 (cowlThing(iV16462) <=> cowlThing(iV16462)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(613,axiom,(cowlThing(iV16462)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_246')).
% 0.17/0.46 tff(614,plain,
% 0.17/0.46 (cowlThing(iV16462)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[613, 612])).
% 0.17/0.46 tff(615,plain,
% 0.17/0.46 (cowlThing(iV16461) <=> cowlThing(iV16461)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(616,axiom,(cowlThing(iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_233')).
% 0.17/0.46 tff(617,plain,
% 0.17/0.46 (cowlThing(iV16461)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[616, 615])).
% 0.17/0.46 tff(618,plain,
% 0.17/0.46 (cowlThing(iV16460) <=> cowlThing(iV16460)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(619,axiom,(cowlThing(iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_223')).
% 0.17/0.46 tff(620,plain,
% 0.17/0.46 (cowlThing(iV16460)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[619, 618])).
% 0.17/0.46 tff(621,plain,
% 0.17/0.46 (cowlThing(iV16459) <=> cowlThing(iV16459)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(622,axiom,(cowlThing(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_205')).
% 0.17/0.46 tff(623,plain,
% 0.17/0.46 (cowlThing(iV16459)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[622, 621])).
% 0.17/0.46 tff(624,plain,
% 0.17/0.46 (cowlThing(iV16457) <=> cowlThing(iV16457)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(625,axiom,(cowlThing(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_195')).
% 0.17/0.46 tff(626,plain,
% 0.17/0.46 (cowlThing(iV16457)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[625, 624])).
% 0.17/0.46 tff(627,plain,
% 0.17/0.46 (cowlThing(iV16455) <=> cowlThing(iV16455)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(628,axiom,(cowlThing(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_184')).
% 0.17/0.46 tff(629,plain,
% 0.17/0.46 (cowlThing(iV16455)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[628, 627])).
% 0.17/0.46 tff(630,plain,
% 0.17/0.46 (cowlThing(iV16453) <=> cowlThing(iV16453)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(631,axiom,(cowlThing(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_175')).
% 0.17/0.46 tff(632,plain,
% 0.17/0.46 (cowlThing(iV16453)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[631, 630])).
% 0.17/0.46 tff(633,plain,
% 0.17/0.46 (cowlThing(iV16448) <=> cowlThing(iV16448)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(634,axiom,(cowlThing(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_162')).
% 0.17/0.46 tff(635,plain,
% 0.17/0.46 (cowlThing(iV16448)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[634, 633])).
% 0.17/0.46 tff(636,plain,
% 0.17/0.46 (cowlThing(iV16440) <=> cowlThing(iV16440)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(637,axiom,(cowlThing(iV16440)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_153')).
% 0.17/0.46 tff(638,plain,
% 0.17/0.46 (cowlThing(iV16440)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[637, 636])).
% 0.17/0.46 tff(639,plain,
% 0.17/0.46 (cowlThing(iV16439) <=> cowlThing(iV16439)),
% 0.17/0.46 inference(rewrite,[status(thm)],[])).
% 0.17/0.46 tff(640,axiom,(cowlThing(iV16439)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_147')).
% 0.17/0.46 tff(641,plain,
% 0.17/0.46 (cowlThing(iV16439)),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[640, 639])).
% 0.17/0.46 tff(642,plain,
% 0.17/0.46 (((cowlNothing(X!114) | (~cowlThing(X!114))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465))) <=> (cowlNothing(X!114) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465)) | (~cowlThing(X!114)))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(643,plain,
% 0.17/0.47 ((~(~(cowlNothing(X!114) | (~cowlThing(X!114))))) <=> (cowlNothing(X!114) | (~cowlThing(X!114)))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(644,plain,
% 0.17/0.47 ((cowlThing(X!114) & (~cowlNothing(X!114))) <=> (~(cowlNothing(X!114) | (~cowlThing(X!114))))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(645,plain,
% 0.17/0.47 ((~(cowlThing(X!114) & (~cowlNothing(X!114)))) <=> (~(~(cowlNothing(X!114) | (~cowlThing(X!114)))))),
% 0.17/0.47 inference(monotonicity,[status(thm)],[644])).
% 0.17/0.47 tff(646,plain,
% 0.17/0.47 ((~(cowlThing(X!114) & (~cowlNothing(X!114)))) <=> (cowlNothing(X!114) | (~cowlThing(X!114)))),
% 0.17/0.47 inference(transitivity,[status(thm)],[645, 643])).
% 0.17/0.47 tff(647,plain,
% 0.17/0.47 (((~(cowlThing(X!114) & (~cowlNothing(X!114)))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465))) <=> ((cowlNothing(X!114) | (~cowlThing(X!114))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465)))),
% 0.17/0.47 inference(monotonicity,[status(thm)],[646])).
% 0.17/0.47 tff(648,plain,
% 0.17/0.47 (((~(cowlThing(X!114) & (~cowlNothing(X!114)))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465))) <=> (cowlNothing(X!114) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465)) | (~cowlThing(X!114)))),
% 0.17/0.47 inference(transitivity,[status(thm)],[647, 642])).
% 0.17/0.47 tff(649,plain,
% 0.17/0.47 (((~(cowlThing(X!114) & (~cowlNothing(X!114)))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465))) <=> ((~(cowlThing(X!114) & (~cowlNothing(X!114)))) | (xsd_integer(X!115) <=> xsd_string(X!115)) | (~cC130(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cowlThing(iV16439)) | (~cC98(iV16440)) | (~cC80(iV16440)) | (~cC82(iV16440)) | (~cowlThing(iV16440)) | (~cC38(iV16448)) | (~cowlThing(iV16448)) | (~cC76(iV16453)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC60(iV16453)) | (~cC56(iV16455)) | (~cC44(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16455)) | (~cC38(iV16457)) | (~cowlThing(iV16457)) | (~cC50(iV16459)) | (~cC88(iV16459)) | (~cC34(iV16459)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC38(iV16460)) | (~cowlThing(iV16460)) | (~cC42(iV16461)) | (~cC56(iV16461)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC38(iV16462)) | (~cowlThing(iV16462)) | (~cC76(iV16463)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC60(iV16463)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC38(iV16465)) | (~cowlThing(iV16465)))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(650,plain,
% 0.17/0.47 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465)) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(651,plain,
% 0.17/0.47 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465)))),
% 0.17/0.47 inference(monotonicity,[status(thm)],[650])).
% 0.17/0.47 tff(652,plain,
% 0.17/0.47 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465)))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(653,plain,
% 0.17/0.47 ((~((((((((((((((((((((((((((((((((((((((((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC130(iV16439)) & cC108(iV16439)) & cC104(iV16439)) & cC106(iV16439)) & cC28(iV16439)) & cowlThing(iV16439)) & cC98(iV16440)) & cC80(iV16440)) & cC82(iV16440)) & cowlThing(iV16440)) & cC38(iV16448)) & cowlThing(iV16448)) & cC76(iV16453)) & cC62(iV16453)) & cowlThing(iV16453)) & cC60(iV16453)) & cC56(iV16455)) & cC44(iV16455)) & cC42(iV16455)) & cowlThing(iV16455)) & cC38(iV16457)) & cowlThing(iV16457)) & cC50(iV16459)) & cC88(iV16459)) & cC34(iV16459)) & cC68(iV16459)) & cowlThing(iV16459)) & cC38(iV16460)) & cowlThing(iV16460)) & cC42(iV16461)) & cC56(iV16461)) & cC44(iV16461)) & cowlThing(iV16461)) & cC38(iV16462)) & cowlThing(iV16462)) & cC76(iV16463)) & cC62(iV16463)) & cowlThing(iV16463)) & cC60(iV16463)) & cC56(iV16464)) & cC42(iV16464)) & cC44(iV16464)) & cowlThing(iV16464)) & cC38(iV16465)) & cowlThing(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465)))),
% 0.17/0.47 inference(rewrite,[status(thm)],[])).
% 0.17/0.47 tff(654,axiom,(~((((((((((((((((((((((((((((((((((((((((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC130(iV16439)) & cC108(iV16439)) & cC104(iV16439)) & cC106(iV16439)) & cC28(iV16439)) & cowlThing(iV16439)) & cC98(iV16440)) & cC80(iV16440)) & cC82(iV16440)) & cowlThing(iV16440)) & cC38(iV16448)) & cowlThing(iV16448)) & cC76(iV16453)) & cC62(iV16453)) & cowlThing(iV16453)) & cC60(iV16453)) & cC56(iV16455)) & cC44(iV16455)) & cC42(iV16455)) & cowlThing(iV16455)) & cC38(iV16457)) & cowlThing(iV16457)) & cC50(iV16459)) & cC88(iV16459)) & cC34(iV16459)) & cC68(iV16459)) & cowlThing(iV16459)) & cC38(iV16460)) & cowlThing(iV16460)) & cC42(iV16461)) & cC56(iV16461)) & cC44(iV16461)) & cowlThing(iV16461)) & cC38(iV16462)) & cowlThing(iV16462)) & cC76(iV16463)) & cC62(iV16463)) & cowlThing(iV16463)) & cC60(iV16463)) & cC56(iV16464)) & cC42(iV16464)) & cC44(iV16464)) & cowlThing(iV16464)) & cC38(iV16465)) & cowlThing(iV16465))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','the_axiom')).
% 0.17/0.47 tff(655,plain,
% 0.17/0.47 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))),
% 0.17/0.47 inference(modus_ponens,[status(thm)],[654, 653])).
% 0.17/0.47 tff(656,plain,
% 0.17/0.47 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))),
% 0.17/0.47 inference(modus_ponens,[status(thm)],[655, 651])).
% 0.17/0.47 tff(657,plain,
% 0.17/0.47 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))),
% 0.17/0.47 inference(modus_ponens,[status(thm)],[656, 652])).
% 0.17/0.47 tff(658,plain,
% 0.17/0.47 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC130(iV16439) & cC108(iV16439) & cC104(iV16439) & cC106(iV16439) & cC28(iV16439) & cowlThing(iV16439) & cC98(iV16440) & cC80(iV16440) & cC82(iV16440) & cowlThing(iV16440) & cC38(iV16448) & cowlThing(iV16448) & cC76(iV16453) & cC62(iV16453) & cowlThing(iV16453) & cC60(iV16453) & cC56(iV16455) & cC44(iV16455) & cC42(iV16455) & cowlThing(iV16455) & cC38(iV16457) & cowlThing(iV16457) & cC50(iV16459) & cC88(iV16459) & cC34(iV16459) & cC68(iV16459) & cowlThing(iV16459) & cC38(iV16460) & cowlThing(iV16460) & cC42(iV16461) & cC56(iV16461) & cC44(iV16461) & cowlThing(iV16461) & cC38(iV16462) & cowlThing(iV16462) & cC76(iV16463) & cC62(iV16463) & cowlThing(iV16463) & cC60(iV16463) & cC56(iV16464) & cC42(iV16464) & cC44(iV16464) & cowlThing(iV16464) & cC38(iV16465) & cowlThing(iV16465))),
% 0.17/0.48 inference(modus_ponens,[status(thm)],[657, 651])).
% 0.17/0.48 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.17/0.48 (a!2 (not (and (cowlThing X!114) (not (cowlNothing X!114)))))
% 0.17/0.48 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.17/0.48 (a!5 (refl (~ (not (cC130 iV16439)) (not (cC130 iV16439)))))
% 0.17/0.48 (a!6 (refl (~ (not (cC108 iV16439)) (not (cC108 iV16439)))))
% 0.17/0.48 (a!7 (refl (~ (not (cC104 iV16439)) (not (cC104 iV16439)))))
% 0.17/0.48 (a!8 (refl (~ (not (cC106 iV16439)) (not (cC106 iV16439)))))
% 0.17/0.48 (a!9 (refl (~ (not (cC28 iV16439)) (not (cC28 iV16439)))))
% 0.17/0.48 (a!10 (refl (~ (not (cowlThing iV16439)) (not (cowlThing iV16439)))))
% 0.17/0.48 (a!11 (refl (~ (not (cC98 iV16440)) (not (cC98 iV16440)))))
% 0.17/0.48 (a!12 (refl (~ (not (cC80 iV16440)) (not (cC80 iV16440)))))
% 0.17/0.48 (a!13 (refl (~ (not (cC82 iV16440)) (not (cC82 iV16440)))))
% 0.17/0.48 (a!14 (refl (~ (not (cowlThing iV16440)) (not (cowlThing iV16440)))))
% 0.17/0.48 (a!15 (refl (~ (not (cC38 iV16448)) (not (cC38 iV16448)))))
% 0.17/0.48 (a!16 (refl (~ (not (cowlThing iV16448)) (not (cowlThing iV16448)))))
% 0.17/0.48 (a!17 (refl (~ (not (cC76 iV16453)) (not (cC76 iV16453)))))
% 0.17/0.48 (a!18 (refl (~ (not (cC62 iV16453)) (not (cC62 iV16453)))))
% 0.17/0.48 (a!19 (refl (~ (not (cowlThing iV16453)) (not (cowlThing iV16453)))))
% 0.17/0.48 (a!20 (refl (~ (not (cC60 iV16453)) (not (cC60 iV16453)))))
% 0.17/0.48 (a!21 (refl (~ (not (cC56 iV16455)) (not (cC56 iV16455)))))
% 0.17/0.48 (a!22 (refl (~ (not (cC44 iV16455)) (not (cC44 iV16455)))))
% 0.17/0.48 (a!23 (refl (~ (not (cC42 iV16455)) (not (cC42 iV16455)))))
% 0.17/0.48 (a!24 (refl (~ (not (cowlThing iV16455)) (not (cowlThing iV16455)))))
% 0.17/0.48 (a!25 (refl (~ (not (cC38 iV16457)) (not (cC38 iV16457)))))
% 0.17/0.48 (a!26 (refl (~ (not (cowlThing iV16457)) (not (cowlThing iV16457)))))
% 0.17/0.48 (a!27 (refl (~ (not (cC50 iV16459)) (not (cC50 iV16459)))))
% 0.17/0.48 (a!28 (refl (~ (not (cC88 iV16459)) (not (cC88 iV16459)))))
% 0.17/0.48 (a!29 (refl (~ (not (cC34 iV16459)) (not (cC34 iV16459)))))
% 0.17/0.48 (a!30 (refl (~ (not (cC68 iV16459)) (not (cC68 iV16459)))))
% 0.17/0.48 (a!31 (refl (~ (not (cowlThing iV16459)) (not (cowlThing iV16459)))))
% 0.17/0.48 (a!32 (refl (~ (not (cC38 iV16460)) (not (cC38 iV16460)))))
% 0.17/0.48 (a!33 (refl (~ (not (cowlThing iV16460)) (not (cowlThing iV16460)))))
% 0.17/0.48 (a!34 (refl (~ (not (cC42 iV16461)) (not (cC42 iV16461)))))
% 0.17/0.48 (a!35 (refl (~ (not (cC56 iV16461)) (not (cC56 iV16461)))))
% 0.17/0.48 (a!36 (refl (~ (not (cC44 iV16461)) (not (cC44 iV16461)))))
% 0.17/0.48 (a!37 (refl (~ (not (cowlThing iV16461)) (not (cowlThing iV16461)))))
% 0.17/0.48 (a!38 (refl (~ (not (cC38 iV16462)) (not (cC38 iV16462)))))
% 0.17/0.48 (a!39 (refl (~ (not (cowlThing iV16462)) (not (cowlThing iV16462)))))
% 0.17/0.48 (a!40 (refl (~ (not (cC76 iV16463)) (not (cC76 iV16463)))))
% 0.17/0.48 (a!41 (refl (~ (not (cC62 iV16463)) (not (cC62 iV16463)))))
% 0.17/0.48 (a!42 (refl (~ (not (cowlThing iV16463)) (not (cowlThing iV16463)))))
% 0.17/0.48 (a!43 (refl (~ (not (cC60 iV16463)) (not (cC60 iV16463)))))
% 0.17/0.48 (a!44 (refl (~ (not (cC56 iV16464)) (not (cC56 iV16464)))))
% 0.17/0.48 (a!45 (refl (~ (not (cC42 iV16464)) (not (cC42 iV16464)))))
% 0.17/0.48 (a!46 (refl (~ (not (cC44 iV16464)) (not (cC44 iV16464)))))
% 0.17/0.48 (a!47 (refl (~ (not (cowlThing iV16464)) (not (cowlThing iV16464)))))
% 0.17/0.48 (a!48 (refl (~ (not (cC38 iV16465)) (not (cC38 iV16465)))))
% 0.17/0.48 (a!49 (refl (~ (not (cowlThing iV16465)) (not (cowlThing iV16465))))))
% 0.17/0.48 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!115) (xsd_string X!115)))))
% 0.17/0.48 (a!50 (~ (not (and a!1
% 0.17/0.48 a!3
% 0.17/0.48 (cC130 iV16439)
% 0.17/0.48 (cC108 iV16439)
% 0.17/0.48 (cC104 iV16439)
% 0.17/0.48 (cC106 iV16439)
% 0.17/0.48 (cC28 iV16439)
% 0.17/0.48 (cowlThing iV16439)
% 0.17/0.48 (cC98 iV16440)
% 0.17/0.48 (cC80 iV16440)
% 0.17/0.48 (cC82 iV16440)
% 0.17/0.48 (cowlThing iV16440)
% 0.17/0.48 (cC38 iV16448)
% 0.17/0.48 (cowlThing iV16448)
% 0.17/0.48 (cC76 iV16453)
% 0.17/0.48 (cC62 iV16453)
% 0.17/0.48 (cowlThing iV16453)
% 0.17/0.48 (cC60 iV16453)
% 0.17/0.48 (cC56 iV16455)
% 0.17/0.48 (cC44 iV16455)
% 0.17/0.48 (cC42 iV16455)
% 0.17/0.48 (cowlThing iV16455)
% 0.17/0.48 (cC38 iV16457)
% 0.17/0.48 (cowlThing iV16457)
% 0.17/0.48 (cC50 iV16459)
% 0.17/0.48 (cC88 iV16459)
% 0.17/0.48 (cC34 iV16459)
% 0.17/0.48 (cC68 iV16459)
% 0.17/0.48 (cowlThing iV16459)
% 0.17/0.48 (cC38 iV16460)
% 0.17/0.48 (cowlThing iV16460)
% 0.17/0.48 (cC42 iV16461)
% 0.17/0.48 (cC56 iV16461)
% 0.17/0.48 (cC44 iV16461)
% 0.17/0.48 (cowlThing iV16461)
% 0.17/0.48 (cC38 iV16462)
% 0.17/0.48 (cowlThing iV16462)
% 0.17/0.48 (cC76 iV16463)
% 0.17/0.48 (cC62 iV16463)
% 0.17/0.48 (cowlThing iV16463)
% 0.17/0.48 (cC60 iV16463)
% 0.17/0.48 (cC56 iV16464)
% 0.17/0.48 (cC42 iV16464)
% 0.17/0.48 (cC44 iV16464)
% 0.17/0.48 (cowlThing iV16464)
% 0.17/0.48 (cC38 iV16465)
% 0.17/0.48 (cowlThing iV16465)))
% 0.17/0.48 (or a!2
% 0.17/0.48 (= (xsd_integer X!115) (xsd_string X!115))
% 0.17/0.48 (not (cC130 iV16439))
% 0.17/0.48 (not (cC108 iV16439))
% 0.17/0.48 (not (cC104 iV16439))
% 0.17/0.48 (not (cC106 iV16439))
% 0.17/0.48 (not (cC28 iV16439))
% 0.17/0.48 (not (cowlThing iV16439))
% 0.17/0.48 (not (cC98 iV16440))
% 0.17/0.48 (not (cC80 iV16440))
% 0.17/0.48 (not (cC82 iV16440))
% 0.17/0.48 (not (cowlThing iV16440))
% 0.17/0.48 (not (cC38 iV16448))
% 0.17/0.48 (not (cowlThing iV16448))
% 0.17/0.48 (not (cC76 iV16453))
% 0.17/0.48 (not (cC62 iV16453))
% 0.17/0.48 (not (cowlThing iV16453))
% 0.17/0.48 (not (cC60 iV16453))
% 0.17/0.48 (not (cC56 iV16455))
% 0.17/0.48 (not (cC44 iV16455))
% 0.17/0.48 (not (cC42 iV16455))
% 0.17/0.48 (not (cowlThing iV16455))
% 0.17/0.48 (not (cC38 iV16457))
% 0.17/0.48 (not (cowlThing iV16457))
% 0.17/0.48 (not (cC50 iV16459))
% 0.17/0.48 (not (cC88 iV16459))
% 0.17/0.48 (not (cC34 iV16459))
% 0.17/0.48 (not (cC68 iV16459))
% 0.17/0.48 (not (cowlThing iV16459))
% 0.17/0.48 (not (cC38 iV16460))
% 0.17/0.48 (not (cowlThing iV16460))
% 0.17/0.48 (not (cC42 iV16461))
% 0.17/0.48 (not (cC56 iV16461))
% 0.17/0.48 (not (cC44 iV16461))
% 0.17/0.48 (not (cowlThing iV16461))
% 0.17/0.48 (not (cC38 iV16462))
% 0.17/0.48 (not (cowlThing iV16462))
% 0.17/0.48 (not (cC76 iV16463))
% 0.17/0.48 (not (cC62 iV16463))
% 0.17/0.48 (not (cowlThing iV16463))
% 0.17/0.48 (not (cC60 iV16463))
% 0.17/0.48 (not (cC56 iV16464))
% 0.17/0.48 (not (cC42 iV16464))
% 0.17/0.48 (not (cC44 iV16464))
% 0.17/0.48 (not (cowlThing iV16464))
% 0.17/0.48 (not (cC38 iV16465))
% 0.17/0.48 (not (cowlThing iV16465))))))
% 0.17/0.48 (nnf-neg (sk (~ (not a!1) a!2))
% 0.17/0.48 a!4
% 0.17/0.48 a!5
% 0.17/0.48 a!6
% 0.17/0.48 a!7
% 0.17/0.48 a!8
% 0.17/0.48 a!9
% 0.17/0.48 a!10
% 0.17/0.48 a!11
% 0.17/0.48 a!12
% 0.17/0.48 a!13
% 0.17/0.48 a!14
% 0.17/0.48 a!15
% 0.17/0.48 a!16
% 0.17/0.48 a!17
% 0.17/0.48 a!18
% 0.17/0.48 a!19
% 0.17/0.48 a!20
% 0.17/0.48 a!21
% 0.17/0.48 a!22
% 0.17/0.48 a!23
% 0.17/0.48 a!24
% 0.17/0.48 a!25
% 0.17/0.48 a!26
% 0.17/0.48 a!27
% 0.17/0.48 a!28
% 0.17/0.48 a!29
% 0.17/0.48 a!30
% 0.17/0.48 a!31
% 0.17/0.48 a!32
% 0.17/0.48 a!33
% 0.17/0.48 a!34
% 0.17/0.48 a!35
% 0.17/0.48 a!36
% 0.17/0.48 a!37
% 0.17/0.48 a!38
% 0.17/0.48 a!39
% 0.17/0.48 a!40
% 0.17/0.48 a!41
% 0.17/0.48 a!42
% 0.17/0.48 a!43
% 0.17/0.48 a!44
% 0.17/0.48 a!45
% 0.17/0.48 a!46
% 0.17/0.48 a!47
% 0.17/0.48 a!48
% 0.17/0.48 a!49
% 0.17/0.48 a!50)))
% 0.17/0.48 Proof display could not be completed: unexpected number of arguments
% 0.17/0.49 % E exiting
%------------------------------------------------------------------------------