%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU325+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 : n004.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 17.63s 4.32s
% Output : CNFRefutation 17.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU325+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n004.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 09:12:36 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.63/4.32 % SZS status Theorem for theBenchmark.p
% 17.63/4.32 % SZS output start CNFRefutation for theBenchmark.p
% 17.63/4.32 fof(d3_pre_topc, axiom, ! [X0] : (('one$usorted$ustr'(X0) => 'cast$uas$ucarrier$usubset'(X0) = 'the$ucarrier'(X0)))).
% 17.63/4.32 fof(d4_tarski, axiom, ! [X0] : ! [X1] : ((X1 = union(X0) <=> ! [X2] : ((in(X2,X1) <=> ? [X3] : ((in(X2,X3) & in(X3,X0)))))))).
% 17.63/4.32 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))))))).
% 17.63/4.32 fof(fc1_struct_0, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ~empty('the$ucarrier'(X0))))).
% 17.63/4.32 fof(fc6_membered, axiom, (empty('empty$uset') & ('v1$umembered'('empty$uset') & ('v2$umembered'('empty$uset') & ('v3$umembered'('empty$uset') & ('v4$umembered'('empty$uset') & 'v5$umembered'('empty$uset'))))))).
% 17.63/4.32 fof(redefinition_k5_setfam_1, axiom, ! [X0] : ! [X1] : ((element(X1,powerset(powerset(X0))) => 'union$uof$usubsets'(X0,X1) = union(X1)))).
% 17.63/4.32 fof(t7_boole, axiom, ! [X0] : ! [X1] : ~((in(X0,X1) & empty(X1)))).
% 17.63/4.32 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'))))))).
% 17.63/4.32 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])).
% 17.63/4.32 cnf(c43, plain, ~'one$usorted$ustr'(X0) | 'cast$uas$ucarrier$usubset'(X0) = 'the$ucarrier'(X0), inference(clausification, [status(esa)], [d3_pre_topc])).
% 17.63/4.32 cnf(c44, plain, X0 != union(X1) | X2(X1,X0), inference(clausification, [status(esa)], [d4_tarski])).
% 17.63/4.32 cnf(c45, plain, X0 = union(X1) | ~X2(X1,X0), inference(clausification, [status(esa)], [d4_tarski])).
% 17.63/4.32 cnf(c47, plain, ~X0(X1,X2) | ~in(X3,X2) | in(sK35(X1,X3),X1), inference(clausification, [status(esa)], [d4_tarski])).
% 17.63/4.32 cnf(c51, plain, X0(X1,X2) | in(sK37(X1,X2),X2) | in(sK39(X1,X2),X1), inference(clausification, [status(esa)], [d4_tarski])).
% 17.63/4.32 cnf(c55, 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])).
% 17.63/4.32 cnf(c61, plain, 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~empty('the$ucarrier'(X0)), inference(clausification, [status(esa)], [fc1_struct_0])).
% 17.63/4.32 cnf(c64, plain, empty('empty$uset'), inference(clausification, [status(esa)], [fc6_membered])).
% 17.63/4.32 cnf(c84, plain, ~element(X0,powerset(powerset(X1))) | 'union$uof$usubsets'(X1,X0) = union(X0), inference(clausification, [status(esa)], [redefinition_k5_setfam_1])).
% 17.63/4.32 cnf(c93, plain, ~in(X0,X1) | ~empty(X1), inference(clausification, [status(esa)], [t7_boole])).
% 17.63/4.32 cnf(c95, plain, ~'empty$ucarrier'(sK80), inference(clausification, [status(esa)], [negated_conjecture])).
% 17.63/4.32 cnf(c96, plain, 'one$usorted$ustr'(sK80), inference(clausification, [status(esa)], [negated_conjecture])).
% 17.63/4.32 cnf(c97, plain, element(sK81,powerset(powerset('the$ucarrier'(sK80)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 17.63/4.32 cnf(c98, plain, 'is$ua$ucover$uof$ucarrier'(sK80,sK81), inference(clausification, [status(esa)], [negated_conjecture])).
% 17.63/4.32 cnf(c99, plain, sK81 = 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 17.63/4.32 cnf(d0, plain, 'cast$uas$ucarrier$usubset'(sK80) = 'the$ucarrier'(sK80), inference(resolution, [status(thm)], [c43,c96])).
% 17.63/4.32 cnf(d1, plain, element('empty$uset',powerset(powerset('the$ucarrier'(sK80)))), inference(demodulation, [status(thm)], [c97,c99])).
% 17.63/4.32 cnf(d2, plain, 'cast$uas$ucarrier$usubset'(sK80) = 'union$uof$usubsets'('the$ucarrier'(sK80),'empty$uset') | ~'one$usorted$ustr'(sK80) | ~'is$ua$ucover$uof$ucarrier'(sK80,'empty$uset'), inference(resolution, [status(thm)], [c55,d1])).
% 17.63/4.32 cnf(d3, plain, 'the$ucarrier'(sK80) = 'union$uof$usubsets'('the$ucarrier'(sK80),'empty$uset') | ~'one$usorted$ustr'(sK80) | ~'is$ua$ucover$uof$ucarrier'(sK80,'empty$uset'), inference(demodulation, [status(thm)], [d2,d0])).
% 17.63/4.32 cnf(d4, plain, 'the$ucarrier'(sK80) = 'union$uof$usubsets'('the$ucarrier'(sK80),'empty$uset') | ~'is$ua$ucover$uof$ucarrier'(sK80,'empty$uset'), inference(resolution, [status(thm)], [c96,d3])).
% 17.63/4.32 cnf(d5, plain, 'is$ua$ucover$uof$ucarrier'(sK80,'empty$uset'), inference(demodulation, [status(thm)], [c98,c99])).
% 17.63/4.32 cnf(d6, plain, 'the$ucarrier'(sK80) = 'union$uof$usubsets'('the$ucarrier'(sK80),'empty$uset'), inference(resolution, [status(thm)], [d5,d4])).
% 17.63/4.32 cnf(d7, plain, 'union$uof$usubsets'('the$ucarrier'(sK80),'empty$uset') = union('empty$uset'), inference(resolution, [status(thm)], [c84,d1])).
% 17.63/4.32 cnf(d8, plain, 'the$ucarrier'(sK80) = union('empty$uset'), inference(demodulation, [status(thm)], [d7,d6])).
% 17.63/4.32 cnf(d9, plain, X0 != 'the$ucarrier'(sK80) | 'Ts31'('empty$uset',X0), inference(superposition, [status(thm)], [d8,c44])).
% 17.63/4.32 cnf(d10, plain, 'Ts31'('empty$uset','the$ucarrier'(sK80)), inference(equality_resolution, [status(thm)], [d9])).
% 17.63/4.32 cnf(d11, plain, ~in(X0,'the$ucarrier'(sK80)) | in(sK35('empty$uset',X0),'empty$uset'), inference(resolution, [status(thm)], [d10,c47])).
% 17.63/4.32 cnf(d12, plain, ~in(X0,'the$ucarrier'(sK80)) | ~empty('empty$uset'), inference(resolution, [status(thm)], [d11,c93])).
% 17.63/4.32 cnf(d13, plain, ~in(X0,'the$ucarrier'(sK80)), inference(resolution, [status(thm)], [c64,d12])).
% 17.63/4.32 cnf(d14, plain, in(sK37('the$ucarrier'(sK80),X0),X0) | 'Ts31'('the$ucarrier'(sK80),X0), inference(resolution, [status(thm)], [d13,c51])).
% 17.63/4.32 cnf(d15, plain, 'Ts31'('the$ucarrier'(sK80),'the$ucarrier'(sK80)), inference(resolution, [status(thm)], [d14,d13])).
% 17.63/4.32 cnf(d16, plain, 'the$ucarrier'(sK80) = union('the$ucarrier'(sK80)), inference(resolution, [status(thm)], [d15,c45])).
% 17.63/4.32 cnf(d17, plain, 'Ts31'('the$ucarrier'(sK80),X0) | ~empty(X0), inference(resolution, [status(thm)], [d14,c93])).
% 17.63/4.32 cnf(d18, plain, ~empty(X0) | X0 = union('the$ucarrier'(sK80)), inference(resolution, [status(thm)], [d17,c45])).
% 17.63/4.32 cnf(d19, plain, X0 = 'the$ucarrier'(sK80) | ~empty(X0), inference(demodulation, [status(thm)], [d18,d16])).
% 17.63/4.32 cnf(d20, plain, 'empty$uset' = 'the$ucarrier'(sK80), inference(resolution, [status(thm)], [d19,c64])).
% 17.63/4.32 cnf(d21, plain, ~empty('empty$uset') | ~'one$usorted$ustr'(sK80) | 'empty$ucarrier'(sK80), inference(superposition, [status(thm)], [d20,c61])).
% 17.63/4.32 cnf(d22, plain, ~empty('empty$uset') | ~'one$usorted$ustr'(sK80), inference(resolution, [status(thm)], [c95,d21])).
% 17.63/4.32 cnf(d23, plain, ~empty('empty$uset'), inference(resolution, [status(thm)], [c96,d22])).
% 17.63/4.32 cnf(d24, plain, $false, inference(resolution, [status(thm)], [c64,d23])).
% 17.63/4.32 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------