%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU325+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 : 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:40 AM UTC 2026
% Result : Theorem 36.79s 5.77s
% Output : CNFRefutation 36.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU325+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 09:15:21 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 36.79/5.77 % SZS status Theorem for theBenchmark.p
% 36.79/5.77 % SZS output start CNFRefutation for theBenchmark.p
% 36.79/5.77 fof(d1_struct_0, axiom, ! [X0] : (('one$usorted$ustr'(X0) => ('empty$ucarrier'(X0) <=> empty('the$ucarrier'(X0)))))).
% 36.79/5.77 fof(d1_xboole_0, axiom, ! [X0] : ((X0 = 'empty$uset' <=> ! [X1] : ~in(X1,X0)))).
% 36.79/5.77 fof(d3_pre_topc, axiom, ! [X0] : (('one$usorted$ustr'(X0) => 'cast$uas$ucarrier$usubset'(X0) = 'the$ucarrier'(X0)))).
% 36.79/5.77 fof(d4_tarski, axiom, ! [X0] : ! [X1] : ((X1 = union(X0) <=> ! [X2] : ((in(X2,X1) <=> ? [X3] : ((in(X2,X3) & in(X3,X0)))))))).
% 36.79/5.77 fof(d8_pre_topc, axiom, ! [X0] : (('one$usorted$ustr'(X0) => ! [X1] : ((element(X1,powerset(powerset('the$ucarrier'(X0)))) => ('is$ua$ucover$uof$ucarrier'(X0,X1) <=> 'cast$uas$ucarrier$usubset'(X0) = 'union$uof$usubsets'('the$ucarrier'(X0),X1))))))).
% 36.79/5.77 fof(fc12_relat_1, axiom, (empty('empty$uset') & (relation('empty$uset') & 'relation$uempty$uyielding'('empty$uset')))).
% 36.79/5.77 fof(redefinition_k5_setfam_1, axiom, ! [X0] : ! [X1] : ((element(X1,powerset(powerset(X0))) => 'union$uof$usubsets'(X0,X1) = union(X1)))).
% 36.79/5.77 fof(t5_tops_2, conjecture, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : ((element(X1,powerset(powerset('the$ucarrier'(X0)))) => ~(('is$ua$ucover$uof$ucarrier'(X0,X1) & X1 = 'empty$uset'))))))).
% 36.79/5.77 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : ((element(X1,powerset(powerset('the$ucarrier'(X0)))) => ~(('is$ua$ucover$uof$ucarrier'(X0,X1) & X1 = 'empty$uset')))))), inference(negate_conjecture, [status(cth)], [t5_tops_2])).
% 36.79/5.77 cnf(c255, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~empty('the$ucarrier'(X0)), inference(clausification, [status(esa)], [d1_struct_0])).
% 36.79/5.77 cnf(c285, plain, X0 != 'empty$uset' | ~in(X1,X0), inference(clausification, [status(esa)], [d1_xboole_0])).
% 36.79/5.77 cnf(c286, plain, X0 = 'empty$uset' | in(sK228(X0),X0), inference(clausification, [status(esa)], [d1_xboole_0])).
% 36.79/5.77 cnf(c364, plain, ~'one$usorted$ustr'(X0) | 'cast$uas$ucarrier$usubset'(X0) = 'the$ucarrier'(X0), inference(clausification, [status(esa)], [d3_pre_topc])).
% 36.79/5.77 cnf(c411, plain, X0 != union(X1) | X2(X1,X0), inference(clausification, [status(esa)], [d4_tarski])).
% 36.79/5.77 cnf(c414, plain, ~X0(X1,X2) | ~in(X3,X2) | in(sK345(X1,X3),X1), inference(clausification, [status(esa)], [d4_tarski])).
% 36.79/5.77 cnf(c538, plain, ~'one$usorted$ustr'(X0) | ~element(X1,powerset(powerset('the$ucarrier'(X0)))) | ~'is$ua$ucover$uof$ucarrier'(X0,X1) | 'cast$uas$ucarrier$usubset'(X0) = 'union$uof$usubsets'('the$ucarrier'(X0),X1), inference(clausification, [status(esa)], [d8_pre_topc])).
% 36.79/5.77 cnf(c630, plain, empty('empty$uset'), inference(clausification, [status(esa)], [fc12_relat_1])).
% 36.79/5.77 cnf(c915, plain, ~element(X0,powerset(powerset(X1))) | 'union$uof$usubsets'(X1,X0) = union(X0), inference(clausification, [status(esa)], [redefinition_k5_setfam_1])).
% 36.79/5.77 cnf(c1613, plain, ~'empty$ucarrier'(sK1653), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.79/5.77 cnf(c1614, plain, 'one$usorted$ustr'(sK1653), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.79/5.77 cnf(c1615, plain, element(sK1654,powerset(powerset('the$ucarrier'(sK1653)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.79/5.77 cnf(c1616, plain, 'is$ua$ucover$uof$ucarrier'(sK1653,sK1654), inference(clausification, [status(esa)], [negated_conjecture])).
% 36.79/5.77 cnf(c1617, plain, sK1654 = 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 36.79/5.77 cnf(d0, plain, 'cast$uas$ucarrier$usubset'(sK1653) = 'the$ucarrier'(sK1653), inference(resolution, [status(thm)], [c364,c1614])).
% 36.79/5.77 cnf(d1, plain, element('empty$uset',powerset(powerset('the$ucarrier'(sK1653)))), inference(demodulation, [status(thm)], [c1615,c1617])).
% 36.79/5.77 cnf(d2, plain, 'cast$uas$ucarrier$usubset'(sK1653) = 'union$uof$usubsets'('the$ucarrier'(sK1653),'empty$uset') | ~'one$usorted$ustr'(sK1653) | ~'is$ua$ucover$uof$ucarrier'(sK1653,'empty$uset'), inference(resolution, [status(thm)], [c538,d1])).
% 36.79/5.77 cnf(d3, plain, 'the$ucarrier'(sK1653) = 'union$uof$usubsets'('the$ucarrier'(sK1653),'empty$uset') | ~'one$usorted$ustr'(sK1653) | ~'is$ua$ucover$uof$ucarrier'(sK1653,'empty$uset'), inference(demodulation, [status(thm)], [d2,d0])).
% 36.79/5.77 cnf(d4, plain, 'the$ucarrier'(sK1653) = 'union$uof$usubsets'('the$ucarrier'(sK1653),'empty$uset') | ~'is$ua$ucover$uof$ucarrier'(sK1653,'empty$uset'), inference(resolution, [status(thm)], [c1614,d3])).
% 36.79/5.77 cnf(d5, plain, 'is$ua$ucover$uof$ucarrier'(sK1653,'empty$uset'), inference(demodulation, [status(thm)], [c1616,c1617])).
% 36.79/5.77 cnf(d6, plain, 'the$ucarrier'(sK1653) = 'union$uof$usubsets'('the$ucarrier'(sK1653),'empty$uset'), inference(resolution, [status(thm)], [d5,d4])).
% 36.79/5.77 cnf(d7, plain, 'union$uof$usubsets'('the$ucarrier'(sK1653),'empty$uset') = union('empty$uset'), inference(resolution, [status(thm)], [c915,d1])).
% 36.79/5.77 cnf(d8, plain, 'the$ucarrier'(sK1653) = union('empty$uset'), inference(demodulation, [status(thm)], [d7,d6])).
% 36.79/5.77 cnf(d9, plain, X0 != 'the$ucarrier'(sK1653) | 'Ts341'('empty$uset',X0), inference(superposition, [status(thm)], [d8,c411])).
% 36.79/5.77 cnf(d10, plain, 'Ts341'('empty$uset','the$ucarrier'(sK1653)), inference(equality_resolution, [status(thm)], [d9])).
% 36.79/5.77 cnf(d11, plain, ~in(X0,'the$ucarrier'(sK1653)) | in(sK345('empty$uset',X0),'empty$uset'), inference(resolution, [status(thm)], [d10,c414])).
% 36.79/5.77 cnf(d12, plain, ~in(X0,'empty$uset'), inference(equality_resolution, [status(thm)], [c285])).
% 36.79/5.77 cnf(d13, plain, ~in(X0,'the$ucarrier'(sK1653)), inference(resolution, [status(thm)], [d12,d11])).
% 36.79/5.77 cnf(d14, plain, 'the$ucarrier'(sK1653) = 'empty$uset', inference(resolution, [status(thm)], [d13,c286])).
% 36.79/5.77 cnf(d15, plain, ~empty('empty$uset') | 'empty$ucarrier'(sK1653) | ~'one$usorted$ustr'(sK1653), inference(superposition, [status(thm)], [d14,c255])).
% 36.79/5.77 cnf(d16, plain, ~empty('empty$uset') | ~'one$usorted$ustr'(sK1653), inference(resolution, [status(thm)], [c1613,d15])).
% 36.79/5.77 cnf(d17, plain, ~empty('empty$uset'), inference(resolution, [status(thm)], [c1614,d16])).
% 36.79/5.77 cnf(d18, plain, $false, inference(resolution, [status(thm)], [c630,d17])).
% 36.79/5.77 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------