%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV678+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 : n020.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:03 AM UTC 2026
% Result : Theorem 67.20s 20.12s
% Output : CNFRefutation 67.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV678+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.12/10.40 % Computer : n020.cluster.edu
% 0.12/10.40 % Model : x86_64 x86_64
% 0.12/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.40 % Memory : 8046.5625MB
% 0.12/10.40 % OS : Linux 6.8.0-71-generic
% 0.12/10.40 % CPULimit : 300
% 0.12/10.40 % WCLimit : 300
% 0.12/10.40 % DateTime : Sat Sep 26 11:38:29 UTC 2026
% 0.16/10.40 % CPUTime :
% 0.16/10.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 67.20/20.12 % SZS status Theorem for theBenchmark.p
% 67.20/20.12 % SZS output start CNFRefutation for theBenchmark.p
% 67.20/20.12 fof($_def_UseAuto.myFact, axiom, (p('cUseAuto$u2emyFact') <=> ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => ('cCoq$u2eInit$u2ePeano$u2ele$u$u$u24a2'(X0,'cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eS$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2eO')))) => 'cUseAuto$u2eP$u$u$u24a1'(X0)))))).
% 67.20/20.12 fof(_HAMMER_GOAL, conjecture, (! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => 'cUseAuto$u2eP$u$u$u24a1'(X0))) => p('cUseAuto$u2emyFact'))).
% 67.20/20.12 fof(negated_conjecture, negated_conjecture, ~((! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) => 'cUseAuto$u2eP$u$u$u24a1'(X0))) => p('cUseAuto$u2emyFact'))), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 67.20/20.12 cnf(c13, plain, p('cUseAuto$u2emyFact') | 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK11), inference(clausification, [status(esa)], [$_def_UseAuto.myFact])).
% 67.20/20.12 cnf(c15, plain, p('cUseAuto$u2emyFact') | ~'cUseAuto$u2eP$u$u$u24a1'(sK11), inference(clausification, [status(esa)], [$_def_UseAuto.myFact])).
% 67.20/20.12 cnf(c260, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | 'cUseAuto$u2eP$u$u$u24a1'(X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.20/20.12 cnf(c261, plain, ~p('cUseAuto$u2emyFact'), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.20/20.12 cnf(d0, plain, ~'cUseAuto$u2eP$u$u$u24a1'(sK11), inference(resolution, [status(thm)], [c261,c15])).
% 67.20/20.12 cnf(d1, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK11), inference(resolution, [status(thm)], [c261,c13])).
% 67.20/20.12 cnf(d2, plain, 'cUseAuto$u2eP$u$u$u24a1'(sK11), inference(resolution, [status(thm)], [d1,c260])).
% 67.20/20.12 cnf(d3, plain, $false, inference(resolution, [status(thm)], [d2,d0])).
% 67.20/20.12 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------