%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS153+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:13:29 AM UTC 2025
% Result : Theorem 0.20s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS153+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 19 19:12:12 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.45 % SZS status Theorem
% 0.20/0.45 % SZS output start Proof
% 0.20/0.45 tff(xsd_string_type, type, (
% 0.20/0.45 xsd_string: $i > $o)).
% 0.20/0.45 tff(tptp_fun_X_29_type, type, (
% 0.20/0.45 tptp_fun_X_29: $i)).
% 0.20/0.45 tff(xsd_integer_type, type, (
% 0.20/0.45 xsd_integer: $i > $o)).
% 0.20/0.45 tff(cowlThing_type, type, (
% 0.20/0.45 cowlThing: $i > $o)).
% 0.20/0.45 tff(tptp_fun_X_28_type, type, (
% 0.20/0.45 tptp_fun_X_28: $i)).
% 0.20/0.45 tff(cowlNothing_type, type, (
% 0.20/0.45 cowlNothing: $i > $o)).
% 0.20/0.45 tff(cC42_type, type, (
% 0.20/0.45 cC42: $i > $o)).
% 0.20/0.45 tff(iV16455_type, type, (
% 0.20/0.45 iV16455: $i)).
% 0.20/0.45 tff(rR1_type, type, (
% 0.20/0.45 rR1: ( $i * $i ) > $o)).
% 0.20/0.45 tff(cC8_type, type, (
% 0.20/0.45 cC8: $i > $o)).
% 0.20/0.45 tff(tptp_fun_Y_14_type, type, (
% 0.20/0.45 tptp_fun_Y_14: $i > $i)).
% 0.20/0.45 tff(iV16460_type, type, (
% 0.20/0.45 iV16460: $i)).
% 0.20/0.45 tff(cC56_type, type, (
% 0.20/0.45 cC56: $i > $o)).
% 0.20/0.45 tff(cC44_type, type, (
% 0.20/0.45 cC44: $i > $o)).
% 0.20/0.45 tff(cC54_type, type, (
% 0.20/0.45 cC54: $i > $o)).
% 0.20/0.45 tff(cC40_type, type, (
% 0.20/0.45 cC40: $i > $o)).
% 0.20/0.45 tff(cC60_type, type, (
% 0.20/0.45 cC60: $i > $o)).
% 0.20/0.45 tff(iV16453_type, type, (
% 0.20/0.45 iV16453: $i)).
% 0.20/0.45 tff(cC12_type, type, (
% 0.20/0.45 cC12: $i > $o)).
% 0.20/0.45 tff(tptp_fun_Y_18_type, type, (
% 0.20/0.45 tptp_fun_Y_18: $i > $i)).
% 0.20/0.45 tff(iV16461_type, type, (
% 0.20/0.45 iV16461: $i)).
% 0.20/0.45 tff(cC62_type, type, (
% 0.20/0.45 cC62: $i > $o)).
% 0.20/0.45 tff(cC58_type, type, (
% 0.20/0.45 cC58: $i > $o)).
% 0.20/0.45 tff(cC76_type, type, (
% 0.20/0.45 cC76: $i > $o)).
% 0.20/0.45 tff(cC74_type, type, (
% 0.20/0.45 cC74: $i > $o)).
% 0.20/0.45 tff(cC38_type, type, (
% 0.20/0.45 cC38: $i > $o)).
% 0.20/0.45 tff(iV16465_type, type, (
% 0.20/0.45 iV16465: $i)).
% 0.20/0.45 tff(iV16464_type, type, (
% 0.20/0.45 iV16464: $i)).
% 0.20/0.45 tff(iV16463_type, type, (
% 0.20/0.45 iV16463: $i)).
% 0.20/0.45 tff(iV16440_type, type, (
% 0.20/0.45 iV16440: $i)).
% 0.20/0.45 tff(iV16462_type, type, (
% 0.20/0.45 iV16462: $i)).
% 0.20/0.45 tff(cC34_type, type, (
% 0.20/0.45 cC34: $i > $o)).
% 0.20/0.45 tff(iV16459_type, type, (
% 0.20/0.45 iV16459: $i)).
% 0.20/0.45 tff(cC32_type, type, (
% 0.20/0.45 cC32: $i > $o)).
% 0.20/0.45 tff(cC30_type, type, (
% 0.20/0.45 cC30: $i > $o)).
% 0.20/0.45 tff(cC50_type, type, (
% 0.20/0.45 cC50: $i > $o)).
% 0.20/0.45 tff(cC48_type, type, (
% 0.20/0.45 cC48: $i > $o)).
% 0.20/0.45 tff(cC46_type, type, (
% 0.20/0.45 cC46: $i > $o)).
% 0.20/0.45 tff(cC88_type, type, (
% 0.20/0.45 cC88: $i > $o)).
% 0.20/0.45 tff(cC86_type, type, (
% 0.20/0.45 cC86: $i > $o)).
% 0.20/0.45 tff(cC84_type, type, (
% 0.20/0.45 cC84: $i > $o)).
% 0.20/0.45 tff(cC68_type, type, (
% 0.20/0.45 cC68: $i > $o)).
% 0.20/0.45 tff(cC66_type, type, (
% 0.20/0.45 cC66: $i > $o)).
% 0.20/0.45 tff(cC64_type, type, (
% 0.20/0.45 cC64: $i > $o)).
% 0.20/0.45 tff(iV16457_type, type, (
% 0.20/0.45 iV16457: $i)).
% 0.20/0.45 tff(cTOP_type, type, (
% 0.20/0.45 cTOP: $i > $o)).
% 0.20/0.45 tff(cC36_type, type, (
% 0.20/0.45 cC36: $i > $o)).
% 0.20/0.45 tff(iV16448_type, type, (
% 0.20/0.45 iV16448: $i)).
% 0.20/0.45 tff(cC98_type, type, (
% 0.20/0.45 cC98: $i > $o)).
% 0.20/0.45 tff(iV16439_type, type, (
% 0.20/0.45 iV16439: $i)).
% 0.20/0.45 tff(cC82_type, type, (
% 0.20/0.45 cC82: $i > $o)).
% 0.20/0.45 tff(cC96_type, type, (
% 0.20/0.45 cC96: $i > $o)).
% 0.20/0.45 tff(cC80_type, type, (
% 0.20/0.45 cC80: $i > $o)).
% 0.20/0.45 tff(cC78_type, type, (
% 0.20/0.45 cC78: $i > $o)).
% 0.20/0.45 tff(cC104_type, type, (
% 0.20/0.45 cC104: $i > $o)).
% 0.20/0.45 tff(cC100_type, type, (
% 0.20/0.45 cC100: $i > $o)).
% 0.20/0.45 tff(cC106_type, type, (
% 0.20/0.45 cC106: $i > $o)).
% 0.20/0.45 tff(cC28_type, type, (
% 0.20/0.45 cC28: $i > $o)).
% 0.20/0.45 tff(cC108_type, type, (
% 0.20/0.45 cC108: $i > $o)).
% 0.20/0.45 tff(cC130_type, type, (
% 0.20/0.45 cC130: $i > $o)).
% 0.20/0.45 tff(cTEST_type, type, (
% 0.20/0.45 cTEST: $i > $o)).
% 0.20/0.45 tff(1,assumption,(cowlNothing(X!28) | (~cowlThing(X!28))), introduced(assumption)).
% 0.20/0.45 tff(2,plain,
% 0.20/0.45 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(3,plain,
% 0.20/0.45 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[2])).
% 0.20/0.45 tff(4,plain,
% 0.20/0.45 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(5,plain,
% 0.20/0.45 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[4])).
% 0.20/0.45 tff(6,plain,
% 0.20/0.45 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(7,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_0')).
% 0.20/0.45 tff(8,plain,
% 0.20/0.45 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.20/0.45 tff(9,plain,(
% 0.20/0.45 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[8])).
% 0.20/0.45 tff(10,plain,
% 0.20/0.45 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[9, 5])).
% 0.20/0.45 tff(11,plain,
% 0.20/0.45 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[10, 3])).
% 0.20/0.45 tff(12,plain,
% 0.20/0.45 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!28) | (~cowlThing(X!28))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(13,plain,
% 0.20/0.45 ($false),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[12, 11, 1])).
% 0.20/0.45 tff(14,plain,(~(cowlNothing(X!28) | (~cowlThing(X!28)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.45 tff(15,plain,
% 0.20/0.45 ((cowlNothing(X!28) | (~cowlThing(X!28))) | cowlThing(X!28)),
% 0.20/0.45 inference(tautology,[status(thm)],[])).
% 0.20/0.45 tff(16,plain,
% 0.20/0.45 (cowlThing(X!28)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[15, 14])).
% 0.20/0.45 tff(17,assumption,((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455)))))))), introduced(assumption)).
% 0.20/0.45 tff(18,plain,
% 0.20/0.45 (^[X: $i] : refl((~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))) <=> (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(19,plain,
% 0.20/0.45 (![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[18])).
% 0.20/0.45 tff(20,plain,
% 0.20/0.45 (^[X: $i] : rewrite((~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))) <=> (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(21,plain,
% 0.20/0.45 (![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[20])).
% 0.20/0.45 tff(22,plain,
% 0.20/0.45 (![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[21, 19])).
% 0.20/0.45 tff(23,plain,
% 0.20/0.45 (^[X: $i] : trans(monotonicity(rewrite(((~cC42(X)) | (rR1(X, tptp_fun_Y_14(X)) & (~cC8(tptp_fun_Y_14(X))))) <=> ((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))), rewrite((cC42(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC8(Y))))) <=> (cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))), ((((~cC42(X)) | (rR1(X, tptp_fun_Y_14(X)) & (~cC8(tptp_fun_Y_14(X))))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC8(Y)))))) <=> (((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X)))))) & (cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))))), rewrite((((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X)))))) & (cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y))))) <=> (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))), ((((~cC42(X)) | (rR1(X, tptp_fun_Y_14(X)) & (~cC8(tptp_fun_Y_14(X))))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC8(Y)))))) <=> (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(24,plain,
% 0.20/0.45 (![X: $i] : (((~cC42(X)) | (rR1(X, tptp_fun_Y_14(X)) & (~cC8(tptp_fun_Y_14(X))))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC8(Y)))))) <=> ![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[23])).
% 0.20/0.46 tff(25,plain,
% 0.20/0.46 (![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC8(Y)))) <=> ![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC8(Y))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(26,axiom,(![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC8(Y))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_29')).
% 0.20/0.46 tff(27,plain,
% 0.20/0.46 (![X: $i] : (cC42(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC8(Y))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.20/0.46 tff(28,plain,(
% 0.20/0.46 ![X: $i] : (((~cC42(X)) | (rR1(X, tptp_fun_Y_14(X)) & (~cC8(tptp_fun_Y_14(X))))) & (cC42(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC8(Y))))))),
% 0.20/0.46 inference(skolemize,[status(sab)],[27])).
% 0.20/0.46 tff(29,plain,
% 0.20/0.46 (![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[28, 24])).
% 0.20/0.46 tff(30,plain,
% 0.20/0.46 (![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.20/0.46 tff(31,plain,
% 0.20/0.46 (((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455)))))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(32,plain,
% 0.20/0.46 ((~((~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))))) <=> (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455)))))))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(33,plain,
% 0.20/0.46 (((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))))))),
% 0.20/0.46 inference(monotonicity,[status(thm)],[32])).
% 0.20/0.46 tff(34,plain,
% 0.20/0.46 (((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))))))) <=> ((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))))))),
% 0.20/0.46 inference(transitivity,[status(thm)],[33, 31])).
% 0.20/0.46 tff(35,plain,
% 0.20/0.46 ((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))) | (~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))))))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(36,plain,
% 0.20/0.46 ((~![X: $i] : (~((~((~cC42(X)) | (~(cC8(tptp_fun_Y_14(X)) | (~rR1(X, tptp_fun_Y_14(X))))))) | (~(cC42(X) | ![Y: $i] : (cC8(Y) | (~rR1(X, Y)))))))) | (~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455)))))))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.20/0.46 tff(37,plain,
% 0.20/0.46 ($false),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[36, 30, 17])).
% 0.20/0.46 tff(38,plain,(~((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455))))))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.46 tff(39,plain,
% 0.20/0.46 (((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | (~((~cC42(iV16455)) | (~(cC8(tptp_fun_Y_14(iV16455)) | (~rR1(iV16455, tptp_fun_Y_14(iV16455)))))))) | (cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(40,plain,
% 0.20/0.46 (cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.20/0.46 tff(41,assumption,(![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))), introduced(assumption)).
% 0.20/0.46 tff(42,plain,
% 0.20/0.46 ((~cC8(iV16460)) <=> (~cC8(iV16460))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(43,axiom,(~cC8(iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_141')).
% 0.20/0.46 tff(44,plain,
% 0.20/0.46 (~cC8(iV16460)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.20/0.46 tff(45,plain,
% 0.20/0.46 (rR1(iV16455, iV16460) <=> rR1(iV16455, iV16460)),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(46,axiom,(rR1(iV16455, iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_107')).
% 0.20/0.46 tff(47,plain,
% 0.20/0.46 (rR1(iV16455, iV16460)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.20/0.46 tff(48,plain,
% 0.20/0.46 (((~![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))) | (cC8(iV16460) | (~rR1(iV16455, iV16460)))) <=> ((~![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))) | cC8(iV16460) | (~rR1(iV16455, iV16460)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(49,plain,
% 0.20/0.46 ((~![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))) | (cC8(iV16460) | (~rR1(iV16455, iV16460)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(50,plain,
% 0.20/0.46 ((~![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))) | cC8(iV16460) | (~rR1(iV16455, iV16460))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.20/0.46 tff(51,plain,
% 0.20/0.46 ($false),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[50, 47, 44, 41])).
% 0.20/0.46 tff(52,plain,(~![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.46 tff(53,plain,
% 0.20/0.46 ((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y)))),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(54,plain,
% 0.20/0.46 ((~(cC42(iV16455) | ![Y: $i] : (cC8(Y) | (~rR1(iV16455, Y))))) | cC42(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[53, 52])).
% 0.20/0.46 tff(55,plain,
% 0.20/0.46 (cC42(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[54, 40])).
% 0.20/0.46 tff(56,plain,
% 0.20/0.46 ((~cC40(iV16455)) <=> (~cC40(iV16455))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(57,axiom,(~cC40(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_98')).
% 0.20/0.46 tff(58,plain,
% 0.20/0.46 (~cC40(iV16455)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.20/0.46 tff(59,plain,
% 0.20/0.46 ((~(cC40(iV16455) | (~cC42(iV16455)))) | cC40(iV16455) | (~cC42(iV16455))),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(60,plain,
% 0.20/0.46 ((~(cC40(iV16455) | (~cC42(iV16455)))) | (~cC42(iV16455))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[59, 58])).
% 0.20/0.46 tff(61,plain,
% 0.20/0.46 (~(cC40(iV16455) | (~cC42(iV16455)))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[60, 55])).
% 0.20/0.46 tff(62,plain,
% 0.20/0.46 (^[X: $i] : refl((~((cC40(X) | (~cC42(X))) <=> cC44(X))) <=> (~((cC40(X) | (~cC42(X))) <=> cC44(X))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(63,plain,
% 0.20/0.46 (![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X))) <=> ![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[62])).
% 0.20/0.46 tff(64,plain,
% 0.20/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC40(X)) & cC42(X)) <=> (~(cC40(X) | (~cC42(X))))), ((cC44(X) <=> ((~cC40(X)) & cC42(X))) <=> (cC44(X) <=> (~(cC40(X) | (~cC42(X))))))), rewrite((cC44(X) <=> (~(cC40(X) | (~cC42(X))))) <=> (~((cC40(X) | (~cC42(X))) <=> cC44(X)))), ((cC44(X) <=> ((~cC40(X)) & cC42(X))) <=> (~((cC40(X) | (~cC42(X))) <=> cC44(X))))), rewrite((~((cC40(X) | (~cC42(X))) <=> cC44(X))) <=> (~((cC40(X) | (~cC42(X))) <=> cC44(X)))), ((cC44(X) <=> ((~cC40(X)) & cC42(X))) <=> (~((cC40(X) | (~cC42(X))) <=> cC44(X)))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(65,plain,
% 0.20/0.46 (![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X))) <=> ![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[64])).
% 0.20/0.46 tff(66,plain,
% 0.20/0.46 (![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X))) <=> ![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X)))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(67,axiom,(![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_30')).
% 0.20/0.46 tff(68,plain,
% 0.20/0.46 (![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[67, 66])).
% 0.20/0.46 tff(69,plain,(
% 0.20/0.46 ![X: $i] : (cC44(X) <=> ((~cC40(X)) & cC42(X)))),
% 0.20/0.46 inference(skolemize,[status(sab)],[68])).
% 0.20/0.46 tff(70,plain,
% 0.20/0.46 (![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[69, 65])).
% 0.20/0.46 tff(71,plain,
% 0.20/0.46 (![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[70, 63])).
% 0.20/0.46 tff(72,plain,
% 0.20/0.46 ((~![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))) | (~((cC40(iV16455) | (~cC42(iV16455))) <=> cC44(iV16455)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(73,plain,
% 0.20/0.46 (~((cC40(iV16455) | (~cC42(iV16455))) <=> cC44(iV16455))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.20/0.46 tff(74,plain,
% 0.20/0.46 (((cC40(iV16455) | (~cC42(iV16455))) <=> cC44(iV16455)) | (cC40(iV16455) | (~cC42(iV16455))) | cC44(iV16455)),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(75,plain,
% 0.20/0.46 ((cC40(iV16455) | (~cC42(iV16455))) | cC44(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.20/0.46 tff(76,plain,
% 0.20/0.46 (cC44(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[75, 61])).
% 0.20/0.46 tff(77,plain,
% 0.20/0.46 ((~cC54(iV16455)) <=> (~cC54(iV16455))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(78,axiom,(~cC54(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_103')).
% 0.20/0.46 tff(79,plain,
% 0.20/0.46 (~cC54(iV16455)),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.20/0.46 tff(80,plain,
% 0.20/0.46 ((~(cC54(iV16455) | (~cC44(iV16455)))) | cC54(iV16455) | (~cC44(iV16455))),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(81,plain,
% 0.20/0.46 ((~(cC54(iV16455) | (~cC44(iV16455)))) | (~cC44(iV16455))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[80, 79])).
% 0.20/0.46 tff(82,plain,
% 0.20/0.46 (~(cC54(iV16455) | (~cC44(iV16455)))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[81, 76])).
% 0.20/0.46 tff(83,plain,
% 0.20/0.46 (^[X: $i] : refl((~((cC54(X) | (~cC44(X))) <=> cC56(X))) <=> (~((cC54(X) | (~cC44(X))) <=> cC56(X))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(84,plain,
% 0.20/0.46 (![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X))) <=> ![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[83])).
% 0.20/0.46 tff(85,plain,
% 0.20/0.46 (^[X: $i] : trans(trans(monotonicity(rewrite((cC44(X) & (~cC54(X))) <=> (~(cC54(X) | (~cC44(X))))), ((cC56(X) <=> (cC44(X) & (~cC54(X)))) <=> (cC56(X) <=> (~(cC54(X) | (~cC44(X))))))), rewrite((cC56(X) <=> (~(cC54(X) | (~cC44(X))))) <=> (~((cC54(X) | (~cC44(X))) <=> cC56(X)))), ((cC56(X) <=> (cC44(X) & (~cC54(X)))) <=> (~((cC54(X) | (~cC44(X))) <=> cC56(X))))), rewrite((~((cC54(X) | (~cC44(X))) <=> cC56(X))) <=> (~((cC54(X) | (~cC44(X))) <=> cC56(X)))), ((cC56(X) <=> (cC44(X) & (~cC54(X)))) <=> (~((cC54(X) | (~cC44(X))) <=> cC56(X)))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(86,plain,
% 0.20/0.46 (![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X)))) <=> ![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[85])).
% 0.20/0.46 tff(87,plain,
% 0.20/0.46 (![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X)))) <=> ![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X))))),
% 0.20/0.46 inference(rewrite,[status(thm)],[])).
% 0.20/0.46 tff(88,axiom,(![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_36')).
% 0.20/0.46 tff(89,plain,
% 0.20/0.46 (![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X))))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.20/0.46 tff(90,plain,(
% 0.20/0.46 ![X: $i] : (cC56(X) <=> (cC44(X) & (~cC54(X))))),
% 0.20/0.46 inference(skolemize,[status(sab)],[89])).
% 0.20/0.46 tff(91,plain,
% 0.20/0.46 (![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[90, 86])).
% 0.20/0.46 tff(92,plain,
% 0.20/0.46 (![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))),
% 0.20/0.46 inference(modus_ponens,[status(thm)],[91, 84])).
% 0.20/0.46 tff(93,plain,
% 0.20/0.46 ((~![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))) | (~((cC54(iV16455) | (~cC44(iV16455))) <=> cC56(iV16455)))),
% 0.20/0.46 inference(quant_inst,[status(thm)],[])).
% 0.20/0.46 tff(94,plain,
% 0.20/0.46 (~((cC54(iV16455) | (~cC44(iV16455))) <=> cC56(iV16455))),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[93, 92])).
% 0.20/0.46 tff(95,plain,
% 0.20/0.46 (((cC54(iV16455) | (~cC44(iV16455))) <=> cC56(iV16455)) | (cC54(iV16455) | (~cC44(iV16455))) | cC56(iV16455)),
% 0.20/0.46 inference(tautology,[status(thm)],[])).
% 0.20/0.46 tff(96,plain,
% 0.20/0.46 ((cC54(iV16455) | (~cC44(iV16455))) | cC56(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[95, 94])).
% 0.20/0.46 tff(97,plain,
% 0.20/0.46 (cC56(iV16455)),
% 0.20/0.46 inference(unit_resolution,[status(thm)],[96, 82])).
% 0.20/0.46 tff(98,assumption,((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453)))))))), introduced(assumption)).
% 0.20/0.46 tff(99,plain,
% 0.20/0.46 (^[X: $i] : refl((~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))) <=> (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(100,plain,
% 0.20/0.46 (![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[99])).
% 0.20/0.46 tff(101,plain,
% 0.20/0.46 (^[X: $i] : rewrite((~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))) <=> (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))))),
% 0.20/0.46 inference(bind,[status(th)],[])).
% 0.20/0.46 tff(102,plain,
% 0.20/0.46 (![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(quant_intro,[status(thm)],[101])).
% 0.20/0.46 tff(103,plain,
% 0.20/0.46 (![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.46 inference(transitivity,[status(thm)],[102, 100])).
% 0.20/0.46 tff(104,plain,
% 0.20/0.46 (^[X: $i] : trans(monotonicity(rewrite(((~cC60(X)) | (rR1(X, tptp_fun_Y_18(X)) & (~cC12(tptp_fun_Y_18(X))))) <=> ((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))), rewrite((cC60(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC12(Y))))) <=> (cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))), ((((~cC60(X)) | (rR1(X, tptp_fun_Y_18(X)) & (~cC12(tptp_fun_Y_18(X))))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC12(Y)))))) <=> (((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X)))))) & (cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))))), rewrite((((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X)))))) & (cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y))))) <=> (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))), ((((~cC60(X)) | (rR1(X, tptp_fun_Y_18(X)) & (~cC12(tptp_fun_Y_18(X))))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC12(Y)))))) <=> (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(105,plain,
% 0.20/0.47 (![X: $i] : (((~cC60(X)) | (rR1(X, tptp_fun_Y_18(X)) & (~cC12(tptp_fun_Y_18(X))))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC12(Y)))))) <=> ![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[104])).
% 0.20/0.47 tff(106,plain,
% 0.20/0.47 (![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC12(Y)))) <=> ![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC12(Y))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(107,axiom,(![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC12(Y))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_39')).
% 0.20/0.47 tff(108,plain,
% 0.20/0.47 (![X: $i] : (cC60(X) <=> ?[Y: $i] : (rR1(X, Y) & (~cC12(Y))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.20/0.47 tff(109,plain,(
% 0.20/0.47 ![X: $i] : (((~cC60(X)) | (rR1(X, tptp_fun_Y_18(X)) & (~cC12(tptp_fun_Y_18(X))))) & (cC60(X) | ![Y: $i] : (~(rR1(X, Y) & (~cC12(Y))))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[108])).
% 0.20/0.47 tff(110,plain,
% 0.20/0.47 (![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[109, 105])).
% 0.20/0.47 tff(111,plain,
% 0.20/0.47 (![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[110, 103])).
% 0.20/0.47 tff(112,plain,
% 0.20/0.47 (((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453)))))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(113,plain,
% 0.20/0.47 ((~((~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))))) <=> (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453)))))))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(114,plain,
% 0.20/0.47 (((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))))))),
% 0.20/0.47 inference(monotonicity,[status(thm)],[113])).
% 0.20/0.47 tff(115,plain,
% 0.20/0.47 (((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))))))) <=> ((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))))))),
% 0.20/0.47 inference(transitivity,[status(thm)],[114, 112])).
% 0.20/0.47 tff(116,plain,
% 0.20/0.47 ((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))) | (~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))))))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(117,plain,
% 0.20/0.47 ((~![X: $i] : (~((~((~cC60(X)) | (~(cC12(tptp_fun_Y_18(X)) | (~rR1(X, tptp_fun_Y_18(X))))))) | (~(cC60(X) | ![Y: $i] : (cC12(Y) | (~rR1(X, Y)))))))) | (~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453)))))))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.20/0.47 tff(118,plain,
% 0.20/0.47 ($false),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[117, 111, 98])).
% 0.20/0.47 tff(119,plain,(~((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453))))))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.47 tff(120,plain,
% 0.20/0.47 (((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | (~((~cC60(iV16453)) | (~(cC12(tptp_fun_Y_18(iV16453)) | (~rR1(iV16453, tptp_fun_Y_18(iV16453)))))))) | (cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(121,plain,
% 0.20/0.47 (cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[120, 119])).
% 0.20/0.47 tff(122,assumption,(![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))), introduced(assumption)).
% 0.20/0.47 tff(123,plain,
% 0.20/0.47 ((~cC12(iV16461)) <=> (~cC12(iV16461))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(124,axiom,(~cC12(iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_151')).
% 0.20/0.47 tff(125,plain,
% 0.20/0.47 (~cC12(iV16461)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.20/0.47 tff(126,plain,
% 0.20/0.47 (rR1(iV16453, iV16461) <=> rR1(iV16453, iV16461)),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(127,axiom,(rR1(iV16453, iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_96')).
% 0.20/0.47 tff(128,plain,
% 0.20/0.47 (rR1(iV16453, iV16461)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[127, 126])).
% 0.20/0.47 tff(129,plain,
% 0.20/0.47 (((~![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))) | (cC12(iV16461) | (~rR1(iV16453, iV16461)))) <=> ((~![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))) | cC12(iV16461) | (~rR1(iV16453, iV16461)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(130,plain,
% 0.20/0.47 ((~![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))) | (cC12(iV16461) | (~rR1(iV16453, iV16461)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(131,plain,
% 0.20/0.47 ((~![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))) | cC12(iV16461) | (~rR1(iV16453, iV16461))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.20/0.47 tff(132,plain,
% 0.20/0.47 ($false),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[131, 128, 125, 122])).
% 0.20/0.47 tff(133,plain,(~![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.47 tff(134,plain,
% 0.20/0.47 ((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y)))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(135,plain,
% 0.20/0.47 ((~(cC60(iV16453) | ![Y: $i] : (cC12(Y) | (~rR1(iV16453, Y))))) | cC60(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[134, 133])).
% 0.20/0.47 tff(136,plain,
% 0.20/0.47 (cC60(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[135, 121])).
% 0.20/0.47 tff(137,plain,
% 0.20/0.47 ((~cC58(iV16453)) <=> (~cC58(iV16453))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(138,axiom,(~cC58(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_91')).
% 0.20/0.47 tff(139,plain,
% 0.20/0.47 (~cC58(iV16453)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.20/0.47 tff(140,plain,
% 0.20/0.47 ((~(cC58(iV16453) | (~cC60(iV16453)))) | cC58(iV16453) | (~cC60(iV16453))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(141,plain,
% 0.20/0.47 ((~(cC58(iV16453) | (~cC60(iV16453)))) | (~cC60(iV16453))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[140, 139])).
% 0.20/0.47 tff(142,plain,
% 0.20/0.47 (~(cC58(iV16453) | (~cC60(iV16453)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[141, 136])).
% 0.20/0.47 tff(143,plain,
% 0.20/0.47 (^[X: $i] : refl((~((cC58(X) | (~cC60(X))) <=> cC62(X))) <=> (~((cC58(X) | (~cC60(X))) <=> cC62(X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(144,plain,
% 0.20/0.47 (![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X))) <=> ![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[143])).
% 0.20/0.47 tff(145,plain,
% 0.20/0.47 (^[X: $i] : trans(trans(monotonicity(rewrite((cC60(X) & (~cC58(X))) <=> (~(cC58(X) | (~cC60(X))))), ((cC62(X) <=> (cC60(X) & (~cC58(X)))) <=> (cC62(X) <=> (~(cC58(X) | (~cC60(X))))))), rewrite((cC62(X) <=> (~(cC58(X) | (~cC60(X))))) <=> (~((cC58(X) | (~cC60(X))) <=> cC62(X)))), ((cC62(X) <=> (cC60(X) & (~cC58(X)))) <=> (~((cC58(X) | (~cC60(X))) <=> cC62(X))))), rewrite((~((cC58(X) | (~cC60(X))) <=> cC62(X))) <=> (~((cC58(X) | (~cC60(X))) <=> cC62(X)))), ((cC62(X) <=> (cC60(X) & (~cC58(X)))) <=> (~((cC58(X) | (~cC60(X))) <=> cC62(X)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(146,plain,
% 0.20/0.47 (![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X)))) <=> ![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[145])).
% 0.20/0.47 tff(147,plain,
% 0.20/0.47 (![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X)))) <=> ![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X))))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(148,axiom,(![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_40')).
% 0.20/0.47 tff(149,plain,
% 0.20/0.47 (![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X))))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[148, 147])).
% 0.20/0.47 tff(150,plain,(
% 0.20/0.47 ![X: $i] : (cC62(X) <=> (cC60(X) & (~cC58(X))))),
% 0.20/0.47 inference(skolemize,[status(sab)],[149])).
% 0.20/0.47 tff(151,plain,
% 0.20/0.47 (![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[150, 146])).
% 0.20/0.47 tff(152,plain,
% 0.20/0.47 (![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[151, 144])).
% 0.20/0.47 tff(153,plain,
% 0.20/0.47 ((~![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))) | (~((cC58(iV16453) | (~cC60(iV16453))) <=> cC62(iV16453)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(154,plain,
% 0.20/0.47 (~((cC58(iV16453) | (~cC60(iV16453))) <=> cC62(iV16453))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[153, 152])).
% 0.20/0.47 tff(155,plain,
% 0.20/0.47 (((cC58(iV16453) | (~cC60(iV16453))) <=> cC62(iV16453)) | (cC58(iV16453) | (~cC60(iV16453))) | cC62(iV16453)),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(156,plain,
% 0.20/0.47 ((cC58(iV16453) | (~cC60(iV16453))) | cC62(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[155, 154])).
% 0.20/0.47 tff(157,plain,
% 0.20/0.47 (cC62(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[156, 142])).
% 0.20/0.47 tff(158,plain,
% 0.20/0.47 ((cowlNothing(X!28) | (~cowlThing(X!28))) | (~cowlNothing(X!28))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(159,plain,
% 0.20/0.47 (~cowlNothing(X!28)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[158, 14])).
% 0.20/0.47 tff(160,plain,
% 0.20/0.47 ((~cC74(iV16453)) <=> (~cC74(iV16453))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(161,axiom,(~cC74(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_92')).
% 0.20/0.47 tff(162,plain,
% 0.20/0.47 (~cC74(iV16453)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[161, 160])).
% 0.20/0.47 tff(163,plain,
% 0.20/0.47 ((~(cC74(iV16453) | (~cC62(iV16453)))) | cC74(iV16453) | (~cC62(iV16453))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(164,plain,
% 0.20/0.47 ((~(cC74(iV16453) | (~cC62(iV16453)))) | (~cC62(iV16453))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[163, 162])).
% 0.20/0.47 tff(165,plain,
% 0.20/0.47 (~(cC74(iV16453) | (~cC62(iV16453)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[164, 157])).
% 0.20/0.47 tff(166,plain,
% 0.20/0.47 (^[X: $i] : refl((~((cC74(X) | (~cC62(X))) <=> cC76(X))) <=> (~((cC74(X) | (~cC62(X))) <=> cC76(X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(167,plain,
% 0.20/0.47 (![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X))) <=> ![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[166])).
% 0.20/0.47 tff(168,plain,
% 0.20/0.47 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC74(X)) & cC62(X)) <=> (~(cC74(X) | (~cC62(X))))), ((cC76(X) <=> ((~cC74(X)) & cC62(X))) <=> (cC76(X) <=> (~(cC74(X) | (~cC62(X))))))), rewrite((cC76(X) <=> (~(cC74(X) | (~cC62(X))))) <=> (~((cC74(X) | (~cC62(X))) <=> cC76(X)))), ((cC76(X) <=> ((~cC74(X)) & cC62(X))) <=> (~((cC74(X) | (~cC62(X))) <=> cC76(X))))), rewrite((~((cC74(X) | (~cC62(X))) <=> cC76(X))) <=> (~((cC74(X) | (~cC62(X))) <=> cC76(X)))), ((cC76(X) <=> ((~cC74(X)) & cC62(X))) <=> (~((cC74(X) | (~cC62(X))) <=> cC76(X)))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(169,plain,
% 0.20/0.47 (![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X))) <=> ![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[168])).
% 0.20/0.47 tff(170,plain,
% 0.20/0.47 (![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X))) <=> ![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(171,axiom,(![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_47')).
% 0.20/0.47 tff(172,plain,
% 0.20/0.47 (![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[171, 170])).
% 0.20/0.47 tff(173,plain,(
% 0.20/0.47 ![X: $i] : (cC76(X) <=> ((~cC74(X)) & cC62(X)))),
% 0.20/0.47 inference(skolemize,[status(sab)],[172])).
% 0.20/0.47 tff(174,plain,
% 0.20/0.47 (![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[173, 169])).
% 0.20/0.47 tff(175,plain,
% 0.20/0.47 (![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[174, 167])).
% 0.20/0.47 tff(176,plain,
% 0.20/0.47 ((~![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))) | (~((cC74(iV16453) | (~cC62(iV16453))) <=> cC76(iV16453)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(177,plain,
% 0.20/0.47 (~((cC74(iV16453) | (~cC62(iV16453))) <=> cC76(iV16453))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[176, 175])).
% 0.20/0.47 tff(178,plain,
% 0.20/0.47 (((cC74(iV16453) | (~cC62(iV16453))) <=> cC76(iV16453)) | (cC74(iV16453) | (~cC62(iV16453))) | cC76(iV16453)),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(179,plain,
% 0.20/0.47 ((cC74(iV16453) | (~cC62(iV16453))) | cC76(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[178, 177])).
% 0.20/0.47 tff(180,plain,
% 0.20/0.47 (cC76(iV16453)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[179, 165])).
% 0.20/0.47 tff(181,plain,
% 0.20/0.47 (rR1(iV16464, iV16465) <=> rR1(iV16464, iV16465)),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(182,axiom,(rR1(iV16464, iV16465)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_188')).
% 0.20/0.47 tff(183,plain,
% 0.20/0.47 (rR1(iV16464, iV16465)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[182, 181])).
% 0.20/0.47 tff(184,plain,
% 0.20/0.47 (^[X: $i] : refl((cC38(X) | (~rR1(iV16464, X))) <=> (cC38(X) | (~rR1(iV16464, X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(185,plain,
% 0.20/0.47 (![X: $i] : (cC38(X) | (~rR1(iV16464, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[184])).
% 0.20/0.47 tff(186,plain,
% 0.20/0.47 (![X: $i] : (cC38(X) | (~rR1(iV16464, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(187,plain,
% 0.20/0.47 (^[X: $i] : rewrite((rR1(iV16464, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16464, X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(188,plain,
% 0.20/0.47 (![X: $i] : (rR1(iV16464, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[187])).
% 0.20/0.47 tff(189,axiom,(![X: $i] : (rR1(iV16464, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_182')).
% 0.20/0.47 tff(190,plain,
% 0.20/0.47 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[189, 188])).
% 0.20/0.47 tff(191,plain,
% 0.20/0.47 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[190, 186])).
% 0.20/0.47 tff(192,plain,(
% 0.20/0.47 ![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(skolemize,[status(sab)],[191])).
% 0.20/0.47 tff(193,plain,
% 0.20/0.47 (![X: $i] : (cC38(X) | (~rR1(iV16464, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[192, 185])).
% 0.20/0.47 tff(194,plain,
% 0.20/0.47 (((~![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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(195,plain,
% 0.20/0.47 ((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | (cC38(iV16465) | (~rR1(iV16464, iV16465)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(196,plain,
% 0.20/0.47 ((~![X: $i] : (cC38(X) | (~rR1(iV16464, X)))) | cC38(iV16465) | (~rR1(iV16464, iV16465))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[195, 194])).
% 0.20/0.47 tff(197,plain,
% 0.20/0.47 (cC38(iV16465)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[196, 193, 183])).
% 0.20/0.47 tff(198,plain,
% 0.20/0.47 ((~![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))) | (~((cC40(iV16464) | (~cC42(iV16464))) <=> cC44(iV16464)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(199,plain,
% 0.20/0.47 (~((cC40(iV16464) | (~cC42(iV16464))) <=> cC44(iV16464))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[198, 71])).
% 0.20/0.47 tff(200,plain,
% 0.20/0.47 ((~![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))) | (~((cC54(iV16464) | (~cC44(iV16464))) <=> cC56(iV16464)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(201,plain,
% 0.20/0.47 (~((cC54(iV16464) | (~cC44(iV16464))) <=> cC56(iV16464))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[200, 92])).
% 0.20/0.47 tff(202,plain,
% 0.20/0.47 (rR1(iV16463, iV16464) <=> rR1(iV16463, iV16464)),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(203,axiom,(rR1(iV16463, iV16464)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_177')).
% 0.20/0.47 tff(204,plain,
% 0.20/0.47 (rR1(iV16463, iV16464)),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[203, 202])).
% 0.20/0.47 tff(205,plain,
% 0.20/0.47 (^[X: $i] : refl((cC56(X) | (~rR1(iV16463, X))) <=> (cC56(X) | (~rR1(iV16463, X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(206,plain,
% 0.20/0.47 (![X: $i] : (cC56(X) | (~rR1(iV16463, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[205])).
% 0.20/0.47 tff(207,plain,
% 0.20/0.47 (![X: $i] : (cC56(X) | (~rR1(iV16463, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(208,plain,
% 0.20/0.47 (^[X: $i] : rewrite((rR1(iV16463, X) => cC56(X)) <=> (cC56(X) | (~rR1(iV16463, X))))),
% 0.20/0.47 inference(bind,[status(th)],[])).
% 0.20/0.47 tff(209,plain,
% 0.20/0.47 (![X: $i] : (rR1(iV16463, X) => cC56(X)) <=> ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(quant_intro,[status(thm)],[208])).
% 0.20/0.47 tff(210,axiom,(![X: $i] : (rR1(iV16463, X) => cC56(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_171')).
% 0.20/0.47 tff(211,plain,
% 0.20/0.47 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[210, 209])).
% 0.20/0.47 tff(212,plain,
% 0.20/0.47 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[211, 207])).
% 0.20/0.47 tff(213,plain,(
% 0.20/0.47 ![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(skolemize,[status(sab)],[212])).
% 0.20/0.47 tff(214,plain,
% 0.20/0.47 (![X: $i] : (cC56(X) | (~rR1(iV16463, X)))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[213, 206])).
% 0.20/0.47 tff(215,plain,
% 0.20/0.47 (((~![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.20/0.47 inference(rewrite,[status(thm)],[])).
% 0.20/0.47 tff(216,plain,
% 0.20/0.47 ((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | (cC56(iV16464) | (~rR1(iV16463, iV16464)))),
% 0.20/0.47 inference(quant_inst,[status(thm)],[])).
% 0.20/0.47 tff(217,plain,
% 0.20/0.47 ((~![X: $i] : (cC56(X) | (~rR1(iV16463, X)))) | cC56(iV16464) | (~rR1(iV16463, iV16464))),
% 0.20/0.47 inference(modus_ponens,[status(thm)],[216, 215])).
% 0.20/0.47 tff(218,plain,
% 0.20/0.47 (cC56(iV16464)),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[217, 214, 204])).
% 0.20/0.47 tff(219,plain,
% 0.20/0.47 (((cC54(iV16464) | (~cC44(iV16464))) <=> cC56(iV16464)) | (~(cC54(iV16464) | (~cC44(iV16464)))) | (~cC56(iV16464))),
% 0.20/0.47 inference(tautology,[status(thm)],[])).
% 0.20/0.47 tff(220,plain,
% 0.20/0.47 (~(cC54(iV16464) | (~cC44(iV16464)))),
% 0.20/0.47 inference(unit_resolution,[status(thm)],[219, 218, 201])).
% 0.20/0.48 tff(221,plain,
% 0.20/0.48 ((cC54(iV16464) | (~cC44(iV16464))) | cC44(iV16464)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(222,plain,
% 0.20/0.48 (cC44(iV16464)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[221, 220])).
% 0.20/0.48 tff(223,plain,
% 0.20/0.48 (((cC40(iV16464) | (~cC42(iV16464))) <=> cC44(iV16464)) | (~(cC40(iV16464) | (~cC42(iV16464)))) | (~cC44(iV16464))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(224,plain,
% 0.20/0.48 (~(cC40(iV16464) | (~cC42(iV16464)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[223, 222, 199])).
% 0.20/0.48 tff(225,plain,
% 0.20/0.48 ((cC40(iV16464) | (~cC42(iV16464))) | cC42(iV16464)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(226,plain,
% 0.20/0.48 (cC42(iV16464)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[225, 224])).
% 0.20/0.48 tff(227,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC58(X) | (~cC60(X))) <=> cC62(X)))) | (~((cC58(iV16463) | (~cC60(iV16463))) <=> cC62(iV16463)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(228,plain,
% 0.20/0.48 (~((cC58(iV16463) | (~cC60(iV16463))) <=> cC62(iV16463))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[227, 152])).
% 0.20/0.48 tff(229,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC74(X) | (~cC62(X))) <=> cC76(X)))) | (~((cC74(iV16463) | (~cC62(iV16463))) <=> cC76(iV16463)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(230,plain,
% 0.20/0.48 (~((cC74(iV16463) | (~cC62(iV16463))) <=> cC76(iV16463))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[229, 175])).
% 0.20/0.48 tff(231,plain,
% 0.20/0.48 (rR1(iV16440, iV16463) <=> rR1(iV16440, iV16463)),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(232,axiom,(rR1(iV16440, iV16463)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_73')).
% 0.20/0.48 tff(233,plain,
% 0.20/0.48 (rR1(iV16440, iV16463)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[232, 231])).
% 0.20/0.48 tff(234,plain,
% 0.20/0.48 (^[X: $i] : refl((cC76(X) | (~rR1(iV16440, X))) <=> (cC76(X) | (~rR1(iV16440, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(235,plain,
% 0.20/0.48 (![X: $i] : (cC76(X) | (~rR1(iV16440, X))) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[234])).
% 0.20/0.48 tff(236,plain,
% 0.20/0.48 (![X: $i] : (cC76(X) | (~rR1(iV16440, X))) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(237,plain,
% 0.20/0.48 (^[X: $i] : rewrite((rR1(iV16440, X) => cC76(X)) <=> (cC76(X) | (~rR1(iV16440, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(238,plain,
% 0.20/0.48 (![X: $i] : (rR1(iV16440, X) => cC76(X)) <=> ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[237])).
% 0.20/0.48 tff(239,axiom,(![X: $i] : (rR1(iV16440, X) => cC76(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_67')).
% 0.20/0.48 tff(240,plain,
% 0.20/0.48 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[239, 238])).
% 0.20/0.48 tff(241,plain,
% 0.20/0.48 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[240, 236])).
% 0.20/0.48 tff(242,plain,(
% 0.20/0.48 ![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(skolemize,[status(sab)],[241])).
% 0.20/0.48 tff(243,plain,
% 0.20/0.48 (![X: $i] : (cC76(X) | (~rR1(iV16440, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[242, 235])).
% 0.20/0.48 tff(244,plain,
% 0.20/0.48 (((~![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.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(245,plain,
% 0.20/0.48 ((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | (cC76(iV16463) | (~rR1(iV16440, iV16463)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(246,plain,
% 0.20/0.48 ((~![X: $i] : (cC76(X) | (~rR1(iV16440, X)))) | cC76(iV16463) | (~rR1(iV16440, iV16463))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[245, 244])).
% 0.20/0.48 tff(247,plain,
% 0.20/0.48 (cC76(iV16463)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[246, 243, 233])).
% 0.20/0.48 tff(248,plain,
% 0.20/0.48 (((cC74(iV16463) | (~cC62(iV16463))) <=> cC76(iV16463)) | (~(cC74(iV16463) | (~cC62(iV16463)))) | (~cC76(iV16463))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(249,plain,
% 0.20/0.48 (~(cC74(iV16463) | (~cC62(iV16463)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[248, 247, 230])).
% 0.20/0.48 tff(250,plain,
% 0.20/0.48 ((cC74(iV16463) | (~cC62(iV16463))) | cC62(iV16463)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(251,plain,
% 0.20/0.48 (cC62(iV16463)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[250, 249])).
% 0.20/0.48 tff(252,plain,
% 0.20/0.48 (((cC58(iV16463) | (~cC60(iV16463))) <=> cC62(iV16463)) | (~(cC58(iV16463) | (~cC60(iV16463)))) | (~cC62(iV16463))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(253,plain,
% 0.20/0.48 (~(cC58(iV16463) | (~cC60(iV16463)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[252, 251, 228])).
% 0.20/0.48 tff(254,plain,
% 0.20/0.48 ((cC58(iV16463) | (~cC60(iV16463))) | cC60(iV16463)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(255,plain,
% 0.20/0.48 (cC60(iV16463)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[254, 253])).
% 0.20/0.48 tff(256,plain,
% 0.20/0.48 (rR1(iV16461, iV16462) <=> rR1(iV16461, iV16462)),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(257,axiom,(rR1(iV16461, iV16462)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_157')).
% 0.20/0.48 tff(258,plain,
% 0.20/0.48 (rR1(iV16461, iV16462)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[257, 256])).
% 0.20/0.48 tff(259,plain,
% 0.20/0.48 (^[X: $i] : refl((cC38(X) | (~rR1(iV16461, X))) <=> (cC38(X) | (~rR1(iV16461, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(260,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16461, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[259])).
% 0.20/0.48 tff(261,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16461, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(262,plain,
% 0.20/0.48 (^[X: $i] : rewrite((rR1(iV16461, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16461, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(263,plain,
% 0.20/0.48 (![X: $i] : (rR1(iV16461, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[262])).
% 0.20/0.48 tff(264,axiom,(![X: $i] : (rR1(iV16461, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_154')).
% 0.20/0.48 tff(265,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[264, 263])).
% 0.20/0.48 tff(266,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[265, 261])).
% 0.20/0.48 tff(267,plain,(
% 0.20/0.48 ![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(skolemize,[status(sab)],[266])).
% 0.20/0.48 tff(268,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16461, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[267, 260])).
% 0.20/0.48 tff(269,plain,
% 0.20/0.48 (((~![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.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(270,plain,
% 0.20/0.48 ((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | (cC38(iV16462) | (~rR1(iV16461, iV16462)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(271,plain,
% 0.20/0.48 ((~![X: $i] : (cC38(X) | (~rR1(iV16461, X)))) | cC38(iV16462) | (~rR1(iV16461, iV16462))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[270, 269])).
% 0.20/0.48 tff(272,plain,
% 0.20/0.48 (cC38(iV16462)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[271, 268, 258])).
% 0.20/0.48 tff(273,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC40(X) | (~cC42(X))) <=> cC44(X)))) | (~((cC40(iV16461) | (~cC42(iV16461))) <=> cC44(iV16461)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(274,plain,
% 0.20/0.48 (~((cC40(iV16461) | (~cC42(iV16461))) <=> cC44(iV16461))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[273, 71])).
% 0.20/0.48 tff(275,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC54(X) | (~cC44(X))) <=> cC56(X)))) | (~((cC54(iV16461) | (~cC44(iV16461))) <=> cC56(iV16461)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(276,plain,
% 0.20/0.48 (~((cC54(iV16461) | (~cC44(iV16461))) <=> cC56(iV16461))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[275, 92])).
% 0.20/0.48 tff(277,plain,
% 0.20/0.48 (^[X: $i] : refl((cC56(X) | (~rR1(iV16453, X))) <=> (cC56(X) | (~rR1(iV16453, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(278,plain,
% 0.20/0.48 (![X: $i] : (cC56(X) | (~rR1(iV16453, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[277])).
% 0.20/0.48 tff(279,plain,
% 0.20/0.48 (![X: $i] : (cC56(X) | (~rR1(iV16453, X))) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(280,plain,
% 0.20/0.48 (^[X: $i] : rewrite((rR1(iV16453, X) => cC56(X)) <=> (cC56(X) | (~rR1(iV16453, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(281,plain,
% 0.20/0.48 (![X: $i] : (rR1(iV16453, X) => cC56(X)) <=> ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[280])).
% 0.20/0.48 tff(282,axiom,(![X: $i] : (rR1(iV16453, X) => cC56(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_93')).
% 0.20/0.48 tff(283,plain,
% 0.20/0.48 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[282, 281])).
% 0.20/0.48 tff(284,plain,
% 0.20/0.48 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[283, 279])).
% 0.20/0.48 tff(285,plain,(
% 0.20/0.48 ![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(skolemize,[status(sab)],[284])).
% 0.20/0.48 tff(286,plain,
% 0.20/0.48 (![X: $i] : (cC56(X) | (~rR1(iV16453, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[285, 278])).
% 0.20/0.48 tff(287,plain,
% 0.20/0.48 (((~![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.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(288,plain,
% 0.20/0.48 ((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | (cC56(iV16461) | (~rR1(iV16453, iV16461)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(289,plain,
% 0.20/0.48 ((~![X: $i] : (cC56(X) | (~rR1(iV16453, X)))) | cC56(iV16461) | (~rR1(iV16453, iV16461))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[288, 287])).
% 0.20/0.48 tff(290,plain,
% 0.20/0.48 (cC56(iV16461)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[289, 286, 128])).
% 0.20/0.48 tff(291,plain,
% 0.20/0.48 (((cC54(iV16461) | (~cC44(iV16461))) <=> cC56(iV16461)) | (~(cC54(iV16461) | (~cC44(iV16461)))) | (~cC56(iV16461))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(292,plain,
% 0.20/0.48 (~(cC54(iV16461) | (~cC44(iV16461)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[291, 290, 276])).
% 0.20/0.48 tff(293,plain,
% 0.20/0.48 ((cC54(iV16461) | (~cC44(iV16461))) | cC44(iV16461)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(294,plain,
% 0.20/0.48 (cC44(iV16461)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[293, 292])).
% 0.20/0.48 tff(295,plain,
% 0.20/0.48 (((cC40(iV16461) | (~cC42(iV16461))) <=> cC44(iV16461)) | (~(cC40(iV16461) | (~cC42(iV16461)))) | (~cC44(iV16461))),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(296,plain,
% 0.20/0.48 (~(cC40(iV16461) | (~cC42(iV16461)))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[295, 294, 274])).
% 0.20/0.48 tff(297,plain,
% 0.20/0.48 ((cC40(iV16461) | (~cC42(iV16461))) | cC42(iV16461)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(298,plain,
% 0.20/0.48 (cC42(iV16461)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[297, 296])).
% 0.20/0.48 tff(299,plain,
% 0.20/0.48 (^[X: $i] : refl((cC38(X) | (~rR1(iV16455, X))) <=> (cC38(X) | (~rR1(iV16455, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(300,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16455, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[299])).
% 0.20/0.48 tff(301,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16455, X))) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(302,plain,
% 0.20/0.48 (^[X: $i] : rewrite((rR1(iV16455, X) => cC38(X)) <=> (cC38(X) | (~rR1(iV16455, X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(303,plain,
% 0.20/0.48 (![X: $i] : (rR1(iV16455, X) => cC38(X)) <=> ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[302])).
% 0.20/0.48 tff(304,axiom,(![X: $i] : (rR1(iV16455, X) => cC38(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_106')).
% 0.20/0.48 tff(305,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[304, 303])).
% 0.20/0.48 tff(306,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[305, 301])).
% 0.20/0.48 tff(307,plain,(
% 0.20/0.48 ![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(skolemize,[status(sab)],[306])).
% 0.20/0.48 tff(308,plain,
% 0.20/0.48 (![X: $i] : (cC38(X) | (~rR1(iV16455, X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[307, 300])).
% 0.20/0.48 tff(309,plain,
% 0.20/0.48 (((~![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.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(310,plain,
% 0.20/0.48 ((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | (cC38(iV16460) | (~rR1(iV16455, iV16460)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(311,plain,
% 0.20/0.48 ((~![X: $i] : (cC38(X) | (~rR1(iV16455, X)))) | cC38(iV16460) | (~rR1(iV16455, iV16460))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[310, 309])).
% 0.20/0.48 tff(312,plain,
% 0.20/0.48 (cC38(iV16460)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[311, 308, 47])).
% 0.20/0.48 tff(313,plain,
% 0.20/0.48 (^[X: $i] : refl((~((cC30(X) | cC32(X)) <=> cC34(X))) <=> (~((cC30(X) | cC32(X)) <=> cC34(X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(314,plain,
% 0.20/0.48 (![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X))) <=> ![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[313])).
% 0.20/0.48 tff(315,plain,
% 0.20/0.48 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC32(X)) & (~cC30(X))) <=> (~(cC30(X) | cC32(X)))), ((cC34(X) <=> ((~cC32(X)) & (~cC30(X)))) <=> (cC34(X) <=> (~(cC30(X) | cC32(X)))))), rewrite((cC34(X) <=> (~(cC30(X) | cC32(X)))) <=> (~((cC30(X) | cC32(X)) <=> cC34(X)))), ((cC34(X) <=> ((~cC32(X)) & (~cC30(X)))) <=> (~((cC30(X) | cC32(X)) <=> cC34(X))))), rewrite((~((cC30(X) | cC32(X)) <=> cC34(X))) <=> (~((cC30(X) | cC32(X)) <=> cC34(X)))), ((cC34(X) <=> ((~cC32(X)) & (~cC30(X)))) <=> (~((cC30(X) | cC32(X)) <=> cC34(X)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(316,plain,
% 0.20/0.48 (![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X)))) <=> ![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[315])).
% 0.20/0.48 tff(317,plain,
% 0.20/0.48 (![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X)))) <=> ![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(318,axiom,(![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_25')).
% 0.20/0.48 tff(319,plain,
% 0.20/0.48 (![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[318, 317])).
% 0.20/0.48 tff(320,plain,(
% 0.20/0.48 ![X: $i] : (cC34(X) <=> ((~cC32(X)) & (~cC30(X))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[319])).
% 0.20/0.48 tff(321,plain,
% 0.20/0.48 (![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[320, 316])).
% 0.20/0.48 tff(322,plain,
% 0.20/0.48 (![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[321, 314])).
% 0.20/0.48 tff(323,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC30(X) | cC32(X)) <=> cC34(X)))) | (~((cC30(iV16459) | cC32(iV16459)) <=> cC34(iV16459)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(324,plain,
% 0.20/0.48 (~((cC30(iV16459) | cC32(iV16459)) <=> cC34(iV16459))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[323, 322])).
% 0.20/0.48 tff(325,plain,
% 0.20/0.48 ((~cC32(iV16459)) <=> (~cC32(iV16459))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(326,axiom,(~cC32(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_135')).
% 0.20/0.48 tff(327,plain,
% 0.20/0.48 (~cC32(iV16459)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[326, 325])).
% 0.20/0.48 tff(328,plain,
% 0.20/0.48 ((~cC30(iV16459)) <=> (~cC30(iV16459))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(329,axiom,(~cC30(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_121')).
% 0.20/0.48 tff(330,plain,
% 0.20/0.48 (~cC30(iV16459)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[329, 328])).
% 0.20/0.48 tff(331,plain,
% 0.20/0.48 ((~(cC30(iV16459) | cC32(iV16459))) | cC30(iV16459) | cC32(iV16459)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(332,plain,
% 0.20/0.48 (~(cC30(iV16459) | cC32(iV16459))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[331, 330, 327])).
% 0.20/0.48 tff(333,plain,
% 0.20/0.48 (((cC30(iV16459) | cC32(iV16459)) <=> cC34(iV16459)) | (cC30(iV16459) | cC32(iV16459)) | cC34(iV16459)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(334,plain,
% 0.20/0.48 (((cC30(iV16459) | cC32(iV16459)) <=> cC34(iV16459)) | cC34(iV16459)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[333, 332])).
% 0.20/0.48 tff(335,plain,
% 0.20/0.48 (cC34(iV16459)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[334, 324])).
% 0.20/0.48 tff(336,plain,
% 0.20/0.48 (^[X: $i] : refl((~((cC46(X) | cC48(X)) <=> cC50(X))) <=> (~((cC46(X) | cC48(X)) <=> cC50(X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(337,plain,
% 0.20/0.48 (![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X))) <=> ![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[336])).
% 0.20/0.48 tff(338,plain,
% 0.20/0.48 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC46(X)) & (~cC48(X))) <=> (~(cC46(X) | cC48(X)))), ((cC50(X) <=> ((~cC46(X)) & (~cC48(X)))) <=> (cC50(X) <=> (~(cC46(X) | cC48(X)))))), rewrite((cC50(X) <=> (~(cC46(X) | cC48(X)))) <=> (~((cC46(X) | cC48(X)) <=> cC50(X)))), ((cC50(X) <=> ((~cC46(X)) & (~cC48(X)))) <=> (~((cC46(X) | cC48(X)) <=> cC50(X))))), rewrite((~((cC46(X) | cC48(X)) <=> cC50(X))) <=> (~((cC46(X) | cC48(X)) <=> cC50(X)))), ((cC50(X) <=> ((~cC46(X)) & (~cC48(X)))) <=> (~((cC46(X) | cC48(X)) <=> cC50(X)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(339,plain,
% 0.20/0.48 (![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X)))) <=> ![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[338])).
% 0.20/0.48 tff(340,plain,
% 0.20/0.48 (![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X)))) <=> ![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(341,axiom,(![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_33')).
% 0.20/0.48 tff(342,plain,
% 0.20/0.48 (![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[341, 340])).
% 0.20/0.48 tff(343,plain,(
% 0.20/0.48 ![X: $i] : (cC50(X) <=> ((~cC46(X)) & (~cC48(X))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[342])).
% 0.20/0.48 tff(344,plain,
% 0.20/0.48 (![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[343, 339])).
% 0.20/0.48 tff(345,plain,
% 0.20/0.48 (![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[344, 337])).
% 0.20/0.48 tff(346,plain,
% 0.20/0.48 ((~![X: $i] : (~((cC46(X) | cC48(X)) <=> cC50(X)))) | (~((cC46(iV16459) | cC48(iV16459)) <=> cC50(iV16459)))),
% 0.20/0.48 inference(quant_inst,[status(thm)],[])).
% 0.20/0.48 tff(347,plain,
% 0.20/0.48 (~((cC46(iV16459) | cC48(iV16459)) <=> cC50(iV16459))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[346, 345])).
% 0.20/0.48 tff(348,plain,
% 0.20/0.48 ((~cC46(iV16459)) <=> (~cC46(iV16459))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(349,axiom,(~cC46(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_124')).
% 0.20/0.48 tff(350,plain,
% 0.20/0.48 (~cC46(iV16459)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[349, 348])).
% 0.20/0.48 tff(351,plain,
% 0.20/0.48 ((~cC48(iV16459)) <=> (~cC48(iV16459))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(352,axiom,(~cC48(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_120')).
% 0.20/0.48 tff(353,plain,
% 0.20/0.48 (~cC48(iV16459)),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[352, 351])).
% 0.20/0.48 tff(354,plain,
% 0.20/0.48 ((~(cC46(iV16459) | cC48(iV16459))) | cC46(iV16459) | cC48(iV16459)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(355,plain,
% 0.20/0.48 (~(cC46(iV16459) | cC48(iV16459))),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[354, 353, 350])).
% 0.20/0.48 tff(356,plain,
% 0.20/0.48 (((cC46(iV16459) | cC48(iV16459)) <=> cC50(iV16459)) | (cC46(iV16459) | cC48(iV16459)) | cC50(iV16459)),
% 0.20/0.48 inference(tautology,[status(thm)],[])).
% 0.20/0.48 tff(357,plain,
% 0.20/0.48 (((cC46(iV16459) | cC48(iV16459)) <=> cC50(iV16459)) | cC50(iV16459)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[356, 355])).
% 0.20/0.48 tff(358,plain,
% 0.20/0.48 (cC50(iV16459)),
% 0.20/0.48 inference(unit_resolution,[status(thm)],[357, 347])).
% 0.20/0.48 tff(359,plain,
% 0.20/0.48 (^[X: $i] : refl((~((cC84(X) | cC86(X)) <=> cC88(X))) <=> (~((cC84(X) | cC86(X)) <=> cC88(X))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(360,plain,
% 0.20/0.48 (![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X))) <=> ![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[359])).
% 0.20/0.48 tff(361,plain,
% 0.20/0.48 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC84(X)) & (~cC86(X))) <=> (~(cC84(X) | cC86(X)))), ((cC88(X) <=> ((~cC84(X)) & (~cC86(X)))) <=> (cC88(X) <=> (~(cC84(X) | cC86(X)))))), rewrite((cC88(X) <=> (~(cC84(X) | cC86(X)))) <=> (~((cC84(X) | cC86(X)) <=> cC88(X)))), ((cC88(X) <=> ((~cC84(X)) & (~cC86(X)))) <=> (~((cC84(X) | cC86(X)) <=> cC88(X))))), rewrite((~((cC84(X) | cC86(X)) <=> cC88(X))) <=> (~((cC84(X) | cC86(X)) <=> cC88(X)))), ((cC88(X) <=> ((~cC84(X)) & (~cC86(X)))) <=> (~((cC84(X) | cC86(X)) <=> cC88(X)))))),
% 0.20/0.48 inference(bind,[status(th)],[])).
% 0.20/0.48 tff(362,plain,
% 0.20/0.48 (![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X)))) <=> ![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X)))),
% 0.20/0.48 inference(quant_intro,[status(thm)],[361])).
% 0.20/0.48 tff(363,plain,
% 0.20/0.48 (![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X)))) <=> ![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X))))),
% 0.20/0.48 inference(rewrite,[status(thm)],[])).
% 0.20/0.48 tff(364,axiom,(![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_53')).
% 0.20/0.48 tff(365,plain,
% 0.20/0.48 (![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X))))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[364, 363])).
% 0.20/0.48 tff(366,plain,(
% 0.20/0.48 ![X: $i] : (cC88(X) <=> ((~cC84(X)) & (~cC86(X))))),
% 0.20/0.48 inference(skolemize,[status(sab)],[365])).
% 0.20/0.48 tff(367,plain,
% 0.20/0.48 (![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X)))),
% 0.20/0.48 inference(modus_ponens,[status(thm)],[366, 362])).
% 0.20/0.48 tff(368,plain,
% 0.20/0.48 (![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[367, 360])).
% 0.20/0.49 tff(369,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC84(X) | cC86(X)) <=> cC88(X)))) | (~((cC84(iV16459) | cC86(iV16459)) <=> cC88(iV16459)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(370,plain,
% 0.20/0.49 (~((cC84(iV16459) | cC86(iV16459)) <=> cC88(iV16459))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[369, 368])).
% 0.20/0.49 tff(371,plain,
% 0.20/0.49 ((~cC84(iV16459)) <=> (~cC84(iV16459))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(372,axiom,(~cC84(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_132')).
% 0.20/0.49 tff(373,plain,
% 0.20/0.49 (~cC84(iV16459)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[372, 371])).
% 0.20/0.49 tff(374,plain,
% 0.20/0.49 ((~cC86(iV16459)) <=> (~cC86(iV16459))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(375,axiom,(~cC86(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_123')).
% 0.20/0.49 tff(376,plain,
% 0.20/0.49 (~cC86(iV16459)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[375, 374])).
% 0.20/0.49 tff(377,plain,
% 0.20/0.49 ((~(cC84(iV16459) | cC86(iV16459))) | cC84(iV16459) | cC86(iV16459)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(378,plain,
% 0.20/0.49 (~(cC84(iV16459) | cC86(iV16459))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[377, 376, 373])).
% 0.20/0.49 tff(379,plain,
% 0.20/0.49 (((cC84(iV16459) | cC86(iV16459)) <=> cC88(iV16459)) | (cC84(iV16459) | cC86(iV16459)) | cC88(iV16459)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(380,plain,
% 0.20/0.49 (((cC84(iV16459) | cC86(iV16459)) <=> cC88(iV16459)) | cC88(iV16459)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[379, 378])).
% 0.20/0.49 tff(381,plain,
% 0.20/0.49 (cC88(iV16459)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[380, 370])).
% 0.20/0.49 tff(382,plain,
% 0.20/0.49 (^[X: $i] : refl((~((cC64(X) | cC66(X)) <=> cC68(X))) <=> (~((cC64(X) | cC66(X)) <=> cC68(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(383,plain,
% 0.20/0.49 (![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X))) <=> ![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[382])).
% 0.20/0.49 tff(384,plain,
% 0.20/0.49 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC64(X)) & (~cC66(X))) <=> (~(cC64(X) | cC66(X)))), ((cC68(X) <=> ((~cC64(X)) & (~cC66(X)))) <=> (cC68(X) <=> (~(cC64(X) | cC66(X)))))), rewrite((cC68(X) <=> (~(cC64(X) | cC66(X)))) <=> (~((cC64(X) | cC66(X)) <=> cC68(X)))), ((cC68(X) <=> ((~cC64(X)) & (~cC66(X)))) <=> (~((cC64(X) | cC66(X)) <=> cC68(X))))), rewrite((~((cC64(X) | cC66(X)) <=> cC68(X))) <=> (~((cC64(X) | cC66(X)) <=> cC68(X)))), ((cC68(X) <=> ((~cC64(X)) & (~cC66(X)))) <=> (~((cC64(X) | cC66(X)) <=> cC68(X)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(385,plain,
% 0.20/0.49 (![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X)))) <=> ![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[384])).
% 0.20/0.49 tff(386,plain,
% 0.20/0.49 (![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X)))) <=> ![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X))))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(387,axiom,(![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_43')).
% 0.20/0.49 tff(388,plain,
% 0.20/0.49 (![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X))))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[387, 386])).
% 0.20/0.49 tff(389,plain,(
% 0.20/0.49 ![X: $i] : (cC68(X) <=> ((~cC64(X)) & (~cC66(X))))),
% 0.20/0.49 inference(skolemize,[status(sab)],[388])).
% 0.20/0.49 tff(390,plain,
% 0.20/0.49 (![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[389, 385])).
% 0.20/0.49 tff(391,plain,
% 0.20/0.49 (![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[390, 383])).
% 0.20/0.49 tff(392,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC64(X) | cC66(X)) <=> cC68(X)))) | (~((cC64(iV16459) | cC66(iV16459)) <=> cC68(iV16459)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(393,plain,
% 0.20/0.49 (~((cC64(iV16459) | cC66(iV16459)) <=> cC68(iV16459))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[392, 391])).
% 0.20/0.49 tff(394,plain,
% 0.20/0.49 ((~cC64(iV16459)) <=> (~cC64(iV16459))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(395,axiom,(~cC64(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_133')).
% 0.20/0.49 tff(396,plain,
% 0.20/0.49 (~cC64(iV16459)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[395, 394])).
% 0.20/0.49 tff(397,plain,
% 0.20/0.49 ((~cC66(iV16459)) <=> (~cC66(iV16459))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(398,axiom,(~cC66(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_127')).
% 0.20/0.49 tff(399,plain,
% 0.20/0.49 (~cC66(iV16459)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[398, 397])).
% 0.20/0.49 tff(400,plain,
% 0.20/0.49 ((~(cC64(iV16459) | cC66(iV16459))) | cC64(iV16459) | cC66(iV16459)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(401,plain,
% 0.20/0.49 (~(cC64(iV16459) | cC66(iV16459))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[400, 399, 396])).
% 0.20/0.49 tff(402,plain,
% 0.20/0.49 (((cC64(iV16459) | cC66(iV16459)) <=> cC68(iV16459)) | (cC64(iV16459) | cC66(iV16459)) | cC68(iV16459)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(403,plain,
% 0.20/0.49 (((cC64(iV16459) | cC66(iV16459)) <=> cC68(iV16459)) | cC68(iV16459)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[402, 401])).
% 0.20/0.49 tff(404,plain,
% 0.20/0.49 (cC68(iV16459)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[403, 393])).
% 0.20/0.49 tff(405,plain,
% 0.20/0.49 (^[X: $i] : refl((~((cC36(X) | (~cTOP(X))) <=> cC38(X))) <=> (~((cC36(X) | (~cTOP(X))) <=> cC38(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(406,plain,
% 0.20/0.49 (![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X))) <=> ![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[405])).
% 0.20/0.49 tff(407,plain,
% 0.20/0.49 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC36(X)) & cTOP(X)) <=> (~(cC36(X) | (~cTOP(X))))), ((cC38(X) <=> ((~cC36(X)) & cTOP(X))) <=> (cC38(X) <=> (~(cC36(X) | (~cTOP(X))))))), rewrite((cC38(X) <=> (~(cC36(X) | (~cTOP(X))))) <=> (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))), ((cC38(X) <=> ((~cC36(X)) & cTOP(X))) <=> (~((cC36(X) | (~cTOP(X))) <=> cC38(X))))), rewrite((~((cC36(X) | (~cTOP(X))) <=> cC38(X))) <=> (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))), ((cC38(X) <=> ((~cC36(X)) & cTOP(X))) <=> (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(408,plain,
% 0.20/0.49 (![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X))) <=> ![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[407])).
% 0.20/0.49 tff(409,plain,
% 0.20/0.49 (![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X))) <=> ![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(410,axiom,(![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_27')).
% 0.20/0.49 tff(411,plain,
% 0.20/0.49 (![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[410, 409])).
% 0.20/0.49 tff(412,plain,(
% 0.20/0.49 ![X: $i] : (cC38(X) <=> ((~cC36(X)) & cTOP(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[411])).
% 0.20/0.49 tff(413,plain,
% 0.20/0.49 (![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[412, 408])).
% 0.20/0.49 tff(414,plain,
% 0.20/0.49 (![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[413, 406])).
% 0.20/0.49 tff(415,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))) | (~((cC36(iV16457) | (~cTOP(iV16457))) <=> cC38(iV16457)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(416,plain,
% 0.20/0.49 (~((cC36(iV16457) | (~cTOP(iV16457))) <=> cC38(iV16457))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[415, 414])).
% 0.20/0.49 tff(417,plain,
% 0.20/0.49 (cTOP(iV16457) <=> cTOP(iV16457)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(418,axiom,(cTOP(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_113')).
% 0.20/0.49 tff(419,plain,
% 0.20/0.49 (cTOP(iV16457)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[418, 417])).
% 0.20/0.49 tff(420,plain,
% 0.20/0.49 ((~cC36(iV16457)) <=> (~cC36(iV16457))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(421,axiom,(~cC36(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_108')).
% 0.20/0.49 tff(422,plain,
% 0.20/0.49 (~cC36(iV16457)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[421, 420])).
% 0.20/0.49 tff(423,plain,
% 0.20/0.49 ((~(cC36(iV16457) | (~cTOP(iV16457)))) | cC36(iV16457) | (~cTOP(iV16457))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(424,plain,
% 0.20/0.49 (~(cC36(iV16457) | (~cTOP(iV16457)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[423, 422, 419])).
% 0.20/0.49 tff(425,plain,
% 0.20/0.49 (((cC36(iV16457) | (~cTOP(iV16457))) <=> cC38(iV16457)) | (cC36(iV16457) | (~cTOP(iV16457))) | cC38(iV16457)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(426,plain,
% 0.20/0.49 (((cC36(iV16457) | (~cTOP(iV16457))) <=> cC38(iV16457)) | cC38(iV16457)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[425, 424])).
% 0.20/0.49 tff(427,plain,
% 0.20/0.49 (cC38(iV16457)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[426, 416])).
% 0.20/0.49 tff(428,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC36(X) | (~cTOP(X))) <=> cC38(X)))) | (~((cC36(iV16448) | (~cTOP(iV16448))) <=> cC38(iV16448)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(429,plain,
% 0.20/0.49 (~((cC36(iV16448) | (~cTOP(iV16448))) <=> cC38(iV16448))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[428, 414])).
% 0.20/0.49 tff(430,plain,
% 0.20/0.49 (cTOP(iV16448) <=> cTOP(iV16448)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(431,axiom,(cTOP(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_79')).
% 0.20/0.49 tff(432,plain,
% 0.20/0.49 (cTOP(iV16448)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[431, 430])).
% 0.20/0.49 tff(433,plain,
% 0.20/0.49 ((~cC36(iV16448)) <=> (~cC36(iV16448))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(434,axiom,(~cC36(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_76')).
% 0.20/0.49 tff(435,plain,
% 0.20/0.49 (~cC36(iV16448)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[434, 433])).
% 0.20/0.49 tff(436,plain,
% 0.20/0.49 ((~(cC36(iV16448) | (~cTOP(iV16448)))) | cC36(iV16448) | (~cTOP(iV16448))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(437,plain,
% 0.20/0.49 (~(cC36(iV16448) | (~cTOP(iV16448)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[436, 435, 432])).
% 0.20/0.49 tff(438,plain,
% 0.20/0.49 (((cC36(iV16448) | (~cTOP(iV16448))) <=> cC38(iV16448)) | (cC36(iV16448) | (~cTOP(iV16448))) | cC38(iV16448)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(439,plain,
% 0.20/0.49 (((cC36(iV16448) | (~cTOP(iV16448))) <=> cC38(iV16448)) | cC38(iV16448)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[438, 437])).
% 0.20/0.49 tff(440,plain,
% 0.20/0.49 (cC38(iV16448)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[439, 429])).
% 0.20/0.49 tff(441,plain,
% 0.20/0.49 (rR1(iV16439, iV16440) <=> rR1(iV16439, iV16440)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(442,axiom,(rR1(iV16439, iV16440)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_64')).
% 0.20/0.49 tff(443,plain,
% 0.20/0.49 (rR1(iV16439, iV16440)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[442, 441])).
% 0.20/0.49 tff(444,plain,
% 0.20/0.49 (^[X: $i] : refl((cC98(X) | (~rR1(iV16439, X))) <=> (cC98(X) | (~rR1(iV16439, X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(445,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) | (~rR1(iV16439, X))) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[444])).
% 0.20/0.49 tff(446,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) | (~rR1(iV16439, X))) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(447,plain,
% 0.20/0.49 (^[X: $i] : rewrite((rR1(iV16439, X) => cC98(X)) <=> (cC98(X) | (~rR1(iV16439, X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(448,plain,
% 0.20/0.49 (![X: $i] : (rR1(iV16439, X) => cC98(X)) <=> ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[447])).
% 0.20/0.49 tff(449,axiom,(![X: $i] : (rR1(iV16439, X) => cC98(X))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_60')).
% 0.20/0.49 tff(450,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[449, 448])).
% 0.20/0.49 tff(451,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[450, 446])).
% 0.20/0.49 tff(452,plain,(
% 0.20/0.49 ![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[451])).
% 0.20/0.49 tff(453,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) | (~rR1(iV16439, X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[452, 445])).
% 0.20/0.49 tff(454,plain,
% 0.20/0.49 (((~![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.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(455,plain,
% 0.20/0.49 ((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | (cC98(iV16440) | (~rR1(iV16439, iV16440)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(456,plain,
% 0.20/0.49 ((~![X: $i] : (cC98(X) | (~rR1(iV16439, X)))) | cC98(iV16440) | (~rR1(iV16439, iV16440))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[455, 454])).
% 0.20/0.49 tff(457,plain,
% 0.20/0.49 (cC98(iV16440)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[456, 453, 443])).
% 0.20/0.49 tff(458,plain,
% 0.20/0.49 (^[X: $i] : refl((~((cC96(X) | (~cC82(X))) <=> cC98(X))) <=> (~((cC96(X) | (~cC82(X))) <=> cC98(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(459,plain,
% 0.20/0.49 (![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X))) <=> ![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[458])).
% 0.20/0.49 tff(460,plain,
% 0.20/0.49 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC96(X)) & cC82(X)) <=> (~(cC96(X) | (~cC82(X))))), ((cC98(X) <=> ((~cC96(X)) & cC82(X))) <=> (cC98(X) <=> (~(cC96(X) | (~cC82(X))))))), rewrite((cC98(X) <=> (~(cC96(X) | (~cC82(X))))) <=> (~((cC96(X) | (~cC82(X))) <=> cC98(X)))), ((cC98(X) <=> ((~cC96(X)) & cC82(X))) <=> (~((cC96(X) | (~cC82(X))) <=> cC98(X))))), rewrite((~((cC96(X) | (~cC82(X))) <=> cC98(X))) <=> (~((cC96(X) | (~cC82(X))) <=> cC98(X)))), ((cC98(X) <=> ((~cC96(X)) & cC82(X))) <=> (~((cC96(X) | (~cC82(X))) <=> cC98(X)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(461,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X))) <=> ![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[460])).
% 0.20/0.49 tff(462,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X))) <=> ![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(463,axiom,(![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_58')).
% 0.20/0.49 tff(464,plain,
% 0.20/0.49 (![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[463, 462])).
% 0.20/0.49 tff(465,plain,(
% 0.20/0.49 ![X: $i] : (cC98(X) <=> ((~cC96(X)) & cC82(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[464])).
% 0.20/0.49 tff(466,plain,
% 0.20/0.49 (![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[465, 461])).
% 0.20/0.49 tff(467,plain,
% 0.20/0.49 (![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[466, 459])).
% 0.20/0.49 tff(468,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC96(X) | (~cC82(X))) <=> cC98(X)))) | (~((cC96(iV16440) | (~cC82(iV16440))) <=> cC98(iV16440)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(469,plain,
% 0.20/0.49 (~((cC96(iV16440) | (~cC82(iV16440))) <=> cC98(iV16440))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[468, 467])).
% 0.20/0.49 tff(470,plain,
% 0.20/0.49 (((cC96(iV16440) | (~cC82(iV16440))) <=> cC98(iV16440)) | (~(cC96(iV16440) | (~cC82(iV16440)))) | (~cC98(iV16440))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(471,plain,
% 0.20/0.49 (~(cC96(iV16440) | (~cC82(iV16440)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[470, 457, 469])).
% 0.20/0.49 tff(472,plain,
% 0.20/0.49 ((cC96(iV16440) | (~cC82(iV16440))) | cC82(iV16440)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(473,plain,
% 0.20/0.49 (cC82(iV16440)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[472, 471])).
% 0.20/0.49 tff(474,plain,
% 0.20/0.49 (^[X: $i] : refl((~((cC78(X) | (~cC80(X))) <=> cC82(X))) <=> (~((cC78(X) | (~cC80(X))) <=> cC82(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(475,plain,
% 0.20/0.49 (![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X))) <=> ![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[474])).
% 0.20/0.49 tff(476,plain,
% 0.20/0.49 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC78(X)) & cC80(X)) <=> (~(cC78(X) | (~cC80(X))))), ((cC82(X) <=> ((~cC78(X)) & cC80(X))) <=> (cC82(X) <=> (~(cC78(X) | (~cC80(X))))))), rewrite((cC82(X) <=> (~(cC78(X) | (~cC80(X))))) <=> (~((cC78(X) | (~cC80(X))) <=> cC82(X)))), ((cC82(X) <=> ((~cC78(X)) & cC80(X))) <=> (~((cC78(X) | (~cC80(X))) <=> cC82(X))))), rewrite((~((cC78(X) | (~cC80(X))) <=> cC82(X))) <=> (~((cC78(X) | (~cC80(X))) <=> cC82(X)))), ((cC82(X) <=> ((~cC78(X)) & cC80(X))) <=> (~((cC78(X) | (~cC80(X))) <=> cC82(X)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(477,plain,
% 0.20/0.49 (![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X))) <=> ![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[476])).
% 0.20/0.49 tff(478,plain,
% 0.20/0.49 (![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X))) <=> ![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(479,axiom,(![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_50')).
% 0.20/0.49 tff(480,plain,
% 0.20/0.49 (![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[479, 478])).
% 0.20/0.49 tff(481,plain,(
% 0.20/0.49 ![X: $i] : (cC82(X) <=> ((~cC78(X)) & cC80(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[480])).
% 0.20/0.49 tff(482,plain,
% 0.20/0.49 (![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[481, 477])).
% 0.20/0.49 tff(483,plain,
% 0.20/0.49 (![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[482, 475])).
% 0.20/0.49 tff(484,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC78(X) | (~cC80(X))) <=> cC82(X)))) | (~((cC78(iV16440) | (~cC80(iV16440))) <=> cC82(iV16440)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(485,plain,
% 0.20/0.49 (~((cC78(iV16440) | (~cC80(iV16440))) <=> cC82(iV16440))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[484, 483])).
% 0.20/0.49 tff(486,plain,
% 0.20/0.49 (((cC78(iV16440) | (~cC80(iV16440))) <=> cC82(iV16440)) | (~(cC78(iV16440) | (~cC80(iV16440)))) | (~cC82(iV16440))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(487,plain,
% 0.20/0.49 (~(cC78(iV16440) | (~cC80(iV16440)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[486, 473, 485])).
% 0.20/0.49 tff(488,plain,
% 0.20/0.49 ((cC78(iV16440) | (~cC80(iV16440))) | cC80(iV16440)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(489,plain,
% 0.20/0.49 (cC80(iV16440)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[488, 487])).
% 0.20/0.49 tff(490,plain,
% 0.20/0.49 (^[X: $i] : refl((~((cC100(X) | (~cC104(X))) <=> cC106(X))) <=> (~((cC100(X) | (~cC104(X))) <=> cC106(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(491,plain,
% 0.20/0.49 (![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X))) <=> ![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[490])).
% 0.20/0.49 tff(492,plain,
% 0.20/0.49 (^[X: $i] : trans(trans(monotonicity(rewrite(((~cC100(X)) & cC104(X)) <=> (~(cC100(X) | (~cC104(X))))), ((cC106(X) <=> ((~cC100(X)) & cC104(X))) <=> (cC106(X) <=> (~(cC100(X) | (~cC104(X))))))), rewrite((cC106(X) <=> (~(cC100(X) | (~cC104(X))))) <=> (~((cC100(X) | (~cC104(X))) <=> cC106(X)))), ((cC106(X) <=> ((~cC100(X)) & cC104(X))) <=> (~((cC100(X) | (~cC104(X))) <=> cC106(X))))), rewrite((~((cC100(X) | (~cC104(X))) <=> cC106(X))) <=> (~((cC100(X) | (~cC104(X))) <=> cC106(X)))), ((cC106(X) <=> ((~cC100(X)) & cC104(X))) <=> (~((cC100(X) | (~cC104(X))) <=> cC106(X)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(493,plain,
% 0.20/0.49 (![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X))) <=> ![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[492])).
% 0.20/0.49 tff(494,plain,
% 0.20/0.49 (![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X))) <=> ![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(495,axiom,(![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_5')).
% 0.20/0.49 tff(496,plain,
% 0.20/0.49 (![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[495, 494])).
% 0.20/0.49 tff(497,plain,(
% 0.20/0.49 ![X: $i] : (cC106(X) <=> ((~cC100(X)) & cC104(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[496])).
% 0.20/0.49 tff(498,plain,
% 0.20/0.49 (![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[497, 493])).
% 0.20/0.49 tff(499,plain,
% 0.20/0.49 (![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[498, 491])).
% 0.20/0.49 tff(500,plain,
% 0.20/0.49 ((~![X: $i] : (~((cC100(X) | (~cC104(X))) <=> cC106(X)))) | (~((cC100(iV16439) | (~cC104(iV16439))) <=> cC106(iV16439)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(501,plain,
% 0.20/0.49 (~((cC100(iV16439) | (~cC104(iV16439))) <=> cC106(iV16439))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[500, 499])).
% 0.20/0.49 tff(502,plain,
% 0.20/0.49 (^[X: $i] : refl((~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))) <=> (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(503,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[502])).
% 0.20/0.49 tff(504,plain,
% 0.20/0.49 (^[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.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(505,plain,
% 0.20/0.49 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X))) <=> ![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[504])).
% 0.20/0.49 tff(506,plain,
% 0.20/0.49 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X))) <=> ![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(507,axiom,(![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_6')).
% 0.20/0.49 tff(508,plain,
% 0.20/0.49 (![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[507, 506])).
% 0.20/0.49 tff(509,plain,(
% 0.20/0.49 ![X: $i] : (cC108(X) <=> (cC28(X) & cC106(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[508])).
% 0.20/0.49 tff(510,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[509, 505])).
% 0.20/0.49 tff(511,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[510, 503])).
% 0.20/0.49 tff(512,plain,
% 0.20/0.49 (((~![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.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(513,plain,
% 0.20/0.49 ((~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(514,plain,
% 0.20/0.49 ((((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)) <=> (((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(515,plain,
% 0.20/0.49 ((~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.20/0.49 inference(monotonicity,[status(thm)],[514])).
% 0.20/0.49 tff(516,plain,
% 0.20/0.49 ((~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439))) <=> (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.20/0.49 inference(transitivity,[status(thm)],[515, 513])).
% 0.20/0.49 tff(517,plain,
% 0.20/0.49 (((~![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.20/0.49 inference(monotonicity,[status(thm)],[516])).
% 0.20/0.49 tff(518,plain,
% 0.20/0.49 (((~![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.20/0.49 inference(transitivity,[status(thm)],[517, 512])).
% 0.20/0.49 tff(519,plain,
% 0.20/0.49 ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC28(iV16439)) | (~cC106(iV16439))) <=> cC108(iV16439)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(520,plain,
% 0.20/0.49 ((~![X: $i] : (~(((~cC28(X)) | (~cC106(X))) <=> cC108(X)))) | (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[519, 518])).
% 0.20/0.49 tff(521,plain,
% 0.20/0.49 (~(((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[520, 511])).
% 0.20/0.49 tff(522,plain,
% 0.20/0.49 (^[X: $i] : refl((~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))) <=> (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(523,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X))) <=> ![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[522])).
% 0.20/0.49 tff(524,plain,
% 0.20/0.49 (^[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.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(525,plain,
% 0.20/0.49 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X))) <=> ![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[524])).
% 0.20/0.49 tff(526,plain,
% 0.20/0.49 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X))) <=> ![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(527,axiom,(![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_59')).
% 0.20/0.49 tff(528,plain,
% 0.20/0.49 (![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[527, 526])).
% 0.20/0.49 tff(529,plain,(
% 0.20/0.49 ![X: $i] : (cTEST(X) <=> (cC108(X) & cC130(X)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[528])).
% 0.20/0.49 tff(530,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[529, 525])).
% 0.20/0.49 tff(531,plain,
% 0.20/0.49 (![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[530, 523])).
% 0.20/0.49 tff(532,plain,
% 0.20/0.49 ((~![X: $i] : (~(((~cC108(X)) | (~cC130(X))) <=> cTEST(X)))) | (~(((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(533,plain,
% 0.20/0.49 (~(((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[532, 531])).
% 0.20/0.49 tff(534,plain,
% 0.20/0.49 (cTEST(iV16439) <=> cTEST(iV16439)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(535,axiom,(cTEST(iV16439)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_61')).
% 0.20/0.49 tff(536,plain,
% 0.20/0.49 (cTEST(iV16439)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[535, 534])).
% 0.20/0.49 tff(537,plain,
% 0.20/0.49 ((((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)) | (~((~cC108(iV16439)) | (~cC130(iV16439)))) | (~cTEST(iV16439))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(538,plain,
% 0.20/0.49 ((((~cC108(iV16439)) | (~cC130(iV16439))) <=> cTEST(iV16439)) | (~((~cC108(iV16439)) | (~cC130(iV16439))))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[537, 536])).
% 0.20/0.49 tff(539,plain,
% 0.20/0.49 (~((~cC108(iV16439)) | (~cC130(iV16439)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[538, 533])).
% 0.20/0.49 tff(540,plain,
% 0.20/0.49 (((~cC108(iV16439)) | (~cC130(iV16439))) | cC108(iV16439)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(541,plain,
% 0.20/0.49 (cC108(iV16439)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[540, 539])).
% 0.20/0.49 tff(542,plain,
% 0.20/0.49 ((((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)) | (~((~cC106(iV16439)) | (~cC28(iV16439)))) | (~cC108(iV16439))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(543,plain,
% 0.20/0.49 ((((~cC106(iV16439)) | (~cC28(iV16439))) <=> cC108(iV16439)) | (~((~cC106(iV16439)) | (~cC28(iV16439))))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[542, 541])).
% 0.20/0.49 tff(544,plain,
% 0.20/0.49 (~((~cC106(iV16439)) | (~cC28(iV16439)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[543, 521])).
% 0.20/0.49 tff(545,plain,
% 0.20/0.49 (((~cC106(iV16439)) | (~cC28(iV16439))) | cC106(iV16439)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(546,plain,
% 0.20/0.49 (cC106(iV16439)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[545, 544])).
% 0.20/0.49 tff(547,plain,
% 0.20/0.49 (((cC100(iV16439) | (~cC104(iV16439))) <=> cC106(iV16439)) | (~(cC100(iV16439) | (~cC104(iV16439)))) | (~cC106(iV16439))),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(548,plain,
% 0.20/0.49 (~(cC100(iV16439) | (~cC104(iV16439)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[547, 546, 501])).
% 0.20/0.49 tff(549,plain,
% 0.20/0.49 ((cC100(iV16439) | (~cC104(iV16439))) | cC104(iV16439)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(550,plain,
% 0.20/0.49 (cC104(iV16439)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[549, 548])).
% 0.20/0.49 tff(551,plain,
% 0.20/0.49 (((~cC108(iV16439)) | (~cC130(iV16439))) | cC130(iV16439)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(552,plain,
% 0.20/0.49 (cC130(iV16439)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[551, 539])).
% 0.20/0.49 tff(553,plain,
% 0.20/0.49 (((~cC106(iV16439)) | (~cC28(iV16439))) | cC28(iV16439)),
% 0.20/0.49 inference(tautology,[status(thm)],[])).
% 0.20/0.49 tff(554,plain,
% 0.20/0.49 (cC28(iV16439)),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[553, 544])).
% 0.20/0.49 tff(555,plain,
% 0.20/0.49 (cowlThing(iV16465) <=> cowlThing(iV16465)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(556,axiom,(cowlThing(iV16465)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_198')).
% 0.20/0.49 tff(557,plain,
% 0.20/0.49 (cowlThing(iV16465)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[556, 555])).
% 0.20/0.49 tff(558,plain,
% 0.20/0.49 (cowlThing(iV16464) <=> cowlThing(iV16464)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(559,axiom,(cowlThing(iV16464)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_187')).
% 0.20/0.49 tff(560,plain,
% 0.20/0.49 (cowlThing(iV16464)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[559, 558])).
% 0.20/0.49 tff(561,plain,
% 0.20/0.49 (cowlThing(iV16463) <=> cowlThing(iV16463)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(562,axiom,(cowlThing(iV16463)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_176')).
% 0.20/0.49 tff(563,plain,
% 0.20/0.49 (cowlThing(iV16463)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[562, 561])).
% 0.20/0.49 tff(564,plain,
% 0.20/0.49 (cowlThing(iV16462) <=> cowlThing(iV16462)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(565,axiom,(cowlThing(iV16462)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_168')).
% 0.20/0.49 tff(566,plain,
% 0.20/0.49 (cowlThing(iV16462)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[565, 564])).
% 0.20/0.49 tff(567,plain,
% 0.20/0.49 (cowlThing(iV16461) <=> cowlThing(iV16461)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(568,axiom,(cowlThing(iV16461)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_155')).
% 0.20/0.49 tff(569,plain,
% 0.20/0.49 (cowlThing(iV16461)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[568, 567])).
% 0.20/0.49 tff(570,plain,
% 0.20/0.49 (cowlThing(iV16460) <=> cowlThing(iV16460)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(571,axiom,(cowlThing(iV16460)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_146')).
% 0.20/0.49 tff(572,plain,
% 0.20/0.49 (cowlThing(iV16460)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[571, 570])).
% 0.20/0.49 tff(573,plain,
% 0.20/0.49 (cowlThing(iV16459) <=> cowlThing(iV16459)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(574,axiom,(cowlThing(iV16459)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_134')).
% 0.20/0.49 tff(575,plain,
% 0.20/0.50 (cowlThing(iV16459)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[574, 573])).
% 0.20/0.50 tff(576,plain,
% 0.20/0.50 (cowlThing(iV16457) <=> cowlThing(iV16457)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(577,axiom,(cowlThing(iV16457)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_117')).
% 0.20/0.50 tff(578,plain,
% 0.20/0.50 (cowlThing(iV16457)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[577, 576])).
% 0.20/0.50 tff(579,plain,
% 0.20/0.50 (cowlThing(iV16455) <=> cowlThing(iV16455)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(580,axiom,(cowlThing(iV16455)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_105')).
% 0.20/0.50 tff(581,plain,
% 0.20/0.50 (cowlThing(iV16455)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[580, 579])).
% 0.20/0.50 tff(582,plain,
% 0.20/0.50 (cowlThing(iV16453) <=> cowlThing(iV16453)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(583,axiom,(cowlThing(iV16453)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_94')).
% 0.20/0.50 tff(584,plain,
% 0.20/0.50 (cowlThing(iV16453)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[583, 582])).
% 0.20/0.50 tff(585,plain,
% 0.20/0.50 (cowlThing(iV16448) <=> cowlThing(iV16448)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(586,axiom,(cowlThing(iV16448)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_84')).
% 0.20/0.50 tff(587,plain,
% 0.20/0.50 (cowlThing(iV16448)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[586, 585])).
% 0.20/0.50 tff(588,plain,
% 0.20/0.50 (cowlThing(iV16440) <=> cowlThing(iV16440)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(589,axiom,(cowlThing(iV16440)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_72')).
% 0.20/0.50 tff(590,plain,
% 0.20/0.50 (cowlThing(iV16440)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[589, 588])).
% 0.20/0.50 tff(591,plain,
% 0.20/0.50 (cowlThing(iV16439) <=> cowlThing(iV16439)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(592,axiom,(cowlThing(iV16439)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom_63')).
% 0.20/0.50 tff(593,plain,
% 0.20/0.50 (cowlThing(iV16439)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[592, 591])).
% 0.20/0.50 tff(594,plain,
% 0.20/0.50 (((cowlNothing(X!28) | (~cowlThing(X!28))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465))) <=> (cowlNothing(X!28) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465)) | (~cowlThing(X!28)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(595,plain,
% 0.20/0.50 ((~(~(cowlNothing(X!28) | (~cowlThing(X!28))))) <=> (cowlNothing(X!28) | (~cowlThing(X!28)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(596,plain,
% 0.20/0.50 ((cowlThing(X!28) & (~cowlNothing(X!28))) <=> (~(cowlNothing(X!28) | (~cowlThing(X!28))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(597,plain,
% 0.20/0.50 ((~(cowlThing(X!28) & (~cowlNothing(X!28)))) <=> (~(~(cowlNothing(X!28) | (~cowlThing(X!28)))))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[596])).
% 0.20/0.50 tff(598,plain,
% 0.20/0.50 ((~(cowlThing(X!28) & (~cowlNothing(X!28)))) <=> (cowlNothing(X!28) | (~cowlThing(X!28)))),
% 0.20/0.50 inference(transitivity,[status(thm)],[597, 595])).
% 0.20/0.50 tff(599,plain,
% 0.20/0.50 (((~(cowlThing(X!28) & (~cowlNothing(X!28)))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465))) <=> ((cowlNothing(X!28) | (~cowlThing(X!28))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465)))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[598])).
% 0.20/0.50 tff(600,plain,
% 0.20/0.50 (((~(cowlThing(X!28) & (~cowlNothing(X!28)))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465))) <=> (cowlNothing(X!28) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465)) | (~cowlThing(X!28)))),
% 0.20/0.50 inference(transitivity,[status(thm)],[599, 594])).
% 0.20/0.50 tff(601,plain,
% 0.20/0.50 (((~(cowlThing(X!28) & (~cowlNothing(X!28)))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465))) <=> ((~(cowlThing(X!28) & (~cowlNothing(X!28)))) | (xsd_integer(X!29) <=> xsd_string(X!29)) | (~cC106(iV16439)) | (~cC28(iV16439)) | (~cC130(iV16439)) | (~cowlThing(iV16439)) | (~cC108(iV16439)) | (~cC104(iV16439)) | (~cC80(iV16440)) | (~cowlThing(iV16440)) | (~cC82(iV16440)) | (~cC98(iV16440)) | (~cowlThing(iV16448)) | (~cC38(iV16448)) | (~cC62(iV16453)) | (~cowlThing(iV16453)) | (~cC76(iV16453)) | (~cC60(iV16453)) | (~cC44(iV16455)) | (~cowlThing(iV16455)) | (~cC56(iV16455)) | (~cC42(iV16455)) | (~cowlThing(iV16457)) | (~cC38(iV16457)) | (~cC68(iV16459)) | (~cowlThing(iV16459)) | (~cC88(iV16459)) | (~cC50(iV16459)) | (~cC34(iV16459)) | (~cowlThing(iV16460)) | (~cC38(iV16460)) | (~cC44(iV16461)) | (~cowlThing(iV16461)) | (~cC56(iV16461)) | (~cC42(iV16461)) | (~cowlThing(iV16462)) | (~cC38(iV16462)) | (~cC62(iV16463)) | (~cowlThing(iV16463)) | (~cC76(iV16463)) | (~cC60(iV16463)) | (~cC44(iV16464)) | (~cowlThing(iV16464)) | (~cC56(iV16464)) | (~cC42(iV16464)) | (~cowlThing(iV16465)) | (~cC38(iV16465)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(602,plain,
% 0.20/0.50 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465)) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(603,plain,
% 0.20/0.50 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465)))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[602])).
% 0.20/0.50 tff(604,plain,
% 0.20/0.50 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465)))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(605,plain,
% 0.20/0.51 ((~((((((((((((((((((((((((((((((((((((((((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC106(iV16439)) & cC28(iV16439)) & cC130(iV16439)) & cowlThing(iV16439)) & cC108(iV16439)) & cC104(iV16439)) & cC80(iV16440)) & cowlThing(iV16440)) & cC82(iV16440)) & cC98(iV16440)) & cowlThing(iV16448)) & cC38(iV16448)) & cC62(iV16453)) & cowlThing(iV16453)) & cC76(iV16453)) & cC60(iV16453)) & cC44(iV16455)) & cowlThing(iV16455)) & cC56(iV16455)) & cC42(iV16455)) & cowlThing(iV16457)) & cC38(iV16457)) & cC68(iV16459)) & cowlThing(iV16459)) & cC88(iV16459)) & cC50(iV16459)) & cC34(iV16459)) & cowlThing(iV16460)) & cC38(iV16460)) & cC44(iV16461)) & cowlThing(iV16461)) & cC56(iV16461)) & cC42(iV16461)) & cowlThing(iV16462)) & cC38(iV16462)) & cC62(iV16463)) & cowlThing(iV16463)) & cC76(iV16463)) & cC60(iV16463)) & cC44(iV16464)) & cowlThing(iV16464)) & cC56(iV16464)) & cC42(iV16464)) & cowlThing(iV16465)) & cC38(iV16465))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465)))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(606,axiom,(~((((((((((((((((((((((((((((((((((((((((((((((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & cC106(iV16439)) & cC28(iV16439)) & cC130(iV16439)) & cowlThing(iV16439)) & cC108(iV16439)) & cC104(iV16439)) & cC80(iV16440)) & cowlThing(iV16440)) & cC82(iV16440)) & cC98(iV16440)) & cowlThing(iV16448)) & cC38(iV16448)) & cC62(iV16453)) & cowlThing(iV16453)) & cC76(iV16453)) & cC60(iV16453)) & cC44(iV16455)) & cowlThing(iV16455)) & cC56(iV16455)) & cC42(iV16455)) & cowlThing(iV16457)) & cC38(iV16457)) & cC68(iV16459)) & cowlThing(iV16459)) & cC88(iV16459)) & cC50(iV16459)) & cC34(iV16459)) & cowlThing(iV16460)) & cC38(iV16460)) & cC44(iV16461)) & cowlThing(iV16461)) & cC56(iV16461)) & cC42(iV16461)) & cowlThing(iV16462)) & cC38(iV16462)) & cC62(iV16463)) & cowlThing(iV16463)) & cC76(iV16463)) & cC60(iV16463)) & cC44(iV16464)) & cowlThing(iV16464)) & cC56(iV16464)) & cC42(iV16464)) & cowlThing(iV16465)) & cC38(iV16465))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','the_axiom')).
% 0.20/0.51 tff(607,plain,
% 0.20/0.51 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[606, 605])).
% 0.20/0.52 tff(608,plain,
% 0.20/0.52 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[607, 603])).
% 0.20/0.52 tff(609,plain,
% 0.20/0.52 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[608, 604])).
% 0.20/0.52 tff(610,plain,
% 0.20/0.52 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & cC106(iV16439) & cC28(iV16439) & cC130(iV16439) & cowlThing(iV16439) & cC108(iV16439) & cC104(iV16439) & cC80(iV16440) & cowlThing(iV16440) & cC82(iV16440) & cC98(iV16440) & cowlThing(iV16448) & cC38(iV16448) & cC62(iV16453) & cowlThing(iV16453) & cC76(iV16453) & cC60(iV16453) & cC44(iV16455) & cowlThing(iV16455) & cC56(iV16455) & cC42(iV16455) & cowlThing(iV16457) & cC38(iV16457) & cC68(iV16459) & cowlThing(iV16459) & cC88(iV16459) & cC50(iV16459) & cC34(iV16459) & cowlThing(iV16460) & cC38(iV16460) & cC44(iV16461) & cowlThing(iV16461) & cC56(iV16461) & cC42(iV16461) & cowlThing(iV16462) & cC38(iV16462) & cC62(iV16463) & cowlThing(iV16463) & cC76(iV16463) & cC60(iV16463) & cC44(iV16464) & cowlThing(iV16464) & cC56(iV16464) & cC42(iV16464) & cowlThing(iV16465) & cC38(iV16465))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[609, 603])).
% 0.20/0.52 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.20/0.52 (a!2 (not (and (cowlThing X!28) (not (cowlNothing X!28)))))
% 0.20/0.52 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.20/0.52 (a!5 (refl (~ (not (cC106 iV16439)) (not (cC106 iV16439)))))
% 0.20/0.52 (a!6 (refl (~ (not (cC28 iV16439)) (not (cC28 iV16439)))))
% 0.20/0.52 (a!7 (refl (~ (not (cC130 iV16439)) (not (cC130 iV16439)))))
% 0.20/0.52 (a!8 (refl (~ (not (cowlThing iV16439)) (not (cowlThing iV16439)))))
% 0.20/0.52 (a!9 (refl (~ (not (cC108 iV16439)) (not (cC108 iV16439)))))
% 0.20/0.52 (a!10 (refl (~ (not (cC104 iV16439)) (not (cC104 iV16439)))))
% 0.20/0.52 (a!11 (refl (~ (not (cC80 iV16440)) (not (cC80 iV16440)))))
% 0.20/0.52 (a!12 (refl (~ (not (cowlThing iV16440)) (not (cowlThing iV16440)))))
% 0.20/0.52 (a!13 (refl (~ (not (cC82 iV16440)) (not (cC82 iV16440)))))
% 0.20/0.52 (a!14 (refl (~ (not (cC98 iV16440)) (not (cC98 iV16440)))))
% 0.20/0.52 (a!15 (refl (~ (not (cowlThing iV16448)) (not (cowlThing iV16448)))))
% 0.20/0.52 (a!16 (refl (~ (not (cC38 iV16448)) (not (cC38 iV16448)))))
% 0.20/0.52 (a!17 (refl (~ (not (cC62 iV16453)) (not (cC62 iV16453)))))
% 0.20/0.52 (a!18 (refl (~ (not (cowlThing iV16453)) (not (cowlThing iV16453)))))
% 0.20/0.52 (a!19 (refl (~ (not (cC76 iV16453)) (not (cC76 iV16453)))))
% 0.20/0.52 (a!20 (refl (~ (not (cC60 iV16453)) (not (cC60 iV16453)))))
% 0.20/0.52 (a!21 (refl (~ (not (cC44 iV16455)) (not (cC44 iV16455)))))
% 0.20/0.52 (a!22 (refl (~ (not (cowlThing iV16455)) (not (cowlThing iV16455)))))
% 0.20/0.52 (a!23 (refl (~ (not (cC56 iV16455)) (not (cC56 iV16455)))))
% 0.20/0.52 (a!24 (refl (~ (not (cC42 iV16455)) (not (cC42 iV16455)))))
% 0.20/0.52 (a!25 (refl (~ (not (cowlThing iV16457)) (not (cowlThing iV16457)))))
% 0.20/0.52 (a!26 (refl (~ (not (cC38 iV16457)) (not (cC38 iV16457)))))
% 0.20/0.52 (a!27 (refl (~ (not (cC68 iV16459)) (not (cC68 iV16459)))))
% 0.20/0.52 (a!28 (refl (~ (not (cowlThing iV16459)) (not (cowlThing iV16459)))))
% 0.20/0.52 (a!29 (refl (~ (not (cC88 iV16459)) (not (cC88 iV16459)))))
% 0.20/0.52 (a!30 (refl (~ (not (cC50 iV16459)) (not (cC50 iV16459)))))
% 0.20/0.52 (a!31 (refl (~ (not (cC34 iV16459)) (not (cC34 iV16459)))))
% 0.20/0.52 (a!32 (refl (~ (not (cowlThing iV16460)) (not (cowlThing iV16460)))))
% 0.20/0.52 (a!33 (refl (~ (not (cC38 iV16460)) (not (cC38 iV16460)))))
% 0.20/0.52 (a!34 (refl (~ (not (cC44 iV16461)) (not (cC44 iV16461)))))
% 0.20/0.52 (a!35 (refl (~ (not (cowlThing iV16461)) (not (cowlThing iV16461)))))
% 0.20/0.52 (a!36 (refl (~ (not (cC56 iV16461)) (not (cC56 iV16461)))))
% 0.20/0.52 (a!37 (refl (~ (not (cC42 iV16461)) (not (cC42 iV16461)))))
% 0.20/0.52 (a!38 (refl (~ (not (cowlThing iV16462)) (not (cowlThing iV16462)))))
% 0.20/0.52 (a!39 (refl (~ (not (cC38 iV16462)) (not (cC38 iV16462)))))
% 0.20/0.52 (a!40 (refl (~ (not (cC62 iV16463)) (not (cC62 iV16463)))))
% 0.20/0.52 (a!41 (refl (~ (not (cowlThing iV16463)) (not (cowlThing iV16463)))))
% 0.20/0.52 (a!42 (refl (~ (not (cC76 iV16463)) (not (cC76 iV16463)))))
% 0.20/0.52 (a!43 (refl (~ (not (cC60 iV16463)) (not (cC60 iV16463)))))
% 0.20/0.52 (a!44 (refl (~ (not (cC44 iV16464)) (not (cC44 iV16464)))))
% 0.20/0.52 (a!45 (refl (~ (not (cowlThing iV16464)) (not (cowlThing iV16464)))))
% 0.20/0.52 (a!46 (refl (~ (not (cC56 iV16464)) (not (cC56 iV16464)))))
% 0.20/0.52 (a!47 (refl (~ (not (cC42 iV16464)) (not (cC42 iV16464)))))
% 0.20/0.52 (a!48 (refl (~ (not (cowlThing iV16465)) (not (cowlThing iV16465)))))
% 0.20/0.52 (a!49 (refl (~ (not (cC38 iV16465)) (not (cC38 iV16465))))))
% 0.20/0.52 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!29) (xsd_string X!29)))))
% 0.20/0.52 (a!50 (~ (not (and a!1
% 0.20/0.52 a!3
% 0.20/0.52 (cC106 iV16439)
% 0.20/0.52 (cC28 iV16439)
% 0.20/0.52 (cC130 iV16439)
% 0.20/0.52 (cowlThing iV16439)
% 0.20/0.52 (cC108 iV16439)
% 0.20/0.52 (cC104 iV16439)
% 0.20/0.52 (cC80 iV16440)
% 0.20/0.52 (cowlThing iV16440)
% 0.20/0.52 (cC82 iV16440)
% 0.20/0.52 (cC98 iV16440)
% 0.20/0.52 (cowlThing iV16448)
% 0.20/0.52 (cC38 iV16448)
% 0.20/0.52 (cC62 iV16453)
% 0.20/0.52 (cowlThing iV16453)
% 0.20/0.52 (cC76 iV16453)
% 0.20/0.52 (cC60 iV16453)
% 0.20/0.52 (cC44 iV16455)
% 0.20/0.52 (cowlThing iV16455)
% 0.20/0.52 (cC56 iV16455)
% 0.20/0.52 (cC42 iV16455)
% 0.20/0.52 (cowlThing iV16457)
% 0.20/0.52 (cC38 iV16457)
% 0.20/0.52 (cC68 iV16459)
% 0.20/0.52 (cowlThing iV16459)
% 0.20/0.52 (cC88 iV16459)
% 0.20/0.52 (cC50 iV16459)
% 0.20/0.52 (cC34 iV16459)
% 0.20/0.52 (cowlThing iV16460)
% 0.20/0.52 (cC38 iV16460)
% 0.20/0.52 (cC44 iV16461)
% 0.20/0.52 (cowlThing iV16461)
% 0.20/0.52 (cC56 iV16461)
% 0.20/0.52 (cC42 iV16461)
% 0.20/0.52 (cowlThing iV16462)
% 0.20/0.52 (cC38 iV16462)
% 0.20/0.52 (cC62 iV16463)
% 0.20/0.52 (cowlThing iV16463)
% 0.20/0.52 (cC76 iV16463)
% 0.20/0.52 (cC60 iV16463)
% 0.20/0.52 (cC44 iV16464)
% 0.20/0.52 (cowlThing iV16464)
% 0.20/0.52 (cC56 iV16464)
% 0.20/0.52 (cC42 iV16464)
% 0.20/0.52 (cowlThing iV16465)
% 0.20/0.52 (cC38 iV16465)))
% 0.20/0.52 (or a!2
% 0.20/0.52 (= (xsd_integer X!29) (xsd_string X!29))
% 0.20/0.52 (not (cC106 iV16439))
% 0.20/0.52 (not (cC28 iV16439))
% 0.20/0.52 (not (cC130 iV16439))
% 0.20/0.52 (not (cowlThing iV16439))
% 0.20/0.52 (not (cC108 iV16439))
% 0.20/0.52 (not (cC104 iV16439))
% 0.20/0.52 (not (cC80 iV16440))
% 0.20/0.52 (not (cowlThing iV16440))
% 0.20/0.52 (not (cC82 iV16440))
% 0.20/0.52 (not (cC98 iV16440))
% 0.20/0.52 (not (cowlThing iV16448))
% 0.20/0.52 (not (cC38 iV16448))
% 0.20/0.52 (not (cC62 iV16453))
% 0.20/0.52 (not (cowlThing iV16453))
% 0.20/0.52 (not (cC76 iV16453))
% 0.20/0.52 (not (cC60 iV16453))
% 0.20/0.52 (not (cC44 iV16455))
% 0.20/0.52 (not (cowlThing iV16455))
% 0.20/0.52 (not (cC56 iV16455))
% 0.20/0.52 (not (cC42 iV16455))
% 0.20/0.52 (not (cowlThing iV16457))
% 0.20/0.52 (not (cC38 iV16457))
% 0.20/0.52 (not (cC68 iV16459))
% 0.20/0.52 (not (cowlThing iV16459))
% 0.20/0.52 (not (cC88 iV16459))
% 0.20/0.52 (not (cC50 iV16459))
% 0.20/0.52 (not (cC34 iV16459))
% 0.20/0.52 (not (cowlThing iV16460))
% 0.20/0.52 (not (cC38 iV16460))
% 0.20/0.52 (not (cC44 iV16461))
% 0.20/0.52 (not (cowlThing iV16461))
% 0.20/0.52 (not (cC56 iV16461))
% 0.20/0.52 (not (cC42 iV16461))
% 0.20/0.52 (not (cowlThing iV16462))
% 0.20/0.52 (not (cC38 iV16462))
% 0.20/0.52 (not (cC62 iV16463))
% 0.20/0.52 (not (cowlThing iV16463))
% 0.20/0.52 (not (cC76 iV16463))
% 0.20/0.52 (not (cC60 iV16463))
% 0.20/0.52 (not (cC44 iV16464))
% 0.20/0.52 (not (cowlThing iV16464))
% 0.20/0.52 (not (cC56 iV16464))
% 0.20/0.52 (not (cC42 iV16464))
% 0.20/0.52 (not (cowlThing iV16465))
% 0.20/0.52 (not (cC38 iV16465))))))
% 0.20/0.52 (nnf-neg (sk (~ (not a!1) a!2))
% 0.20/0.52 a!4
% 0.20/0.52 a!5
% 0.20/0.52 a!6
% 0.20/0.52 a!7
% 0.20/0.52 a!8
% 0.20/0.52 a!9
% 0.20/0.52 a!10
% 0.20/0.52 a!11
% 0.20/0.52 a!12
% 0.20/0.52 a!13
% 0.20/0.52 a!14
% 0.20/0.52 a!15
% 0.20/0.52 a!16
% 0.20/0.52 a!17
% 0.20/0.52 a!18
% 0.20/0.52 a!19
% 0.20/0.52 a!20
% 0.20/0.52 a!21
% 0.20/0.52 a!22
% 0.20/0.52 a!23
% 0.20/0.52 a!24
% 0.20/0.52 a!25
% 0.20/0.52 a!26
% 0.20/0.52 a!27
% 0.20/0.52 a!28
% 0.20/0.52 a!29
% 0.20/0.52 a!30
% 0.20/0.52 a!31
% 0.20/0.52 a!32
% 0.20/0.52 a!33
% 0.20/0.52 a!34
% 0.20/0.52 a!35
% 0.20/0.52 a!36
% 0.20/0.52 a!37
% 0.20/0.52 a!38
% 0.20/0.52 a!39
% 0.20/0.52 a!40
% 0.20/0.52 a!41
% 0.20/0.52 a!42
% 0.20/0.52 a!43
% 0.20/0.52 a!44
% 0.20/0.52 a!45
% 0.20/0.52 a!46
% 0.20/0.52 a!47
% 0.20/0.52 a!48
% 0.20/0.52 a!49
% 0.20/0.52 a!50)))
% 0.20/0.52 Proof display could not be completed: unexpected number of arguments
% 0.20/0.52 % E exiting
%------------------------------------------------------------------------------