%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU310+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 : 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:37 AM UTC 2026
% Result : Theorem 15.99s 7.43s
% Output : CNFRefutation 15.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU310+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n002.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 09:12:57 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.99/7.43 % SZS status Theorem for theBenchmark.p
% 15.99/7.43 % SZS output start CNFRefutation for theBenchmark.p
% 15.99/7.43 fof(s1_tarski__e2_37_1_1__pre_topc__1, axiom, ! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset(powerset('the$ucarrier'(X0)))))) => (! [X2] : ! [X3] : ! [X4] : (((X2 = X3 & (in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X3),X1) & (X2 = X4 & in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X4),X1)))) => X3 = X4)) => ? [X2] : ! [X3] : ((in(X3,X2) <=> ? [X4] : ((in(X4,powerset('the$ucarrier'(X0))) & (X4 = X3 & in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X3),X1)))))))))).
% 15.99/7.43 fof(s1_xboole_0__e2_37_1_1__pre_topc__1, conjecture, ! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset(powerset('the$ucarrier'(X0)))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset('the$ucarrier'(X0))) & in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X3),X1))))))).
% 15.99/7.43 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('topological$uspace'(X0) & ('top$ustr'(X0) & element(X1,powerset(powerset('the$ucarrier'(X0)))))) => ? [X2] : ! [X3] : ((in(X3,X2) <=> (in(X3,powerset('the$ucarrier'(X0))) & in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X3),X1)))))), inference(negate_conjecture, [status(cth)], [s1_xboole_0__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c75, plain, ~'topological$uspace'(X0) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))) | ~'top$ustr'(X0) | in(sK57(X0,X1,X2),powerset('the$ucarrier'(X0))) | X3(X0,X1) | ~in(X2,sK55(X0,X1)), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c76, plain, ~'top$ustr'(X0) | ~'topological$uspace'(X0) | sK57(X0,X1,X2) = X2 | ~element(X1,powerset(powerset('the$ucarrier'(X0)))) | X3(X0,X1) | ~in(X2,sK55(X0,X1)), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c77, plain, ~'top$ustr'(X0) | ~'topological$uspace'(X0) | in('set$udifference'('cast$uas$ucarrier$usubset'(X0),X1),X2) | ~element(X2,powerset(powerset('the$ucarrier'(X0)))) | X3(X0,X2) | ~in(X1,sK55(X0,X2)), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c78, plain, in(X0,sK55(X1,X2)) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | X3(X1,X2) | ~in(X4,powerset('the$ucarrier'(X1))) | ~element(X2,powerset(powerset('the$ucarrier'(X1)))) | X4 != X0 | ~in('set$udifference'('cast$uas$ucarrier$usubset'(X1),X0),X2), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c79, plain, ~X0(X1,X2) | sK59(X1,X2) = sK60(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c81, plain, ~X0(X1,X2) | sK59(X1,X2) = sK61(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c83, plain, ~X0(X1,X2) | sK60(X1,X2) != sK61(X1,X2), inference(clausification, [status(esa)], [s1_tarski__e2_37_1_1__pre_topc__1])).
% 15.99/7.43 cnf(c84, plain, 'topological$uspace'(sK62), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(c85, plain, 'top$ustr'(sK62), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(c86, plain, element(sK63,powerset(powerset('the$ucarrier'(sK62)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(c88, plain, in(sK65(X0),X0) | in(sK65(X0),powerset('the$ucarrier'(sK62))), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(c89, plain, in(sK65(X0),X0) | in('set$udifference'('cast$uas$ucarrier$usubset'(sK62),sK65(X0)),sK63), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(c90, plain, ~in(sK65(X0),powerset('the$ucarrier'(sK62))) | ~in('set$udifference'('cast$uas$ucarrier$usubset'(sK62),sK65(X0)),sK63) | ~in(sK65(X0),X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.99/7.43 cnf(d0, plain, sK57(sK62,sK63,X0) = X0 | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(X0,sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c76,c86])).
% 15.99/7.43 cnf(d1, plain, sK57(sK62,sK63,X0) = X0 | ~'top$ustr'(sK62) | ~in(X0,sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d0])).
% 15.99/7.43 cnf(d2, plain, sK57(sK62,sK63,X0) = X0 | ~in(X0,sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d1])).
% 15.99/7.43 cnf(d3, plain, ~element(X0,powerset(powerset('the$ucarrier'(X1)))) | ~'topological$uspace'(X1) | ~'top$ustr'(X1) | in(X2,sK55(X1,X0)) | ~in(X2,powerset('the$ucarrier'(X1))) | ~in('set$udifference'('cast$uas$ucarrier$usubset'(X1),X2),X0) | 'Ts52'(X1,X0), inference(equality_resolution, [status(thm)], [c78])).
% 15.99/7.43 cnf(d4, plain, ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(sK65(X0),powerset('the$ucarrier'(sK62))) | in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63) | in(sK65(X0),X0), inference(resolution, [status(thm)], [d3,c89])).
% 15.99/7.43 cnf(d5, plain, ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'top$ustr'(sK62) | in(sK65(X0),X0) | ~in(sK65(X0),powerset('the$ucarrier'(sK62))) | in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d4])).
% 15.99/7.43 cnf(d6, plain, ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | in(sK65(X0),X0) | ~in(sK65(X0),powerset('the$ucarrier'(sK62))) | in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d5])).
% 15.99/7.43 cnf(d7, plain, in(sK65(X0),X0) | ~in(sK65(X0),powerset('the$ucarrier'(sK62))) | in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c86,d6])).
% 15.99/7.43 cnf(d8, plain, in(sK65(X0),X0) | in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63) | in(sK65(X0),X0), inference(resolution, [status(thm)], [d7,c88])).
% 15.99/7.43 cnf(d9, plain, in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(factoring, [status(thm)], [d8])).
% 15.99/7.43 cnf(d10, plain, 'Ts52'(sK62,sK63) | sK57(sK62,sK63,sK65(sK55(sK62,sK63))) = sK65(sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d9,d2])).
% 15.99/7.43 cnf(d11, plain, ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(X0,sK55(sK62,sK63)) | in('set$udifference'('cast$uas$ucarrier$usubset'(sK62),X0),sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c77,c86])).
% 15.99/7.43 cnf(d12, plain, ~'top$ustr'(sK62) | ~in(X0,sK55(sK62,sK63)) | in('set$udifference'('cast$uas$ucarrier$usubset'(sK62),X0),sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d11])).
% 15.99/7.43 cnf(d13, plain, ~in(X0,sK55(sK62,sK63)) | in('set$udifference'('cast$uas$ucarrier$usubset'(sK62),X0),sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d12])).
% 15.99/7.43 cnf(d14, plain, ~in(sK65(X0),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63) | ~in(sK65(X0),X0) | ~in(sK65(X0),powerset('the$ucarrier'(sK62))), inference(resolution, [status(thm)], [d13,c90])).
% 15.99/7.43 cnf(d15, plain, 'Ts52'(sK62,sK63) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | ~in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d9,d14])).
% 15.99/7.43 cnf(d16, plain, ~in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | 'Ts52'(sK62,sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d15,d9])).
% 15.99/7.43 cnf(d17, plain, sK57(sK62,sK63,sK65(sK55(sK62,sK63))) = sK65(sK55(sK62,sK63)) | sK59(sK62,sK63) = sK61(sK62,sK63), inference(resolution, [status(thm)], [d10,c81])).
% 15.99/7.43 cnf(d18, plain, in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63) | sK59(sK62,sK63) = sK61(sK62,sK63), inference(superposition, [status(thm)], [d17,c75])).
% 15.99/7.43 cnf(d19, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'top$ustr'(sK62) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d18])).
% 15.99/7.43 cnf(d20, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d19])).
% 15.99/7.43 cnf(d21, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c86,d20])).
% 15.99/7.43 cnf(d22, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | 'Ts52'(sK62,sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d21,d9])).
% 15.99/7.43 cnf(d23, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | 'Ts52'(sK62,sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d22,d16])).
% 15.99/7.43 cnf(d24, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | sK59(sK62,sK63) = sK61(sK62,sK63), inference(resolution, [status(thm)], [d23,c81])).
% 15.99/7.43 cnf(d25, plain, sK59(sK62,sK63) = sK61(sK62,sK63) | sK59(sK62,sK63) = sK60(sK62,sK63), inference(resolution, [status(thm)], [d23,c79])).
% 15.99/7.43 cnf(d26, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | sK59(sK62,sK63) = sK61(sK62,sK63), inference(demodulation, [status(thm)], [d25,d24])).
% 15.99/7.43 cnf(d27, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | sK61(sK62,sK63) = sK61(sK62,sK63), inference(demodulation, [status(thm)], [d26,d24])).
% 15.99/7.43 cnf(d28, plain, sK57(sK62,sK63,sK65(sK55(sK62,sK63))) = sK65(sK55(sK62,sK63)) | sK59(sK62,sK63) = sK60(sK62,sK63), inference(resolution, [status(thm)], [d10,c79])).
% 15.99/7.43 cnf(d29, plain, in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63) | sK59(sK62,sK63) = sK60(sK62,sK63), inference(superposition, [status(thm)], [d28,c75])).
% 15.99/7.43 cnf(d30, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(demodulation, [status(thm)], [d29,d24])).
% 15.99/7.43 cnf(d31, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'top$ustr'(sK62) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d30])).
% 15.99/7.43 cnf(d32, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d31])).
% 15.99/7.43 cnf(d33, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c86,d32])).
% 15.99/7.43 cnf(d34, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | 'Ts52'(sK62,sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d33,d9])).
% 15.99/7.43 cnf(d35, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | 'Ts52'(sK62,sK63) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [d34,d16])).
% 15.99/7.43 cnf(d36, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | sK59(sK62,sK63) = sK60(sK62,sK63), inference(resolution, [status(thm)], [d35,c79])).
% 15.99/7.43 cnf(d37, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | sK61(sK62,sK63) = sK60(sK62,sK63), inference(demodulation, [status(thm)], [d36,d24])).
% 15.99/7.43 cnf(d38, plain, sK61(sK62,sK63) = sK60(sK62,sK63) | sK61(sK62,sK63) = sK60(sK62,sK63) | sK61(sK62,sK63) = sK60(sK62,sK63), inference(superposition, [status(thm)], [d37,d27])).
% 15.99/7.43 cnf(d39, plain, sK60(sK62,sK63) != sK60(sK62,sK63) | ~'Ts52'(sK62,sK63), inference(superposition, [status(thm)], [d38,c83])).
% 15.99/7.43 cnf(d40, plain, ~'Ts52'(sK62,sK63), inference(equality_resolution, [status(thm)], [d39])).
% 15.99/7.43 cnf(d41, plain, sK57(sK62,sK63,sK65(sK55(sK62,sK63))) = sK65(sK55(sK62,sK63)), inference(resolution, [status(thm)], [d40,d10])).
% 15.99/7.43 cnf(d42, plain, in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'topological$uspace'(sK62) | ~'top$ustr'(sK62) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(superposition, [status(thm)], [d41,c75])).
% 15.99/7.43 cnf(d43, plain, ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | ~'top$ustr'(sK62) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c84,d42])).
% 15.99/7.43 cnf(d44, plain, ~element(sK63,powerset(powerset('the$ucarrier'(sK62)))) | in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c85,d43])).
% 15.99/7.43 cnf(d45, plain, in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)) | 'Ts52'(sK62,sK63), inference(resolution, [status(thm)], [c86,d44])).
% 15.99/7.43 cnf(d46, plain, in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))) | ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)), inference(resolution, [status(thm)], [d40,d45])).
% 15.99/7.43 cnf(d47, plain, ~in(sK65(sK55(sK62,sK63)),powerset('the$ucarrier'(sK62))), inference(resolution, [status(thm)], [d40,d16])).
% 15.99/7.43 cnf(d48, plain, ~in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)), inference(resolution, [status(thm)], [d47,d46])).
% 15.99/7.43 cnf(d49, plain, in(sK65(sK55(sK62,sK63)),sK55(sK62,sK63)), inference(resolution, [status(thm)], [d40,d9])).
% 15.99/7.43 cnf(d50, plain, $false, inference(resolution, [status(thm)], [d49,d48])).
% 15.99/7.43 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------