%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU361+2 : 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 : 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:46 AM UTC 2026
% Result : Theorem 102.61s 17.84s
% Output : CNFRefutation 102.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU361+2 : 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.08/0.56 % Computer : n006.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.56 % CPULimit : 300
% 0.08/0.56 % WCLimit : 300
% 0.08/0.56 % DateTime : Sat Sep 26 09:18:59 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.57 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 102.61/17.84 % SZS status Theorem for theBenchmark.p
% 102.61/17.84 % SZS output start CNFRefutation for theBenchmark.p
% 102.61/17.84 fof(d11_yellow_0, axiom, ! [X0] : (('rel$ustr'(X0) => 'bottom$uof$urelstr'(X0) = 'join$uon$urelstr'(X0,'empty$uset')))).
% 102.61/17.84 fof(d9_yellow_0, axiom, ! [X0] : (('rel$ustr'(X0) => ! [X1] : ! [X2] : ((element(X2,'the$ucarrier'(X0)) => ('ex$usup$uof$urelstr$uset'(X0,X1) => (X2 = 'join$uon$urelstr'(X0,X1) <=> ('relstr$uset$usmaller'(X0,X1,X2) & ! [X3] : ((element(X3,'the$ucarrier'(X0)) => ('relstr$uset$usmaller'(X0,X1,X3) => related(X0,X2,X3)))))))))))).
% 102.61/17.84 fof(dt_k1_yellow_0, axiom, ! [X0] : ! [X1] : (('rel$ustr'(X0) => element('join$uon$urelstr'(X0,X1),'the$ucarrier'(X0))))).
% 102.61/17.84 fof(t42_yellow_0, lemma, ! [X0] : (((~'empty$ucarrier'(X0) & ('antisymmetric$urelstr'(X0) & ('lower$ubounded$urelstr'(X0) & 'rel$ustr'(X0)))) => ('ex$usup$uof$urelstr$uset'(X0,'empty$uset') & 'ex$uinf$uof$urelstr$uset'(X0,'the$ucarrier'(X0)))))).
% 102.61/17.84 fof(t6_yellow_0, lemma, ! [X0] : (('rel$ustr'(X0) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => ('relstr$uset$usmaller'(X0,'empty$uset',X1) & 'relstr$uelement$usmaller'(X0,'empty$uset',X1))))))).
% 102.61/17.84 fof(t44_yellow_0, conjecture, ! [X0] : (((~'empty$ucarrier'(X0) & ('antisymmetric$urelstr'(X0) & ('lower$ubounded$urelstr'(X0) & 'rel$ustr'(X0)))) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => related(X0,'bottom$uof$urelstr'(X0),X1)))))).
% 102.61/17.84 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'empty$ucarrier'(X0) & ('antisymmetric$urelstr'(X0) & ('lower$ubounded$urelstr'(X0) & 'rel$ustr'(X0)))) => ! [X1] : ((element(X1,'the$ucarrier'(X0)) => related(X0,'bottom$uof$urelstr'(X0),X1))))), inference(negate_conjecture, [status(cth)], [t44_yellow_0])).
% 102.61/17.84 cnf(c144, plain, ~'rel$ustr'(X0) | 'join$uon$urelstr'(X0,'empty$uset') = 'bottom$uof$urelstr'(X0), inference(clausification, [status(esa)], [d11_yellow_0])).
% 102.61/17.84 cnf(c666, plain, ~'rel$ustr'(X0) | ~element(X1,'the$ucarrier'(X0)) | X2(X0,X3,X1) | ~'ex$usup$uof$urelstr$uset'(X0,X3), inference(clausification, [status(esa)], [d9_yellow_0])).
% 102.61/17.84 cnf(c668, plain, ~X0(X1,X2,X3) | ~'relstr$uset$usmaller'(X1,X2,X4) | 'join$uon$urelstr'(X1,X2) != X3 | related(X1,X3,X4) | ~element(X4,'the$ucarrier'(X1)), inference(clausification, [status(esa)], [d9_yellow_0])).
% 102.61/17.84 cnf(c687, plain, ~'rel$ustr'(X0) | element('join$uon$urelstr'(X0,X1),'the$ucarrier'(X0)), inference(clausification, [status(esa)], [dt_k1_yellow_0])).
% 102.61/17.84 cnf(c1905, plain, ~'antisymmetric$urelstr'(X0) | ~'rel$ustr'(X0) | 'ex$usup$uof$urelstr$uset'(X0,'empty$uset') | 'empty$ucarrier'(X0) | ~'lower$ubounded$urelstr'(X0), inference(clausification, [status(esa)], [t42_yellow_0])).
% 102.61/17.84 cnf(c2009, plain, ~'rel$ustr'(X0) | ~element(X1,'the$ucarrier'(X0)) | 'relstr$uset$usmaller'(X0,'empty$uset',X1), inference(clausification, [status(esa)], [t6_yellow_0])).
% 102.61/17.84 cnf(c2059, plain, 'antisymmetric$urelstr'(sK2215), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(c2060, plain, 'rel$ustr'(sK2215), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(c2061, plain, 'lower$ubounded$urelstr'(sK2215), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(c2062, plain, ~'empty$ucarrier'(sK2215), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(c2063, plain, element(sK2216,'the$ucarrier'(sK2215)), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(c2064, plain, ~related(sK2215,'bottom$uof$urelstr'(sK2215),sK2216), inference(clausification, [status(esa)], [negated_conjecture])).
% 102.61/17.84 cnf(d0, plain, 'join$uon$urelstr'(sK2215,'empty$uset') = 'bottom$uof$urelstr'(sK2215), inference(resolution, [status(thm)], [c144,c2060])).
% 102.61/17.84 cnf(d1, plain, 'bottom$uof$urelstr'(sK2215) != X0 | ~element(X1,'the$ucarrier'(sK2215)) | related(sK2215,X0,X1) | ~'relstr$uset$usmaller'(sK2215,'empty$uset',X1) | ~'Ts625'(sK2215,'empty$uset',X0), inference(superposition, [status(thm)], [d0,c668])).
% 102.61/17.84 cnf(d2, plain, ~element(X0,'the$ucarrier'(sK2215)) | related(sK2215,'bottom$uof$urelstr'(sK2215),X0) | ~'relstr$uset$usmaller'(sK2215,'empty$uset',X0) | ~'Ts625'(sK2215,'empty$uset','bottom$uof$urelstr'(sK2215)), inference(equality_resolution, [status(thm)], [d1])).
% 102.61/17.84 cnf(d3, plain, element('bottom$uof$urelstr'(sK2215),'the$ucarrier'(sK2215)) | ~'rel$ustr'(sK2215), inference(superposition, [status(thm)], [d0,c687])).
% 102.61/17.84 cnf(d4, plain, element('bottom$uof$urelstr'(sK2215),'the$ucarrier'(sK2215)), inference(resolution, [status(thm)], [c2060,d3])).
% 102.61/17.84 cnf(d5, plain, ~'rel$ustr'(sK2215) | ~'ex$usup$uof$urelstr$uset'(sK2215,X0) | 'Ts625'(sK2215,X0,'bottom$uof$urelstr'(sK2215)), inference(resolution, [status(thm)], [d4,c666])).
% 102.61/17.84 cnf(d6, plain, ~'ex$usup$uof$urelstr$uset'(sK2215,X0) | 'Ts625'(sK2215,X0,'bottom$uof$urelstr'(sK2215)), inference(resolution, [status(thm)], [c2060,d5])).
% 102.61/17.84 cnf(d7, plain, ~'ex$usup$uof$urelstr$uset'(sK2215,'empty$uset') | ~element(X0,'the$ucarrier'(sK2215)) | related(sK2215,'bottom$uof$urelstr'(sK2215),X0) | ~'relstr$uset$usmaller'(sK2215,'empty$uset',X0), inference(resolution, [status(thm)], [d6,d2])).
% 102.61/17.84 cnf(d8, plain, ~element(sK2216,'the$ucarrier'(sK2215)) | ~'ex$usup$uof$urelstr$uset'(sK2215,'empty$uset') | ~'relstr$uset$usmaller'(sK2215,'empty$uset',sK2216), inference(resolution, [status(thm)], [d7,c2064])).
% 102.61/17.84 cnf(d9, plain, ~'ex$usup$uof$urelstr$uset'(sK2215,'empty$uset') | ~'relstr$uset$usmaller'(sK2215,'empty$uset',sK2216), inference(resolution, [status(thm)], [c2063,d8])).
% 102.61/17.84 cnf(d10, plain, ~'rel$ustr'(sK2215) | 'relstr$uset$usmaller'(sK2215,'empty$uset',sK2216), inference(resolution, [status(thm)], [c2009,c2063])).
% 102.61/17.84 cnf(d11, plain, 'relstr$uset$usmaller'(sK2215,'empty$uset',sK2216), inference(resolution, [status(thm)], [c2060,d10])).
% 102.61/17.84 cnf(d12, plain, ~'ex$usup$uof$urelstr$uset'(sK2215,'empty$uset'), inference(resolution, [status(thm)], [d11,d9])).
% 102.61/17.84 cnf(d13, plain, ~'rel$ustr'(sK2215) | 'empty$ucarrier'(sK2215) | ~'lower$ubounded$urelstr'(sK2215) | ~'antisymmetric$urelstr'(sK2215), inference(resolution, [status(thm)], [d12,c1905])).
% 102.61/17.84 cnf(d14, plain, ~'rel$ustr'(sK2215) | 'empty$ucarrier'(sK2215) | ~'lower$ubounded$urelstr'(sK2215), inference(resolution, [status(thm)], [c2059,d13])).
% 102.61/17.84 cnf(d15, plain, 'empty$ucarrier'(sK2215) | ~'lower$ubounded$urelstr'(sK2215), inference(resolution, [status(thm)], [c2060,d14])).
% 102.61/17.84 cnf(d16, plain, 'empty$ucarrier'(sK2215), inference(resolution, [status(thm)], [c2061,d15])).
% 102.61/17.84 cnf(d17, plain, $false, inference(resolution, [status(thm)], [c2062,d16])).
% 102.61/17.84 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------