%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU003+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 : n018.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:44 AM UTC 2026
% Result : Theorem 30.98s 7.97s
% Output : CNFRefutation 30.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU003+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 08:32:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.98/7.97 % SZS status Theorem for theBenchmark.p
% 30.98/7.97 % SZS output start CNFRefutation for theBenchmark.p
% 30.98/7.97 fof(d3_tarski, axiom, ! [X0] : ! [X1] : ((subset(X0,X1) <=> ! [X2] : ((in(X2,X0) => in(X2,X1)))))).
% 30.98/7.97 fof(d5_funct_1, axiom, ! [X0] : (((relation(X0) & function(X0)) => ! [X1] : ((X1 = 'relation$urng'(X0) <=> ! [X2] : ((in(X2,X1) <=> ? [X3] : ((in(X3,'relation$udom'(X0)) & X2 = apply(X0,X3)))))))))).
% 30.98/7.97 fof(t21_funct_1, axiom, ! [X0] : ! [X1] : (((relation(X1) & function(X1)) => ! [X2] : (((relation(X2) & function(X2)) => (in(X0,'relation$udom'('relation$ucomposition'(X2,X1))) <=> (in(X0,'relation$udom'(X2)) & in(apply(X2,X0),'relation$udom'(X1))))))))).
% 30.98/7.97 fof(t27_funct_1, conjecture, ! [X0] : (((relation(X0) & function(X0)) => ! [X1] : (((relation(X1) & function(X1)) => ('relation$udom'('relation$ucomposition'(X1,X0)) = 'relation$udom'(X1) => subset('relation$urng'(X1),'relation$udom'(X0)))))))).
% 30.98/7.97 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((relation(X0) & function(X0)) => ! [X1] : (((relation(X1) & function(X1)) => ('relation$udom'('relation$ucomposition'(X1,X0)) = 'relation$udom'(X1) => subset('relation$urng'(X1),'relation$udom'(X0))))))), inference(negate_conjecture, [status(cth)], [t27_funct_1])).
% 30.98/7.97 cnf(c4, plain, subset(X0,X1) | in(sK7(X0,X1),X0), inference(clausification, [status(esa)], [d3_tarski])).
% 30.98/7.97 cnf(c5, plain, subset(X0,X1) | ~in(sK7(X0,X1),X1), inference(clausification, [status(esa)], [d3_tarski])).
% 30.98/7.97 cnf(c6, plain, ~relation(X0) | ~function(X0) | X1 != 'relation$urng'(X0) | X2(X0,X1), inference(clausification, [status(esa)], [d5_funct_1])).
% 30.98/7.97 cnf(c7, plain, ~relation(X0) | ~function(X0) | X1 = 'relation$urng'(X0) | ~X2(X0,X1), inference(clausification, [status(esa)], [d5_funct_1])).
% 30.98/7.97 cnf(c8, plain, ~X0(X1,X2) | ~in(X3,X2) | in(sK12(X1,X3),'relation$udom'(X1)), inference(clausification, [status(esa)], [d5_funct_1])).
% 30.98/7.97 cnf(c9, plain, ~X0(X1,X2) | ~in(X3,X2) | X3 = apply(X1,sK12(X1,X3)), inference(clausification, [status(esa)], [d5_funct_1])).
% 30.98/7.97 cnf(c55, plain, ~in(X0,'relation$udom'('relation$ucomposition'(X1,X2))) | in(apply(X1,X0),'relation$udom'(X2)) | ~function(X1) | ~function(X2) | ~relation(X1) | ~relation(X2), inference(clausification, [status(esa)], [t21_funct_1])).
% 30.98/7.97 cnf(c65, plain, relation(sK64), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(c66, plain, function(sK64), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(c67, plain, relation(sK65), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(c68, plain, function(sK65), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(c69, plain, 'relation$udom'('relation$ucomposition'(sK65,sK64)) = 'relation$udom'(sK65), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(c70, plain, ~subset('relation$urng'(sK65),'relation$udom'(sK64)), inference(clausification, [status(esa)], [negated_conjecture])).
% 30.98/7.97 cnf(d0, plain, ~function(X0) | ~relation(X0) | 'Ts8'(X0,'relation$urng'(X0)), inference(equality_resolution, [status(thm)], [c6])).
% 30.98/7.97 cnf(d1, plain, ~subset(X0,'relation$udom'(sK64)) | ~function(sK65) | ~relation(sK65) | ~'Ts8'(sK65,X0), inference(superposition, [status(thm)], [c7,c70])).
% 30.98/7.97 cnf(d2, plain, ~function(sK65) | ~subset(X0,'relation$udom'(sK64)) | ~'Ts8'(sK65,X0), inference(resolution, [status(thm)], [c67,d1])).
% 30.98/7.97 cnf(d3, plain, ~subset(X0,'relation$udom'(sK64)) | ~'Ts8'(sK65,X0), inference(resolution, [status(thm)], [c68,d2])).
% 30.98/7.97 cnf(d4, plain, ~in(X0,'relation$udom'(sK65)) | in(apply(sK65,X0),'relation$udom'(sK64)) | ~function(sK65) | ~function(sK64) | ~relation(sK65) | ~relation(sK64), inference(superposition, [status(thm)], [c69,c55])).
% 30.98/7.97 cnf(d5, plain, ~in(X0,'relation$udom'(sK65)) | in(apply(sK65,X0),'relation$udom'(sK64)) | ~function(sK64) | ~function(sK65) | ~relation(sK65), inference(resolution, [status(thm)], [c65,d4])).
% 30.98/7.97 cnf(d6, plain, ~in(X0,'relation$udom'(sK65)) | in(apply(sK65,X0),'relation$udom'(sK64)) | ~function(sK65) | ~relation(sK65), inference(resolution, [status(thm)], [c66,d5])).
% 30.98/7.97 cnf(d7, plain, ~in(X0,'relation$udom'(sK65)) | in(apply(sK65,X0),'relation$udom'(sK64)) | ~function(sK65), inference(resolution, [status(thm)], [c67,d6])).
% 30.98/7.97 cnf(d8, plain, ~in(X0,'relation$udom'(sK65)) | in(apply(sK65,X0),'relation$udom'(sK64)), inference(resolution, [status(thm)], [c68,d7])).
% 30.98/7.97 cnf(d9, plain, in(X0,'relation$udom'(sK64)) | ~in(sK12(sK65,X0),'relation$udom'(sK65)) | ~in(X0,X1) | ~'Ts8'(sK65,X1), inference(superposition, [status(thm)], [c9,d8])).
% 30.98/7.97 cnf(d10, plain, ~in(X0,X1) | in(X0,'relation$udom'(sK64)) | ~'Ts8'(sK65,X1) | ~in(X0,X2) | ~'Ts8'(sK65,X2), inference(resolution, [status(thm)], [d9,c8])).
% 30.98/7.97 cnf(d11, plain, ~in(sK7(X0,'relation$udom'(sK64)),X1) | ~in(sK7(X0,'relation$udom'(sK64)),X2) | ~'Ts8'(sK65,X1) | ~'Ts8'(sK65,X2) | subset(X0,'relation$udom'(sK64)), inference(resolution, [status(thm)], [d10,c5])).
% 30.98/7.97 cnf(d12, plain, ~in(sK7(X0,'relation$udom'(sK64)),X1) | subset(X0,'relation$udom'(sK64)) | ~'Ts8'(sK65,X1) | ~'Ts8'(sK65,X0) | subset(X0,'relation$udom'(sK64)), inference(resolution, [status(thm)], [d11,c4])).
% 30.98/7.97 cnf(d13, plain, subset(X0,'relation$udom'(sK64)) | ~'Ts8'(sK65,X0) | ~'Ts8'(sK65,X0) | subset(X0,'relation$udom'(sK64)), inference(resolution, [status(thm)], [d12,c4])).
% 30.98/7.97 cnf(d14, plain, ~'Ts8'(sK65,X0) | ~'Ts8'(sK65,X0), inference(resolution, [status(thm)], [d13,d3])).
% 30.98/7.97 cnf(d15, plain, ~function(sK65) | ~relation(sK65), inference(resolution, [status(thm)], [d14,d0])).
% 30.98/7.97 cnf(d16, plain, ~function(sK65), inference(resolution, [status(thm)], [c67,d15])).
% 30.98/7.97 cnf(d17, plain, $false, inference(resolution, [status(thm)], [c68,d16])).
% 30.98/7.97 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------