%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:38 AM UTC 2026
% Result : Theorem 29.38s 8.41s
% Output : CNFRefutation 29.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU314+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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 09:10:10 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.38/8.41 % SZS status Theorem for theBenchmark.p
% 29.38/8.41 % SZS output start CNFRefutation for theBenchmark.p
% 29.38/8.41 fof(s1_tarski__e1_40__pre_topc__1, axiom, ! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0))))) => (! [X2] : ! [X3] : ! [X4] : (((X2 = X3 & (? [X5] : ((element(X5,powerset('the$ucarrier'(X0))) & (X5 = X3 & ('closed$usubset'(X5,X0) & subset(X1,X3))))) & (X2 = X4 & ? [X6] : ((element(X6,powerset('the$ucarrier'(X0))) & (X6 = X4 & ('closed$usubset'(X6,X0) & subset(X1,X4)))))))) => X3 = X4)) => ? [X2] : ! [X3] : ((in(X3,X2) <=> ? [X4] : ((in(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & ? [X7] : ((element(X7,powerset('the$ucarrier'(X0))) & (X7 = X3 & ('closed$usubset'(X7,X0) & subset(X1,X3)))))))))))))).
% 29.38/8.41 fof(s1_xboole_0__e1_40__pre_topc__1, conjecture, ! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset('the$ucarrier'(X0))) & ? [X4] : ((element(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & ('closed$usubset'(X4,X0) & subset(X1,X3))))))))))).
% 29.38/8.41 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset('the$ucarrier'(X0))) & ? [X4] : ((element(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & ('closed$usubset'(X4,X0) & subset(X1,X3)))))))))), inference(negate_conjecture, [status(cth)], [s1_xboole_0__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c58, plain, X0(X1,X2) | ~in(X3,sK45(X1,X2)) | ~'top$ustr'(X1) | X4(X1,X2,X3) | ~element(X2,powerset('the$ucarrier'(X1))) | ~'topological$uspace'(X1), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c59, plain, X0(X1,X2) | ~'closed$usubset'(X3,X1) | X4 != X5 | ~element(X3,powerset('the$ucarrier'(X1))) | ~'top$ustr'(X1) | ~in(X5,powerset('the$ucarrier'(X1))) | in(X4,sK45(X1,X2)) | ~subset(X2,X4) | ~element(X2,powerset('the$ucarrier'(X1))) | X4 != X3 | ~'topological$uspace'(X1), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c60, plain, ~X0(X1,X2,X3) | in(sK49(X1,X2,X3),powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c61, plain, ~X0(X1,X2,X3) | element(sK50(X1,X2,X3),powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c62, plain, ~X0(X1,X2,X3) | 'closed$usubset'(sK50(X1,X2,X3),X1), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c63, plain, ~X0(X1,X2,X3) | subset(X2,X3), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c64, plain, ~X0(X1,X2,X3) | X3 = sK50(X1,X2,X3), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c65, plain, ~X0(X1,X2,X3) | X3 = sK49(X1,X2,X3), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c74, plain, ~X0(X1,X2) | sK53(X1,X2) = sK51(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c75, plain, ~X0(X1,X2) | sK52(X1,X2) = sK51(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c76, plain, ~X0(X1,X2) | sK53(X1,X2) != sK52(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e1_40__pre_topc__1])).
% 29.38/8.41 cnf(c77, plain, 'top$ustr'(sK57), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c78, plain, element(sK58,powerset('the$ucarrier'(sK57))), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c79, plain, 'topological$uspace'(sK57), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c80, plain, in(sK60(X0),X0) | X1(sK57,sK58,X0,sK60(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c81, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~in(sK60(X1),powerset('the$ucarrier'(sK57))) | ~'closed$usubset'(X0,sK57) | X2(sK57,sK58,X1,sK60(X1)) | ~subset(sK58,sK60(X1)) | sK60(X1) != X0, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c82, plain, ~X0(X1,X2,X3,X4) | ~in(X4,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c83, plain, ~X0(X1,X2,X3,X4) | element(sK62(X4,X1,X2),powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c84, plain, ~X0(X1,X2,X3,X4) | 'closed$usubset'(sK62(X4,X1,X2),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c85, plain, ~X0(X1,X2,X3,X4) | subset(X2,X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c86, plain, ~X0(X1,X2,X3,X4) | X4 = sK62(X4,X1,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(c87, plain, ~X0(X1,X2,X3,X4) | in(X4,powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.38/8.41 cnf(d0, plain, ~in(X0,sK45(sK57,sK58)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | 'Ts41'(sK57,sK58,X0) | 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [c58,c78])).
% 29.38/8.41 cnf(d1, plain, ~in(X0,sK45(sK57,sK58)) | ~'topological$uspace'(sK57) | 'Ts41'(sK57,sK58,X0) | 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [c77,d0])).
% 29.38/8.41 cnf(d2, plain, ~in(X0,sK45(sK57,sK58)) | 'Ts41'(sK57,sK58,X0) | 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [c79,d1])).
% 29.38/8.41 cnf(d3, plain, 'Ts41'(sK57,sK58,sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d2,c80])).
% 29.38/8.41 cnf(d4, plain, 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'closed$usubset'(sK50(sK57,sK58,sK60(sK45(sK57,sK58))),sK57), inference(resolution, [status(thm)], [d3,c62])).
% 29.38/8.41 cnf(d5, plain, sK60(sK45(sK57,sK58)) = sK50(sK57,sK58,sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [c64,d3])).
% 29.38/8.41 cnf(d6, plain, 'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(superposition, [status(thm)], [d5,d4])).
% 29.38/8.41 cnf(d7, plain, 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | in(sK49(sK57,sK58,sK60(sK45(sK57,sK58))),powerset('the$ucarrier'(sK57))), inference(resolution, [status(thm)], [d3,c60])).
% 29.38/8.41 cnf(d8, plain, sK60(sK45(sK57,sK58)) = sK49(sK57,sK58,sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [c65,d3])).
% 29.38/8.41 cnf(d9, plain, in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(superposition, [status(thm)], [d8,d7])).
% 29.38/8.41 cnf(d10, plain, subset(sK58,sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [c63,d3])).
% 29.38/8.41 cnf(d11, plain, 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | element(sK50(sK57,sK58,sK60(sK45(sK57,sK58))),powerset('the$ucarrier'(sK57))), inference(resolution, [status(thm)], [d3,c61])).
% 29.38/8.41 cnf(d12, plain, element(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(superposition, [status(thm)], [d5,d11])).
% 29.38/8.41 cnf(d13, plain, ~element(sK60(X0),powerset('the$ucarrier'(sK57))) | ~subset(sK58,sK60(X0)) | ~in(sK60(X0),powerset('the$ucarrier'(sK57))) | ~'closed$usubset'(sK60(X0),sK57) | 'Ts56'(sK57,sK58,X0,sK60(X0)), inference(equality_resolution, [status(thm)], [c81])).
% 29.38/8.41 cnf(d14, plain, ~subset(sK58,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d13,d12])).
% 29.38/8.41 cnf(d15, plain, ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d14,d10])).
% 29.38/8.41 cnf(d16, plain, ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d15,d9])).
% 29.38/8.41 cnf(d17, plain, 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d16,d6])).
% 29.38/8.41 cnf(d18, plain, 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | sK53(sK57,sK58) = sK51(sK57,sK58), inference(resolution, [status(thm)], [d17,c74])).
% 29.38/8.41 cnf(d19, plain, 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | sK52(sK57,sK58) = sK51(sK57,sK58), inference(resolution, [status(thm)], [d17,c75])).
% 29.38/8.41 cnf(d20, plain, sK53(sK57,sK58) = sK52(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(superposition, [status(thm)], [d19,d18])).
% 29.38/8.41 cnf(d21, plain, sK52(sK57,sK58) != sK52(sK57,sK58) | ~'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(superposition, [status(thm)], [d20,c76])).
% 29.38/8.41 cnf(d22, plain, ~'Ts42'(sK57,sK58) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(equality_resolution, [status(thm)], [d21])).
% 29.38/8.41 cnf(d23, plain, 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))) | 'Ts56'(sK57,sK58,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d22,d17])).
% 29.38/8.41 cnf(d24, plain, sK60(sK45(sK57,sK58)) = sK62(sK60(sK45(sK57,sK58)),sK57,sK58), inference(resolution, [status(thm)], [d23,c86])).
% 29.38/8.41 cnf(d25, plain, X0 != X1 | ~element(X2,powerset('the$ucarrier'(X3))) | ~element(X1,powerset('the$ucarrier'(X3))) | ~subset(X2,X0) | in(X0,sK45(X3,X2)) | ~in(X0,powerset('the$ucarrier'(X3))) | ~'top$ustr'(X3) | ~'topological$uspace'(X3) | ~'closed$usubset'(X1,X3) | 'Ts42'(X3,X2), inference(equality_resolution, [status(thm)], [c59])).
% 29.38/8.41 cnf(d26, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~element(X2,powerset('the$ucarrier'(X1))) | ~subset(X0,X2) | ~in(X2,powerset('the$ucarrier'(X1))) | in(X2,sK45(X1,X0)) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | ~'closed$usubset'(X2,X1) | 'Ts42'(X1,X0), inference(equality_resolution, [status(thm)], [d25])).
% 29.38/8.41 cnf(d27, plain, element(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),powerset('the$ucarrier'(sK57))), inference(resolution, [status(thm)], [d23,c83])).
% 29.38/8.41 cnf(d28, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK62(sK60(sK45(sK57,sK58)),sK57,sK58)) | ~in(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),powerset('the$ucarrier'(sK57))) | in(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK45(sK57,X0)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK57) | 'Ts42'(sK57,X0), inference(resolution, [status(thm)], [d27,d26])).
% 29.38/8.41 cnf(d29, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),powerset('the$ucarrier'(sK57))) | in(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK45(sK57,X0)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK57) | 'Ts42'(sK57,X0), inference(demodulation, [status(thm)], [d28,d24])).
% 29.38/8.41 cnf(d30, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | in(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK45(sK57,X0)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK57) | 'Ts42'(sK57,X0), inference(demodulation, [status(thm)], [d29,d24])).
% 29.38/8.41 cnf(d31, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK57) | 'Ts42'(sK57,X0), inference(demodulation, [status(thm)], [d30,d24])).
% 29.38/8.41 cnf(d32, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | ~'top$ustr'(sK57) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,X0), inference(demodulation, [status(thm)], [d31,d24])).
% 29.38/8.41 cnf(d33, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | ~'topological$uspace'(sK57) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,X0), inference(resolution, [status(thm)], [c77,d32])).
% 29.38/8.41 cnf(d34, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | ~in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,X0), inference(resolution, [status(thm)], [c79,d33])).
% 29.38/8.41 cnf(d35, plain, in(sK60(sK45(sK57,sK58)),powerset('the$ucarrier'(sK57))), inference(resolution, [status(thm)], [d23,c87])).
% 29.38/8.41 cnf(d36, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | ~'closed$usubset'(sK60(sK45(sK57,sK58)),sK57) | 'Ts42'(sK57,X0), inference(resolution, [status(thm)], [d35,d34])).
% 29.38/8.41 cnf(d37, plain, 'closed$usubset'(sK62(sK60(sK45(sK57,sK58)),sK57,sK58),sK57), inference(resolution, [status(thm)], [d23,c84])).
% 29.38/8.41 cnf(d38, plain, 'closed$usubset'(sK60(sK45(sK57,sK58)),sK57), inference(demodulation, [status(thm)], [d37,d24])).
% 29.38/8.41 cnf(d39, plain, ~element(X0,powerset('the$ucarrier'(sK57))) | ~subset(X0,sK60(sK45(sK57,sK58))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,X0)) | 'Ts42'(sK57,X0), inference(resolution, [status(thm)], [d38,d36])).
% 29.38/8.41 cnf(d40, plain, ~subset(sK58,sK60(sK45(sK57,sK58))) | in(sK60(sK45(sK57,sK58)),sK45(sK57,sK58)) | 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [d39,c78])).
% 29.38/8.41 cnf(d41, plain, subset(sK58,sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d23,c85])).
% 29.38/8.41 cnf(d42, plain, in(sK60(sK45(sK57,sK58)),sK45(sK57,sK58)) | 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [d41,d40])).
% 29.38/8.41 cnf(d43, plain, 'Ts42'(sK57,sK58) | ~'Ts56'(X0,X1,sK45(sK57,sK58),sK60(sK45(sK57,sK58))), inference(resolution, [status(thm)], [d42,c82])).
% 29.38/8.41 cnf(d44, plain, 'Ts42'(sK57,sK58), inference(resolution, [status(thm)], [d43,d23])).
% 29.38/8.41 cnf(d45, plain, sK52(sK57,sK58) = sK51(sK57,sK58), inference(resolution, [status(thm)], [d44,c75])).
% 29.38/8.41 cnf(d46, plain, sK53(sK57,sK58) = sK51(sK57,sK58), inference(resolution, [status(thm)], [d44,c74])).
% 29.38/8.41 cnf(d47, plain, sK53(sK57,sK58) = sK52(sK57,sK58), inference(demodulation, [status(thm)], [d46,d45])).
% 29.38/8.41 cnf(d48, plain, sK52(sK57,sK58) != sK52(sK57,sK58) | ~'Ts42'(sK57,sK58), inference(superposition, [status(thm)], [d47,c76])).
% 29.38/8.41 cnf(d49, plain, sK52(sK57,sK58) != sK52(sK57,sK58), inference(resolution, [status(thm)], [d44,d48])).
% 29.38/8.41 cnf(d50, plain, $false, inference(equality_resolution, [status(thm)], [d49])).
% 29.38/8.41 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------