%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV606+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:48:57 AM UTC 2026
% Result : Theorem 62.18s 18.30s
% Output : CNFRefutation 62.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV606+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/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 11:23:13 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.18/18.30 % SZS status Theorem for theBenchmark.p
% 62.18/18.30 % SZS output start CNFRefutation for theBenchmark.p
% 62.18/18.30 fof(Coq.ZArith.BinInt.Z.square_le_simpl_nonneg, axiom, ! [X0] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X1) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X1)) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X0,X0),'cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X1,X1))) => p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(X0,X1))))))))).
% 62.18/18.30 fof(_HAMMER_GOAL, conjecture, ! [X0] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X1) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X0)) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X1)) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X1,X1),'cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X0,X0))) => p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(X1,X0)))))))))).
% 62.18/18.30 fof(negated_conjecture, negated_conjecture, ~! [X0] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X0) => ! [X1] : (('cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X1) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X0)) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X1)) => (p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X1,X1),'cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X0,X0))) => p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(X1,X0))))))))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 62.18/18.30 cnf(c147, plain, ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',X0)) | ~'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X1) | p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(X1,X0)) | ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X1,X1),'cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(X0,X0))) | ~'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(X0), inference(clausification, [status(esa)], [Coq.ZArith.BinInt.Z.square_le_simpl_nonneg])).
% 62.18/18.30 cnf(c170, plain, 'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(sK295), inference(clausification, [status(esa)], [negated_conjecture])).
% 62.18/18.30 cnf(c171, plain, 'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(sK296), inference(clausification, [status(esa)], [negated_conjecture])).
% 62.18/18.30 cnf(c172, plain, p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',sK295)), inference(clausification, [status(esa)], [negated_conjecture])).
% 62.18/18.30 cnf(c174, plain, p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(sK296,sK296),'cCoq$u2eZArith$u2eBinIntDef$u2eZ$u2emul$u$u$u24a2'(sK295,sK295))), inference(clausification, [status(esa)], [negated_conjecture])).
% 62.18/18.30 cnf(c175, plain, ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(sK296,sK295)), inference(clausification, [status(esa)], [negated_conjecture])).
% 62.18/18.30 cnf(d0, plain, ~'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(sK296) | ~'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(sK295) | p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(sK296,sK295)) | ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',sK295)), inference(resolution, [status(thm)], [c147,c174])).
% 62.18/18.30 cnf(d1, plain, ~'cCoq$u2eNumbers$u2eBinNums$u2eZ$u$u$u24t'(sK296) | ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',sK295)) | p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(sK296,sK295)), inference(resolution, [status(thm)], [c170,d0])).
% 62.18/18.30 cnf(d2, plain, ~p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'('cCoq$u2eNumbers$u2eBinNums$u2eZ0',sK295)) | p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(sK296,sK295)), inference(resolution, [status(thm)], [c171,d1])).
% 62.18/18.30 cnf(d3, plain, p('cCoq$u2eZArith$u2eBinInt$u2eZ$u2ele$u$u$u24a2'(sK296,sK295)), inference(resolution, [status(thm)], [c172,d2])).
% 62.18/18.30 cnf(d4, plain, $false, inference(resolution, [status(thm)], [c175,d3])).
% 62.18/18.30 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------