%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KRS145+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:13:28 AM UTC 2025
% Result : Theorem 0.11s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : KRS145+1 : TPTP v9.0.0. Released v3.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n005.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 19:11:35 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.11/0.37 % SZS status Theorem
% 0.11/0.37 % SZS output start Proof
% 0.11/0.37 tff(rp_type, type, (
% 0.11/0.37 rp: ( $i * $i ) > $o)).
% 0.11/0.37 tff(tptp_fun_X_4_type, type, (
% 0.11/0.37 tptp_fun_X_4: $i)).
% 0.11/0.37 tff(tptp_fun_Y2_5_type, type, (
% 0.11/0.37 tptp_fun_Y2_5: $i)).
% 0.11/0.37 tff(tptp_fun_Y0_7_type, type, (
% 0.11/0.37 tptp_fun_Y0_7: $i)).
% 0.11/0.37 tff(tptp_fun_Y1_6_type, type, (
% 0.11/0.37 tptp_fun_Y1_6: $i)).
% 0.11/0.37 tff(cc_type, type, (
% 0.11/0.37 cc: $i > $o)).
% 0.11/0.37 tff(tptp_fun_Y0_1_type, type, (
% 0.11/0.37 tptp_fun_Y0_1: $i > $i)).
% 0.11/0.37 tff(tptp_fun_Y1_0_type, type, (
% 0.11/0.37 tptp_fun_Y1_0: $i > $i)).
% 0.11/0.37 tff(xsd_string_type, type, (
% 0.11/0.37 xsd_string: $i > $o)).
% 0.11/0.37 tff(tptp_fun_X_3_type, type, (
% 0.11/0.37 tptp_fun_X_3: $i)).
% 0.11/0.37 tff(xsd_integer_type, type, (
% 0.11/0.37 xsd_integer: $i > $o)).
% 0.11/0.37 tff(cowlNothing_type, type, (
% 0.11/0.37 cowlNothing: $i > $o)).
% 0.11/0.37 tff(tptp_fun_X_2_type, type, (
% 0.11/0.37 tptp_fun_X_2: $i)).
% 0.11/0.37 tff(cowlThing_type, type, (
% 0.11/0.37 cowlThing: $i > $o)).
% 0.11/0.37 tff(1,assumption,(~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))), introduced(assumption)).
% 0.11/0.37 tff(2,plain,
% 0.11/0.37 (((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))))) | cc(X!4)),
% 0.11/0.37 inference(tautology,[status(thm)],[])).
% 0.11/0.37 tff(3,plain,
% 0.11/0.37 (cc(X!4)),
% 0.11/0.37 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.11/0.37 tff(4,plain,
% 0.11/0.37 (^[X: $i] : rewrite(((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2))))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(5,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[4])).
% 0.11/0.37 tff(6,plain,
% 0.11/0.37 (^[X: $i] : refl(((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(7,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[6])).
% 0.11/0.37 tff(8,plain,
% 0.11/0.37 (^[X: $i] : rewrite(((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(9,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[8])).
% 0.11/0.37 tff(10,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(transitivity,[status(thm)],[9, 7])).
% 0.11/0.37 tff(11,plain,
% 0.11/0.37 (^[X: $i] : rewrite(((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(12,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))) <=> ![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[11])).
% 0.11/0.37 tff(13,plain,
% 0.11/0.37 (^[X: $i] : rewrite(((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & (rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))) <=> ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(14,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & (rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))) <=> ![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[13])).
% 0.11/0.37 tff(15,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))))) <=> ![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))),
% 0.11/0.37 inference(rewrite,[status(thm)],[])).
% 0.11/0.37 tff(16,plain,
% 0.11/0.37 (^[X: $i] : trans(monotonicity(rewrite((![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))) & ?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1)))) <=> (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))))), ((cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))) & ?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1))))) <=> (cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))))))), rewrite((cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))))) <=> ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))), ((cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))) & ?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1))))) <=> ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))))),
% 0.11/0.37 inference(bind,[status(th)],[])).
% 0.11/0.37 tff(17,plain,
% 0.11/0.37 (![X: $i] : (cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))) & ?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1))))) <=> ![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))),
% 0.11/0.37 inference(quant_intro,[status(thm)],[16])).
% 0.11/0.37 tff(18,axiom,(![X: $i] : (cc(X) => (![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))) & ?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_2')).
% 0.11/0.37 tff(19,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.11/0.37 tff(20,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & ?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1)))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[19, 15])).
% 0.11/0.37 tff(21,plain,(
% 0.11/0.37 ![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & (rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X))))))),
% 0.11/0.37 inference(skolemize,[status(sab)],[20])).
% 0.11/0.37 tff(22,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))) & rp(X, tptp_fun_Y0_1(X)) & rp(X, tptp_fun_Y1_0(X)) & (~(tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[21, 14])).
% 0.11/0.37 tff(23,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[22, 12])).
% 0.11/0.37 tff(24,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))) | (~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[23, 10])).
% 0.11/0.37 tff(25,plain,
% 0.11/0.37 (![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))),
% 0.11/0.37 inference(modus_ponens,[status(thm)],[24, 5])).
% 0.11/0.37 tff(26,plain,
% 0.11/0.37 (((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | ((~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))))))) <=> ((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | (~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))))))),
% 0.11/0.37 inference(rewrite,[status(thm)],[])).
% 0.11/0.37 tff(27,plain,
% 0.11/0.37 (((~cc(X!4)) | (~((~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)) | (~rp(X!4, Y2))))))) <=> ((~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))))))),
% 0.11/0.37 inference(rewrite,[status(thm)],[])).
% 0.11/0.37 tff(28,plain,
% 0.11/0.37 (((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | ((~cc(X!4)) | (~((~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)))))))) <=> ((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | ((~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))))))),
% 0.11/0.37 inference(monotonicity,[status(thm)],[27])).
% 0.11/0.37 tff(29,plain,
% 0.11/0.37 (((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | ((~cc(X!4)) | (~((~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)))))))) <=> ((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | (~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))))))),
% 0.11/0.37 inference(transitivity,[status(thm)],[28, 26])).
% 0.11/0.37 tff(30,plain,
% 0.11/0.37 ((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | ((~cc(X!4)) | (~((~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)))))))),
% 0.11/0.38 inference(quant_inst,[status(thm)],[])).
% 0.11/0.38 tff(31,plain,
% 0.11/0.38 ((~![X: $i] : ((~cc(X)) | (~((~rp(X, tptp_fun_Y0_1(X))) | (~rp(X, tptp_fun_Y1_0(X))) | (tptp_fun_Y0_1(X) = tptp_fun_Y1_0(X)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X, Y0)) | (~rp(X, Y1)) | (~rp(X, Y2)))))))) | (~cc(X!4)) | (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))))),
% 0.11/0.38 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.11/0.38 tff(32,plain,
% 0.11/0.38 (~((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[31, 25, 3])).
% 0.11/0.38 tff(33,plain,
% 0.11/0.38 (((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))) | rp(X!4, tptp_fun_Y0_1(X!4))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(34,plain,
% 0.11/0.38 (rp(X!4, tptp_fun_Y0_1(X!4))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[33, 32])).
% 0.11/0.38 tff(35,plain,
% 0.11/0.38 (((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))) | rp(X!4, tptp_fun_Y1_0(X!4))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(36,plain,
% 0.11/0.38 (rp(X!4, tptp_fun_Y1_0(X!4))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[35, 32])).
% 0.11/0.38 tff(37,plain,
% 0.11/0.38 (((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))) | (~(tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(38,plain,
% 0.11/0.38 (~(tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[37, 32])).
% 0.11/0.38 tff(39,plain,
% 0.11/0.38 (((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))))) | ((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(40,plain,
% 0.11/0.38 ((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[39, 1])).
% 0.11/0.38 tff(41,plain,
% 0.11/0.38 (((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))) | ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(42,plain,
% 0.11/0.38 (![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[41, 32])).
% 0.11/0.38 tff(43,assumption,(![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))), introduced(assumption)).
% 0.11/0.38 tff(44,assumption,(~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))), introduced(assumption)).
% 0.11/0.38 tff(45,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | (~(Y0!7 = Y2!5))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(46,plain,
% 0.11/0.38 (~(Y0!7 = Y2!5)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[45, 44])).
% 0.11/0.38 tff(47,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | (~(Y0!7 = Y1!6))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(48,plain,
% 0.11/0.38 (~(Y0!7 = Y1!6)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[47, 44])).
% 0.11/0.38 tff(49,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | (~(Y1!6 = Y2!5))),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(50,plain,
% 0.11/0.38 (~(Y1!6 = Y2!5)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[49, 44])).
% 0.11/0.38 tff(51,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | rp(X!4, Y0!7)),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(52,plain,
% 0.11/0.38 (rp(X!4, Y0!7)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[51, 44])).
% 0.11/0.38 tff(53,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | rp(X!4, Y2!5)),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(54,plain,
% 0.11/0.38 (rp(X!4, Y2!5)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[53, 44])).
% 0.11/0.38 tff(55,plain,
% 0.11/0.38 (((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | rp(X!4, Y1!6)),
% 0.11/0.38 inference(tautology,[status(thm)],[])).
% 0.11/0.38 tff(56,plain,
% 0.11/0.38 (rp(X!4, Y1!6)),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[55, 44])).
% 0.11/0.38 tff(57,plain,
% 0.11/0.38 (((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | ((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) <=> ((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))),
% 0.11/0.38 inference(rewrite,[status(thm)],[])).
% 0.11/0.38 tff(58,plain,
% 0.11/0.38 (((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7))) <=> ((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))),
% 0.11/0.38 inference(rewrite,[status(thm)],[])).
% 0.11/0.38 tff(59,plain,
% 0.11/0.38 (((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | ((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)))) <=> ((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | ((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))),
% 0.11/0.38 inference(monotonicity,[status(thm)],[58])).
% 0.11/0.38 tff(60,plain,
% 0.11/0.38 (((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | ((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)))) <=> ((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))),
% 0.11/0.38 inference(transitivity,[status(thm)],[59, 57])).
% 0.11/0.38 tff(61,plain,
% 0.11/0.38 ((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | ((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)))),
% 0.11/0.38 inference(quant_inst,[status(thm)],[])).
% 0.11/0.38 tff(62,plain,
% 0.11/0.38 ((~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0)))) | (~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)),
% 0.11/0.38 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.11/0.38 tff(63,plain,
% 0.11/0.38 ($false),
% 0.11/0.38 inference(unit_resolution,[status(thm)],[62, 56, 54, 52, 50, 48, 46, 43])).
% 0.11/0.38 tff(64,plain,(((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)) | (~![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~rp(X!4, Y1)) | (~rp(X!4, Y2)) | (~rp(X!4, Y0))))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.39 tff(65,plain,
% 0.11/0.39 ((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[64, 42])).
% 0.11/0.39 tff(66,plain,
% 0.11/0.39 ((~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))),
% 0.11/0.39 inference(tautology,[status(thm)],[])).
% 0.11/0.39 tff(67,plain,
% 0.11/0.39 (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[66, 65, 40])).
% 0.11/0.39 tff(68,plain,
% 0.11/0.39 (((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))))) <=> ((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(69,plain,
% 0.11/0.39 (((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4)))) <=> ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(70,plain,
% 0.11/0.39 (((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))))) <=> ((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4)))))),
% 0.11/0.39 inference(monotonicity,[status(thm)],[69])).
% 0.11/0.39 tff(71,plain,
% 0.11/0.39 (((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))))) <=> ((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4))))),
% 0.11/0.39 inference(transitivity,[status(thm)],[70, 68])).
% 0.11/0.39 tff(72,plain,
% 0.11/0.39 ((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | ((tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y0_1(X!4))) | (~rp(X!4, tptp_fun_Y1_0(X!4))))),
% 0.11/0.39 inference(quant_inst,[status(thm)],[])).
% 0.11/0.39 tff(73,plain,
% 0.11/0.39 ((~![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))) | (tptp_fun_Y0_1(X!4) = tptp_fun_Y1_0(X!4)) | (~rp(X!4, tptp_fun_Y1_0(X!4))) | (~rp(X!4, tptp_fun_Y0_1(X!4)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[72, 71])).
% 0.11/0.39 tff(74,plain,
% 0.11/0.39 ($false),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[73, 67, 38, 36, 34])).
% 0.11/0.39 tff(75,plain,((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.39 tff(76,assumption,(xsd_integer(X!3) <=> xsd_string(X!3)), introduced(assumption)).
% 0.11/0.39 tff(77,plain,
% 0.11/0.39 (^[X: $i] : refl((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X))))),
% 0.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(78,plain,
% 0.11/0.39 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(quant_intro,[status(thm)],[77])).
% 0.11/0.39 tff(79,plain,
% 0.11/0.39 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(80,plain,
% 0.11/0.39 (^[X: $i] : trans(rewrite((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), rewrite((~(xsd_integer(X) <=> xsd_string(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))), ((xsd_string(X) <=> (~xsd_integer(X))) <=> (~(xsd_integer(X) <=> xsd_string(X)))))),
% 0.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(81,plain,
% 0.11/0.39 (![X: $i] : (xsd_string(X) <=> (~xsd_integer(X))) <=> ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(quant_intro,[status(thm)],[80])).
% 0.11/0.39 tff(82,axiom,(![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_1')).
% 0.11/0.39 tff(83,plain,
% 0.11/0.39 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[82, 81])).
% 0.11/0.39 tff(84,plain,
% 0.11/0.39 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[83, 79])).
% 0.11/0.39 tff(85,plain,(
% 0.11/0.39 ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(skolemize,[status(sab)],[84])).
% 0.11/0.39 tff(86,plain,
% 0.11/0.39 (![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[85, 78])).
% 0.11/0.39 tff(87,plain,
% 0.11/0.39 ((~![X: $i] : (~(xsd_integer(X) <=> xsd_string(X)))) | (~(xsd_integer(X!3) <=> xsd_string(X!3)))),
% 0.11/0.39 inference(quant_inst,[status(thm)],[])).
% 0.11/0.39 tff(88,plain,
% 0.11/0.39 ($false),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[87, 86, 76])).
% 0.11/0.39 tff(89,plain,(~(xsd_integer(X!3) <=> xsd_string(X!3))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.39 tff(90,assumption,(cowlNothing(X!2) | (~cowlThing(X!2))), introduced(assumption)).
% 0.11/0.39 tff(91,plain,
% 0.11/0.39 (^[X: $i] : refl((~(cowlNothing(X) | (~cowlThing(X)))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(92,plain,
% 0.11/0.39 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X)))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.11/0.39 inference(quant_intro,[status(thm)],[91])).
% 0.11/0.39 tff(93,plain,
% 0.11/0.39 (^[X: $i] : rewrite((cowlThing(X) & (~cowlNothing(X))) <=> (~(cowlNothing(X) | (~cowlThing(X)))))),
% 0.11/0.39 inference(bind,[status(th)],[])).
% 0.11/0.39 tff(94,plain,
% 0.11/0.39 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.11/0.39 inference(quant_intro,[status(thm)],[93])).
% 0.11/0.39 tff(95,plain,
% 0.11/0.39 (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) <=> ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(96,axiom,(![X: $i] : (cowlThing(X) & (~cowlNothing(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom_0')).
% 0.11/0.39 tff(97,plain,
% 0.11/0.39 (![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.11/0.39 tff(98,plain,(
% 0.11/0.39 ![X: $i] : (cowlThing(X) & (~cowlNothing(X)))),
% 0.11/0.39 inference(skolemize,[status(sab)],[97])).
% 0.11/0.39 tff(99,plain,
% 0.11/0.39 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[98, 94])).
% 0.11/0.39 tff(100,plain,
% 0.11/0.39 (![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))),
% 0.11/0.39 inference(modus_ponens,[status(thm)],[99, 92])).
% 0.11/0.39 tff(101,plain,
% 0.11/0.39 ((~![X: $i] : (~(cowlNothing(X) | (~cowlThing(X))))) | (~(cowlNothing(X!2) | (~cowlThing(X!2))))),
% 0.11/0.39 inference(quant_inst,[status(thm)],[])).
% 0.11/0.39 tff(102,plain,
% 0.11/0.39 ($false),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[101, 100, 90])).
% 0.11/0.39 tff(103,plain,(~(cowlNothing(X!2) | (~cowlThing(X!2)))), inference(lemma,lemma(discharge,[]))).
% 0.11/0.39 tff(104,plain,
% 0.11/0.39 ((cowlNothing(X!2) | (~cowlThing(X!2))) | (~cowlNothing(X!2))),
% 0.11/0.39 inference(tautology,[status(thm)],[])).
% 0.11/0.39 tff(105,plain,
% 0.11/0.39 (~cowlNothing(X!2)),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[104, 103])).
% 0.11/0.39 tff(106,plain,
% 0.11/0.39 ((cowlNothing(X!2) | (~cowlThing(X!2))) | cowlThing(X!2)),
% 0.11/0.39 inference(tautology,[status(thm)],[])).
% 0.11/0.39 tff(107,plain,
% 0.11/0.39 (cowlThing(X!2)),
% 0.11/0.39 inference(unit_resolution,[status(thm)],[106, 103])).
% 0.11/0.39 tff(108,plain,
% 0.11/0.39 (((~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3))) <=> ((~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(109,plain,
% 0.11/0.39 ((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) <=> (~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(110,plain,
% 0.11/0.39 (((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3))) <=> ((~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)))),
% 0.11/0.39 inference(monotonicity,[status(thm)],[109])).
% 0.11/0.39 tff(111,plain,
% 0.11/0.39 (((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3))) <=> ((~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (~((~cc(X!4)) | (~((~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))) | ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))))),
% 0.11/0.39 inference(transitivity,[status(thm)],[110, 108])).
% 0.11/0.39 tff(112,plain,
% 0.11/0.39 (((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3))) <=> ((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(113,plain,
% 0.11/0.39 ((((~cowlThing(X!2)) | cowlNothing(X!2)) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))))))) <=> ((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(114,plain,
% 0.11/0.39 ((cc(X!4) & (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))) <=> (~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(115,plain,
% 0.11/0.39 ((![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))) <=> (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))),
% 0.11/0.39 inference(rewrite,[status(thm)],[])).
% 0.11/0.39 tff(116,plain,
% 0.11/0.39 ((~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5))))) <=> (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(117,plain,
% 0.11/0.40 (^[Y0: $i, Y1: $i] : trans(monotonicity(rewrite((rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1))) <=> (~((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))), ((~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) <=> (~(~((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))))), rewrite((~(~((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))))) <=> ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))), ((~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) <=> ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))))),
% 0.11/0.40 inference(bind,[status(th)],[])).
% 0.11/0.40 tff(118,plain,
% 0.11/0.40 (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) <=> ![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1)))),
% 0.11/0.40 inference(quant_intro,[status(thm)],[117])).
% 0.11/0.40 tff(119,plain,
% 0.11/0.40 ((![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))) <=> (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[118, 116])).
% 0.11/0.40 tff(120,plain,
% 0.11/0.40 ((![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))) <=> (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))),
% 0.11/0.40 inference(transitivity,[status(thm)],[119, 115])).
% 0.11/0.40 tff(121,plain,
% 0.11/0.40 ((cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5))))))) <=> (cc(X!4) & (![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[120])).
% 0.11/0.40 tff(122,plain,
% 0.11/0.40 ((cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5))))))) <=> (~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5)))))))),
% 0.11/0.40 inference(transitivity,[status(thm)],[121, 114])).
% 0.11/0.40 tff(123,plain,
% 0.11/0.40 ((~(~((~cowlThing(X!2)) | cowlNothing(X!2)))) <=> ((~cowlThing(X!2)) | cowlNothing(X!2))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(124,plain,
% 0.11/0.40 ((cowlThing(X!2) & (~cowlNothing(X!2))) <=> (~((~cowlThing(X!2)) | cowlNothing(X!2)))),
% 0.11/0.40 inference(rewrite,[status(thm)],[])).
% 0.11/0.40 tff(125,plain,
% 0.11/0.40 ((~(cowlThing(X!2) & (~cowlNothing(X!2)))) <=> (~(~((~cowlThing(X!2)) | cowlNothing(X!2))))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[124])).
% 0.11/0.40 tff(126,plain,
% 0.11/0.40 ((~(cowlThing(X!2) & (~cowlNothing(X!2)))) <=> ((~cowlThing(X!2)) | cowlNothing(X!2))),
% 0.11/0.40 inference(transitivity,[status(thm)],[125, 123])).
% 0.11/0.40 tff(127,plain,
% 0.11/0.40 (((~(cowlThing(X!2) & (~cowlNothing(X!2)))) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))))) <=> (((~cowlThing(X!2)) | cowlNothing(X!2)) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))))),
% 0.11/0.40 inference(monotonicity,[status(thm)],[126, 122])).
% 0.11/0.40 tff(128,plain,
% 0.11/0.40 (((~(cowlThing(X!2) & (~cowlNothing(X!2)))) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))))) <=> ((~((~cc(X!4)) | (~(![Y0: $i, Y1: $i] : ((Y0 = Y1) | (~rp(X!4, Y0)) | (~rp(X!4, Y1))) | (~((~rp(X!4, Y1!6)) | (~rp(X!4, Y2!5)) | (~rp(X!4, Y0!7)) | (Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5))))))) | (~cowlThing(X!2)) | cowlNothing(X!2) | (xsd_integer(X!3) <=> xsd_string(X!3)))),
% 0.18/0.40 inference(transitivity,[status(thm)],[127, 113])).
% 0.18/0.40 tff(129,plain,
% 0.18/0.40 ((cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5))))))) <=> (cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(130,plain,
% 0.18/0.40 (((~(cowlThing(X!2) & (~cowlNothing(X!2)))) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5)))))))) <=> ((~(cowlThing(X!2) & (~cowlNothing(X!2)))) | (xsd_integer(X!3) <=> xsd_string(X!3)) | (cc(X!4) & (![Y0: $i, Y1: $i] : (~(rp(X!4, Y0) & rp(X!4, Y1) & (~(Y0 = Y1)))) | (~((Y1!6 = Y2!5) | (Y0!7 = Y1!6) | (Y0!7 = Y2!5) | (~(rp(X!4, Y0!7) & rp(X!4, Y1!6) & rp(X!4, Y2!5))))))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[129])).
% 0.18/0.40 tff(131,plain,
% 0.18/0.40 ((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2))))))) <=> (![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(132,plain,
% 0.18/0.40 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2))))))))),
% 0.18/0.40 inference(monotonicity,[status(thm)],[131])).
% 0.18/0.40 tff(133,plain,
% 0.18/0.40 ((~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2))))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(134,plain,
% 0.18/0.40 ((~((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i] : (cc(X) => (?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))))))) <=> (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2))))))))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(135,axiom,(~((![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (xsd_string(X) <=> (~xsd_integer(X)))) & ![X: $i] : (cc(X) => (?[Y0: $i, Y1: $i] : ((rp(X, Y0) & rp(X, Y1)) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : (((rp(X, Y0) & rp(X, Y1)) & rp(X, Y2)) => (((Y0 = Y1) | (Y0 = Y2)) | (Y1 = Y2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','the_axiom')).
% 0.18/0.41 tff(136,plain,
% 0.18/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[135, 134])).
% 0.18/0.41 tff(137,plain,
% 0.18/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[136, 132])).
% 0.18/0.41 tff(138,plain,
% 0.18/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[137, 133])).
% 0.18/0.41 tff(139,plain,
% 0.18/0.41 (~(![X: $i] : (cowlThing(X) & (~cowlNothing(X))) & ![X: $i] : (~(xsd_integer(X) <=> xsd_string(X))) & ![X: $i] : ((~cc(X)) | (?[Y0: $i, Y1: $i] : (rp(X, Y0) & rp(X, Y1) & (~(Y0 = Y1))) & ![Y0: $i, Y1: $i, Y2: $i] : ((Y1 = Y2) | (Y0 = Y1) | (Y0 = Y2) | (~(rp(X, Y0) & rp(X, Y1) & rp(X, Y2)))))))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[138, 132])).
% 0.18/0.41 unexpected number of arguments: (let ((a!1 (forall ((X $i)) (and (cowlThing X) (not (cowlNothing X)))))
% 0.18/0.41 (a!2 (not (and (cowlThing X!2) (not (cowlNothing X!2)))))
% 0.18/0.41 (a!3 (forall ((X $i)) (not (= (xsd_integer X) (xsd_string X)))))
% 0.18/0.41 (a!5 (forall ((X $i))
% 0.18/0.41 (let ((a!1 (exists ((Y0 $i) (Y1 $i))
% 0.18/0.41 (and (rp X Y0) (rp X Y1) (not (= Y0 Y1)))))
% 0.18/0.41 (a!2 (forall ((Y0 $i) (Y1 $i) (Y2 $i))
% 0.18/0.41 (or (= Y1 Y2)
% 0.18/0.41 (= Y0 Y1)
% 0.18/0.41 (= Y0 Y2)
% 0.18/0.41 (not (and (rp X Y0) (rp X Y1) (rp X Y2)))))))
% 0.18/0.41 (or (not (cc X)) (and a!1 a!2)))))
% 0.18/0.41 (a!6 (exists ((Y0 $i) (Y1 $i))
% 0.18/0.41 (and (rp X!4 Y0) (rp X!4 Y1) (not (= Y0 Y1)))))
% 0.18/0.41 (a!7 (forall ((Y0 $i) (Y1 $i) (Y2 $i))
% 0.18/0.41 (or (= Y1 Y2)
% 0.18/0.41 (= Y0 Y1)
% 0.18/0.41 (= Y0 Y2)
% 0.18/0.41 (not (and (rp X!4 Y0) (rp X!4 Y1) (rp X!4 Y2))))))
% 0.18/0.41 (a!9 (lambda ((Y0 $i) (Y1 $i))
% 0.18/0.41 (let ((a!1 (and (rp X!4 Y0) (rp X!4 Y1) (not (= Y0 Y1)))))
% 0.18/0.41 (refl (~ (not a!1) (not a!1))))))
% 0.18/0.41 (a!10 (forall ((Y0 $i) (Y1 $i))
% 0.18/0.41 (let ((a!1 (and (rp X!4 Y0) (rp X!4 Y1) (not (= Y0 Y1)))))
% 0.18/0.41 (not a!1))))
% 0.18/0.41 (a!11 (or (= Y1!6 Y2!5)
% 0.18/0.41 (= Y0!7 Y1!6)
% 0.18/0.41 (= Y0!7 Y2!5)
% 0.18/0.41 (not (and (rp X!4 Y0!7) (rp X!4 Y1!6) (rp X!4 Y2!5))))))
% 0.18/0.41 (let ((a!4 (sk (~ (not a!3) (= (xsd_integer X!3) (xsd_string X!3)))))
% 0.18/0.41 (a!8 (not (or (not (cc X!4)) (and a!6 a!7))))
% 0.18/0.41 (a!12 (nnf-neg (nnf-neg (proof-bind a!9) (~ (not a!6) a!10))
% 0.18/0.41 (sk (~ (not a!7) (not a!11)))
% 0.18/0.41 (~ (not (and a!6 a!7)) (or a!10 (not a!11)))))
% 0.18/0.41 (a!15 (~ (not a!5) (and (cc X!4) (or a!10 (not a!11)))))
% 0.18/0.41 (a!17 (or a!2
% 0.18/0.41 (= (xsd_integer X!3) (xsd_string X!3))
% 0.18/0.41 (and (cc X!4) (or a!10 (not a!11))))))
% 0.18/0.41 (let ((a!13 (~ a!8 (and (cc X!4) (or a!10 (not a!11))))))
% 0.18/0.41 (let ((a!14 (nnf-neg (refl (~ (cc X!4) (cc X!4))) a!12 a!13)))
% 0.18/0.41 (let ((a!16 (trans (sk (~ (not a!5) a!8)) a!14 a!15)))
% 0.18/0.41 (nnf-neg (sk (~ (not a!1) a!2)) a!4 a!16 (~ (not (and a!1 a!3 a!5)) a!17)))))))
% 0.18/0.41 Proof display could not be completed: unexpected number of arguments
% 0.18/0.41 % E exiting
%------------------------------------------------------------------------------