%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : TOP023+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 09:52:39 AM UTC 2026
% Result : Theorem 18.51s 3.02s
% Output : CNFRefutation 18.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : TOP023+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 20:32:29 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.51/3.02 % SZS status Theorem for theBenchmark.p
% 18.51/3.02 % SZS output start CNFRefutation for theBenchmark.p
% 18.51/3.02 fof(d4_tsp_2, axiom, ! [X0] : (('l1$upre$utopc'(X0) => ! [X1] : (('m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => ('v1$utsp$u2'(X1,X0) <=> ('v1$utsp$u1'(X1,X0) & ! [X2] : (('m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => (('v1$utsp$u1'(X2,X0) & 'r1$utarski'(X1,X2)) => X1 = X2)))))))))).
% 18.51/3.02 fof(dt_u1_pre_topc, axiom, ! [X0] : (('l1$upre$utopc'(X0) => 'm1$usubset$u1'('u1$upre$utopc'(X0),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(X0))))))).
% 18.51/3.02 fof(free_g1_pre_topc, axiom, ! [X0] : ! [X1] : (('m1$usubset$u1'(X1,'k1$uzfmisc$u1'('k1$uzfmisc$u1'(X0))) => ! [X2] : ! [X3] : (('g1$upre$utopc'(X0,X1) = 'g1$upre$utopc'(X2,X3) => (X0 = X2 & X1 = X3)))))).
% 18.51/3.02 fof(t5_tsp_1, axiom, ! [X0] : (('l1$upre$utopc'(X0) => ! [X1] : (('l1$upre$utopc'(X1) => ! [X2] : (('m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => ! [X3] : (('m1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) => (('g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) = 'g1$upre$utopc'('u1$ustruct$u0'(X1),'u1$upre$utopc'(X1)) & (X2 = X3 & 'v1$utsp$u1'(X2,X0))) => 'v1$utsp$u1'(X3,X1))))))))))).
% 18.51/3.02 fof(t1_tsp_2, conjecture, ! [X0] : (('l1$upre$utopc'(X0) => ! [X1] : (('l1$upre$utopc'(X1) => ! [X2] : (('m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => ! [X3] : (('m1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) => (('g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) = 'g1$upre$utopc'('u1$ustruct$u0'(X1),'u1$upre$utopc'(X1)) & (X2 = X3 & 'v1$utsp$u2'(X2,X0))) => 'v1$utsp$u2'(X3,X1))))))))))).
% 18.51/3.02 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('l1$upre$utopc'(X0) => ! [X1] : (('l1$upre$utopc'(X1) => ! [X2] : (('m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => ! [X3] : (('m1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) => (('g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) = 'g1$upre$utopc'('u1$ustruct$u0'(X1),'u1$upre$utopc'(X1)) & (X2 = X3 & 'v1$utsp$u2'(X2,X0))) => 'v1$utsp$u2'(X3,X1)))))))))), inference(negate_conjecture, [status(cth)], [t1_tsp_2])).
% 18.51/3.02 cnf(c45, plain, ~'l1$upre$utopc'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | ~'v1$utsp$u2'(X1,X0) | X2(X0,X1), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c46, plain, ~'l1$upre$utopc'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | 'v1$utsp$u2'(X1,X0) | ~X2(X0,X1), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c47, plain, ~X0(X1,X2) | 'v1$utsp$u1'(X2,X1), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c48, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) | ~'r1$utarski'(X2,X0) | X2 = X0 | ~'v1$utsp$u1'(X0,X1) | ~X3(X1,X2), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c49, plain, X0(X1,X2) | ~'v1$utsp$u1'(X2,X1) | 'm1$usubset$u1'(sK37(X1,X2),'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c50, plain, X0(X1,X2) | ~'v1$utsp$u1'(X2,X1) | 'v1$utsp$u1'(sK37(X1,X2),X1), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c51, plain, X0(X1,X2) | ~'v1$utsp$u1'(X2,X1) | 'r1$utarski'(X2,sK37(X1,X2)), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c52, plain, X0(X1,X2) | ~'v1$utsp$u1'(X2,X1) | X2 != sK37(X1,X2), inference(clausification, [status(esa)], [d4_tsp_2])).
% 18.51/3.02 cnf(c56, plain, ~'l1$upre$utopc'(X0) | 'm1$usubset$u1'('u1$upre$utopc'(X0),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))), inference(clausification, [status(esa)], [dt_u1_pre_topc])).
% 18.51/3.02 cnf(c67, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('k1$uzfmisc$u1'(X1))) | 'g1$upre$utopc'(X1,X0) != 'g1$upre$utopc'(X2,X3) | X1 = X2, inference(clausification, [status(esa)], [free_g1_pre_topc])).
% 18.51/3.02 cnf(c68, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('k1$uzfmisc$u1'(X1))) | 'g1$upre$utopc'(X1,X0) != 'g1$upre$utopc'(X2,X3) | X0 = X3, inference(clausification, [status(esa)], [free_g1_pre_topc])).
% 18.51/3.02 cnf(c97, plain, 'g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) != 'g1$upre$utopc'('u1$ustruct$u0'(X1),'u1$upre$utopc'(X1)) | 'v1$utsp$u1'(X2,X1) | ~'l1$upre$utopc'(X1) | ~'m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) | ~'l1$upre$utopc'(X0) | ~'v1$utsp$u1'(X3,X0) | ~'m1$usubset$u1'(X3,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | X3 != X2, inference(clausification, [status(esa)], [t5_tsp_1])).
% 18.51/3.02 cnf(c101, plain, 'l1$upre$utopc'(sK83), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c102, plain, 'l1$upre$utopc'(sK84), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c103, plain, 'm1$usubset$u1'(sK85,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c104, plain, 'm1$usubset$u1'(sK86,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c105, plain, 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) = 'g1$upre$utopc'('u1$ustruct$u0'(sK84),'u1$upre$utopc'(sK84)), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c106, plain, sK85 = sK86, inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c107, plain, 'v1$utsp$u2'(sK85,sK83), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(c108, plain, ~'v1$utsp$u2'(sK86,sK84), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.51/3.02 cnf(d0, plain, 'g1$upre$utopc'(X0,X1) != 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) | X0 = 'u1$ustruct$u0'(sK84) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('k1$uzfmisc$u1'(X0))), inference(superposition, [status(thm)], [c105,c67])).
% 18.51/3.02 cnf(d1, plain, 'u1$ustruct$u0'(sK83) = 'u1$ustruct$u0'(sK84) | ~'m1$usubset$u1'('u1$upre$utopc'(sK83),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(sK83)))), inference(equality_resolution, [status(thm)], [d0])).
% 18.51/3.02 cnf(d2, plain, 'u1$ustruct$u0'(sK83) = 'u1$ustruct$u0'(sK84) | ~'l1$upre$utopc'(sK83), inference(resolution, [status(thm)], [d1,c56])).
% 18.51/3.02 cnf(d3, plain, 'u1$ustruct$u0'(sK83) = 'u1$ustruct$u0'(sK84), inference(resolution, [status(thm)], [c101,d2])).
% 18.51/3.02 cnf(d4, plain, 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'(X0,X1) | 'u1$upre$utopc'(sK84) = X1 | ~'m1$usubset$u1'('u1$upre$utopc'(sK84),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(sK84)))), inference(superposition, [status(thm)], [c105,c68])).
% 18.51/3.02 cnf(d5, plain, 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'(X0,X1) | 'u1$upre$utopc'(sK84) = X1 | ~'m1$usubset$u1'('u1$upre$utopc'(sK84),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(sK83)))), inference(demodulation, [status(thm)], [d4,d3])).
% 18.51/3.02 cnf(d6, plain, 'm1$usubset$u1'('u1$upre$utopc'(sK84),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(sK83)))) | ~'l1$upre$utopc'(sK84), inference(superposition, [status(thm)], [d3,c56])).
% 18.51/3.02 cnf(d7, plain, 'm1$usubset$u1'('u1$upre$utopc'(sK84),'k1$uzfmisc$u1'('k1$uzfmisc$u1'('u1$ustruct$u0'(sK83)))), inference(resolution, [status(thm)], [c102,d6])).
% 18.51/3.02 cnf(d8, plain, 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'(X0,X1) | 'u1$upre$utopc'(sK84) = X1, inference(resolution, [status(thm)], [d7,d5])).
% 18.51/3.02 cnf(d9, plain, 'u1$upre$utopc'(sK84) = 'u1$upre$utopc'(sK83), inference(equality_resolution, [status(thm)], [d8])).
% 18.51/3.02 cnf(d10, plain, 'g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) != 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK84)) | X1 != X2 | ~'l1$upre$utopc'(sK84) | ~'l1$upre$utopc'(X0) | ~'m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | 'v1$utsp$u1'(X2,sK84) | ~'v1$utsp$u1'(X1,X0), inference(superposition, [status(thm)], [d3,c97])).
% 18.51/3.02 cnf(d11, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) != 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) | ~'l1$upre$utopc'(X2) | ~'l1$upre$utopc'(sK84) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | 'v1$utsp$u1'(X1,sK84) | ~'v1$utsp$u1'(X0,X2), inference(demodulation, [status(thm)], [d10,d9])).
% 18.51/3.02 cnf(d12, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) != 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) | ~'l1$upre$utopc'(X2) | ~'l1$upre$utopc'(sK84) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | 'v1$utsp$u1'(X1,sK84) | ~'v1$utsp$u1'(X0,X2), inference(demodulation, [status(thm)], [d11,d3])).
% 18.51/3.02 cnf(d13, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) != 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) | ~'l1$upre$utopc'(X2) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | 'v1$utsp$u1'(X1,sK84) | ~'v1$utsp$u1'(X0,X2), inference(resolution, [status(thm)], [c102,d12])).
% 18.51/3.02 cnf(d14, plain, X0 != X1 | ~'l1$upre$utopc'(sK83) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,sK84) | ~'v1$utsp$u1'(X0,sK83), inference(equality_resolution, [status(thm)], [d13])).
% 18.51/3.02 cnf(d15, plain, X0 != X1 | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,sK84) | ~'v1$utsp$u1'(X0,sK83), inference(resolution, [status(thm)], [c101,d14])).
% 18.51/3.02 cnf(d16, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X0,sK84) | ~'v1$utsp$u1'(X0,sK83), inference(equality_resolution, [status(thm)], [d15])).
% 18.51/3.02 cnf(d17, plain, ~'v1$utsp$u1'(sK85,sK83) | 'v1$utsp$u1'(sK85,sK84), inference(resolution, [status(thm)], [d16,c103])).
% 18.51/3.02 cnf(d18, plain, ~'l1$upre$utopc'(sK83) | ~'v1$utsp$u2'(sK85,sK83) | 'Ts33'(sK83,sK85), inference(resolution, [status(thm)], [c45,c103])).
% 18.51/3.02 cnf(d19, plain, ~'v1$utsp$u2'(sK85,sK83) | 'Ts33'(sK83,sK85), inference(resolution, [status(thm)], [c101,d18])).
% 18.51/3.02 cnf(d20, plain, 'Ts33'(sK83,sK85), inference(resolution, [status(thm)], [c107,d19])).
% 18.51/3.02 cnf(d21, plain, 'v1$utsp$u1'(sK85,sK83), inference(resolution, [status(thm)], [d20,c47])).
% 18.51/3.02 cnf(d22, plain, 'v1$utsp$u1'(sK85,sK84), inference(resolution, [status(thm)], [d21,d17])).
% 18.51/3.02 cnf(d23, plain, 'm1$usubset$u1'(sK37(sK84,X0),'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84), inference(superposition, [status(thm)], [d3,c49])).
% 18.51/3.02 cnf(d24, plain, 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84) | X1 = sK37(sK84,X0) | ~'Ts33'(sK83,X1) | ~'v1$utsp$u1'(sK37(sK84,X0),sK83) | ~'r1$utarski'(X1,sK37(sK84,X0)), inference(resolution, [status(thm)], [d23,c48])).
% 18.51/3.02 cnf(d25, plain, X0 = sK37(sK84,X0) | ~'Ts33'(sK83,X0) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84) | ~'v1$utsp$u1'(sK37(sK84,X0),sK83) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [d24,c51])).
% 18.51/3.02 cnf(d26, plain, 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK84)) != 'g1$upre$utopc'('u1$ustruct$u0'(X0),'u1$upre$utopc'(X0)) | X1 != X2 | ~'l1$upre$utopc'(X0) | ~'l1$upre$utopc'(sK84) | ~'m1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))) | 'v1$utsp$u1'(X2,X0) | ~'v1$utsp$u1'(X1,sK84), inference(superposition, [status(thm)], [d3,c97])).
% 18.51/3.02 cnf(d27, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) | ~'l1$upre$utopc'(X2) | ~'l1$upre$utopc'(sK84) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))) | 'v1$utsp$u1'(X1,X2) | ~'v1$utsp$u1'(X0,sK84), inference(demodulation, [status(thm)], [d26,d9])).
% 18.51/3.02 cnf(d28, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) | ~'l1$upre$utopc'(X2) | ~'l1$upre$utopc'(sK84) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,X2) | ~'v1$utsp$u1'(X0,sK84), inference(demodulation, [status(thm)], [d27,d3])).
% 18.51/3.02 cnf(d29, plain, X0 != X1 | 'g1$upre$utopc'('u1$ustruct$u0'(sK83),'u1$upre$utopc'(sK83)) != 'g1$upre$utopc'('u1$ustruct$u0'(X2),'u1$upre$utopc'(X2)) | ~'l1$upre$utopc'(X2) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,X2) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [c102,d28])).
% 18.51/3.02 cnf(d30, plain, X0 != X1 | ~'l1$upre$utopc'(sK83) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,sK83) | ~'v1$utsp$u1'(X0,sK84), inference(equality_resolution, [status(thm)], [d29])).
% 18.51/3.02 cnf(d31, plain, X0 != X1 | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X1,sK83) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [c101,d30])).
% 18.51/3.02 cnf(d32, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK83))) | 'v1$utsp$u1'(X0,sK83) | ~'v1$utsp$u1'(X0,sK84), inference(equality_resolution, [status(thm)], [d31])).
% 18.51/3.02 cnf(d33, plain, 'v1$utsp$u1'(sK37(sK84,X0),sK83) | ~'v1$utsp$u1'(sK37(sK84,X0),sK84) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [d32,d23])).
% 18.51/3.02 cnf(d34, plain, 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84) | 'v1$utsp$u1'(sK37(sK84,X0),sK83) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [d33,c50])).
% 18.51/3.02 cnf(d35, plain, 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84) | X0 = sK37(sK84,X0) | ~'Ts33'(sK83,X0) | 'Ts33'(sK84,X0) | ~'v1$utsp$u1'(X0,sK84), inference(resolution, [status(thm)], [d34,d25])).
% 18.51/3.02 cnf(d36, plain, sK85 = sK37(sK84,sK85) | ~'Ts33'(sK83,sK85) | 'Ts33'(sK84,sK85), inference(resolution, [status(thm)], [d35,d22])).
% 18.51/3.02 cnf(d37, plain, sK85 = sK37(sK84,sK85) | 'Ts33'(sK84,sK85), inference(resolution, [status(thm)], [d20,d36])).
% 18.51/3.02 cnf(d38, plain, 'm1$usubset$u1'(sK85,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK84))), inference(demodulation, [status(thm)], [c104,c106])).
% 18.51/3.02 cnf(d39, plain, ~'l1$upre$utopc'(sK84) | 'v1$utsp$u2'(sK85,sK84) | ~'Ts33'(sK84,sK85), inference(resolution, [status(thm)], [c46,d38])).
% 18.51/3.02 cnf(d40, plain, 'v1$utsp$u2'(sK85,sK84) | ~'Ts33'(sK84,sK85), inference(resolution, [status(thm)], [c102,d39])).
% 18.51/3.02 cnf(d41, plain, ~'v1$utsp$u2'(sK85,sK84), inference(demodulation, [status(thm)], [c108,c106])).
% 18.51/3.02 cnf(d42, plain, ~'Ts33'(sK84,sK85), inference(resolution, [status(thm)], [d41,d40])).
% 18.51/3.02 cnf(d43, plain, sK85 = sK37(sK84,sK85), inference(resolution, [status(thm)], [d42,d37])).
% 18.51/3.02 cnf(d44, plain, sK85 != sK85 | 'Ts33'(sK84,sK85) | ~'v1$utsp$u1'(sK85,sK84), inference(superposition, [status(thm)], [d43,c52])).
% 18.51/3.02 cnf(d45, plain, sK85 != sK85 | ~'v1$utsp$u1'(sK85,sK84), inference(resolution, [status(thm)], [d42,d44])).
% 18.51/3.02 cnf(d46, plain, sK85 != sK85, inference(resolution, [status(thm)], [d22,d45])).
% 18.51/3.02 cnf(d47, plain, $false, inference(equality_resolution, [status(thm)], [d46])).
% 18.51/3.02 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------