%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU277+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:41:31 AM UTC 2026
% Result : Theorem 147.36s 30.15s
% Output : CNFRefutation 147.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU277+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/10.47 % Computer : n017.cluster.edu
% 0.20/10.47 % Model : x86_64 x86_64
% 0.20/10.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/10.47 % Memory : 8046.5625MB
% 0.20/10.47 % OS : Linux 6.8.0-71-generic
% 0.20/10.47 % CPULimit : 300
% 0.20/10.47 % WCLimit : 300
% 0.20/10.47 % DateTime : Sat Sep 26 08:59:14 UTC 2026
% 0.20/10.47 % CPUTime :
% 0.20/10.47 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 147.36/30.15 % SZS status Theorem for theBenchmark.p
% 147.36/30.15 % SZS output start CNFRefutation for theBenchmark.p
% 147.36/30.15 fof(s1_tarski__e6_21__wellord2__1, axiom, ! [X0] : ! [X1] : ! [X2] : (((relation(X1) & (relation(X2) & function(X2))) => (! [X3] : ! [X4] : ! [X5] : (((X3 = X4 & (? [X6] : ? [X7] : ((X4 = 'ordered$upair'(X6,X7) & in('ordered$upair'(apply(X2,X6),apply(X2,X7)),X1))) & (X3 = X5 & ? [X8] : ? [X9] : ((X5 = 'ordered$upair'(X8,X9) & in('ordered$upair'(apply(X2,X8),apply(X2,X9)),X1)))))) => X4 = X5)) => ? [X3] : ! [X4] : ((in(X4,X3) <=> ? [X5] : ((in(X5,'cartesian$uproduct2'(X0,X0)) & (X5 = X4 & ? [X10] : ? [X11] : ((X4 = 'ordered$upair'(X10,X11) & in('ordered$upair'(apply(X2,X10),apply(X2,X11)),X1)))))))))))).
% 147.36/30.15 fof(s1_xboole_0__e6_21__wellord2__1, conjecture, ! [X0] : ! [X1] : ! [X2] : (((relation(X1) & (relation(X2) & function(X2))) => ? [X3] : ! [X4] : ((in(X4,X3) <=> (in(X4,'cartesian$uproduct2'(X0,X0)) & ? [X5] : ? [X6] : ((X4 = 'ordered$upair'(X5,X6) & in('ordered$upair'(apply(X2,X5),apply(X2,X6)),X1))))))))).
% 147.36/30.15 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : (((relation(X1) & (relation(X2) & function(X2))) => ? [X3] : ! [X4] : ((in(X4,X3) <=> (in(X4,'cartesian$uproduct2'(X0,X0)) & ? [X5] : ? [X6] : ((X4 = 'ordered$upair'(X5,X6) & in('ordered$upair'(apply(X2,X5),apply(X2,X6)),X1)))))))), inference(negate_conjecture, [status(cth)], [s1_xboole_0__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c36, plain, ~relation(X0) | ~relation(X1) | ~in(X2,sK22(X3,X1,X0)) | ~function(X0) | X4(X1,X0) | X5(X3,X1,X0,X2), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c37, plain, ~relation(X0) | ~relation(X1) | ~function(X0) | ~X2(X3,X1,X0,X4) | in(X4,sK22(X3,X1,X0)) | X5(X1,X0), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c38, plain, ~X0(X1,X2,X3,X4) | in(sK24(X3,X1,X4,X2),'cartesian$uproduct2'(X1,X1)), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c39, plain, ~X0(X1,X2,X3,X4) | sK24(X3,X1,X4,X2) = X4, inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c40, plain, ~X0(X1,X2,X3,X4) | X4 = 'ordered$upair'(sK25(X3,X4,X2),sK26(X3,X4,X2)), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c41, plain, ~X0(X1,X2,X3,X4) | in('ordered$upair'(apply(X3,sK25(X3,X4,X2)),apply(X3,sK26(X3,X4,X2))),X2), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c42, plain, X0 != 'ordered$upair'(X1,X2) | X3(X4,X5,X6,X0) | ~in('ordered$upair'(apply(X6,X1),apply(X6,X2)),X5) | X7 != X0 | ~in(X7,'cartesian$uproduct2'(X4,X4)), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c43, plain, ~X0(X1,X2) | sK30(X1,X2) = sK31(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c46, plain, ~X0(X1,X2) | sK30(X1,X2) = sK32(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c49, plain, ~X0(X1,X2) | sK31(X1,X2) != sK32(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e6_21__wellord2__1])).
% 147.36/30.15 cnf(c50, plain, relation(sK38), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c51, plain, relation(sK39), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c52, plain, function(sK39), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c54, plain, in(sK41(X0),X0) | in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c55, plain, in(sK41(X0),X0) | sK41(X0) = 'ordered$upair'(sK44(X0),sK45(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c56, plain, in(sK41(X0),X0) | in('ordered$upair'(apply(sK39,sK44(X0)),apply(sK39,sK45(X0))),sK38), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c57, plain, ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)) | sK41(X0) != 'ordered$upair'(X1,X2) | ~in('ordered$upair'(apply(sK39,X1),apply(sK39,X2)),sK38) | ~in(sK41(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(c59, plain, ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)) | sK41(X0) != 'ordered$upair'(X1,X2) | ~in('ordered$upair'(apply(sK39,X1),apply(sK39,X2)),sK38) | sK41(X0) = 'ordered$upair'(sK44(X0),sK45(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 147.36/30.15 cnf(d0, plain, ~relation(X0) | ~relation(X1) | ~function(X1) | 'Ts18'(X0,X1) | 'Ts17'(X2,X0,X1,sK41(sK22(X2,X0,X1))) | in(sK41(sK22(X2,X0,X1)),'cartesian$uproduct2'(sK37,sK37)), inference(resolution, [status(thm)], [c36,c54])).
% 147.36/30.15 cnf(d1, plain, X0 != 'ordered$upair'(X1,X2) | ~in(X0,'cartesian$uproduct2'(X3,X3)) | ~in('ordered$upair'(apply(X4,X1),apply(X4,X2)),X5) | 'Ts17'(X3,X5,X4,'ordered$upair'(X1,X2)), inference(equality_resolution, [status(thm)], [c42])).
% 147.36/30.15 cnf(d2, plain, ~in('ordered$upair'(X0,X1),'cartesian$uproduct2'(X2,X2)) | ~in('ordered$upair'(apply(X3,X0),apply(X3,X1)),X4) | 'Ts17'(X2,X4,X3,'ordered$upair'(X0,X1)), inference(equality_resolution, [status(thm)], [d1])).
% 147.36/30.15 cnf(d3, plain, ~in('ordered$upair'(sK44(X0),sK45(X0)),'cartesian$uproduct2'(X1,X1)) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK44(X0),sK45(X0))) | in(sK41(X0),X0), inference(resolution, [status(thm)], [d2,c56])).
% 147.36/30.15 cnf(d4, plain, ~relation(X0) | ~relation(X1) | ~function(X1) | 'Ts18'(X0,X1) | 'Ts17'(X2,X0,X1,sK41(sK22(X2,X0,X1))) | sK41(sK22(X2,X0,X1)) = 'ordered$upair'(sK44(sK22(X2,X0,X1)),sK45(sK22(X2,X0,X1))), inference(resolution, [status(thm)], [c36,c55])).
% 147.36/30.15 cnf(d5, plain, sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK44(sK22(X0,X1,X2)),sK45(sK22(X0,X1,X2))) | ~relation(X2) | ~relation(X1) | ~function(X2) | 'Ts18'(X1,X2) | sK24(X2,X0,sK41(sK22(X0,X1,X2)),X1) = sK41(sK22(X0,X1,X2)), inference(resolution, [status(thm)], [d4,c39])).
% 147.36/30.15 cnf(d6, plain, sK24(X0,X1,sK41(sK22(X1,X2,X0)),X2) = sK41(sK22(X1,X2,X0)) | sK41(sK22(X1,X2,X0)) = 'ordered$upair'(sK44(sK22(X1,X2,X0)),sK45(sK22(X1,X2,X0))) | ~relation(X0) | ~relation(X2) | ~function(X0) | sK30(X2,X0) = sK31(X2,X0), inference(resolution, [status(thm)], [d5,c43])).
% 147.36/30.15 cnf(d7, plain, sK24(sK39,X0,sK41(sK22(X0,X1,sK39)),X1) = sK41(sK22(X0,X1,sK39)) | sK30(X1,sK39) = sK31(X1,sK39) | sK41(sK22(X0,X1,sK39)) = 'ordered$upair'(sK44(sK22(X0,X1,sK39)),sK45(sK22(X0,X1,sK39))) | ~relation(X1) | ~relation(sK39), inference(resolution, [status(thm)], [d6,c52])).
% 147.36/30.15 cnf(d8, plain, sK24(sK39,X0,sK41(sK22(X0,X1,sK39)),X1) = sK41(sK22(X0,X1,sK39)) | sK30(X1,sK39) = sK31(X1,sK39) | sK41(sK22(X0,X1,sK39)) = 'ordered$upair'(sK44(sK22(X0,X1,sK39)),sK45(sK22(X0,X1,sK39))) | ~relation(X1), inference(resolution, [status(thm)], [c51,d7])).
% 147.36/30.15 cnf(d9, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d8,c50])).
% 147.36/30.15 cnf(d10, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d9,d3])).
% 147.36/30.15 cnf(d11, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d10,c54])).
% 147.36/30.15 cnf(d12, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d9,d11])).
% 147.36/30.15 cnf(d13, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d12,c36])).
% 147.36/30.15 cnf(d14, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c50,d13])).
% 147.36/30.15 cnf(d15, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c51,d14])).
% 147.36/30.15 cnf(d16, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c52,d15])).
% 147.36/30.15 cnf(d17, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d16,c39])).
% 147.36/30.15 cnf(d18, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | sK24(sK39,sK37,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d17,c39])).
% 147.36/30.15 cnf(d19, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(resolution, [status(thm)], [d18,c43])).
% 147.36/30.15 cnf(d20, plain, sK41(sK22(sK37,sK38,sK39)) != sK41(sK22(sK37,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(equality_factoring, [status(thm)], [d19])).
% 147.36/30.15 cnf(d21, plain, sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(equality_resolution, [status(thm)], [d20])).
% 147.36/30.15 cnf(d22, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d21,c38])).
% 147.36/30.15 cnf(d23, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~relation(sK39) | ~relation(sK38) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d22,d0])).
% 147.36/30.15 cnf(d24, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~relation(sK39) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c50,d23])).
% 147.36/30.15 cnf(d25, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c51,d24])).
% 147.36/30.15 cnf(d26, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c52,d25])).
% 147.36/30.15 cnf(d27, plain, sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK44(sK22(X0,X1,X2)),sK45(sK22(X0,X1,X2))) | ~relation(X2) | ~relation(X1) | ~function(X2) | 'Ts18'(X1,X2) | in('ordered$upair'(apply(X2,sK25(X2,sK41(sK22(X0,X1,X2)),X1)),apply(X2,sK26(X2,sK41(sK22(X0,X1,X2)),X1))),X1), inference(resolution, [status(thm)], [d4,c41])).
% 147.36/30.15 cnf(d28, plain, ~in('ordered$upair'(sK25(X0,sK41(sK22(X1,X2,X0)),X2),sK26(X0,sK41(sK22(X1,X2,X0)),X2)),'cartesian$uproduct2'(X3,X3)) | 'Ts17'(X3,X2,X0,'ordered$upair'(sK25(X0,sK41(sK22(X1,X2,X0)),X2),sK26(X0,sK41(sK22(X1,X2,X0)),X2))) | sK41(sK22(X1,X2,X0)) = 'ordered$upair'(sK44(sK22(X1,X2,X0)),sK45(sK22(X1,X2,X0))) | ~relation(X0) | ~relation(X2) | ~function(X0) | 'Ts18'(X2,X0), inference(resolution, [status(thm)], [d2,d27])).
% 147.36/30.16 cnf(d29, plain, sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK44(sK22(X0,X1,X2)),sK45(sK22(X0,X1,X2))) | ~relation(X2) | ~relation(X1) | ~function(X2) | 'Ts18'(X1,X2) | sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK25(X2,sK41(sK22(X0,X1,X2)),X1),sK26(X2,sK41(sK22(X0,X1,X2)),X1)), inference(resolution, [status(thm)], [d4,c40])).
% 147.36/30.16 cnf(d30, plain, sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK25(X2,sK41(sK22(X0,X1,X2)),X1),sK26(X2,sK41(sK22(X0,X1,X2)),X1)) | sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK44(sK22(X0,X1,X2)),sK45(sK22(X0,X1,X2))) | ~relation(X2) | ~relation(X1) | ~function(X2) | sK30(X1,X2) = sK31(X1,X2), inference(resolution, [status(thm)], [d29,c43])).
% 147.36/30.16 cnf(d31, plain, sK30(X0,sK39) = sK31(X0,sK39) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X1,X0,sK39)),X0),sK26(sK39,sK41(sK22(X1,X0,sK39)),X0)) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK44(sK22(X1,X0,sK39)),sK45(sK22(X1,X0,sK39))) | ~relation(sK39) | ~relation(X0), inference(resolution, [status(thm)], [d30,c52])).
% 147.36/30.16 cnf(d32, plain, sK30(X0,sK39) = sK31(X0,sK39) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X1,X0,sK39)),X0),sK26(sK39,sK41(sK22(X1,X0,sK39)),X0)) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK44(sK22(X1,X0,sK39)),sK45(sK22(X1,X0,sK39))) | ~relation(X0), inference(resolution, [status(thm)], [c51,d31])).
% 147.36/30.16 cnf(d33, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d32,c50])).
% 147.36/30.16 cnf(d34, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d33,d28])).
% 147.36/30.16 cnf(d35, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c50,d34])).
% 147.36/30.16 cnf(d36, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c51,d35])).
% 147.36/30.16 cnf(d37, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c52,d36])).
% 147.36/30.16 cnf(d38, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d37,d26])).
% 147.36/30.16 cnf(d39, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(superposition, [status(thm)], [d33,d38])).
% 147.36/30.16 cnf(d40, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d39,c41])).
% 147.36/30.16 cnf(d41, plain, sK41(X1) != sK41(sK22(X0,sK38,sK39)) | sK41(X1) = 'ordered$upair'(sK44(X1),sK45(X1)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(X1),'cartesian$uproduct2'(sK37,sK37)) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d33,c59])).
% 147.36/30.16 cnf(d42, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d41])).
% 147.36/30.16 cnf(d43, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d42,d40])).
% 147.36/30.16 cnf(d44, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d43,d26])).
% 147.36/30.16 cnf(d45, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(resolution, [status(thm)], [d44,c43])).
% 147.36/30.16 cnf(d46, plain, ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(X0,X0)) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(X0,sK38,sK39,'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39)))) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d45,d3])).
% 147.36/30.16 cnf(d47, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39)))) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)), inference(resolution, [status(thm)], [d46,c54])).
% 147.36/30.16 cnf(d48, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK31(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d45,d47])).
% 147.36/30.16 cnf(d49, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d48,c36])).
% 147.36/30.16 cnf(d50, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d49])).
% 147.36/30.16 cnf(d51, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d50])).
% 147.36/30.16 cnf(d52, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d51])).
% 147.36/30.16 cnf(d53, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d52,c41])).
% 147.36/30.16 cnf(d54, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)), inference(resolution, [status(thm)], [d52,c40])).
% 147.36/30.16 cnf(d55, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(resolution, [status(thm)], [d54,c43])).
% 147.36/30.16 cnf(d56, plain, sK41(X0) != sK41(sK22(sK37,sK38,sK39)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | ~in(sK41(X0),X0) | ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(superposition, [status(thm)], [d55,c57])).
% 147.36/30.16 cnf(d57, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d56])).
% 147.36/30.16 cnf(d58, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d57,d53])).
% 147.36/30.16 cnf(d59, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d58,c37])).
% 147.36/30.16 cnf(d60, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~relation(sK39) | ~function(sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d59])).
% 147.36/30.16 cnf(d61, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~function(sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d60])).
% 147.36/30.16 cnf(d62, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d61])).
% 147.36/30.16 cnf(d63, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d62,d52])).
% 147.36/30.16 cnf(d64, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d63,d26])).
% 147.36/30.16 cnf(d65, plain, sK30(sK38,sK39) = sK31(sK38,sK39) | sK30(sK38,sK39) = sK31(sK38,sK39), inference(resolution, [status(thm)], [d64,c43])).
% 147.36/30.16 cnf(d66, plain, sK24(X0,X1,sK41(sK22(X1,X2,X0)),X2) = sK41(sK22(X1,X2,X0)) | sK41(sK22(X1,X2,X0)) = 'ordered$upair'(sK44(sK22(X1,X2,X0)),sK45(sK22(X1,X2,X0))) | ~relation(X0) | ~relation(X2) | ~function(X0) | sK30(X2,X0) = sK32(X2,X0), inference(resolution, [status(thm)], [d5,c46])).
% 147.36/30.16 cnf(d67, plain, sK24(sK39,X0,sK41(sK22(X0,X1,sK39)),X1) = sK41(sK22(X0,X1,sK39)) | sK30(X1,sK39) = sK32(X1,sK39) | sK41(sK22(X0,X1,sK39)) = 'ordered$upair'(sK44(sK22(X0,X1,sK39)),sK45(sK22(X0,X1,sK39))) | ~relation(X1) | ~relation(sK39), inference(resolution, [status(thm)], [d66,c52])).
% 147.36/30.16 cnf(d68, plain, sK24(sK39,X0,sK41(sK22(X0,X1,sK39)),X1) = sK41(sK22(X0,X1,sK39)) | sK30(X1,sK39) = sK32(X1,sK39) | sK41(sK22(X0,X1,sK39)) = 'ordered$upair'(sK44(sK22(X0,X1,sK39)),sK45(sK22(X0,X1,sK39))) | ~relation(X1), inference(resolution, [status(thm)], [c51,d67])).
% 147.36/30.16 cnf(d69, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d68,c50])).
% 147.36/30.16 cnf(d70, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d69,d3])).
% 147.36/30.16 cnf(d71, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d70,c54])).
% 147.36/30.16 cnf(d72, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d69,d71])).
% 147.36/30.16 cnf(d73, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d72,c36])).
% 147.36/30.16 cnf(d74, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c50,d73])).
% 147.36/30.16 cnf(d75, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c51,d74])).
% 147.36/30.16 cnf(d76, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c52,d75])).
% 147.36/30.16 cnf(d77, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d76,c39])).
% 147.36/30.16 cnf(d78, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | sK24(sK39,sK37,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d77,c39])).
% 147.36/30.16 cnf(d79, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(resolution, [status(thm)], [d78,c46])).
% 147.36/30.16 cnf(d80, plain, sK41(sK22(sK37,sK38,sK39)) != sK41(sK22(sK37,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(equality_factoring, [status(thm)], [d79])).
% 147.36/30.16 cnf(d81, plain, sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(equality_resolution, [status(thm)], [d80])).
% 147.36/30.16 cnf(d82, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d81,c38])).
% 147.36/30.16 cnf(d83, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~relation(sK39) | ~relation(sK38) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d82,d0])).
% 147.36/30.16 cnf(d84, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | ~relation(sK39) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c50,d83])).
% 147.36/30.16 cnf(d85, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c51,d84])).
% 147.36/30.16 cnf(d86, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c52,d85])).
% 147.36/30.16 cnf(d87, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(demodulation, [status(thm)], [d86,d65])).
% 147.36/30.16 cnf(d88, plain, sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK25(X2,sK41(sK22(X0,X1,X2)),X1),sK26(X2,sK41(sK22(X0,X1,X2)),X1)) | sK41(sK22(X0,X1,X2)) = 'ordered$upair'(sK44(sK22(X0,X1,X2)),sK45(sK22(X0,X1,X2))) | ~relation(X2) | ~relation(X1) | ~function(X2) | sK30(X1,X2) = sK32(X1,X2), inference(resolution, [status(thm)], [d29,c46])).
% 147.36/30.16 cnf(d89, plain, sK30(X0,sK39) = sK32(X0,sK39) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X1,X0,sK39)),X0),sK26(sK39,sK41(sK22(X1,X0,sK39)),X0)) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK44(sK22(X1,X0,sK39)),sK45(sK22(X1,X0,sK39))) | ~relation(sK39) | ~relation(X0), inference(resolution, [status(thm)], [d88,c52])).
% 147.36/30.16 cnf(d90, plain, sK30(X0,sK39) = sK32(X0,sK39) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X1,X0,sK39)),X0),sK26(sK39,sK41(sK22(X1,X0,sK39)),X0)) | sK41(sK22(X1,X0,sK39)) = 'ordered$upair'(sK44(sK22(X1,X0,sK39)),sK45(sK22(X1,X0,sK39))) | ~relation(X0), inference(resolution, [status(thm)], [c51,d89])).
% 147.36/30.16 cnf(d91, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d90,c50])).
% 147.36/30.16 cnf(d92, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d91,d28])).
% 147.36/30.16 cnf(d93, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c50,d92])).
% 147.36/30.16 cnf(d94, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c51,d93])).
% 147.36/30.16 cnf(d95, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c52,d94])).
% 147.36/30.16 cnf(d96, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))) | sK30(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d95,d86])).
% 147.36/30.16 cnf(d97, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(superposition, [status(thm)], [d91,d96])).
% 147.36/30.16 cnf(d98, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d97,c41])).
% 147.36/30.16 cnf(d99, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | 'Ts18'(sK38,sK39), inference(demodulation, [status(thm)], [d98,d65])).
% 147.36/30.16 cnf(d100, plain, sK41(X1) != sK41(sK22(X0,sK38,sK39)) | sK41(X1) = 'ordered$upair'(sK44(X1),sK45(X1)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(X1),'cartesian$uproduct2'(sK37,sK37)) | sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d91,c59])).
% 147.36/30.16 cnf(d101, plain, sK30(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d100])).
% 147.36/30.16 cnf(d102, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(demodulation, [status(thm)], [d101,d65])).
% 147.36/30.16 cnf(d103, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d102,d99])).
% 147.36/30.16 cnf(d104, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts18'(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d103,d87])).
% 147.36/30.16 cnf(d105, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(resolution, [status(thm)], [d104,c46])).
% 147.36/30.16 cnf(d106, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(demodulation, [status(thm)], [d105,d65])).
% 147.36/30.16 cnf(d107, plain, ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(X0,X0)) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(X0,sK38,sK39,'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39)))) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d106,d3])).
% 147.36/30.16 cnf(d108, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39)))) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)), inference(resolution, [status(thm)], [d107,c54])).
% 147.36/30.16 cnf(d109, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK31(sK38,sK39) = sK32(sK38,sK39) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d106,d108])).
% 147.36/30.16 cnf(d110, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d109,c36])).
% 147.36/30.16 cnf(d111, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d110])).
% 147.36/30.16 cnf(d112, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d111])).
% 147.36/30.16 cnf(d113, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d112])).
% 147.36/30.16 cnf(d114, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d113,c41])).
% 147.36/30.16 cnf(d115, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)), inference(resolution, [status(thm)], [d113,c40])).
% 147.36/30.16 cnf(d116, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(resolution, [status(thm)], [d115,c46])).
% 147.36/30.16 cnf(d117, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)), inference(demodulation, [status(thm)], [d116,d65])).
% 147.36/30.16 cnf(d118, plain, sK41(X0) != sK41(sK22(sK37,sK38,sK39)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | ~in(sK41(X0),X0) | ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)) | sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39), inference(superposition, [status(thm)], [d117,c57])).
% 147.36/30.16 cnf(d119, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d118])).
% 147.36/30.16 cnf(d120, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d119,d114])).
% 147.36/30.16 cnf(d121, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d120,c37])).
% 147.36/30.16 cnf(d122, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~relation(sK39) | ~function(sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d121])).
% 147.36/30.16 cnf(d123, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~function(sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d122])).
% 147.36/30.16 cnf(d124, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d123])).
% 147.36/30.16 cnf(d125, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d124,d113])).
% 147.36/30.16 cnf(d126, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d125,d87])).
% 147.36/30.16 cnf(d127, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK30(sK38,sK39) = sK32(sK38,sK39), inference(resolution, [status(thm)], [d126,c46])).
% 147.36/30.16 cnf(d128, plain, sK31(sK38,sK39) = sK32(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39), inference(demodulation, [status(thm)], [d127,d65])).
% 147.36/30.16 cnf(d129, plain, sK31(sK38,sK39) != sK31(sK38,sK39) | sK31(sK38,sK39) = sK32(sK38,sK39), inference(equality_factoring, [status(thm)], [d128])).
% 147.36/30.16 cnf(d130, plain, sK31(sK38,sK39) = sK32(sK38,sK39), inference(equality_resolution, [status(thm)], [d129])).
% 147.36/30.16 cnf(d131, plain, sK31(sK38,sK39) != sK31(sK38,sK39) | ~'Ts18'(sK38,sK39), inference(superposition, [status(thm)], [d130,c49])).
% 147.36/30.16 cnf(d132, plain, ~'Ts18'(sK38,sK39), inference(equality_resolution, [status(thm)], [d131])).
% 147.36/30.16 cnf(d133, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~relation(sK38) | ~function(sK39), inference(resolution, [status(thm)], [d132,d5])).
% 147.36/30.16 cnf(d134, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~function(sK39), inference(resolution, [status(thm)], [c50,d133])).
% 147.36/30.16 cnf(d135, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~function(sK39), inference(resolution, [status(thm)], [c51,d134])).
% 147.36/30.16 cnf(d136, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c52,d135])).
% 147.36/30.16 cnf(d137, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(superposition, [status(thm)], [d136,d3])).
% 147.36/30.16 cnf(d138, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39)))) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d137,c54])).
% 147.36/30.16 cnf(d139, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | in(sK41(sK22(X0,sK38,sK39)),sK22(X0,sK38,sK39)) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(superposition, [status(thm)], [d136,d138])).
% 147.36/30.16 cnf(d140, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d139,c36])).
% 147.36/30.16 cnf(d141, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c50,d140])).
% 147.36/30.16 cnf(d142, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c51,d141])).
% 147.36/30.16 cnf(d143, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | 'Ts18'(sK38,sK39) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c52,d142])).
% 147.36/30.16 cnf(d144, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | 'Ts17'(X0,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [d132,d143])).
% 147.36/30.16 cnf(d145, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(X0,sK38,sK39))) | sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d144,c39])).
% 147.36/30.16 cnf(d146, plain, sK24(sK39,X0,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(X0,sK38,sK39)),sK38) = sK41(sK22(X0,sK38,sK39)), inference(resolution, [status(thm)], [d145,c39])).
% 147.36/30.16 cnf(d147, plain, sK41(sK22(sK37,sK38,sK39)) != sK41(sK22(sK37,sK38,sK39)) | sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)), inference(equality_factoring, [status(thm)], [d146])).
% 147.36/30.16 cnf(d148, plain, sK24(sK39,sK37,sK41(sK22(sK37,sK38,sK39)),sK38) = sK41(sK22(sK37,sK38,sK39)), inference(equality_resolution, [status(thm)], [d147])).
% 147.36/30.16 cnf(d149, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(superposition, [status(thm)], [d148,c38])).
% 147.36/30.16 cnf(d150, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | ~relation(sK39) | ~relation(sK38) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [d149,d0])).
% 147.36/30.16 cnf(d151, plain, ~relation(sK39) | ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c50,d150])).
% 147.36/30.16 cnf(d152, plain, ~function(sK39) | in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c51,d151])).
% 147.36/30.16 cnf(d153, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | 'Ts18'(sK38,sK39), inference(resolution, [status(thm)], [c52,d152])).
% 147.36/30.16 cnf(d154, plain, in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(resolution, [status(thm)], [d132,d153])).
% 147.36/30.16 cnf(d155, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~relation(sK38) | ~function(sK39), inference(resolution, [status(thm)], [d132,d29])).
% 147.36/30.16 cnf(d156, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~function(sK39), inference(resolution, [status(thm)], [c50,d155])).
% 147.36/30.16 cnf(d157, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~function(sK39), inference(resolution, [status(thm)], [c51,d156])).
% 147.36/30.16 cnf(d158, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(resolution, [status(thm)], [c52,d157])).
% 147.36/30.16 cnf(d159, plain, ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d158,d28])).
% 147.36/30.16 cnf(d160, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~relation(sK39) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c50,d159])).
% 147.36/30.16 cnf(d161, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~function(sK39) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c51,d160])).
% 147.36/30.16 cnf(d162, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts18'(sK38,sK39) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [c52,d161])).
% 147.36/30.16 cnf(d163, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(X1,X1)) | 'Ts17'(X1,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [d132,d162])).
% 147.36/30.16 cnf(d164, plain, sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | 'Ts17'(sK37,sK38,sK39,'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))), inference(resolution, [status(thm)], [d163,d154])).
% 147.36/30.16 cnf(d165, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(superposition, [status(thm)], [d158,d164])).
% 147.36/30.16 cnf(d166, plain, sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d165,c41])).
% 147.36/30.16 cnf(d167, plain, sK41(X1) != sK41(sK22(X0,sK38,sK39)) | sK41(X1) = 'ordered$upair'(sK44(X1),sK45(X1)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(X1),'cartesian$uproduct2'(sK37,sK37)) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))), inference(superposition, [status(thm)], [d158,c59])).
% 147.36/30.16 cnf(d168, plain, sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | sK41(sK22(X0,sK38,sK39)) = 'ordered$upair'(sK44(sK22(X0,sK38,sK39)),sK45(sK22(X0,sK38,sK39))) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(X0,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(X0,sK38,sK39)),sK38))),sK38) | ~in(sK41(sK22(X0,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d167])).
% 147.36/30.16 cnf(d169, plain, sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)) | sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d168,d166])).
% 147.36/30.16 cnf(d170, plain, sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d154,d169])).
% 147.36/30.16 cnf(d171, plain, ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(X0,X0)) | in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(X0,sK38,sK39,'ordered$upair'(sK44(sK22(sK37,sK38,sK39)),sK45(sK22(sK37,sK38,sK39)))), inference(superposition, [status(thm)], [d170,d3])).
% 147.36/30.16 cnf(d172, plain, in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(X0,X0)) | 'Ts17'(X0,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(demodulation, [status(thm)], [d171,d170])).
% 147.36/30.16 cnf(d173, plain, in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d172,d154])).
% 147.36/30.16 cnf(d174, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))) | ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d173,c36])).
% 147.36/30.16 cnf(d175, plain, ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d174])).
% 147.36/30.16 cnf(d176, plain, ~function(sK39) | 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d175])).
% 147.36/30.16 cnf(d177, plain, 'Ts18'(sK38,sK39) | 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d176])).
% 147.36/30.16 cnf(d178, plain, 'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d132,d177])).
% 147.36/30.16 cnf(d179, plain, sK41(sK22(sK37,sK38,sK39)) = 'ordered$upair'(sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38),sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)), inference(resolution, [status(thm)], [d178,c40])).
% 147.36/30.16 cnf(d180, plain, sK41(X0) != sK41(sK22(sK37,sK38,sK39)) | ~in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38) | ~in(sK41(X0),X0) | ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)), inference(superposition, [status(thm)], [d179,c57])).
% 147.36/30.16 cnf(d181, plain, in('ordered$upair'(apply(sK39,sK25(sK39,sK41(sK22(sK37,sK38,sK39)),sK38)),apply(sK39,sK26(sK39,sK41(sK22(sK37,sK38,sK39)),sK38))),sK38), inference(resolution, [status(thm)], [d178,c41])).
% 147.36/30.16 cnf(d182, plain, sK41(X0) != sK41(sK22(sK37,sK38,sK39)) | ~in(sK41(X0),X0) | ~in(sK41(X0),'cartesian$uproduct2'(sK37,sK37)), inference(resolution, [status(thm)], [d181,d180])).
% 147.36/30.16 cnf(d183, plain, ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)) | ~in(sK41(sK22(sK37,sK38,sK39)),'cartesian$uproduct2'(sK37,sK37)), inference(equality_resolution, [status(thm)], [d182])).
% 147.36/30.16 cnf(d184, plain, ~in(sK41(sK22(sK37,sK38,sK39)),sK22(sK37,sK38,sK39)), inference(resolution, [status(thm)], [d154,d183])).
% 147.36/30.16 cnf(d185, plain, ~relation(sK38) | ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d184,c37])).
% 147.36/30.16 cnf(d186, plain, ~relation(sK39) | ~function(sK39) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c50,d185])).
% 147.36/30.16 cnf(d187, plain, ~function(sK39) | 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c51,d186])).
% 147.36/30.16 cnf(d188, plain, 'Ts18'(sK38,sK39) | ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [c52,d187])).
% 147.36/30.16 cnf(d189, plain, ~'Ts17'(sK37,sK38,sK39,sK41(sK22(sK37,sK38,sK39))), inference(resolution, [status(thm)], [d132,d188])).
% 147.36/30.16 cnf(d190, plain, $false, inference(resolution, [status(thm)], [d178,d189])).
% 147.36/30.16 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------