%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEV645+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 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 : Thu Sep 24 02:35:22 PM UTC 2026
% Result : Theorem 0.31s 0.79s
% Output : CNFRefutation 0.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 16
% Syntax : Number of formulae : 75 ( 22 unt; 0 def)
% Number of atoms : 249 ( 31 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 290 ( 116 ~; 118 |; 16 &)
% ( 7 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-5 aty)
% Number of variables : 106 ( 0 sgn 61 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof('_HAMMER_GOAL',conjecture,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ! [X988] :
( cLF_2ePoly_2elist___24t(cCoq_2eInit_2eDatatypes_2enat,X988)
=> ( cLogic_2eIn___24a3(cCoq_2eInit_2eDatatypes_2enat,X31,cLF_2ePoly_2emap___24a4(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,X988))
=> X31 = cCoq_2eInit_2eDatatypes_2eO ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof('$_type_706',axiom,
! [X1,X2,X795] :
( c_24__type__706___24t(X1,X2,X795)
<=> ! [X3] :
( t(X3,X1)
=> t(happ(X795,X3),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_706') ).
fof('$tdef_Coq.Init.Datatypes.nat',axiom,
! [X987] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X987)
<=> t(X987,cCoq_2eInit_2eDatatypes_2enat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$tdef_Coq.Init.Datatypes.nat') ).
fof('$adef_$_lam_174703_$a1',axiom,
! [X972] : happ(c_24__lam__174703,X972) = c_24__lam__174703___24a1(X972),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_$_lam_174703_$a1') ).
fof('$_lam_174703',axiom,
! [X1] : c_24__lam__174703___24a1(X1) = cCoq_2eInit_2eNat_2emul___24a2(X1,cCoq_2eInit_2eDatatypes_2eO),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_lam_174703') ).
fof('Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_ge_lt',axiom,
! [X37] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X37)
=> ! [X38] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X38)
=> ( ~ cCoq_2eInit_2ePeano_2ele___24a2(X38,X37)
=> p(cCoq_2eInit_2ePeano_2elt___24a2(X37,X38)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_ge_lt') ).
fof('Coq.Arith.PeanoNat.Nat.le_ge_cases',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ! [X32] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X32)
=> ( cCoq_2eInit_2ePeano_2ele___24a2(X32,X31)
| cCoq_2eInit_2ePeano_2ele___24a2(X31,X32) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.le_ge_cases') ).
fof('Coq.Arith.PeanoNat.Nat.lt_lt_0',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ! [X32] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X32)
=> ( p(cCoq_2eInit_2ePeano_2elt___24a2(X31,X32))
=> p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X32)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.lt_lt_0') ).
fof('Coq.Init.Peano.mult_n_O',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> cCoq_2eInit_2eDatatypes_2eO = cCoq_2eInit_2eNat_2emul___24a2(X31,cCoq_2eInit_2eDatatypes_2eO) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Init.Peano.mult_n_O') ).
fof('Coq.Arith.PeanoNat.Nat.le_0_r',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ( cCoq_2eInit_2ePeano_2ele___24a2(X31,cCoq_2eInit_2eDatatypes_2eO)
<=> X31 = cCoq_2eInit_2eDatatypes_2eO ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.le_0_r') ).
fof('$_typeof_Coq.Init.Datatypes.O',axiom,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_Coq.Init.Datatypes.O') ).
fof('Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_antisym',axiom,
! [X37] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X37)
=> ! [X38] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X38)
=> ( cCoq_2eInit_2ePeano_2ele___24a2(X37,X38)
=> ( cCoq_2eInit_2ePeano_2ele___24a2(X38,X37)
=> X37 = X38 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_antisym') ).
fof('Coq.Arith.PeanoNat.Nat.neq_0_lt_0',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ( X31 != cCoq_2eInit_2eDatatypes_2eO
<=> p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X31)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.neq_0_lt_0') ).
fof('Logic.In_map_iff',axiom,
! [X18] :
( cType___24t(X18)
=> ! [X72] :
( cType___24t(X72)
=> ! [X78] :
( c_24__type__706___24t(X18,X72,X78)
=> ! [X127] :
( cLF_2ePoly_2elist___24t(X18,X127)
=> ! [X968] :
( t(X968,X72)
=> ( cLogic_2eIn___24a3(X72,X968,cLF_2ePoly_2emap___24a4(X18,X72,X78,X127))
<=> ? [X969] :
( cLogic_2eIn___24a3(X18,X969,X127)
& happ(X78,X969) = X968
& t(X969,X18) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Logic.In_map_iff') ).
fof('$_typeof_Coq.Init.Datatypes.nat',axiom,
cType___24t(cCoq_2eInit_2eDatatypes_2enat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_Coq.Init.Datatypes.nat') ).
fof('Coq.Arith.PeanoNat.Nat.lt_0_mul\\',axiom,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ! [X32] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X32)
=> ( p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eNat_2emul___24a2(X31,X32)))
<=> ( p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X32))
& p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X31)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Arith.PeanoNat.Nat.lt_0_mul\\') ).
fof(c_0_16,negated_conjecture,
~ ! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ! [X988] :
( cLF_2ePoly_2elist___24t(cCoq_2eInit_2eDatatypes_2enat,X988)
=> ( cLogic_2eIn___24a3(cCoq_2eInit_2eDatatypes_2enat,X31,cLF_2ePoly_2emap___24a4(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,X988))
=> X31 = cCoq_2eInit_2eDatatypes_2eO ) ) ),
inference(assume_negation,[status(cth)],['_HAMMER_GOAL']) ).
fof(c_0_17,plain,
! [X1350,X1351,X1352,X1353,X1354,X1355,X1356] :
( ( c_24__type__706___24t(X1354,X1355,X1356)
| ~ t(happ(X1356,esk18_3(X1354,X1355,X1356)),X1355) )
& ( c_24__type__706___24t(X1354,X1355,X1356)
| t(esk18_3(X1354,X1355,X1356),X1354) )
& ( t(happ(X1352,X1353),X1351)
| ~ t(X1353,X1350)
| ~ c_24__type__706___24t(X1350,X1351,X1352) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['$_type_706'])])])])])])]) ).
fof(c_0_18,plain,
! [X1020] :
( ( cCoq_2eInit_2eDatatypes_2enat___24t(X1020)
| ~ t(X1020,cCoq_2eInit_2eDatatypes_2enat) )
& ( t(X1020,cCoq_2eInit_2eDatatypes_2enat)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1020) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['$tdef_Coq.Init.Datatypes.nat'])])]) ).
fof(c_0_19,plain,
! [X1019] : happ(c_24__lam__174703,X1019) = c_24__lam__174703___24a1(X1019),
inference(variable_rename,[status(thm)],['$adef_$_lam_174703_$a1']) ).
fof(c_0_20,plain,
! [X1362] : c_24__lam__174703___24a1(X1362) = cCoq_2eInit_2eNat_2emul___24a2(X1362,cCoq_2eInit_2eDatatypes_2eO),
inference(variable_rename,[status(thm)],['$_lam_174703']) ).
fof(c_0_21,plain,
! [X37] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X37)
=> ! [X38] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X38)
=> ( ~ cCoq_2eInit_2ePeano_2ele___24a2(X38,X37)
=> p(cCoq_2eInit_2ePeano_2elt___24a2(X37,X38)) ) ) ),
inference(fof_simplification,[status(thm)],['Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.not_ge_lt']) ).
fof(c_0_22,plain,
! [X1390,X1391] :
( cCoq_2eInit_2ePeano_2ele___24a2(X1391,X1390)
| cCoq_2eInit_2ePeano_2ele___24a2(X1390,X1391)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1391)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1390) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Arith.PeanoNat.Nat.le_ge_cases'])])])]) ).
fof(c_0_23,negated_conjecture,
( esk1_0 != cCoq_2eInit_2eDatatypes_2eO
& cLogic_2eIn___24a3(cCoq_2eInit_2eDatatypes_2enat,esk1_0,cLF_2ePoly_2emap___24a4(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,esk2_0))
& cLF_2ePoly_2elist___24t(cCoq_2eInit_2eDatatypes_2enat,esk2_0)
& cCoq_2eInit_2eDatatypes_2enat___24t(esk1_0) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])]) ).
cnf(c_0_24,plain,
( ~ t(happ(X1,esk18_3(X2,X3,X1)),X3)
| c_24__type__706___24t(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_25,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| t(X1,cCoq_2eInit_2eDatatypes_2enat) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_26,plain,
happ(c_24__lam__174703,X1) = c_24__lam__174703___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_27,plain,
c_24__lam__174703___24a1(X1) = cCoq_2eInit_2eNat_2emul___24a2(X1,cCoq_2eInit_2eDatatypes_2eO),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
fof(c_0_28,plain,
! [X1432,X1433] :
( p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1433))
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(X1432,X1433))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1433)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1432) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Arith.PeanoNat.Nat.lt_lt_0'])])])]) ).
fof(c_0_29,plain,
! [X1378,X1379] :
( p(cCoq_2eInit_2ePeano_2elt___24a2(X1378,X1379))
| cCoq_2eInit_2ePeano_2ele___24a2(X1379,X1378)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1379)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1378) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])]) ).
cnf(c_0_30,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| cCoq_2eInit_2ePeano_2ele___24a2(X2,X1)
| cCoq_2eInit_2ePeano_2ele___24a2(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_31,negated_conjecture,
cCoq_2eInit_2eDatatypes_2enat___24t(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_32,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(happ(X2,esk18_3(X1,cCoq_2eInit_2eDatatypes_2enat,X2)))
| c_24__type__706___24t(X1,cCoq_2eInit_2eDatatypes_2enat,X2) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_33,plain,
happ(c_24__lam__174703,X1) = cCoq_2eInit_2eNat_2emul___24a2(X1,cCoq_2eInit_2eDatatypes_2eO),
inference(rw,[status(thm)],[c_0_26,c_0_27]) ).
fof(c_0_34,plain,
! [X1327] :
( cCoq_2eInit_2eDatatypes_2eO = cCoq_2eInit_2eNat_2emul___24a2(X1327,cCoq_2eInit_2eDatatypes_2eO)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1327) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Init.Peano.mult_n_O'])])]) ).
cnf(c_0_35,plain,
( ~ p(cCoq_2eInit_2ePeano_2elt___24a2(X1,X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_36,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| p(cCoq_2eInit_2ePeano_2elt___24a2(X1,X2))
| cCoq_2eInit_2ePeano_2ele___24a2(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_37,plain,
! [X1387] :
( ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1387)
| cCoq_2eInit_2ePeano_2ele___24a2(X1387,cCoq_2eInit_2eDatatypes_2eO)
| X1387 != cCoq_2eInit_2eDatatypes_2eO )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1387)
| X1387 = cCoq_2eInit_2eDatatypes_2eO
| ~ cCoq_2eInit_2ePeano_2ele___24a2(X1387,cCoq_2eInit_2eDatatypes_2eO) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Arith.PeanoNat.Nat.le_0_r'])])])]) ).
cnf(c_0_38,negated_conjecture,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| cCoq_2eInit_2ePeano_2ele___24a2(X1,esk1_0)
| cCoq_2eInit_2ePeano_2ele___24a2(esk1_0,X1) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_39,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO),
inference(split_conjunct,[status(thm)],['$_typeof_Coq.Init.Datatypes.O']) ).
cnf(c_0_40,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eNat_2emul___24a2(esk18_3(X1,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703),cCoq_2eInit_2eDatatypes_2eO))
| c_24__type__706___24t(X1,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703) ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_41,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| cCoq_2eInit_2eDatatypes_2eO = cCoq_2eInit_2eNat_2emul___24a2(X1,cCoq_2eInit_2eDatatypes_2eO) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_42,plain,
( ~ t(X1,cCoq_2eInit_2eDatatypes_2enat)
| cCoq_2eInit_2eDatatypes_2enat___24t(X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_43,plain,
( c_24__type__706___24t(X1,X2,X3)
| t(esk18_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_44,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1))
| cCoq_2eInit_2ePeano_2ele___24a2(X1,X2) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
fof(c_0_45,plain,
! [X1369,X1370] :
( X1369 = X1370
| ~ cCoq_2eInit_2ePeano_2ele___24a2(X1370,X1369)
| ~ cCoq_2eInit_2ePeano_2ele___24a2(X1369,X1370)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1370)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1369) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Arith.PeanoNat.Nat.Private_OrderTac.Tac.le_antisym'])])])]) ).
cnf(c_0_46,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| ~ cCoq_2eInit_2ePeano_2ele___24a2(X1,cCoq_2eInit_2eDatatypes_2eO)
| X1 = cCoq_2eInit_2eDatatypes_2eO ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_47,negated_conjecture,
( cCoq_2eInit_2ePeano_2ele___24a2(esk1_0,cCoq_2eInit_2eDatatypes_2eO)
| cCoq_2eInit_2ePeano_2ele___24a2(cCoq_2eInit_2eDatatypes_2eO,esk1_0) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_48,negated_conjecture,
esk1_0 != cCoq_2eInit_2eDatatypes_2eO,
inference(split_conjunct,[status(thm)],[c_0_23]) ).
fof(c_0_49,plain,
! [X31] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X31)
=> ( X31 != cCoq_2eInit_2eDatatypes_2eO
<=> p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X31)) ) ),
inference(fof_simplification,[status(thm)],['Coq.Arith.PeanoNat.Nat.neq_0_lt_0']) ).
fof(c_0_50,plain,
! [X1012,X1013,X1014,X1015,X1016,X1018] :
( ( ~ cType___24t(X1012)
| ~ cType___24t(X1013)
| ~ c_24__type__706___24t(X1012,X1013,X1014)
| ~ cLF_2ePoly_2elist___24t(X1012,X1015)
| ~ t(X1016,X1013)
| cLogic_2eIn___24a3(X1013,X1016,cLF_2ePoly_2emap___24a4(X1012,X1013,X1014,X1015))
| ~ cLogic_2eIn___24a3(X1012,X1018,X1015)
| happ(X1014,X1018) != X1016
| ~ t(X1018,X1012) )
& ( ~ cType___24t(X1012)
| ~ cType___24t(X1013)
| ~ c_24__type__706___24t(X1012,X1013,X1014)
| ~ cLF_2ePoly_2elist___24t(X1012,X1015)
| ~ t(X1016,X1013)
| ~ cLogic_2eIn___24a3(X1013,X1016,cLF_2ePoly_2emap___24a4(X1012,X1013,X1014,X1015))
| cLogic_2eIn___24a3(X1012,esk7_5(X1012,X1013,X1014,X1015,X1016),X1015) )
& ( ~ cType___24t(X1012)
| ~ cType___24t(X1013)
| ~ c_24__type__706___24t(X1012,X1013,X1014)
| ~ cLF_2ePoly_2elist___24t(X1012,X1015)
| ~ t(X1016,X1013)
| ~ cLogic_2eIn___24a3(X1013,X1016,cLF_2ePoly_2emap___24a4(X1012,X1013,X1014,X1015))
| happ(X1014,esk7_5(X1012,X1013,X1014,X1015,X1016)) = X1016 )
& ( ~ cType___24t(X1012)
| ~ cType___24t(X1013)
| ~ c_24__type__706___24t(X1012,X1013,X1014)
| ~ cLF_2ePoly_2elist___24t(X1012,X1015)
| ~ t(X1016,X1013)
| ~ cLogic_2eIn___24a3(X1013,X1016,cLF_2ePoly_2emap___24a4(X1012,X1013,X1014,X1015))
| t(esk7_5(X1012,X1013,X1014,X1015,X1016),X1012) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Logic.In_map_iff'])])])])])]) ).
cnf(c_0_51,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(esk18_3(X1,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703))
| c_24__type__706___24t(X1,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_39])]) ).
cnf(c_0_52,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(esk18_3(cCoq_2eInit_2eDatatypes_2enat,X1,X2))
| c_24__type__706___24t(cCoq_2eInit_2eDatatypes_2enat,X1,X2) ),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
cnf(c_0_53,negated_conjecture,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,esk1_0))
| cCoq_2eInit_2ePeano_2ele___24a2(esk1_0,X1) ),
inference(spm,[status(thm)],[c_0_44,c_0_31]) ).
cnf(c_0_54,plain,
( ~ cCoq_2eInit_2ePeano_2ele___24a2(X2,X1)
| ~ cCoq_2eInit_2ePeano_2ele___24a2(X1,X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_55,negated_conjecture,
cCoq_2eInit_2ePeano_2ele___24a2(cCoq_2eInit_2eDatatypes_2eO,esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_31])]),c_0_48]) ).
fof(c_0_56,plain,
! [X1440] :
( ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1440)
| X1440 != cCoq_2eInit_2eDatatypes_2eO
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1440)) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1440)
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1440))
| X1440 = cCoq_2eInit_2eDatatypes_2eO ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])])]) ).
cnf(c_0_57,plain,
( ~ cType___24t(X1)
| ~ cType___24t(X2)
| ~ c_24__type__706___24t(X1,X2,X3)
| ~ cLF_2ePoly_2elist___24t(X1,X4)
| ~ t(X5,X2)
| ~ cLogic_2eIn___24a3(X2,X5,cLF_2ePoly_2emap___24a4(X1,X2,X3,X4))
| t(esk7_5(X1,X2,X3,X4,X5),X1) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_58,negated_conjecture,
cLogic_2eIn___24a3(cCoq_2eInit_2eDatatypes_2enat,esk1_0,cLF_2ePoly_2emap___24a4(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,esk2_0)),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_59,plain,
c_24__type__706___24t(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703),
inference(spm,[status(thm)],[c_0_51,c_0_52]) ).
cnf(c_0_60,negated_conjecture,
cLF_2ePoly_2elist___24t(cCoq_2eInit_2eDatatypes_2enat,esk2_0),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_61,plain,
cType___24t(cCoq_2eInit_2eDatatypes_2enat),
inference(split_conjunct,[status(thm)],['$_typeof_Coq.Init.Datatypes.nat']) ).
fof(c_0_62,plain,
! [X1215,X1216] :
( ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1215)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1216)
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eNat_2emul___24a2(X1215,X1216)))
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1216))
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1215)) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1215)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1216)
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eNat_2emul___24a2(X1215,X1216)))
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1216)) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1215)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1216)
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eNat_2emul___24a2(X1215,X1216)))
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1215)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Arith.PeanoNat.Nat.lt_0_mul\\'])])])])]) ).
cnf(c_0_63,plain,
( ~ cType___24t(X2)
| ~ cType___24t(X3)
| ~ c_24__type__706___24t(X2,X3,X1)
| ~ cLF_2ePoly_2elist___24t(X2,X4)
| ~ t(X5,X3)
| ~ cLogic_2eIn___24a3(X3,X5,cLF_2ePoly_2emap___24a4(X2,X3,X1,X4))
| happ(X1,esk7_5(X2,X3,X1,X4,X5)) = X5 ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_64,negated_conjecture,
( p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,esk1_0))
| cCoq_2eInit_2ePeano_2ele___24a2(esk1_0,cCoq_2eInit_2eDatatypes_2eO) ),
inference(spm,[status(thm)],[c_0_53,c_0_39]) ).
cnf(c_0_65,negated_conjecture,
~ cCoq_2eInit_2ePeano_2ele___24a2(esk1_0,cCoq_2eInit_2eDatatypes_2eO),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_39]),c_0_31])]),c_0_48]) ).
cnf(c_0_66,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| X1 != cCoq_2eInit_2eDatatypes_2eO
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_67,negated_conjecture,
( ~ t(esk1_0,cCoq_2eInit_2eDatatypes_2enat)
| t(esk7_5(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,esk2_0,esk1_0),cCoq_2eInit_2eDatatypes_2enat) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_59]),c_0_60]),c_0_61])]) ).
cnf(c_0_68,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| ~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eNat_2emul___24a2(X2,X1)))
| p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
cnf(c_0_69,negated_conjecture,
( ~ t(esk1_0,cCoq_2eInit_2eDatatypes_2enat)
| cCoq_2eInit_2eNat_2emul___24a2(esk7_5(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,esk2_0,esk1_0),cCoq_2eInit_2eDatatypes_2eO) = esk1_0 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_58]),c_0_33]),c_0_59]),c_0_60]),c_0_61])]) ).
cnf(c_0_70,negated_conjecture,
p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,esk1_0)),
inference(sr,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_71,plain,
~ p(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eInit_2eDatatypes_2eO,cCoq_2eInit_2eDatatypes_2eO)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[c_0_66]),c_0_39])]) ).
cnf(c_0_72,negated_conjecture,
( ~ t(esk1_0,cCoq_2eInit_2eDatatypes_2enat)
| cCoq_2eInit_2eDatatypes_2enat___24t(esk7_5(cCoq_2eInit_2eDatatypes_2enat,cCoq_2eInit_2eDatatypes_2enat,c_24__lam__174703,esk2_0,esk1_0)) ),
inference(spm,[status(thm)],[c_0_42,c_0_67]) ).
cnf(c_0_73,negated_conjecture,
~ t(esk1_0,cCoq_2eInit_2eDatatypes_2enat),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_69]),c_0_39]),c_0_70])]),c_0_71]),c_0_72]) ).
cnf(c_0_74,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_25]),c_0_31])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV645+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n020.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 07:35:17 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/0.79 % Version: 3.5.1
% 0.31/0.79 % Preprocessing class: FMLLSMSLSSSNFFN.
% 0.31/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.79 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 0.31/0.79 % Starting new_bool_3 with 300s (1) cores
% 0.31/0.79 % Starting new_bool_1 with 300s (1) cores
% 0.31/0.79 % Starting sh5l with 300s (1) cores
% 0.31/0.79 % new_bool_1 with pid 2389852 completed with status 0
% 0.31/0.79 % Result found by new_bool_1
% 0.31/0.79 % Preprocessing class: FMLLSMSLSSSNFFN.
% 0.31/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.79 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 0.31/0.79 % Starting new_bool_3 with 300s (1) cores
% 0.31/0.79 % Starting new_bool_1 with 300s (1) cores
% 0.31/0.79 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.31/0.79 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.31/0.79 % Search class: FGHSS-FSLM32-DFFFFFNN
% 0.31/0.79 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.31/0.79 % Starting SubtermCWHack with 31s (1) cores
% 0.31/0.79 % SubtermCWHack with pid 2389855 completed with status 0
% 0.31/0.79 % Result found by SubtermCWHack
% 0.31/0.79 % Preprocessing class: FMLLSMSLSSSNFFN.
% 0.31/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.31/0.79 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 0.31/0.79 % Starting new_bool_3 with 300s (1) cores
% 0.31/0.79 % Starting new_bool_1 with 300s (1) cores
% 0.31/0.79 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.31/0.79 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.31/0.79 % Search class: FGHSS-FSLM32-DFFFFFNN
% 0.31/0.79 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.31/0.79 % Starting SubtermCWHack with 31s (1) cores
% 0.31/0.79 % Preprocessing time : 0.006 s
% 0.31/0.79
% 0.31/0.79 % Proof found!
% 0.31/0.79 % SZS status Theorem
% 0.31/0.79 % SZS output start CNFRefutation
% See solution above
% 0.31/0.79 % Parsed axioms : 1985
% 0.31/0.79 % Removed by relevancy pruning/SinE : 1771
% 0.31/0.79 % Initial clauses : 316
% 0.31/0.79 % Removed in clause preprocessing : 32
% 0.31/0.79 % Initial clauses in saturation : 284
% 0.31/0.79 % Processed clauses : 3781
% 0.31/0.79 % ...of these trivial : 3
% 0.31/0.79 % ...subsumed : 3031
% 0.31/0.79 % ...remaining for further processing : 747
% 0.31/0.79 % Other redundant clauses eliminated : 113
% 0.31/0.79 % Clauses deleted for lack of memory : 0
% 0.31/0.79 % Backward-subsumed : 36
% 0.31/0.79 % Backward-rewritten : 12
% 0.31/0.79 % Generated clauses : 15402
% 0.31/0.79 % ...of the previous two non-redundant : 13176
% 0.31/0.79 % ...aggressively subsumed : 0
% 0.31/0.79 % Contextual simplify-reflections : 74
% 0.31/0.79 % Paramodulations : 15279
% 0.31/0.79 % Factorizations : 0
% 0.31/0.79 % NegExts : 0
% 0.31/0.79 % Equation resolutions : 121
% 0.31/0.79 % Disequality decompositions : 0
% 0.31/0.79 % Total rewrite steps : 10924
% 0.31/0.79 % ...of those cached : 10899
% 0.31/0.79 % Propositional unsat checks : 0
% 0.31/0.79 % Propositional check models : 0
% 0.31/0.79 % Propositional check unsatisfiable : 0
% 0.31/0.79 % Propositional clauses : 0
% 0.31/0.79 % Propositional clauses after purity: 0
% 0.31/0.79 % Propositional unsat core size : 0
% 0.31/0.79 % Propositional preprocessing time : 0.000
% 0.31/0.79 % Propositional encoding time : 0.000
% 0.31/0.79 % Propositional solver time : 0.000
% 0.31/0.79 % Success case prop preproc time : 0.000
% 0.31/0.79 % Success case prop encoding time : 0.000
% 0.31/0.79 % Success case prop solver time : 0.000
% 0.31/0.79 % Current number of processed clauses : 653
% 0.31/0.79 % Positive orientable unit clauses : 30
% 0.31/0.79 % Positive unorientable unit clauses: 0
% 0.31/0.79 % Negative unit clauses : 11
% 0.31/0.79 % Non-unit-clauses : 612
% 0.31/0.79 % Current number of unprocessed clauses: 9590
% 0.31/0.79 % ...number of literals in the above : 48666
% 0.31/0.79 % Current number of archived formulas : 0
% 0.31/0.79 % Current number of archived clauses : 52
% 0.31/0.79 % Clause-clause subsumption calls (NU) : 106190
% 0.31/0.79 % Rec. Clause-clause subsumption calls : 61357
% 0.31/0.79 % Non-unit clause-clause subsumptions : 2752
% 0.31/0.79 % Unit Clause-clause subsumption calls : 605
% 0.31/0.79 % Rewrite failures with RHS unbound : 0
% 0.31/0.79 % BW rewrite match attempts : 7
% 0.31/0.79 % BW rewrite match successes : 7
% 0.31/0.79 % Condensation attempts : 0
% 0.31/0.79 % Condensation successes : 0
% 0.31/0.79 % Termbank termtop insertions : 359479
% 0.31/0.79 % Search garbage collected termcells : 24919
% 0.31/0.79
% 0.31/0.79 % -------------------------------------------------
% 0.31/0.79 % User time : 0.178 s
% 0.31/0.79 % System time : 0.021 s
% 0.31/0.79 % Total time : 0.199 s
% 0.31/0.79 % Maximum resident set size: 10136 pages
% 0.31/0.79
% 0.31/0.79 % -------------------------------------------------
% 0.31/0.79 % User time : 0.335 s
% 0.31/0.79 % System time : 0.029 s
% 0.31/0.79 % Total time : 0.364 s
% 0.31/0.79 % Maximum resident set size: 8448 pages
% 0.31/0.79 % E exiting
%------------------------------------------------------------------------------