%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV637+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:49:00 AM UTC 2026
% Result : Theorem 84.20s 29.09s
% Output : CNFRefutation 84.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV637+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n015.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 11:31:04 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.20/29.09 % SZS status Theorem for theBenchmark.p
% 84.20/29.09 % SZS output start CNFRefutation for theBenchmark.p
% 84.20/29.09 fof($_def_Coq.Init.Peano.lt, axiom, ! [X0] : ! [X1] : ((p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) <=> p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1))))).
% 84.20/29.09 fof($_def_IndProp.lt, axiom, ! [X0] : ! [X1] : (('cIndProp$u2elt$u$u$u24a2'(X0,X1) <=> p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1))))).
% 84.20/29.09 fof(Coq.Arith.PeanoNat.Nat.lt_lt_succ_r, axiom, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) => (p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) => p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1))))))))).
% 84.20/29.09 fof(Coq.Arith.PeanoNat.Nat.nlt_succ_r, axiom, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) => (~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X1,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0))) <=> p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)))))))).
% 84.20/29.09 fof(_HAMMER_GOAL, conjecture, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) => ('cIndProp$u2elt$u$u$u24a2'(X0,X1) => 'cIndProp$u2elt$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1)))))))).
% 84.20/29.09 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) => ('cIndProp$u2elt$u$u$u24a2'(X0,X1) => 'cIndProp$u2elt$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1))))))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 84.20/29.09 cnf(c15, plain, ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) | p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1)), inference(clausification, [status(esa)], [$_def_Coq.Init.Peano.lt])).
% 84.20/29.09 cnf(c16, plain, p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) | ~p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1)), inference(clausification, [status(esa)], [$_def_Coq.Init.Peano.lt])).
% 84.20/29.09 cnf(c17, plain, ~'cIndProp$u2elt$u$u$u24a2'(X0,X1) | p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1)), inference(clausification, [status(esa)], [$_def_IndProp.lt])).
% 84.20/29.09 cnf(c18, plain, 'cIndProp$u2elt$u$u$u24a2'(X0,X1) | ~p('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0),X1)), inference(clausification, [status(esa)], [$_def_IndProp.lt])).
% 84.20/29.09 cnf(c197, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1))), inference(clausification, [status(esa)], [Coq.Arith.PeanoNat.Nat.lt_lt_succ_r])).
% 84.20/29.09 cnf(c253, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X1,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0))) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)), inference(clausification, [status(esa)], [Coq.Arith.PeanoNat.Nat.nlt_succ_r])).
% 84.20/29.09 cnf(c254, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X1,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X0))) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)), inference(clausification, [status(esa)], [Coq.Arith.PeanoNat.Nat.nlt_succ_r])).
% 84.20/29.09 cnf(c340, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK472), inference(clausification, [status(esa)], [negated_conjecture])).
% 84.20/29.09 cnf(c341, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK473), inference(clausification, [status(esa)], [negated_conjecture])).
% 84.20/29.09 cnf(c342, plain, 'cIndProp$u2elt$u$u$u24a2'(sK472,sK473), inference(clausification, [status(esa)], [negated_conjecture])).
% 84.20/29.09 cnf(c343, plain, ~'cIndProp$u2elt$u$u$u24a2'(sK472,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(sK473)), inference(clausification, [status(esa)], [negated_conjecture])).
% 84.20/29.09 cnf(d0, plain, ~'cIndProp$u2elt$u$u$u24a2'(X0,X1) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)), inference(resolution, [status(thm)], [c17,c16])).
% 84.20/29.09 cnf(d1, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X1,X0)), inference(resolution, [status(thm)], [c254,c197])).
% 84.20/29.09 cnf(d2, plain, 'cIndProp$u2elt$u$u$u24a2'(X0,X1) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X0,X1)), inference(resolution, [status(thm)], [c18,c15])).
% 84.20/29.09 cnf(d3, plain, 'cIndProp$u2elt$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'(X1)) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(X1,X0)), inference(resolution, [status(thm)], [d2,c253])).
% 84.20/29.09 cnf(d4, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK473) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK472) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK473,sK472)), inference(resolution, [status(thm)], [d3,c343])).
% 84.20/29.09 cnf(d5, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK473) | p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK473,sK472)), inference(resolution, [status(thm)], [c340,d4])).
% 84.20/29.09 cnf(d6, plain, p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK473,sK472)), inference(resolution, [status(thm)], [c341,d5])).
% 84.20/29.09 cnf(d7, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK472) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK473) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK472,sK473)), inference(resolution, [status(thm)], [d6,d1])).
% 84.20/29.09 cnf(d8, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK473) | ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK472,sK473)), inference(resolution, [status(thm)], [c340,d7])).
% 84.20/29.09 cnf(d9, plain, ~p('cCoq$u2eInit$u2ePeano$u2elt$u$u$u24a2'(sK472,sK473)), inference(resolution, [status(thm)], [c341,d8])).
% 84.20/29.09 cnf(d10, plain, ~'cIndProp$u2elt$u$u$u24a2'(sK472,sK473), inference(resolution, [status(thm)], [d9,d0])).
% 84.20/29.09 cnf(d11, plain, $false, inference(resolution, [status(thm)], [c342,d10])).
% 84.20/29.09 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------