%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU315+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 : n002.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 100.35s 27.20s
% Output : CNFRefutation 100.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU315+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.08/0.43 % Computer : n002.cluster.edu
% 0.08/0.43 % Model : x86_64 x86_64
% 0.08/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.43 % Memory : 8046.5625MB
% 0.08/0.43 % OS : Linux 6.8.0-71-generic
% 0.08/0.43 % CPULimit : 300
% 0.08/0.43 % WCLimit : 300
% 0.08/0.43 % DateTime : Sat Sep 26 09:13:35 UTC 2026
% 0.08/0.43 % CPUTime :
% 0.08/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 100.35/27.20 % SZS status Theorem for theBenchmark.p
% 100.35/27.20 % SZS output start CNFRefutation for theBenchmark.p
% 100.35/27.20 fof(fc1_subset_1, axiom, ! [X0] : ~empty(powerset(X0))).
% 100.35/27.20 fof(s1_xboole_0__e1_40__pre_topc__1, axiom, ! [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))))))))))).
% 100.35/27.20 fof(d2_subset_1, axiom, ! [X0] : ! [X1] : (((~empty(X0) => (element(X1,X0) <=> in(X1,X0))) & (empty(X0) => (element(X1,X0) <=> empty(X1)))))).
% 100.35/27.20 fof(l71_subset_1, axiom, ! [X0] : ! [X1] : ((! [X2] : ((in(X2,X0) => in(X2,X1))) => element(X0,powerset(X1))))).
% 100.35/27.20 fof(s3_subset_1__e1_40__pre_topc, conjecture, ! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0))))) => ? [X2] : ((element(X2,powerset(powerset('the$ucarrier'(X0)))) & ! [X3] : ((element(X3,powerset('the$ucarrier'(X0))) => (in(X3,X2) <=> ? [X4] : ((element(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & ('closed$usubset'(X4,X0) & subset(X1,X3))))))))))))).
% 100.35/27.20 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0))))) => ? [X2] : ((element(X2,powerset(powerset('the$ucarrier'(X0)))) & ! [X3] : ((element(X3,powerset('the$ucarrier'(X0))) => (in(X3,X2) <=> ? [X4] : ((element(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & ('closed$usubset'(X4,X0) & subset(X1,X3)))))))))))), inference(negate_conjecture, [status(cth)], [s3_subset_1__e1_40__pre_topc])).
% 100.35/27.20 cnf(c57, plain, ~empty(powerset(X0)), inference(clausification, [status(esa)], [fc1_subset_1])).
% 100.35/27.20 cnf(c58, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~in(X2,sK44(X1,X0)) | X3(X1,X0,X2) | ~'top$ustr'(X1) | ~'topological$uspace'(X1), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c59, plain, ~element(X0,powerset('the$ucarrier'(X1))) | in(X2,sK44(X1,X0)) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | ~X3(X1,X0,X2), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c60, plain, ~X0(X1,X2,X3) | in(X3,powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c62, plain, ~X0(X1,X2,X3) | sK46(X1,X2,X3) = X3, inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c63, plain, ~X0(X1,X2,X3) | 'closed$usubset'(sK46(X1,X2,X3),X1), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c64, plain, ~X0(X1,X2,X3) | subset(X2,X3), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c65, plain, ~in(X0,powerset('the$ucarrier'(X1))) | X2(X1,X3,X0) | ~element(X4,powerset('the$ucarrier'(X1))) | X4 != X0 | ~'closed$usubset'(X4,X1) | ~subset(X3,X0), inference(clausification, [status(esa)], [s1_xboole_0__e1_40__pre_topc__1])).
% 100.35/27.20 cnf(c66, plain, empty(X0) | ~element(X1,X0) | in(X1,X0), inference(clausification, [status(esa)], [d2_subset_1])).
% 100.35/27.20 cnf(c72, plain, in(sK54(X0,X1),X0) | element(X0,powerset(X1)), inference(clausification, [status(esa)], [l71_subset_1])).
% 100.35/27.20 cnf(c73, plain, ~in(sK54(X0,X1),X1) | element(X0,powerset(X1)), inference(clausification, [status(esa)], [l71_subset_1])).
% 100.35/27.20 cnf(c79, plain, 'topological$uspace'(sK63), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c80, plain, 'top$ustr'(sK63), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c81, plain, element(sK64,powerset('the$ucarrier'(sK63))), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c82, plain, ~element(X0,powerset(powerset('the$ucarrier'(sK63)))) | element(sK66(X0),powerset('the$ucarrier'(sK63))), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c84, plain, ~element(X0,powerset(powerset('the$ucarrier'(sK63)))) | in(sK66(X0),X0) | X1(sK63,sK64,sK66(X0)), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c85, plain, ~element(X0,powerset(powerset('the$ucarrier'(sK63)))) | ~X1(sK63,sK64,sK66(X0)) | ~in(sK66(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c88, plain, ~X0(X1,X2,X3) | sK67(X1,X2,X3) = X3, inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c89, plain, ~X0(X1,X2,X3) | 'closed$usubset'(sK67(X1,X2,X3),X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c90, plain, ~X0(X1,X2,X3) | subset(X2,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(c91, plain, ~'closed$usubset'(X0,X1) | ~element(X0,powerset('the$ucarrier'(X1))) | ~subset(X2,X3) | X0 != X3 | X4(X1,X2,X3), inference(clausification, [status(esa)], [negated_conjecture])).
% 100.35/27.20 cnf(d0, plain, element(sK44(X0,X1),powerset(X2)) | ~element(X1,powerset('the$ucarrier'(X0))) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'Ts41'(X0,X1,sK54(sK44(X0,X1),X2)), inference(resolution, [status(thm)], [c72,c58])).
% 100.35/27.20 cnf(d1, plain, ~element(X0,powerset('the$ucarrier'(X1))) | element(sK44(X1,X0),powerset(X2)) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | in(sK54(sK44(X1,X0),X2),powerset('the$ucarrier'(X1))), inference(resolution, [status(thm)], [d0,c60])).
% 100.35/27.20 cnf(d2, plain, ~element(X0,powerset('the$ucarrier'(X1))) | element(sK44(X1,X0),powerset(powerset('the$ucarrier'(X1)))) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | element(sK44(X1,X0),powerset(powerset('the$ucarrier'(X1)))), inference(resolution, [status(thm)], [d1,c73])).
% 100.35/27.20 cnf(d3, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63) | ~'topological$uspace'(sK63) | in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d2,c84])).
% 100.35/27.20 cnf(d4, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | ~'top$ustr'(sK63) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c79,d3])).
% 100.35/27.20 cnf(d5, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c80,d4])).
% 100.35/27.20 cnf(d6, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))) | ~element(X0,powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63) | ~'topological$uspace'(sK63) | 'Ts41'(sK63,X0,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d5,c58])).
% 100.35/27.20 cnf(d7, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63) | 'Ts41'(sK63,X0,sK66(sK44(sK63,X0))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c79,d6])).
% 100.35/27.20 cnf(d8, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | 'Ts41'(sK63,X0,sK66(sK44(sK63,X0))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c80,d7])).
% 100.35/27.20 cnf(d9, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))) | sK46(sK63,X0,sK66(sK44(sK63,X0))) = sK66(sK44(sK63,X0)), inference(resolution, [status(thm)], [d8,c62])).
% 100.35/27.20 cnf(d10, plain, sK46(sK63,X0,sK66(sK44(sK63,X0))) = sK66(sK44(sK63,X0)) | ~element(X0,powerset('the$ucarrier'(sK63))) | sK67(sK63,sK64,sK66(sK44(sK63,X0))) = sK66(sK44(sK63,X0)), inference(resolution, [status(thm)], [d9,c88])).
% 100.35/27.20 cnf(d11, plain, sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)) | sK67(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)), inference(resolution, [status(thm)], [d10,c81])).
% 100.35/27.20 cnf(d12, plain, 'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))) | sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)), inference(superposition, [status(thm)], [d11,c89])).
% 100.35/27.20 cnf(d13, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~subset(X2,X0) | ~'closed$usubset'(X0,X1) | 'Ts62'(X1,X2,X0), inference(equality_resolution, [status(thm)], [c91])).
% 100.35/27.20 cnf(d14, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63) | ~'topological$uspace'(sK63) | element(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [d2,c82])).
% 100.35/27.20 cnf(d15, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | element(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63), inference(resolution, [status(thm)], [c79,d14])).
% 100.35/27.20 cnf(d16, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | element(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [c80,d15])).
% 100.35/27.20 cnf(d17, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~subset(X1,sK66(sK44(sK63,X0))) | ~'closed$usubset'(sK66(sK44(sK63,X0)),sK63) | 'Ts62'(sK63,X1,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d16,d13])).
% 100.35/27.20 cnf(d18, plain, in(X0,sK44(sK63,sK64)) | ~'top$ustr'(sK63) | ~'topological$uspace'(sK63) | ~'Ts41'(sK63,sK64,X0), inference(resolution, [status(thm)], [c59,c81])).
% 100.35/27.20 cnf(d19, plain, in(X0,sK44(sK63,sK64)) | ~'top$ustr'(sK63) | ~'Ts41'(sK63,sK64,X0), inference(resolution, [status(thm)], [c79,d18])).
% 100.35/27.20 cnf(d20, plain, in(X0,sK44(sK63,sK64)) | ~'Ts41'(sK63,sK64,X0), inference(resolution, [status(thm)], [c80,d19])).
% 100.35/27.20 cnf(d21, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~'top$ustr'(sK63) | ~'topological$uspace'(sK63) | ~in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d2,c85])).
% 100.35/27.20 cnf(d22, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | ~'top$ustr'(sK63) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c79,d21])).
% 100.35/27.20 cnf(d23, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~in(sK66(sK44(sK63,X0)),sK44(sK63,X0)) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [c80,d22])).
% 100.35/27.20 cnf(d24, plain, ~element(sK64,powerset('the$ucarrier'(sK63))) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))) | ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d23,d20])).
% 100.35/27.20 cnf(d25, plain, ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [c81,d24])).
% 100.35/27.20 cnf(d26, plain, ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))) | ~element(sK64,powerset('the$ucarrier'(sK63))) | ~subset(sK64,sK66(sK44(sK63,sK64))) | ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63), inference(resolution, [status(thm)], [d25,d17])).
% 100.35/27.20 cnf(d27, plain, ~subset(sK64,sK66(sK44(sK63,sK64))) | ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [c81,d26])).
% 100.35/27.20 cnf(d28, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,X0))) | subset(X0,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d8,c64])).
% 100.35/27.20 cnf(d29, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | subset(X0,sK66(sK44(sK63,X0))) | subset(sK64,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d28,c90])).
% 100.35/27.20 cnf(d30, plain, ~element(sK64,powerset('the$ucarrier'(sK63))) | subset(sK64,sK66(sK44(sK63,sK64))), inference(factoring, [status(thm)], [d29])).
% 100.35/27.20 cnf(d31, plain, subset(sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [c81,d30])).
% 100.35/27.20 cnf(d32, plain, ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d31,d27])).
% 100.35/27.20 cnf(d33, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~subset(X2,X0) | ~in(X0,powerset('the$ucarrier'(X1))) | ~'closed$usubset'(X0,X1) | 'Ts41'(X1,X2,X0), inference(equality_resolution, [status(thm)], [c65])).
% 100.35/27.20 cnf(d34, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | empty(powerset('the$ucarrier'(sK63))) | in(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [d16,c66])).
% 100.35/27.20 cnf(d35, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | in(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [c57,d34])).
% 100.35/27.20 cnf(d36, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~element(sK66(sK44(sK63,X0)),powerset('the$ucarrier'(sK63))) | ~subset(X1,sK66(sK44(sK63,X0))) | ~'closed$usubset'(sK66(sK44(sK63,X0)),sK63) | 'Ts41'(sK63,X1,sK66(sK44(sK63,X0))), inference(resolution, [status(thm)], [d35,d33])).
% 100.35/27.20 cnf(d37, plain, ~element(X0,powerset('the$ucarrier'(sK63))) | ~subset(X1,sK66(sK44(sK63,X0))) | ~'closed$usubset'(sK66(sK44(sK63,X0)),sK63) | 'Ts41'(sK63,X1,sK66(sK44(sK63,X0))) | ~element(X0,powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [d36,d16])).
% 100.35/27.20 cnf(d38, plain, ~element(sK64,powerset('the$ucarrier'(sK63))) | ~subset(sK64,sK66(sK44(sK63,sK64))) | ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63), inference(resolution, [status(thm)], [d37,d32])).
% 100.35/27.20 cnf(d39, plain, ~subset(sK64,sK66(sK44(sK63,sK64))) | ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63), inference(resolution, [status(thm)], [c81,d38])).
% 100.35/27.20 cnf(d40, plain, ~'closed$usubset'(sK66(sK44(sK63,sK64)),sK63), inference(resolution, [status(thm)], [d31,d39])).
% 100.35/27.20 cnf(d41, plain, sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d40,d12])).
% 100.35/27.20 cnf(d42, plain, sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)) | sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)) | ~element(sK64,powerset('the$ucarrier'(sK63))), inference(resolution, [status(thm)], [d41,d9])).
% 100.35/27.20 cnf(d43, plain, sK46(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)), inference(resolution, [status(thm)], [c81,d42])).
% 100.35/27.20 cnf(d44, plain, 'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(superposition, [status(thm)], [d43,c63])).
% 100.35/27.20 cnf(d45, plain, ~'Ts41'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d40,d44])).
% 100.35/27.20 cnf(d46, plain, ~element(sK64,powerset('the$ucarrier'(sK63))) | 'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d45,d8])).
% 100.35/27.20 cnf(d47, plain, 'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [c81,d46])).
% 100.35/27.20 cnf(d48, plain, sK67(sK63,sK64,sK66(sK44(sK63,sK64))) = sK66(sK44(sK63,sK64)), inference(resolution, [status(thm)], [d47,c88])).
% 100.35/27.20 cnf(d49, plain, 'closed$usubset'(sK66(sK44(sK63,sK64)),sK63) | ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(superposition, [status(thm)], [d48,c89])).
% 100.35/27.20 cnf(d50, plain, ~'Ts62'(sK63,sK64,sK66(sK44(sK63,sK64))), inference(resolution, [status(thm)], [d40,d49])).
% 100.35/27.20 cnf(d51, plain, $false, inference(resolution, [status(thm)], [d47,d50])).
% 100.35/27.20 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------