%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEV612+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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:48:58 AM UTC 2026
% Result : Theorem 60.70s 10.15s
% Output : CNFRefutation 60.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV612+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n018.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Sat Sep 26 11:22:22 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.58 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 60.70/10.15 % SZS status Theorem for theBenchmark.p
% 60.70/10.15 % SZS output start CNFRefutation for theBenchmark.p
% 60.70/10.15 fof($_def_ZornsLemma.FunctionProperties.injective, axiom, ! [X0] : ! [X1] : ! [X2] : (('cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'(X0,X1,X2) <=> ! [X3] : ((t(X3,X0) => ! [X4] : ((t(X4,X0) => (happ(X2,X3) = happ(X2,X4) => X3 = X4)))))))).
% 60.70/10.15 fof($_type_102, axiom, ! [X0] : ! [X1] : (('c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) <=> ! [X2] : ((t(X2,X0) => 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(happ(X1,X2))))))).
% 60.70/10.15 fof($_type_1386, axiom, ! [X0] : ! [X1] : (('c$u24$u$utype$u$u1386$u$u$u24t'(X0,X1) <=> ! [X2] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X2) => t(happ(X1,X2),X0)))))).
% 60.70/10.15 fof($_typeof_Coq.Init.Datatypes.nat, axiom, 'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat')).
% 60.70/10.15 fof(ZornsLemma.CountableTypes.intro_nat_injection, axiom, ! [X0] : (('cType$u$u$u24t'(X0) => ! [X1] : (('c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) => ('cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'(X0,'cCoq$u2eInit$u2eDatatypes$u2enat',X1) => 'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'(X0))))))).
% 60.70/10.15 fof(ZornsLemma.InfiniteTypes.infinite_nat_inj, axiom, ! [X0] : (('cType$u$u$u24t'(X0) => (~p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'(X0)) => ? [X1] : (('c$u24$u$utype$u$u1386$u$u$u24t'(X0,X1) & 'cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'('cCoq$u2eInit$u2eDatatypes$u2enat',X0,X1))))))).
% 60.70/10.15 fof(ZornsLemma.InfiniteTypes.nat_infinite, axiom, ~p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat'))).
% 60.70/10.15 fof($tdef_Coq.Init.Datatypes.nat, axiom, ! [X0] : (('cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) <=> t(X0,'cCoq$u2eInit$u2eDatatypes$u2enat')))).
% 60.70/10.15 fof(_HAMMER_GOAL, conjecture, 'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')).
% 60.70/10.15 fof(negated_conjecture, negated_conjecture, ~'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(negate_conjecture, [status(cth)], [_HAMMER_GOAL])).
% 60.70/10.15 cnf(c19, plain, ~'cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'(X0,X1,X2) | X3(X0,X2), inference(clausification, [status(esa)], [$_def_ZornsLemma.FunctionProperties.injective])).
% 60.70/10.15 cnf(c20, plain, 'cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'(X0,X1,X2) | ~X3(X0,X2), inference(clausification, [status(esa)], [$_def_ZornsLemma.FunctionProperties.injective])).
% 60.70/10.15 cnf(c30, plain, 'c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) | t(sK21(X0,X1),X0), inference(clausification, [status(esa)], [$_type_102])).
% 60.70/10.15 cnf(c31, plain, 'c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(happ(X1,sK21(X0,X1))), inference(clausification, [status(esa)], [$_type_102])).
% 60.70/10.15 cnf(c32, plain, ~'c$u24$u$utype$u$u1386$u$u$u24t'(X0,X1) | ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X2) | t(happ(X1,X2),X0), inference(clausification, [status(esa)], [$_type_1386])).
% 60.70/10.15 cnf(c46, plain, 'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(clausification, [status(esa)], [$_typeof_Coq.Init.Datatypes.nat])).
% 60.70/10.15 cnf(c78, plain, ~'cType$u$u$u24t'(X0) | ~'c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) | ~'cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'(X0,'cCoq$u2eInit$u2eDatatypes$u2enat',X1) | 'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'(X0), inference(clausification, [status(esa)], [ZornsLemma.CountableTypes.intro_nat_injection])).
% 60.70/10.15 cnf(c97, plain, ~'cType$u$u$u24t'(X0) | p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'(X0)) | 'c$u24$u$utype$u$u1386$u$u$u24t'(X0,sK122(X0)), inference(clausification, [status(esa)], [ZornsLemma.InfiniteTypes.infinite_nat_inj])).
% 60.70/10.15 cnf(c98, plain, ~'cType$u$u$u24t'(X0) | p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'(X0)) | 'cZornsLemma$u2eFunctionProperties$u2einjective$u$u$u24a3'('cCoq$u2eInit$u2eDatatypes$u2enat',X0,sK122(X0)), inference(clausification, [status(esa)], [ZornsLemma.InfiniteTypes.infinite_nat_inj])).
% 60.70/10.15 cnf(c99, plain, ~p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')), inference(clausification, [status(esa)], [ZornsLemma.InfiniteTypes.nat_infinite])).
% 60.70/10.15 cnf(c101, plain, 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~t(X0,'cCoq$u2eInit$u2eDatatypes$u2enat'), inference(clausification, [status(esa)], [$tdef_Coq.Init.Datatypes.nat])).
% 60.70/10.15 cnf(c102, plain, ~'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(clausification, [status(esa)], [negated_conjecture])).
% 60.70/10.15 cnf(d0, plain, p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'(X0)) | ~'cType$u$u$u24t'(X0) | 'Ts8'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122(X0)), inference(resolution, [status(thm)], [c98,c19])).
% 60.70/10.15 cnf(d1, plain, 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X0) | 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK21('cCoq$u2eInit$u2eDatatypes$u2enat',X0)), inference(resolution, [status(thm)], [c30,c101])).
% 60.70/10.15 cnf(d2, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(X0) | ~'c$u24$u$utype$u$u1386$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X1) | 'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(happ(X1,X0)), inference(resolution, [status(thm)], [c32,c101])).
% 60.70/10.15 cnf(d3, plain, ~'cCoq$u2eInit$u2eDatatypes$u2enat$u$u$u24t'(sK21(X0,X1)) | ~'c$u24$u$utype$u$u1386$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X1) | 'c$u24$u$utype$u$u102$u$u$u24t'(X0,X1), inference(resolution, [status(thm)], [d2,c31])).
% 60.70/10.15 cnf(d4, plain, 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X0) | ~'c$u24$u$utype$u$u1386$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X0) | 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',X0), inference(resolution, [status(thm)], [d3,d1])).
% 60.70/10.15 cnf(d5, plain, 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')) | p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')) | ~'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(resolution, [status(thm)], [d4,c97])).
% 60.70/10.15 cnf(d6, plain, p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')) | 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')), inference(resolution, [status(thm)], [c46,d5])).
% 60.70/10.15 cnf(d7, plain, 'c$u24$u$utype$u$u102$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')), inference(resolution, [status(thm)], [c99,d6])).
% 60.70/10.15 cnf(d8, plain, 'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'(X0) | ~'cType$u$u$u24t'(X0) | ~'c$u24$u$utype$u$u102$u$u$u24t'(X0,X1) | ~'Ts8'(X0,X1), inference(resolution, [status(thm)], [c78,c20])).
% 60.70/10.15 cnf(d9, plain, ~'Ts8'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')) | 'cZornsLemma$u2eCountableTypes$u2eCountableT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat') | ~'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(resolution, [status(thm)], [d8,d7])).
% 60.70/10.15 cnf(d10, plain, ~'Ts8'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')) | ~'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(resolution, [status(thm)], [c102,d9])).
% 60.70/10.15 cnf(d11, plain, ~'Ts8'('cCoq$u2eInit$u2eDatatypes$u2enat',sK122('cCoq$u2eInit$u2eDatatypes$u2enat')), inference(resolution, [status(thm)], [c46,d10])).
% 60.70/10.15 cnf(d12, plain, p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')) | ~'cType$u$u$u24t'('cCoq$u2eInit$u2eDatatypes$u2enat'), inference(resolution, [status(thm)], [d11,d0])).
% 60.70/10.15 cnf(d13, plain, p('cZornsLemma$u2eFiniteTypes$u2eFiniteT$u$u$u24a1'('cCoq$u2eInit$u2eDatatypes$u2enat')), inference(resolution, [status(thm)], [c46,d12])).
% 60.70/10.15 cnf(d14, plain, $false, inference(resolution, [status(thm)], [c99,d13])).
% 60.70/10.15 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------