%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU108+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:40:53 AM UTC 2026
% Result : Theorem 3.66s 17.99s
% Output : CNFRefutation 3.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU108+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n014.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Sat Sep 26 08:36:31 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.66/17.99 % SZS status Theorem for theBenchmark.p
% 3.66/17.99 % SZS output start CNFRefutation for theBenchmark.p
% 3.66/17.99 fof(dt_k4_subset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (((element(X1,powerset(X0)) & element(X2,powerset(X0))) => element('subset$uunion2'(X0,X1,X2),powerset(X0))))).
% 3.66/17.99 fof(dt_k6_subset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (((element(X1,powerset(X0)) & element(X2,powerset(X0))) => element('subset$udifference'(X0,X1,X2),powerset(X0))))).
% 3.66/17.99 fof(fc1_subset_1, axiom, ! [X0] : ~empty(powerset(X0))).
% 3.66/17.99 fof(redefinition_k4_subset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (((element(X1,powerset(X0)) & element(X2,powerset(X0))) => 'subset$uunion2'(X0,X1,X2) = 'set$uunion2'(X1,X2)))).
% 3.66/17.99 fof(redefinition_k6_subset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (((element(X1,powerset(X0)) & element(X2,powerset(X0))) => 'subset$udifference'(X0,X1,X2) = 'set$udifference'(X1,X2)))).
% 3.66/17.99 fof(t10_finsub_1, axiom, ! [X0] : ((preboolean(X0) <=> ! [X1] : ! [X2] : (((in(X1,X0) & in(X2,X0)) => (in('set$uunion2'(X1,X2),X0) & in('set$udifference'(X1,X2),X0))))))).
% 3.66/17.99 fof(t1_subset, axiom, ! [X0] : ! [X1] : ((in(X0,X1) => element(X0,X1)))).
% 3.66/17.99 fof(t2_subset, axiom, ! [X0] : ! [X1] : ((element(X0,X1) => (empty(X1) | in(X0,X1))))).
% 3.66/17.99 fof(t20_finsub_1, conjecture, ! [X0] : preboolean(powerset(X0))).
% 3.66/17.99 fof(negated_conjecture, negated_conjecture, ~! [X0] : preboolean(powerset(X0)), inference(negate_conjecture, [status(cth)], [t20_finsub_1])).
% 3.66/17.99 cnf(c8, plain, ~element(X0,powerset(X1)) | ~element(X2,powerset(X1)) | element('subset$uunion2'(X1,X0,X2),powerset(X1)), inference(clausification, [status(esa)], [dt_k4_subset_1])).
% 3.66/17.99 cnf(c9, plain, ~element(X0,powerset(X1)) | ~element(X2,powerset(X1)) | element('subset$udifference'(X1,X0,X2),powerset(X1)), inference(clausification, [status(esa)], [dt_k6_subset_1])).
% 3.66/17.99 cnf(c12, plain, ~empty(powerset(X0)), inference(clausification, [status(esa)], [fc1_subset_1])).
% 3.66/17.99 cnf(c48, plain, ~element(X0,powerset(X1)) | ~element(X2,powerset(X1)) | 'subset$uunion2'(X1,X0,X2) = 'set$uunion2'(X0,X2), inference(clausification, [status(esa)], [redefinition_k4_subset_1])).
% 3.66/17.99 cnf(c49, plain, ~element(X0,powerset(X1)) | ~element(X2,powerset(X1)) | 'subset$udifference'(X1,X0,X2) = 'set$udifference'(X0,X2), inference(clausification, [status(esa)], [redefinition_k6_subset_1])).
% 3.66/17.99 cnf(c52, plain, preboolean(X0) | ~X1(X0), inference(clausification, [status(esa)], [t10_finsub_1])).
% 3.66/17.99 cnf(c55, plain, X0(X1) | in(sK60(X1),X1), inference(clausification, [status(esa)], [t10_finsub_1])).
% 3.66/17.99 cnf(c56, plain, X0(X1) | in(sK61(X1),X1), inference(clausification, [status(esa)], [t10_finsub_1])).
% 3.66/17.99 cnf(c57, plain, X0(X1) | ~in('set$uunion2'(sK60(X1),sK61(X1)),X1) | ~in('set$udifference'(sK60(X1),sK61(X1)),X1), inference(clausification, [status(esa)], [t10_finsub_1])).
% 3.66/17.99 cnf(c59, plain, ~in(X0,X1) | element(X0,X1), inference(clausification, [status(esa)], [t1_subset])).
% 3.66/17.99 cnf(c60, plain, ~element(X0,X1) | empty(X1) | in(X0,X1), inference(clausification, [status(esa)], [t2_subset])).
% 3.66/17.99 cnf(c70, plain, ~preboolean(powerset(sK82)), inference(clausification, [status(esa)], [negated_conjecture])).
% 3.66/17.99 cnf(d0, plain, element(sK60(X0),X0) | 'Ts56'(X0), inference(resolution, [status(thm)], [c59,c55])).
% 3.66/17.99 cnf(d1, plain, 'Ts56'(X0) | element(sK61(X0),X0), inference(resolution, [status(thm)], [c56,c59])).
% 3.66/17.99 cnf(d2, plain, in('subset$uunion2'(X0,X1,X2),powerset(X0)) | empty(powerset(X0)) | ~element(X1,powerset(X0)) | ~element(X2,powerset(X0)), inference(resolution, [status(thm)], [c60,c8])).
% 3.66/17.99 cnf(d3, plain, in('subset$uunion2'(X0,X1,X2),powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)), inference(resolution, [status(thm)], [c12,d2])).
% 3.66/17.99 cnf(d4, plain, in('set$uunion2'(X1,X2),powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)) | ~element(X1,powerset(X0)) | ~element(X2,powerset(X0)), inference(superposition, [status(thm)], [c48,d3])).
% 3.66/17.99 cnf(d5, plain, in('subset$udifference'(X0,X1,X2),powerset(X0)) | empty(powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)), inference(resolution, [status(thm)], [c60,c9])).
% 3.66/17.99 cnf(d6, plain, in('subset$udifference'(X0,X1,X2),powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)), inference(resolution, [status(thm)], [c12,d5])).
% 3.66/17.99 cnf(d7, plain, in('set$udifference'(X1,X2),powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)) | ~element(X2,powerset(X0)) | ~element(X1,powerset(X0)), inference(superposition, [status(thm)], [c49,d6])).
% 3.66/17.99 cnf(d8, plain, ~element(sK61(powerset(X0)),powerset(X0)) | ~element(sK60(powerset(X0)),powerset(X0)) | ~in('set$uunion2'(sK60(powerset(X0)),sK61(powerset(X0))),powerset(X0)) | 'Ts56'(powerset(X0)), inference(resolution, [status(thm)], [d7,c57])).
% 3.66/17.99 cnf(d9, plain, ~element(sK60(powerset(X0)),powerset(X0)) | ~element(sK61(powerset(X0)),powerset(X0)) | 'Ts56'(powerset(X0)) | ~element(sK61(powerset(X0)),powerset(X0)) | ~element(sK60(powerset(X0)),powerset(X0)), inference(resolution, [status(thm)], [d8,d4])).
% 3.66/17.99 cnf(d10, plain, ~element(sK60(powerset(X0)),powerset(X0)) | 'Ts56'(powerset(X0)) | 'Ts56'(powerset(X0)), inference(resolution, [status(thm)], [d9,d1])).
% 3.66/17.99 cnf(d11, plain, 'Ts56'(powerset(X0)) | 'Ts56'(powerset(X0)), inference(resolution, [status(thm)], [d10,d0])).
% 3.66/17.99 cnf(d12, plain, preboolean(powerset(X0)), inference(resolution, [status(thm)], [d11,c52])).
% 3.66/17.99 cnf(d13, plain, $false, inference(resolution, [status(thm)], [d12,c70])).
% 3.66/17.99 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------