%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU318+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 : n016.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:39 AM UTC 2026
% Result : Theorem 53.31s 10.40s
% Output : CNFRefutation 53.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU318+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.38 % Computer : n016.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 26 09:16:01 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.31/10.40 % SZS status Theorem for theBenchmark.p
% 53.31/10.40 % SZS output start CNFRefutation for theBenchmark.p
% 53.31/10.40 fof(d10_xboole_0, axiom, ! [X0] : ! [X1] : ((X0 = X1 <=> (subset(X0,X1) & subset(X1,X0))))).
% 53.31/10.40 fof(d3_tarski, axiom, ! [X0] : ! [X1] : ((subset(X0,X1) <=> ! [X2] : ((in(X2,X0) => in(X2,X1)))))).
% 53.31/10.40 fof(dt_k6_pre_topc, axiom, ! [X0] : ! [X1] : ((('top$ustr'(X0) & element(X1,powerset('the$ucarrier'(X0)))) => element('topstr$uclosure'(X0,X1),powerset('the$ucarrier'(X0)))))).
% 53.31/10.40 fof(reflexivity_r1_tarski, axiom, ! [X0] : ! [X1] : subset(X0,X0)).
% 53.31/10.40 fof(t3_subset, axiom, ! [X0] : ! [X1] : ((element(X0,powerset(X1)) <=> subset(X0,X1)))).
% 53.31/10.40 fof(t44_pre_topc, axiom, ! [X0] : ((('topological$uspace'(X0) & 'top$ustr'(X0)) => ! [X1] : ((element(X1,powerset(powerset('the$ucarrier'(X0)))) => (! [X2] : ((element(X2,powerset('the$ucarrier'(X0))) => (in(X2,X1) => 'closed$usubset'(X2,X0)))) => 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),X1),X0))))))).
% 53.31/10.40 fof(t45_pre_topc, axiom, ! [X0] : (('top$ustr'(X0) => ! [X1] : ((element(X1,powerset('the$ucarrier'(X0))) => ! [X2] : ((in(X2,'the$ucarrier'(X0)) => (in(X2,'topstr$uclosure'(X0,X1)) <=> ! [X3] : ((element(X3,powerset('the$ucarrier'(X0))) => (('closed$usubset'(X3,X0) & subset(X1,X3)) => in(X2,X3)))))))))))).
% 53.31/10.40 fof(t46_pre_topc, axiom, ! [X0] : ((('topological$uspace'(X0) & 'top$ustr'(X0)) => ! [X1] : ((element(X1,powerset('the$ucarrier'(X0))) => ? [X2] : ((element(X2,powerset(powerset('the$ucarrier'(X0)))) & (! [X3] : ((element(X3,powerset('the$ucarrier'(X0))) => (in(X3,X2) <=> ('closed$usubset'(X3,X0) & subset(X1,X3))))) & 'topstr$uclosure'(X0,X1) = 'meet$uof$usubsets'('the$ucarrier'(X0),X2))))))))).
% 53.31/10.40 fof(t48_pre_topc, axiom, ! [X0] : (('top$ustr'(X0) => ! [X1] : ((element(X1,powerset('the$ucarrier'(X0))) => subset(X1,'topstr$uclosure'(X0,X1))))))).
% 53.31/10.40 fof(t52_pre_topc, conjecture, ! [X0] : (('top$ustr'(X0) => ! [X1] : ((element(X1,powerset('the$ucarrier'(X0))) => (('closed$usubset'(X1,X0) => 'topstr$uclosure'(X0,X1) = X1) & (('topological$uspace'(X0) & 'topstr$uclosure'(X0,X1) = X1) => 'closed$usubset'(X1,X0)))))))).
% 53.31/10.40 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('top$ustr'(X0) => ! [X1] : ((element(X1,powerset('the$ucarrier'(X0))) => (('closed$usubset'(X1,X0) => 'topstr$uclosure'(X0,X1) = X1) & (('topological$uspace'(X0) & 'topstr$uclosure'(X0,X1) = X1) => 'closed$usubset'(X1,X0))))))), inference(negate_conjecture, [status(cth)], [t52_pre_topc])).
% 53.31/10.40 cnf(c45, plain, X0 = X1 | ~subset(X0,X1) | ~subset(X1,X0), inference(clausification, [status(esa)], [d10_xboole_0])).
% 53.31/10.40 cnf(c46, plain, ~subset(X0,X1) | ~in(X2,X0) | in(X2,X1), inference(clausification, [status(esa)], [d3_tarski])).
% 53.31/10.40 cnf(c47, plain, subset(X0,X1) | in(sK35(X0,X1),X0), inference(clausification, [status(esa)], [d3_tarski])).
% 53.31/10.40 cnf(c48, plain, subset(X0,X1) | ~in(sK35(X0,X1),X1), inference(clausification, [status(esa)], [d3_tarski])).
% 53.31/10.40 cnf(c49, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~'top$ustr'(X1) | element('topstr$uclosure'(X1,X0),powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [dt_k6_pre_topc])).
% 53.31/10.40 cnf(c75, plain, subset(X0,X0), inference(clausification, [status(esa)], [reflexivity_r1_tarski])).
% 53.31/10.40 cnf(c78, plain, ~element(X0,powerset(X1)) | subset(X0,X1), inference(clausification, [status(esa)], [t3_subset])).
% 53.31/10.40 cnf(c80, plain, ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),X1),X0) | element(sK65(X0,X1),powerset('the$ucarrier'(X0))) | ~'top$ustr'(X0) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))), inference(clausification, [status(esa)], [t44_pre_topc])).
% 53.31/10.40 cnf(c81, plain, ~'closed$usubset'(sK65(X0,X1),X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),X1),X0) | ~'top$ustr'(X0) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))), inference(clausification, [status(esa)], [t44_pre_topc])).
% 53.31/10.40 cnf(c82, plain, ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),X1),X0) | ~'top$ustr'(X0) | in(sK65(X0,X1),X1) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))), inference(clausification, [status(esa)], [t44_pre_topc])).
% 53.31/10.40 cnf(c83, plain, ~'top$ustr'(X0) | ~element(X1,powerset('the$ucarrier'(X0))) | ~in(X2,'the$ucarrier'(X0)) | X3(X0,X1,X2), inference(clausification, [status(esa)], [t45_pre_topc])).
% 53.31/10.40 cnf(c84, plain, ~subset(X0,X1) | ~'closed$usubset'(X1,X2) | ~X3(X2,X0,X4) | ~in(X4,'topstr$uclosure'(X2,X0)) | ~element(X1,powerset('the$ucarrier'(X2))) | in(X4,X1), inference(clausification, [status(esa)], [t45_pre_topc])).
% 53.31/10.40 cnf(c89, plain, ~'top$ustr'(X0) | ~'topological$uspace'(X0) | ~element(X1,powerset('the$ucarrier'(X0))) | X2(X0,X1), inference(clausification, [status(esa)], [t46_pre_topc])).
% 53.31/10.40 cnf(c90, plain, ~X0(X1,X2) | element(sK75(X1,X2),powerset(powerset('the$ucarrier'(X1)))), inference(clausification, [status(esa)], [t46_pre_topc])).
% 53.31/10.40 cnf(c91, plain, ~X0(X1,X2) | 'meet$uof$usubsets'('the$ucarrier'(X1),sK75(X1,X2)) = 'topstr$uclosure'(X1,X2), inference(clausification, [status(esa)], [t46_pre_topc])).
% 53.31/10.40 cnf(c92, plain, ~X0(X1,X2) | ~element(X3,powerset('the$ucarrier'(X1))) | ~in(X3,sK75(X1,X2)) | 'closed$usubset'(X3,X1), inference(clausification, [status(esa)], [t46_pre_topc])).
% 53.31/10.40 cnf(c95, plain, ~'top$ustr'(X0) | ~element(X1,powerset('the$ucarrier'(X0))) | subset(X1,'topstr$uclosure'(X0,X1)), inference(clausification, [status(esa)], [t48_pre_topc])).
% 53.31/10.40 cnf(c101, plain, 'top$ustr'(sK91), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c102, plain, element(sK92,powerset('the$ucarrier'(sK91))), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c103, plain, 'closed$usubset'(sK92,sK91) | X0(sK91,sK92), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c104, plain, 'topstr$uclosure'(sK91,sK92) != sK92 | X0(sK91,sK92), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c105, plain, ~X0(X1,X2) | 'topstr$uclosure'(X1,X2) = X2, inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c106, plain, ~X0(X1,X2) | 'topological$uspace'(X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(c107, plain, ~X0(X1,X2) | ~'closed$usubset'(X2,X1), inference(clausification, [status(esa)], [negated_conjecture])).
% 53.31/10.40 cnf(d0, plain, ~'Ts72'(X0,X1) | in(sK65(X0,sK75(X0,X1)),sK75(X0,X1)) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),sK75(X0,X1)),X0), inference(resolution, [status(thm)], [c90,c82])).
% 53.31/10.40 cnf(d1, plain, ~in(sK65(X0,X1),sK75(X0,X2)) | 'closed$usubset'(sK65(X0,X1),X0) | ~'Ts72'(X0,X2) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),X1),X0), inference(resolution, [status(thm)], [c92,c80])).
% 53.31/10.40 cnf(d2, plain, ~element(X0,powerset(powerset('the$ucarrier'(X1)))) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X1),X0),X1) | ~in(sK65(X1,X0),sK75(X1,X2)) | ~element(X0,powerset(powerset('the$ucarrier'(X1)))) | ~'top$ustr'(X1) | ~'topological$uspace'(X1) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X1),X0),X1) | ~'Ts72'(X1,X2), inference(resolution, [status(thm)], [c81,d1])).
% 53.31/10.40 cnf(d3, plain, ~element(sK75(X0,X1),powerset(powerset('the$ucarrier'(X0)))) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),sK75(X0,X1)),X0) | ~'Ts72'(X0,X1) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),sK75(X0,X1)),X0) | ~'Ts72'(X0,X1), inference(resolution, [status(thm)], [d2,d0])).
% 53.31/10.40 cnf(d4, plain, ~'Ts72'(X0,X1) | ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'closed$usubset'('meet$uof$usubsets'('the$ucarrier'(X0),sK75(X0,X1)),X0) | ~'Ts72'(X0,X1), inference(resolution, [status(thm)], [c90,d3])).
% 53.31/10.40 cnf(d5, plain, subset(sK92,'topstr$uclosure'(sK91,sK92)) | ~'top$ustr'(sK91), inference(resolution, [status(thm)], [c95,c102])).
% 53.31/10.40 cnf(d6, plain, subset(sK92,'topstr$uclosure'(sK91,sK92)), inference(resolution, [status(thm)], [c101,d5])).
% 53.31/10.40 cnf(d7, plain, sK92 = 'topstr$uclosure'(sK91,sK92) | ~subset('topstr$uclosure'(sK91,sK92),sK92), inference(resolution, [status(thm)], [d6,c45])).
% 53.31/10.40 cnf(d8, plain, 'topstr$uclosure'(sK91,sK92) = sK92 | 'closed$usubset'(sK92,sK91), inference(resolution, [status(thm)], [c105,c103])).
% 53.31/10.40 cnf(d9, plain, in(X0,sK92) | ~in(X0,'topstr$uclosure'(sK91,X1)) | ~subset(X1,sK92) | ~'closed$usubset'(sK92,sK91) | ~'Ts66'(sK91,X1,X0), inference(resolution, [status(thm)], [c84,c102])).
% 53.31/10.40 cnf(d10, plain, in(sK35('topstr$uclosure'(sK91,X0),X1),sK92) | ~subset(X0,sK92) | ~'closed$usubset'(sK92,sK91) | ~'Ts66'(sK91,X0,sK35('topstr$uclosure'(sK91,X0),X1)) | subset('topstr$uclosure'(sK91,X0),X1), inference(resolution, [status(thm)], [d9,c47])).
% 53.31/10.40 cnf(d11, plain, ~in(X0,'the$ucarrier'(sK91)) | ~'top$ustr'(sK91) | 'Ts66'(sK91,sK92,X0), inference(resolution, [status(thm)], [c83,c102])).
% 53.31/10.40 cnf(d12, plain, ~in(X0,'the$ucarrier'(sK91)) | 'Ts66'(sK91,sK92,X0), inference(resolution, [status(thm)], [c101,d11])).
% 53.31/10.40 cnf(d13, plain, subset('topstr$uclosure'(X0,X1),'the$ucarrier'(X0)) | ~element(X1,powerset('the$ucarrier'(X0))) | ~'top$ustr'(X0), inference(resolution, [status(thm)], [c78,c49])).
% 53.31/10.40 cnf(d14, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~'top$ustr'(X1) | in(X2,'the$ucarrier'(X1)) | ~in(X2,'topstr$uclosure'(X1,X0)), inference(resolution, [status(thm)], [d13,c46])).
% 53.31/10.40 cnf(d15, plain, in(X0,'the$ucarrier'(sK91)) | ~in(X0,'topstr$uclosure'(sK91,sK92)) | ~'top$ustr'(sK91), inference(resolution, [status(thm)], [d14,c102])).
% 53.31/10.40 cnf(d16, plain, in(X0,'the$ucarrier'(sK91)) | ~in(X0,'topstr$uclosure'(sK91,sK92)), inference(resolution, [status(thm)], [c101,d15])).
% 53.31/10.40 cnf(d17, plain, in(sK35('topstr$uclosure'(sK91,sK92),X0),'the$ucarrier'(sK91)) | subset('topstr$uclosure'(sK91,sK92),X0), inference(resolution, [status(thm)], [d16,c47])).
% 53.31/10.40 cnf(d18, plain, subset('topstr$uclosure'(sK91,sK92),X0) | 'Ts66'(sK91,sK92,sK35('topstr$uclosure'(sK91,sK92),X0)), inference(resolution, [status(thm)], [d17,d12])).
% 53.31/10.40 cnf(d19, plain, subset('topstr$uclosure'(sK91,sK92),X0) | in(sK35('topstr$uclosure'(sK91,sK92),X0),sK92) | ~subset(sK92,sK92) | subset('topstr$uclosure'(sK91,sK92),X0) | ~'closed$usubset'(sK92,sK91), inference(resolution, [status(thm)], [d18,d10])).
% 53.31/10.40 cnf(d20, plain, in(sK35('topstr$uclosure'(sK91,sK92),X0),sK92) | subset('topstr$uclosure'(sK91,sK92),X0) | ~'closed$usubset'(sK92,sK91), inference(resolution, [status(thm)], [c75,d19])).
% 53.31/10.40 cnf(d21, plain, subset('topstr$uclosure'(sK91,sK92),sK92) | ~'closed$usubset'(sK92,sK91) | subset('topstr$uclosure'(sK91,sK92),sK92), inference(resolution, [status(thm)], [d20,c48])).
% 53.31/10.40 cnf(d22, plain, ~'closed$usubset'(sK92,sK91) | sK92 = 'topstr$uclosure'(sK91,sK92), inference(resolution, [status(thm)], [d21,d7])).
% 53.31/10.40 cnf(d23, plain, sK92 = 'topstr$uclosure'(sK91,sK92) | 'topstr$uclosure'(sK91,sK92) = sK92, inference(resolution, [status(thm)], [d22,d8])).
% 53.31/10.40 cnf(d24, plain, ~subset(sK92,sK92) | sK92 = 'topstr$uclosure'(sK91,sK92) | sK92 = 'topstr$uclosure'(sK91,sK92), inference(superposition, [status(thm)], [d23,d7])).
% 53.31/10.40 cnf(d25, plain, sK92 = 'topstr$uclosure'(sK91,sK92), inference(resolution, [status(thm)], [c75,d24])).
% 53.31/10.40 cnf(d26, plain, ~'top$ustr'(sK91) | ~'topological$uspace'(sK91) | 'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [c89,c102])).
% 53.31/10.40 cnf(d27, plain, ~'topological$uspace'(sK91) | 'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [c101,d26])).
% 53.31/10.40 cnf(d28, plain, 'meet$uof$usubsets'('the$ucarrier'(sK91),sK75(sK91,sK92)) = 'topstr$uclosure'(sK91,sK92) | ~'topological$uspace'(sK91), inference(resolution, [status(thm)], [c91,d27])).
% 53.31/10.40 cnf(d29, plain, 'meet$uof$usubsets'('the$ucarrier'(sK91),sK75(sK91,sK92)) = sK92 | ~'topological$uspace'(sK91), inference(demodulation, [status(thm)], [d28,d25])).
% 53.31/10.40 cnf(d30, plain, sK92 != sK92 | 'Ts90'(sK91,sK92), inference(demodulation, [status(thm)], [c104,d25])).
% 53.31/10.40 cnf(d31, plain, 'Ts90'(sK91,sK92), inference(equality_resolution, [status(thm)], [d30])).
% 53.31/10.40 cnf(d32, plain, 'topological$uspace'(sK91), inference(resolution, [status(thm)], [d31,c106])).
% 53.31/10.40 cnf(d33, plain, 'meet$uof$usubsets'('the$ucarrier'(sK91),sK75(sK91,sK92)) = sK92, inference(resolution, [status(thm)], [d32,d29])).
% 53.31/10.40 cnf(d34, plain, 'closed$usubset'(sK92,sK91) | ~'top$ustr'(sK91) | ~'topological$uspace'(sK91) | ~'Ts72'(sK91,sK92), inference(superposition, [status(thm)], [d33,d4])).
% 53.31/10.40 cnf(d35, plain, ~'topological$uspace'(sK91) | 'closed$usubset'(sK92,sK91) | ~'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [c101,d34])).
% 53.31/10.40 cnf(d36, plain, 'closed$usubset'(sK92,sK91) | ~'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [d32,d35])).
% 53.31/10.40 cnf(d37, plain, ~'closed$usubset'(sK92,sK91), inference(resolution, [status(thm)], [d31,c107])).
% 53.31/10.40 cnf(d38, plain, ~'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [d37,d36])).
% 53.31/10.40 cnf(d39, plain, 'Ts72'(sK91,sK92), inference(resolution, [status(thm)], [d32,d27])).
% 53.31/10.40 cnf(d40, plain, $false, inference(resolution, [status(thm)], [d39,d38])).
% 53.31/10.40 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------