%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SET794+4 : 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:33:14 AM UTC 2026
% Result : Theorem 18.59s 2.85s
% Output : CNFRefutation 18.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET794+4 : 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.18/0.43 % Computer : n014.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 08:16:31 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.59/2.85 % SZS status Theorem for theBenchmark.p
% 18.59/2.85 % SZS output start CNFRefutation for theBenchmark.p
% 18.59/2.85 fof(total_order, axiom, ! [X0] : ! [X1] : (('total$uorder'(X0,X1) <=> (order(X0,X1) & ! [X2] : ! [X3] : (((member(X2,X1) & member(X3,X1)) => (apply(X0,X2,X3) | apply(X0,X3,X2)))))))).
% 18.59/2.85 fof(least, axiom, ! [X0] : ! [X1] : ! [X2] : ((least(X2,X0,X1) <=> (member(X2,X1) & ! [X3] : ((member(X3,X1) => apply(X0,X2,X3))))))).
% 18.59/2.85 fof(min, axiom, ! [X0] : ! [X1] : ! [X2] : ((min(X2,X0,X1) <=> (member(X2,X1) & ! [X3] : (((member(X3,X1) & apply(X0,X3,X2)) => X2 = X3)))))).
% 18.59/2.85 fof(thIV6, conjecture, ! [X0] : ! [X1] : ! [X2] : ((('total$uorder'(X0,X1) & min(X2,X0,X1)) => least(X2,X0,X1)))).
% 18.59/2.85 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ! [X2] : ((('total$uorder'(X0,X1) & min(X2,X0,X1)) => least(X2,X0,X1))), inference(negate_conjecture, [status(cth)], [thIV6])).
% 18.59/2.85 cnf(c20, plain, ~'total$uorder'(X0,X1) | X2(X1,X0), inference(clausification, [status(esa)], [total_order])).
% 18.59/2.85 cnf(c23, plain, ~X0(X1,X2) | ~member(X3,X1) | ~member(X4,X1) | apply(X2,X4,X3) | apply(X2,X3,X4), inference(clausification, [status(esa)], [total_order])).
% 18.59/2.85 cnf(c40, plain, least(X0,X1,X2) | ~member(X0,X2) | member(sK43(X1,X2,X0),X2), inference(clausification, [status(esa)], [least])).
% 18.59/2.85 cnf(c41, plain, least(X0,X1,X2) | ~member(X0,X2) | ~apply(X1,X0,sK43(X1,X2,X0)), inference(clausification, [status(esa)], [least])).
% 18.59/2.85 cnf(c49, plain, ~min(X0,X1,X2) | X3(X2,X0,X1), inference(clausification, [status(esa)], [min])).
% 18.59/2.85 cnf(c51, plain, ~X0(X1,X2,X3) | member(X2,X1), inference(clausification, [status(esa)], [min])).
% 18.59/2.85 cnf(c52, plain, ~X0(X1,X2,X3) | ~member(X4,X1) | ~apply(X3,X4,X2) | X2 = X4, inference(clausification, [status(esa)], [min])).
% 18.59/2.85 cnf(c72, plain, 'total$uorder'(sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.59/2.85 cnf(c73, plain, min(sK72,sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.59/2.85 cnf(c74, plain, ~least(sK72,sK70,sK71), inference(clausification, [status(esa)], [negated_conjecture])).
% 18.59/2.85 cnf(d0, plain, 'Ts17'(sK71,sK70), inference(resolution, [status(thm)], [c20,c72])).
% 18.59/2.85 cnf(d1, plain, ~member(X0,sK71) | ~member(X1,sK71) | apply(sK70,X0,X1) | apply(sK70,X1,X0), inference(resolution, [status(thm)], [c23,d0])).
% 18.59/2.85 cnf(d2, plain, ~member(X0,sK71) | ~member(X0,sK71) | apply(sK70,X0,X0), inference(factoring, [status(thm)], [d1])).
% 18.59/2.85 cnf(d3, plain, 'Ts50'(sK71,sK72,sK70), inference(resolution, [status(thm)], [c49,c73])).
% 18.59/2.85 cnf(d4, plain, sK72 = X0 | ~member(X0,sK71) | ~apply(sK70,X0,sK72), inference(resolution, [status(thm)], [c52,d3])).
% 18.59/2.85 cnf(d5, plain, sK72 = X0 | ~member(X0,sK71) | ~member(sK72,sK71) | ~member(X0,sK71) | apply(sK70,sK72,X0), inference(resolution, [status(thm)], [d4,d1])).
% 18.59/2.85 cnf(d6, plain, member(sK72,sK71), inference(resolution, [status(thm)], [d3,c51])).
% 18.59/2.85 cnf(d7, plain, sK72 = X0 | ~member(X0,sK71) | apply(sK70,sK72,X0), inference(resolution, [status(thm)], [d6,d5])).
% 18.59/2.85 cnf(d8, plain, sK72 = sK43(sK70,X0,sK72) | ~member(sK43(sK70,X0,sK72),sK71) | ~member(sK72,X0) | least(sK72,sK70,X0), inference(resolution, [status(thm)], [d7,c41])).
% 18.59/2.85 cnf(d9, plain, sK72 = sK43(sK70,sK71,sK72) | ~member(sK72,sK71) | least(sK72,sK70,sK71) | ~member(sK72,sK71) | least(sK72,sK70,sK71), inference(resolution, [status(thm)], [d8,c40])).
% 18.59/2.85 cnf(d10, plain, sK72 = sK43(sK70,sK71,sK72) | ~member(sK72,sK71), inference(resolution, [status(thm)], [c74,d9])).
% 18.59/2.85 cnf(d11, plain, sK72 = sK43(sK70,sK71,sK72), inference(resolution, [status(thm)], [d6,d10])).
% 18.59/2.85 cnf(d12, plain, ~apply(sK70,sK72,sK72) | ~member(sK72,sK71) | least(sK72,sK70,sK71), inference(superposition, [status(thm)], [d11,c41])).
% 18.59/2.85 cnf(d13, plain, ~member(sK72,sK71) | ~apply(sK70,sK72,sK72), inference(resolution, [status(thm)], [c74,d12])).
% 18.59/2.85 cnf(d14, plain, ~apply(sK70,sK72,sK72), inference(resolution, [status(thm)], [d6,d13])).
% 18.59/2.85 cnf(d15, plain, ~member(sK72,sK71), inference(resolution, [status(thm)], [d14,d2])).
% 18.59/2.85 cnf(d16, plain, $false, inference(resolution, [status(thm)], [d6,d15])).
% 18.59/2.85 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------