%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV634+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 12:58:28 PM UTC 2026
% Result : Theorem 36.56s 6.27s
% Output : Refutation 37.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 96
% Syntax : Number of formulae : 554 ( 165 unt; 89 def)
% Number of atoms : 1174 ( 107 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1166 ( 546 ~; 534 |; 28 &)
% ( 43 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 45 ( 10 avg)
% Number of predicates : 48 ( 46 usr; 42 prp; 0-2 aty)
% Number of functors : 58 ( 58 usr; 52 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 47 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f85,axiom,
cCoq_2eInit_2eNat_2eone = cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_def_Coq.Init.Nat.one') ).
fof(f93,axiom,
cCoq_2eInit_2eNat_2esucc = cCoq_2eInit_2eDatatypes_2eS,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_def_Coq.Init.Nat.succ') ).
fof(f647,axiom,
! [X0] :
( c_24__type__7___24t(X0)
<=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_type_7') ).
fof(f799,axiom,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eNat_2eone),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_typeof_Coq.Init.Nat.one') ).
fof(f807,axiom,
c_24__type__7___24t(cCoq_2eInit_2eNat_2esucc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_typeof_Coq.Init.Nat.succ') ).
fof(f1908,axiom,
! [X0] : happ(cCoq_2eInit_2eDatatypes_2eS,X0) = cCoq_2eInit_2eDatatypes_2eS___24a1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Coq.Init.Datatypes.S_$a1') ).
fof(f2535,conjecture,
! [X0] :
( c_24__type__912___24t(X0)
=> ! [X1] :
( c_24__type__16291___24t(X1)
=> ( ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& p(happ(happ(X0,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),X2)) )
=> ( ! [X3] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X3)
=> ! [X4] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X4)
=> ( p(happ(happ(X0,X3),X4))
=> p(happ(X1,X3)) ) ) )
=> p(happ(X1,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO)))))))))))))))))))))))))))))))))))))))))))) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f2536,negated_conjecture,
~ ! [X0] :
( c_24__type__912___24t(X0)
=> ! [X1] :
( c_24__type__16291___24t(X1)
=> ( ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& p(happ(happ(X0,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),X2)) )
=> ( ! [X3] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X3)
=> ! [X4] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X4)
=> ( p(happ(happ(X0,X3),X4))
=> p(happ(X1,X3)) ) ) )
=> p(happ(X1,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO)))))))))))))))))))))))))))))))))))))))))))) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2535]) ).
fof(f3192,plain,
! [X0] :
( c_24__type__7___24t(X0)
<=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X1))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) ),
inference(ennf_transformation,[],[f647]) ).
fof(f4271,plain,
? [X0] :
( ? [X1] :
( ~ p(happ(X1,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))))
& ! [X3] :
( ! [X4] :
( p(happ(X1,X3))
| ~ p(happ(happ(X0,X3),X4))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& p(happ(happ(X0,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),X2)) )
& c_24__type__16291___24t(X1) )
& c_24__type__912___24t(X0) ),
inference(ennf_transformation,[],[f2536]) ).
fof(f4272,plain,
? [X0] :
( ? [X1] :
( ~ p(happ(X1,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))))
& ! [X3] :
( ! [X4] :
( p(happ(X1,X3))
| ~ p(happ(happ(X0,X3),X4))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& p(happ(happ(X0,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),X2)) )
& c_24__type__16291___24t(X1) )
& c_24__type__912___24t(X0) ),
inference(flattening,[],[f4271]) ).
fof(f6453,plain,
! [X0] :
( ( c_24__type__7___24t(X0)
| ? [X1] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X1))
& cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
& ( ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X1))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) )
| ~ c_24__type__7___24t(X0) ) ),
inference(nnf_transformation,[],[f3192]) ).
fof(f6454,plain,
! [X0] :
( ( c_24__type__7___24t(X0)
| ? [X1] :
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X1))
& cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
& ( ! [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
| ~ c_24__type__7___24t(X0) ) ),
inference(rectify,[],[f6453]) ).
fof(f6455,plain,
! [X0] :
( ( c_24__type__7___24t(X0)
| ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,sK1479(X0)))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK1479(X0)) ) )
& ( ! [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
| ~ c_24__type__7___24t(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1479]),skolemize(X1,sK1479(X0))],[f6454]) ).
fof(f7242,plain,
? [X0] :
( ? [X1] :
( ~ p(happ(X1,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))))
& ! [X2] :
( ! [X3] :
( p(happ(X1,X2))
| ~ p(happ(happ(X0,X2),X3))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
& ? [X4] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X4)
& p(happ(happ(X0,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),X4)) )
& c_24__type__16291___24t(X1) )
& c_24__type__912___24t(X0) ),
inference(rectify,[],[f4272]) ).
fof(f7243,plain,
( ~ p(happ(sK1733,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))))
& ! [X2] :
( ! [X3] :
( p(happ(sK1733,X2))
| ~ p(happ(happ(sK1732,X2),X3))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
& cCoq_2eInit_2eDatatypes_2enat___24t(sK1734)
& p(happ(happ(sK1732,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),sK1734))
& c_24__type__16291___24t(sK1733)
& c_24__type__912___24t(sK1732) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1732,sK1733,sK1734]),skolemize(X0,sK1732),skolemize(X1,sK1733),skolemize(X4,sK1734)],[f7242]) ).
fof(f7732,plain,
cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO) = cCoq_2eInit_2eNat_2eone,
inference(cnf_transformation,[],[f85]) ).
fof(f7768,plain,
cCoq_2eInit_2eNat_2esucc = cCoq_2eInit_2eDatatypes_2eS,
inference(cnf_transformation,[],[f93]) ).
fof(f10757,plain,
! [X2,X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(happ(X0,X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ c_24__type__7___24t(X0) ),
inference(cnf_transformation,[],[f6455]) ).
fof(f11099,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eNat_2eone),
inference(cnf_transformation,[],[f799]) ).
fof(f11107,plain,
c_24__type__7___24t(cCoq_2eInit_2eNat_2esucc),
inference(cnf_transformation,[],[f807]) ).
fof(f12577,plain,
! [X0] : cCoq_2eInit_2eDatatypes_2eS___24a1(X0) = happ(cCoq_2eInit_2eDatatypes_2eS,X0),
inference(cnf_transformation,[],[f1908]) ).
fof(f13544,plain,
p(happ(happ(sK1732,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),sK1734)),
inference(cnf_transformation,[],[f7243]) ).
fof(f13545,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(sK1734),
inference(cnf_transformation,[],[f7243]) ).
fof(f13546,plain,
! [X2,X3] :
( p(happ(sK1733,X2))
| ~ p(happ(happ(sK1732,X2),X3))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) ),
inference(cnf_transformation,[],[f7243]) ).
fof(f13547,plain,
~ p(happ(sK1733,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO)))))))))))))))))))))))))))))))))))))))))))),
inference(cnf_transformation,[],[f7243]) ).
fof(f13952,plain,
cCoq_2eInit_2eNat_2eone = happ(cCoq_2eInit_2eDatatypes_2eS,cCoq_2eInit_2eDatatypes_2eO),
inference(definition_unfolding,[],[f7732,f12577]) ).
fof(f15325,plain,
c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS),
inference(definition_unfolding,[],[f11107,f7768]) ).
fof(f16327,plain,
~ p(happ(sK1733,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,cCoq_2eInit_2eDatatypes_2eO)))))))))))))))))))))))))))))))))))))))))))),
inference(definition_unfolding,[],[f13547,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577]) ).
fof(f16328,plain,
p(happ(happ(sK1732,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,happ(cCoq_2eInit_2eDatatypes_2eS,cCoq_2eInit_2eDatatypes_2eO))))))))))))))))))))))))))))))))))))))))))),sK1734)),
inference(definition_unfolding,[],[f13544,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577,f12577]) ).
fof(f16416,definition,
sF1735 = happ(cCoq_2eInit_2eDatatypes_2eS,cCoq_2eInit_2eDatatypes_2eO),
introduced(definition,[new_symbols(definition,[sF1735])],[function_definition]) ).
fof(f16417,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,cCoq_2eInit_2eDatatypes_2eO) = sF1735,
inference(reorient_equations,[],[f16416]) ).
fof(f16418,definition,
sF1736 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1735),
introduced(definition,[new_symbols(definition,[sF1736])],[function_definition]) ).
fof(f16419,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1735) = sF1736,
inference(reorient_equations,[],[f16418]) ).
fof(f16420,definition,
sF1737 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1736),
introduced(definition,[new_symbols(definition,[sF1737])],[function_definition]) ).
fof(f16421,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1736) = sF1737,
inference(reorient_equations,[],[f16420]) ).
fof(f16422,definition,
sF1738 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1737),
introduced(definition,[new_symbols(definition,[sF1738])],[function_definition]) ).
fof(f16423,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1737) = sF1738,
inference(reorient_equations,[],[f16422]) ).
fof(f16424,definition,
sF1739 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1738),
introduced(definition,[new_symbols(definition,[sF1739])],[function_definition]) ).
fof(f16425,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1738) = sF1739,
inference(reorient_equations,[],[f16424]) ).
fof(f16426,definition,
sF1740 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1739),
introduced(definition,[new_symbols(definition,[sF1740])],[function_definition]) ).
fof(f16427,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1739) = sF1740,
inference(reorient_equations,[],[f16426]) ).
fof(f16428,definition,
sF1741 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1740),
introduced(definition,[new_symbols(definition,[sF1741])],[function_definition]) ).
fof(f16429,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1740) = sF1741,
inference(reorient_equations,[],[f16428]) ).
fof(f16430,definition,
sF1742 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1741),
introduced(definition,[new_symbols(definition,[sF1742])],[function_definition]) ).
fof(f16431,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1741) = sF1742,
inference(reorient_equations,[],[f16430]) ).
fof(f16432,definition,
sF1743 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1742),
introduced(definition,[new_symbols(definition,[sF1743])],[function_definition]) ).
fof(f16433,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1742) = sF1743,
inference(reorient_equations,[],[f16432]) ).
fof(f16434,definition,
sF1744 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1743),
introduced(definition,[new_symbols(definition,[sF1744])],[function_definition]) ).
fof(f16435,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1743) = sF1744,
inference(reorient_equations,[],[f16434]) ).
fof(f16436,definition,
sF1745 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1744),
introduced(definition,[new_symbols(definition,[sF1745])],[function_definition]) ).
fof(f16437,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1744) = sF1745,
inference(reorient_equations,[],[f16436]) ).
fof(f16438,definition,
sF1746 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1745),
introduced(definition,[new_symbols(definition,[sF1746])],[function_definition]) ).
fof(f16439,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1745) = sF1746,
inference(reorient_equations,[],[f16438]) ).
fof(f16440,definition,
sF1747 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1746),
introduced(definition,[new_symbols(definition,[sF1747])],[function_definition]) ).
fof(f16441,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1746) = sF1747,
inference(reorient_equations,[],[f16440]) ).
fof(f16442,definition,
sF1748 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1747),
introduced(definition,[new_symbols(definition,[sF1748])],[function_definition]) ).
fof(f16443,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1747) = sF1748,
inference(reorient_equations,[],[f16442]) ).
fof(f16444,definition,
sF1749 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1748),
introduced(definition,[new_symbols(definition,[sF1749])],[function_definition]) ).
fof(f16445,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1748) = sF1749,
inference(reorient_equations,[],[f16444]) ).
fof(f16446,definition,
sF1750 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1749),
introduced(definition,[new_symbols(definition,[sF1750])],[function_definition]) ).
fof(f16447,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1749) = sF1750,
inference(reorient_equations,[],[f16446]) ).
fof(f16448,definition,
sF1751 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1750),
introduced(definition,[new_symbols(definition,[sF1751])],[function_definition]) ).
fof(f16449,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1750) = sF1751,
inference(reorient_equations,[],[f16448]) ).
fof(f16450,definition,
sF1752 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1751),
introduced(definition,[new_symbols(definition,[sF1752])],[function_definition]) ).
fof(f16451,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1751) = sF1752,
inference(reorient_equations,[],[f16450]) ).
fof(f16452,definition,
sF1753 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1752),
introduced(definition,[new_symbols(definition,[sF1753])],[function_definition]) ).
fof(f16453,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1752) = sF1753,
inference(reorient_equations,[],[f16452]) ).
fof(f16454,definition,
sF1754 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1753),
introduced(definition,[new_symbols(definition,[sF1754])],[function_definition]) ).
fof(f16455,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1753) = sF1754,
inference(reorient_equations,[],[f16454]) ).
fof(f16456,definition,
sF1755 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1754),
introduced(definition,[new_symbols(definition,[sF1755])],[function_definition]) ).
fof(f16457,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1754) = sF1755,
inference(reorient_equations,[],[f16456]) ).
fof(f16458,definition,
sF1756 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1755),
introduced(definition,[new_symbols(definition,[sF1756])],[function_definition]) ).
fof(f16459,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1755) = sF1756,
inference(reorient_equations,[],[f16458]) ).
fof(f16460,definition,
sF1757 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1756),
introduced(definition,[new_symbols(definition,[sF1757])],[function_definition]) ).
fof(f16461,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1756) = sF1757,
inference(reorient_equations,[],[f16460]) ).
fof(f16462,definition,
sF1758 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1757),
introduced(definition,[new_symbols(definition,[sF1758])],[function_definition]) ).
fof(f16463,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1757) = sF1758,
inference(reorient_equations,[],[f16462]) ).
fof(f16464,definition,
sF1759 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1758),
introduced(definition,[new_symbols(definition,[sF1759])],[function_definition]) ).
fof(f16465,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1758) = sF1759,
inference(reorient_equations,[],[f16464]) ).
fof(f16466,definition,
sF1760 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1759),
introduced(definition,[new_symbols(definition,[sF1760])],[function_definition]) ).
fof(f16467,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1759) = sF1760,
inference(reorient_equations,[],[f16466]) ).
fof(f16468,definition,
sF1761 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1760),
introduced(definition,[new_symbols(definition,[sF1761])],[function_definition]) ).
fof(f16469,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1760) = sF1761,
inference(reorient_equations,[],[f16468]) ).
fof(f16470,definition,
sF1762 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1761),
introduced(definition,[new_symbols(definition,[sF1762])],[function_definition]) ).
fof(f16471,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1761) = sF1762,
inference(reorient_equations,[],[f16470]) ).
fof(f16472,definition,
sF1763 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1762),
introduced(definition,[new_symbols(definition,[sF1763])],[function_definition]) ).
fof(f16473,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1762) = sF1763,
inference(reorient_equations,[],[f16472]) ).
fof(f16474,definition,
sF1764 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1763),
introduced(definition,[new_symbols(definition,[sF1764])],[function_definition]) ).
fof(f16475,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1763) = sF1764,
inference(reorient_equations,[],[f16474]) ).
fof(f16476,definition,
sF1765 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1764),
introduced(definition,[new_symbols(definition,[sF1765])],[function_definition]) ).
fof(f16477,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1764) = sF1765,
inference(reorient_equations,[],[f16476]) ).
fof(f16478,definition,
sF1766 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1765),
introduced(definition,[new_symbols(definition,[sF1766])],[function_definition]) ).
fof(f16479,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1765) = sF1766,
inference(reorient_equations,[],[f16478]) ).
fof(f16480,definition,
sF1767 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1766),
introduced(definition,[new_symbols(definition,[sF1767])],[function_definition]) ).
fof(f16481,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1766) = sF1767,
inference(reorient_equations,[],[f16480]) ).
fof(f16482,definition,
sF1768 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1767),
introduced(definition,[new_symbols(definition,[sF1768])],[function_definition]) ).
fof(f16483,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1767) = sF1768,
inference(reorient_equations,[],[f16482]) ).
fof(f16484,definition,
sF1769 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1768),
introduced(definition,[new_symbols(definition,[sF1769])],[function_definition]) ).
fof(f16485,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1768) = sF1769,
inference(reorient_equations,[],[f16484]) ).
fof(f16486,definition,
sF1770 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1769),
introduced(definition,[new_symbols(definition,[sF1770])],[function_definition]) ).
fof(f16487,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1769) = sF1770,
inference(reorient_equations,[],[f16486]) ).
fof(f16488,definition,
sF1771 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1770),
introduced(definition,[new_symbols(definition,[sF1771])],[function_definition]) ).
fof(f16489,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1770) = sF1771,
inference(reorient_equations,[],[f16488]) ).
fof(f16490,definition,
sF1772 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1771),
introduced(definition,[new_symbols(definition,[sF1772])],[function_definition]) ).
fof(f16491,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1771) = sF1772,
inference(reorient_equations,[],[f16490]) ).
fof(f16492,definition,
sF1773 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1772),
introduced(definition,[new_symbols(definition,[sF1773])],[function_definition]) ).
fof(f16493,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1772) = sF1773,
inference(reorient_equations,[],[f16492]) ).
fof(f16494,definition,
sF1774 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1773),
introduced(definition,[new_symbols(definition,[sF1774])],[function_definition]) ).
fof(f16495,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1773) = sF1774,
inference(reorient_equations,[],[f16494]) ).
fof(f16496,definition,
sF1775 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1774),
introduced(definition,[new_symbols(definition,[sF1775])],[function_definition]) ).
fof(f16497,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1774) = sF1775,
inference(reorient_equations,[],[f16496]) ).
fof(f16498,definition,
sF1776 = happ(cCoq_2eInit_2eDatatypes_2eS,sF1775),
introduced(definition,[new_symbols(definition,[sF1776])],[function_definition]) ).
fof(f16499,plain,
happ(cCoq_2eInit_2eDatatypes_2eS,sF1775) = sF1776,
inference(reorient_equations,[],[f16498]) ).
fof(f16500,definition,
sF1777 = happ(sK1733,sF1776),
introduced(definition,[new_symbols(definition,[sF1777])],[function_definition]) ).
fof(f16501,plain,
happ(sK1733,sF1776) = sF1777,
inference(reorient_equations,[],[f16500]) ).
fof(f16502,plain,
~ p(sF1777),
inference(definition_folding,[],[f16327,f16501,f16499,f16497,f16495,f16493,f16491,f16489,f16487,f16485,f16483,f16481,f16479,f16477,f16475,f16473,f16471,f16469,f16467,f16465,f16463,f16461,f16459,f16457,f16455,f16453,f16451,f16449,f16447,f16445,f16443,f16441,f16439,f16437,f16435,f16433,f16431,f16429,f16427,f16425,f16423,f16421,f16419,f16417]) ).
fof(f16503,definition,
! [X2] : sF1778(X2) = happ(sK1733,X2),
introduced(definition,[new_symbols(definition,[sF1778])],[function_definition]) ).
fof(f16504,plain,
! [X2] : happ(sK1733,X2) = sF1778(X2),
inference(reorient_equations,[],[f16503]) ).
fof(f16505,definition,
! [X2] : sF1779(X2) = happ(sK1732,X2),
introduced(definition,[new_symbols(definition,[sF1779])],[function_definition]) ).
fof(f16506,plain,
! [X2] : happ(sK1732,X2) = sF1779(X2),
inference(reorient_equations,[],[f16505]) ).
fof(f16507,definition,
! [X2,X3] : sF1780(X2,X3) = happ(sF1779(X2),X3),
introduced(definition,[new_symbols(definition,[sF1780])],[function_definition]) ).
fof(f16508,plain,
! [X2,X3] : happ(sF1779(X2),X3) = sF1780(X2,X3),
inference(reorient_equations,[],[f16507]) ).
fof(f16509,plain,
! [X2,X3] :
( ~ p(sF1780(X2,X3))
| p(sF1778(X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) ),
inference(definition_folding,[],[f13546,f16508,f16506,f16504]) ).
fof(f16510,definition,
sF1781 = happ(sK1732,sF1776),
introduced(definition,[new_symbols(definition,[sF1781])],[function_definition]) ).
fof(f16511,plain,
happ(sK1732,sF1776) = sF1781,
inference(reorient_equations,[],[f16510]) ).
fof(f16512,definition,
sF1782 = happ(sF1781,sK1734),
introduced(definition,[new_symbols(definition,[sF1782])],[function_definition]) ).
fof(f16513,plain,
happ(sF1781,sK1734) = sF1782,
inference(reorient_equations,[],[f16512]) ).
fof(f16514,plain,
p(sF1782),
inference(definition_folding,[],[f16328,f16513,f16511,f16499,f16497,f16495,f16493,f16491,f16489,f16487,f16485,f16483,f16481,f16479,f16477,f16475,f16473,f16471,f16469,f16467,f16465,f16463,f16461,f16459,f16457,f16455,f16453,f16451,f16449,f16447,f16445,f16443,f16441,f16439,f16437,f16435,f16433,f16431,f16429,f16427,f16425,f16423,f16421,f16419,f16417]) ).
fof(f16984,plain,
cCoq_2eInit_2eNat_2eone = sF1735,
inference(forward_demodulation,[],[f16417,f13952]) ).
fof(f16985,plain,
sF1781 = sF1779(sF1776),
inference(forward_demodulation,[],[f16511,f16506]) ).
fof(f17246,plain,
sF1777 = sF1778(sF1776),
inference(superposition,[],[f16501,f16504]) ).
fof(f17247,plain,
! [X0] : sF1780(sF1776,X0) = happ(sF1781,X0),
inference(superposition,[],[f16508,f16985]) ).
fof(f17310,definition,
( spl1783_41
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1775) ),
introduced(definition,[new_symbols(definition,[spl1783_41])],[avatar_definition]) ).
fof(f17311,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1775)
| ~ spl1783_41 ),
inference(avatar_component_clause,[],[f17310]) ).
fof(f17312,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1775)
| spl1783_41 ),
inference(avatar_component_clause,[],[f17310]) ).
fof(f17319,definition,
( spl1783_43
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1774) ),
introduced(definition,[new_symbols(definition,[spl1783_43])],[avatar_definition]) ).
fof(f17320,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1774)
| ~ spl1783_43 ),
inference(avatar_component_clause,[],[f17319]) ).
fof(f17321,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1774)
| spl1783_43 ),
inference(avatar_component_clause,[],[f17319]) ).
fof(f17328,definition,
( spl1783_45
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1773) ),
introduced(definition,[new_symbols(definition,[spl1783_45])],[avatar_definition]) ).
fof(f17329,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1773)
| ~ spl1783_45 ),
inference(avatar_component_clause,[],[f17328]) ).
fof(f17330,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1773)
| spl1783_45 ),
inference(avatar_component_clause,[],[f17328]) ).
fof(f17337,definition,
( spl1783_47
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1772) ),
introduced(definition,[new_symbols(definition,[spl1783_47])],[avatar_definition]) ).
fof(f17338,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1772)
| ~ spl1783_47 ),
inference(avatar_component_clause,[],[f17337]) ).
fof(f17339,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1772)
| spl1783_47 ),
inference(avatar_component_clause,[],[f17337]) ).
fof(f17346,definition,
( spl1783_49
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1771) ),
introduced(definition,[new_symbols(definition,[spl1783_49])],[avatar_definition]) ).
fof(f17347,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1771)
| ~ spl1783_49 ),
inference(avatar_component_clause,[],[f17346]) ).
fof(f17348,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1771)
| spl1783_49 ),
inference(avatar_component_clause,[],[f17346]) ).
fof(f17355,definition,
( spl1783_51
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1770) ),
introduced(definition,[new_symbols(definition,[spl1783_51])],[avatar_definition]) ).
fof(f17356,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1770)
| ~ spl1783_51 ),
inference(avatar_component_clause,[],[f17355]) ).
fof(f17357,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1770)
| spl1783_51 ),
inference(avatar_component_clause,[],[f17355]) ).
fof(f17364,definition,
( spl1783_53
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1769) ),
introduced(definition,[new_symbols(definition,[spl1783_53])],[avatar_definition]) ).
fof(f17365,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1769)
| ~ spl1783_53 ),
inference(avatar_component_clause,[],[f17364]) ).
fof(f17366,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1769)
| spl1783_53 ),
inference(avatar_component_clause,[],[f17364]) ).
fof(f17373,definition,
( spl1783_55
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1768) ),
introduced(definition,[new_symbols(definition,[spl1783_55])],[avatar_definition]) ).
fof(f17374,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1768)
| ~ spl1783_55 ),
inference(avatar_component_clause,[],[f17373]) ).
fof(f17375,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1768)
| spl1783_55 ),
inference(avatar_component_clause,[],[f17373]) ).
fof(f17382,definition,
( spl1783_57
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1767) ),
introduced(definition,[new_symbols(definition,[spl1783_57])],[avatar_definition]) ).
fof(f17383,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1767)
| ~ spl1783_57 ),
inference(avatar_component_clause,[],[f17382]) ).
fof(f17384,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1767)
| spl1783_57 ),
inference(avatar_component_clause,[],[f17382]) ).
fof(f17391,definition,
( spl1783_59
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1766) ),
introduced(definition,[new_symbols(definition,[spl1783_59])],[avatar_definition]) ).
fof(f17392,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1766)
| ~ spl1783_59 ),
inference(avatar_component_clause,[],[f17391]) ).
fof(f17393,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1766)
| spl1783_59 ),
inference(avatar_component_clause,[],[f17391]) ).
fof(f17400,definition,
( spl1783_61
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1765) ),
introduced(definition,[new_symbols(definition,[spl1783_61])],[avatar_definition]) ).
fof(f17401,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1765)
| ~ spl1783_61 ),
inference(avatar_component_clause,[],[f17400]) ).
fof(f17402,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1765)
| spl1783_61 ),
inference(avatar_component_clause,[],[f17400]) ).
fof(f17409,definition,
( spl1783_63
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1764) ),
introduced(definition,[new_symbols(definition,[spl1783_63])],[avatar_definition]) ).
fof(f17410,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1764)
| ~ spl1783_63 ),
inference(avatar_component_clause,[],[f17409]) ).
fof(f17411,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1764)
| spl1783_63 ),
inference(avatar_component_clause,[],[f17409]) ).
fof(f17418,definition,
( spl1783_65
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1763) ),
introduced(definition,[new_symbols(definition,[spl1783_65])],[avatar_definition]) ).
fof(f17419,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1763)
| ~ spl1783_65 ),
inference(avatar_component_clause,[],[f17418]) ).
fof(f17420,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1763)
| spl1783_65 ),
inference(avatar_component_clause,[],[f17418]) ).
fof(f17427,definition,
( spl1783_67
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1762) ),
introduced(definition,[new_symbols(definition,[spl1783_67])],[avatar_definition]) ).
fof(f17428,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1762)
| ~ spl1783_67 ),
inference(avatar_component_clause,[],[f17427]) ).
fof(f17429,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1762)
| spl1783_67 ),
inference(avatar_component_clause,[],[f17427]) ).
fof(f17436,definition,
( spl1783_69
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1761) ),
introduced(definition,[new_symbols(definition,[spl1783_69])],[avatar_definition]) ).
fof(f17437,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1761)
| ~ spl1783_69 ),
inference(avatar_component_clause,[],[f17436]) ).
fof(f17438,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1761)
| spl1783_69 ),
inference(avatar_component_clause,[],[f17436]) ).
fof(f17445,definition,
( spl1783_71
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1760) ),
introduced(definition,[new_symbols(definition,[spl1783_71])],[avatar_definition]) ).
fof(f17446,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1760)
| ~ spl1783_71 ),
inference(avatar_component_clause,[],[f17445]) ).
fof(f17447,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1760)
| spl1783_71 ),
inference(avatar_component_clause,[],[f17445]) ).
fof(f17454,definition,
( spl1783_73
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1759) ),
introduced(definition,[new_symbols(definition,[spl1783_73])],[avatar_definition]) ).
fof(f17455,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1759)
| ~ spl1783_73 ),
inference(avatar_component_clause,[],[f17454]) ).
fof(f17456,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1759)
| spl1783_73 ),
inference(avatar_component_clause,[],[f17454]) ).
fof(f17463,definition,
( spl1783_75
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1758) ),
introduced(definition,[new_symbols(definition,[spl1783_75])],[avatar_definition]) ).
fof(f17464,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1758)
| ~ spl1783_75 ),
inference(avatar_component_clause,[],[f17463]) ).
fof(f17465,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1758)
| spl1783_75 ),
inference(avatar_component_clause,[],[f17463]) ).
fof(f17472,definition,
( spl1783_77
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1757) ),
introduced(definition,[new_symbols(definition,[spl1783_77])],[avatar_definition]) ).
fof(f17473,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1757)
| ~ spl1783_77 ),
inference(avatar_component_clause,[],[f17472]) ).
fof(f17474,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1757)
| spl1783_77 ),
inference(avatar_component_clause,[],[f17472]) ).
fof(f17481,definition,
( spl1783_79
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1756) ),
introduced(definition,[new_symbols(definition,[spl1783_79])],[avatar_definition]) ).
fof(f17482,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1756)
| ~ spl1783_79 ),
inference(avatar_component_clause,[],[f17481]) ).
fof(f17483,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1756)
| spl1783_79 ),
inference(avatar_component_clause,[],[f17481]) ).
fof(f17490,definition,
( spl1783_81
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1755) ),
introduced(definition,[new_symbols(definition,[spl1783_81])],[avatar_definition]) ).
fof(f17491,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1755)
| ~ spl1783_81 ),
inference(avatar_component_clause,[],[f17490]) ).
fof(f17492,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1755)
| spl1783_81 ),
inference(avatar_component_clause,[],[f17490]) ).
fof(f17499,definition,
( spl1783_83
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1754) ),
introduced(definition,[new_symbols(definition,[spl1783_83])],[avatar_definition]) ).
fof(f17500,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1754)
| ~ spl1783_83 ),
inference(avatar_component_clause,[],[f17499]) ).
fof(f17501,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1754)
| spl1783_83 ),
inference(avatar_component_clause,[],[f17499]) ).
fof(f17508,definition,
( spl1783_85
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1753) ),
introduced(definition,[new_symbols(definition,[spl1783_85])],[avatar_definition]) ).
fof(f17509,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1753)
| ~ spl1783_85 ),
inference(avatar_component_clause,[],[f17508]) ).
fof(f17510,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1753)
| spl1783_85 ),
inference(avatar_component_clause,[],[f17508]) ).
fof(f17517,definition,
( spl1783_87
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1752) ),
introduced(definition,[new_symbols(definition,[spl1783_87])],[avatar_definition]) ).
fof(f17518,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1752)
| ~ spl1783_87 ),
inference(avatar_component_clause,[],[f17517]) ).
fof(f17519,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1752)
| spl1783_87 ),
inference(avatar_component_clause,[],[f17517]) ).
fof(f17526,definition,
( spl1783_89
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1751) ),
introduced(definition,[new_symbols(definition,[spl1783_89])],[avatar_definition]) ).
fof(f17527,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1751)
| ~ spl1783_89 ),
inference(avatar_component_clause,[],[f17526]) ).
fof(f17528,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1751)
| spl1783_89 ),
inference(avatar_component_clause,[],[f17526]) ).
fof(f17535,definition,
( spl1783_91
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1750) ),
introduced(definition,[new_symbols(definition,[spl1783_91])],[avatar_definition]) ).
fof(f17536,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1750)
| ~ spl1783_91 ),
inference(avatar_component_clause,[],[f17535]) ).
fof(f17537,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1750)
| spl1783_91 ),
inference(avatar_component_clause,[],[f17535]) ).
fof(f17544,definition,
( spl1783_93
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1749) ),
introduced(definition,[new_symbols(definition,[spl1783_93])],[avatar_definition]) ).
fof(f17545,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1749)
| ~ spl1783_93 ),
inference(avatar_component_clause,[],[f17544]) ).
fof(f17546,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1749)
| spl1783_93 ),
inference(avatar_component_clause,[],[f17544]) ).
fof(f17553,definition,
( spl1783_95
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1748) ),
introduced(definition,[new_symbols(definition,[spl1783_95])],[avatar_definition]) ).
fof(f17554,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1748)
| ~ spl1783_95 ),
inference(avatar_component_clause,[],[f17553]) ).
fof(f17555,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1748)
| spl1783_95 ),
inference(avatar_component_clause,[],[f17553]) ).
fof(f17562,definition,
( spl1783_97
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1747) ),
introduced(definition,[new_symbols(definition,[spl1783_97])],[avatar_definition]) ).
fof(f17563,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1747)
| ~ spl1783_97 ),
inference(avatar_component_clause,[],[f17562]) ).
fof(f17564,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1747)
| spl1783_97 ),
inference(avatar_component_clause,[],[f17562]) ).
fof(f17571,definition,
( spl1783_99
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1746) ),
introduced(definition,[new_symbols(definition,[spl1783_99])],[avatar_definition]) ).
fof(f17572,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1746)
| ~ spl1783_99 ),
inference(avatar_component_clause,[],[f17571]) ).
fof(f17573,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1746)
| spl1783_99 ),
inference(avatar_component_clause,[],[f17571]) ).
fof(f17580,definition,
( spl1783_101
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1745) ),
introduced(definition,[new_symbols(definition,[spl1783_101])],[avatar_definition]) ).
fof(f17581,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1745)
| ~ spl1783_101 ),
inference(avatar_component_clause,[],[f17580]) ).
fof(f17582,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1745)
| spl1783_101 ),
inference(avatar_component_clause,[],[f17580]) ).
fof(f17589,definition,
( spl1783_103
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1744) ),
introduced(definition,[new_symbols(definition,[spl1783_103])],[avatar_definition]) ).
fof(f17590,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1744)
| ~ spl1783_103 ),
inference(avatar_component_clause,[],[f17589]) ).
fof(f17591,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1744)
| spl1783_103 ),
inference(avatar_component_clause,[],[f17589]) ).
fof(f17598,definition,
( spl1783_105
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1743) ),
introduced(definition,[new_symbols(definition,[spl1783_105])],[avatar_definition]) ).
fof(f17599,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1743)
| ~ spl1783_105 ),
inference(avatar_component_clause,[],[f17598]) ).
fof(f17600,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1743)
| spl1783_105 ),
inference(avatar_component_clause,[],[f17598]) ).
fof(f17607,definition,
( spl1783_107
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1742) ),
introduced(definition,[new_symbols(definition,[spl1783_107])],[avatar_definition]) ).
fof(f17608,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1742)
| ~ spl1783_107 ),
inference(avatar_component_clause,[],[f17607]) ).
fof(f17609,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1742)
| spl1783_107 ),
inference(avatar_component_clause,[],[f17607]) ).
fof(f17616,definition,
( spl1783_109
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1741) ),
introduced(definition,[new_symbols(definition,[spl1783_109])],[avatar_definition]) ).
fof(f17617,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1741)
| ~ spl1783_109 ),
inference(avatar_component_clause,[],[f17616]) ).
fof(f17618,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1741)
| spl1783_109 ),
inference(avatar_component_clause,[],[f17616]) ).
fof(f17625,definition,
( spl1783_111
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1740) ),
introduced(definition,[new_symbols(definition,[spl1783_111])],[avatar_definition]) ).
fof(f17626,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1740)
| ~ spl1783_111 ),
inference(avatar_component_clause,[],[f17625]) ).
fof(f17627,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1740)
| spl1783_111 ),
inference(avatar_component_clause,[],[f17625]) ).
fof(f17634,definition,
( spl1783_113
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1739) ),
introduced(definition,[new_symbols(definition,[spl1783_113])],[avatar_definition]) ).
fof(f17635,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1739)
| ~ spl1783_113 ),
inference(avatar_component_clause,[],[f17634]) ).
fof(f17636,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1739)
| spl1783_113 ),
inference(avatar_component_clause,[],[f17634]) ).
fof(f17643,definition,
( spl1783_115
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1738) ),
introduced(definition,[new_symbols(definition,[spl1783_115])],[avatar_definition]) ).
fof(f17644,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1738)
| ~ spl1783_115 ),
inference(avatar_component_clause,[],[f17643]) ).
fof(f17645,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1738)
| spl1783_115 ),
inference(avatar_component_clause,[],[f17643]) ).
fof(f17652,definition,
( spl1783_117
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1737) ),
introduced(definition,[new_symbols(definition,[spl1783_117])],[avatar_definition]) ).
fof(f17653,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1737)
| ~ spl1783_117 ),
inference(avatar_component_clause,[],[f17652]) ).
fof(f17654,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1737)
| spl1783_117 ),
inference(avatar_component_clause,[],[f17652]) ).
fof(f17661,definition,
( spl1783_119
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1736) ),
introduced(definition,[new_symbols(definition,[spl1783_119])],[avatar_definition]) ).
fof(f17662,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1736)
| ~ spl1783_119 ),
inference(avatar_component_clause,[],[f17661]) ).
fof(f17663,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1736)
| spl1783_119 ),
inference(avatar_component_clause,[],[f17661]) ).
fof(f17680,definition,
( spl1783_123
<=> cCoq_2eInit_2eDatatypes_2enat___24t(sF1776) ),
introduced(definition,[new_symbols(definition,[spl1783_123])],[avatar_definition]) ).
fof(f17681,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1776)
| ~ spl1783_123 ),
inference(avatar_component_clause,[],[f17680]) ).
fof(f17682,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1776)
| spl1783_123 ),
inference(avatar_component_clause,[],[f17680]) ).
fof(f17982,plain,
! [X0] :
( ~ p(happ(sF1781,X0))
| p(sF1778(sF1776))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1776) ),
inference(superposition,[],[f16509,f17247]) ).
fof(f65329,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1736)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1735)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16419]) ).
fof(f65330,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1737)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1736)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16421]) ).
fof(f65331,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1738)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1737)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16423]) ).
fof(f65332,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1739)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1738)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16425]) ).
fof(f65333,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1740)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1739)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16427]) ).
fof(f65334,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1741)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1740)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16429]) ).
fof(f65335,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1742)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1741)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16431]) ).
fof(f65336,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1743)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1742)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16433]) ).
fof(f65337,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1744)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1743)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16435]) ).
fof(f65338,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1745)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1744)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16437]) ).
fof(f65339,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1746)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1745)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16439]) ).
fof(f65340,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1747)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1746)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16441]) ).
fof(f65341,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1748)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1747)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16443]) ).
fof(f65342,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1749)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1748)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16445]) ).
fof(f65343,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1750)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1749)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16447]) ).
fof(f65344,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1751)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1750)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16449]) ).
fof(f65345,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1752)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1751)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16451]) ).
fof(f65346,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1753)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1752)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16453]) ).
fof(f65347,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1754)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1753)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16455]) ).
fof(f65348,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1755)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1754)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16457]) ).
fof(f65349,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1756)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1755)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16459]) ).
fof(f65350,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1757)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1756)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16461]) ).
fof(f65351,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1758)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1757)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16463]) ).
fof(f65352,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1759)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1758)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16465]) ).
fof(f65353,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1760)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1759)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16467]) ).
fof(f65354,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1761)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1760)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16469]) ).
fof(f65355,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1762)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1761)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16471]) ).
fof(f65356,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1763)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1762)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16473]) ).
fof(f65357,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1764)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1763)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16475]) ).
fof(f65358,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1765)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1764)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16477]) ).
fof(f65359,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1766)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1765)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16479]) ).
fof(f65360,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1767)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1766)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16481]) ).
fof(f65361,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1768)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1767)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16483]) ).
fof(f65362,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1769)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1768)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16485]) ).
fof(f65363,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1770)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1769)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16487]) ).
fof(f65364,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1771)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1770)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16489]) ).
fof(f65365,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1772)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1771)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16491]) ).
fof(f65366,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1773)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1772)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16493]) ).
fof(f65367,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1774)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1773)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16495]) ).
fof(f65368,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1775)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1774)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16497]) ).
fof(f65369,plain,
( cCoq_2eInit_2eDatatypes_2enat___24t(sF1776)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1775)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS) ),
inference(superposition,[],[f10757,f16499]) ).
fof(f65462,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1735)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_119 ),
inference(forward_subsumption_resolution,[],[f65329,f17663]) ).
fof(f65703,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1735)
| spl1783_119 ),
inference(forward_subsumption_resolution,[],[f65462,f15325]) ).
fof(f65738,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eNat_2eone)
| spl1783_119 ),
inference(forward_demodulation,[],[f65703,f16984]) ).
fof(f65747,plain,
( $false
| spl1783_119 ),
inference(forward_subsumption_resolution,[],[f65738,f11099]) ).
fof(f65748,plain,
spl1783_119,
inference(avatar_contradiction_clause,[],[f65747]) ).
fof(f65815,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1736)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_117 ),
inference(forward_subsumption_resolution,[],[f65330,f17654]) ).
fof(f65860,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_117
| ~ spl1783_119 ),
inference(forward_subsumption_resolution,[],[f65815,f17662]) ).
fof(f65872,plain,
( $false
| spl1783_117
| ~ spl1783_119 ),
inference(forward_subsumption_resolution,[],[f65860,f15325]) ).
fof(f65873,plain,
( spl1783_117
| ~ spl1783_119 ),
inference(avatar_contradiction_clause,[],[f65872]) ).
fof(f65900,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1737)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_115 ),
inference(forward_subsumption_resolution,[],[f65331,f17645]) ).
fof(f65943,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_115
| ~ spl1783_117 ),
inference(forward_subsumption_resolution,[],[f65900,f17653]) ).
fof(f65954,plain,
( $false
| spl1783_115
| ~ spl1783_117 ),
inference(forward_subsumption_resolution,[],[f65943,f15325]) ).
fof(f65955,plain,
( spl1783_115
| ~ spl1783_117 ),
inference(avatar_contradiction_clause,[],[f65954]) ).
fof(f65983,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1738)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_113 ),
inference(forward_subsumption_resolution,[],[f65332,f17636]) ).
fof(f66023,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_113
| ~ spl1783_115 ),
inference(forward_subsumption_resolution,[],[f65983,f17644]) ).
fof(f66031,plain,
( $false
| spl1783_113
| ~ spl1783_115 ),
inference(forward_subsumption_resolution,[],[f66023,f15325]) ).
fof(f66032,plain,
( spl1783_113
| ~ spl1783_115 ),
inference(avatar_contradiction_clause,[],[f66031]) ).
fof(f66057,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1739)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_111 ),
inference(forward_subsumption_resolution,[],[f65333,f17627]) ).
fof(f66097,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_111
| ~ spl1783_113 ),
inference(forward_subsumption_resolution,[],[f66057,f17635]) ).
fof(f66105,plain,
( $false
| spl1783_111
| ~ spl1783_113 ),
inference(forward_subsumption_resolution,[],[f66097,f15325]) ).
fof(f66106,plain,
( spl1783_111
| ~ spl1783_113 ),
inference(avatar_contradiction_clause,[],[f66105]) ).
fof(f66133,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1740)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_109 ),
inference(forward_subsumption_resolution,[],[f65334,f17618]) ).
fof(f66174,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_109
| ~ spl1783_111 ),
inference(forward_subsumption_resolution,[],[f66133,f17626]) ).
fof(f66183,plain,
( $false
| spl1783_109
| ~ spl1783_111 ),
inference(forward_subsumption_resolution,[],[f66174,f15325]) ).
fof(f66184,plain,
( spl1783_109
| ~ spl1783_111 ),
inference(avatar_contradiction_clause,[],[f66183]) ).
fof(f66211,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1741)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_107 ),
inference(forward_subsumption_resolution,[],[f65335,f17609]) ).
fof(f66251,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_107
| ~ spl1783_109 ),
inference(forward_subsumption_resolution,[],[f66211,f17617]) ).
fof(f66259,plain,
( $false
| spl1783_107
| ~ spl1783_109 ),
inference(forward_subsumption_resolution,[],[f66251,f15325]) ).
fof(f66260,plain,
( spl1783_107
| ~ spl1783_109 ),
inference(avatar_contradiction_clause,[],[f66259]) ).
fof(f66287,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1742)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_105 ),
inference(forward_subsumption_resolution,[],[f65336,f17600]) ).
fof(f66328,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_105
| ~ spl1783_107 ),
inference(forward_subsumption_resolution,[],[f66287,f17608]) ).
fof(f66337,plain,
( $false
| spl1783_105
| ~ spl1783_107 ),
inference(forward_subsumption_resolution,[],[f66328,f15325]) ).
fof(f66338,plain,
( spl1783_105
| ~ spl1783_107 ),
inference(avatar_contradiction_clause,[],[f66337]) ).
fof(f66365,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1743)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_103 ),
inference(forward_subsumption_resolution,[],[f65337,f17591]) ).
fof(f66405,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_103
| ~ spl1783_105 ),
inference(forward_subsumption_resolution,[],[f66365,f17599]) ).
fof(f66413,plain,
( $false
| spl1783_103
| ~ spl1783_105 ),
inference(forward_subsumption_resolution,[],[f66405,f15325]) ).
fof(f66414,plain,
( spl1783_103
| ~ spl1783_105 ),
inference(avatar_contradiction_clause,[],[f66413]) ).
fof(f66440,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1744)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_101 ),
inference(forward_subsumption_resolution,[],[f65338,f17582]) ).
fof(f66480,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_101
| ~ spl1783_103 ),
inference(forward_subsumption_resolution,[],[f66440,f17590]) ).
fof(f66488,plain,
( $false
| spl1783_101
| ~ spl1783_103 ),
inference(forward_subsumption_resolution,[],[f66480,f15325]) ).
fof(f66489,plain,
( spl1783_101
| ~ spl1783_103 ),
inference(avatar_contradiction_clause,[],[f66488]) ).
fof(f66514,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1745)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_99 ),
inference(forward_subsumption_resolution,[],[f65339,f17573]) ).
fof(f66554,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_99
| ~ spl1783_101 ),
inference(forward_subsumption_resolution,[],[f66514,f17581]) ).
fof(f66562,plain,
( $false
| spl1783_99
| ~ spl1783_101 ),
inference(forward_subsumption_resolution,[],[f66554,f15325]) ).
fof(f66563,plain,
( spl1783_99
| ~ spl1783_101 ),
inference(avatar_contradiction_clause,[],[f66562]) ).
fof(f66589,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1746)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_97 ),
inference(forward_subsumption_resolution,[],[f65340,f17564]) ).
fof(f66629,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_97
| ~ spl1783_99 ),
inference(forward_subsumption_resolution,[],[f66589,f17572]) ).
fof(f66637,plain,
( $false
| spl1783_97
| ~ spl1783_99 ),
inference(forward_subsumption_resolution,[],[f66629,f15325]) ).
fof(f66638,plain,
( spl1783_97
| ~ spl1783_99 ),
inference(avatar_contradiction_clause,[],[f66637]) ).
fof(f66663,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1747)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_95 ),
inference(forward_subsumption_resolution,[],[f65341,f17555]) ).
fof(f66703,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_95
| ~ spl1783_97 ),
inference(forward_subsumption_resolution,[],[f66663,f17563]) ).
fof(f66711,plain,
( $false
| spl1783_95
| ~ spl1783_97 ),
inference(forward_subsumption_resolution,[],[f66703,f15325]) ).
fof(f66712,plain,
( spl1783_95
| ~ spl1783_97 ),
inference(avatar_contradiction_clause,[],[f66711]) ).
fof(f66738,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1748)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_93 ),
inference(forward_subsumption_resolution,[],[f65342,f17546]) ).
fof(f66778,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_93
| ~ spl1783_95 ),
inference(forward_subsumption_resolution,[],[f66738,f17554]) ).
fof(f66786,plain,
( $false
| spl1783_93
| ~ spl1783_95 ),
inference(forward_subsumption_resolution,[],[f66778,f15325]) ).
fof(f66787,plain,
( spl1783_93
| ~ spl1783_95 ),
inference(avatar_contradiction_clause,[],[f66786]) ).
fof(f66812,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1749)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_91 ),
inference(forward_subsumption_resolution,[],[f65343,f17537]) ).
fof(f66852,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_91
| ~ spl1783_93 ),
inference(forward_subsumption_resolution,[],[f66812,f17545]) ).
fof(f66860,plain,
( $false
| spl1783_91
| ~ spl1783_93 ),
inference(forward_subsumption_resolution,[],[f66852,f15325]) ).
fof(f66861,plain,
( spl1783_91
| ~ spl1783_93 ),
inference(avatar_contradiction_clause,[],[f66860]) ).
fof(f66886,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1750)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_89 ),
inference(forward_subsumption_resolution,[],[f65344,f17528]) ).
fof(f66926,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_89
| ~ spl1783_91 ),
inference(forward_subsumption_resolution,[],[f66886,f17536]) ).
fof(f66934,plain,
( $false
| spl1783_89
| ~ spl1783_91 ),
inference(forward_subsumption_resolution,[],[f66926,f15325]) ).
fof(f66935,plain,
( spl1783_89
| ~ spl1783_91 ),
inference(avatar_contradiction_clause,[],[f66934]) ).
fof(f66960,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1751)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_87 ),
inference(forward_subsumption_resolution,[],[f65345,f17519]) ).
fof(f67000,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_87
| ~ spl1783_89 ),
inference(forward_subsumption_resolution,[],[f66960,f17527]) ).
fof(f67008,plain,
( $false
| spl1783_87
| ~ spl1783_89 ),
inference(forward_subsumption_resolution,[],[f67000,f15325]) ).
fof(f67009,plain,
( spl1783_87
| ~ spl1783_89 ),
inference(avatar_contradiction_clause,[],[f67008]) ).
fof(f67034,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1752)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_85 ),
inference(forward_subsumption_resolution,[],[f65346,f17510]) ).
fof(f67074,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_85
| ~ spl1783_87 ),
inference(forward_subsumption_resolution,[],[f67034,f17518]) ).
fof(f67082,plain,
( $false
| spl1783_85
| ~ spl1783_87 ),
inference(forward_subsumption_resolution,[],[f67074,f15325]) ).
fof(f67083,plain,
( spl1783_85
| ~ spl1783_87 ),
inference(avatar_contradiction_clause,[],[f67082]) ).
fof(f67109,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1753)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_83 ),
inference(forward_subsumption_resolution,[],[f65347,f17501]) ).
fof(f67149,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_83
| ~ spl1783_85 ),
inference(forward_subsumption_resolution,[],[f67109,f17509]) ).
fof(f67157,plain,
( $false
| spl1783_83
| ~ spl1783_85 ),
inference(forward_subsumption_resolution,[],[f67149,f15325]) ).
fof(f67158,plain,
( spl1783_83
| ~ spl1783_85 ),
inference(avatar_contradiction_clause,[],[f67157]) ).
fof(f67185,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1754)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_81 ),
inference(forward_subsumption_resolution,[],[f65348,f17492]) ).
fof(f67226,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_81
| ~ spl1783_83 ),
inference(forward_subsumption_resolution,[],[f67185,f17500]) ).
fof(f67235,plain,
( $false
| spl1783_81
| ~ spl1783_83 ),
inference(forward_subsumption_resolution,[],[f67226,f15325]) ).
fof(f67236,plain,
( spl1783_81
| ~ spl1783_83 ),
inference(avatar_contradiction_clause,[],[f67235]) ).
fof(f67263,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1755)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_79 ),
inference(forward_subsumption_resolution,[],[f65349,f17483]) ).
fof(f67303,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_79
| ~ spl1783_81 ),
inference(forward_subsumption_resolution,[],[f67263,f17491]) ).
fof(f67311,plain,
( $false
| spl1783_79
| ~ spl1783_81 ),
inference(forward_subsumption_resolution,[],[f67303,f15325]) ).
fof(f67312,plain,
( spl1783_79
| ~ spl1783_81 ),
inference(avatar_contradiction_clause,[],[f67311]) ).
fof(f67337,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1756)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_77 ),
inference(forward_subsumption_resolution,[],[f65350,f17474]) ).
fof(f67377,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_77
| ~ spl1783_79 ),
inference(forward_subsumption_resolution,[],[f67337,f17482]) ).
fof(f67385,plain,
( $false
| spl1783_77
| ~ spl1783_79 ),
inference(forward_subsumption_resolution,[],[f67377,f15325]) ).
fof(f67386,plain,
( spl1783_77
| ~ spl1783_79 ),
inference(avatar_contradiction_clause,[],[f67385]) ).
fof(f67412,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1757)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_75 ),
inference(forward_subsumption_resolution,[],[f65351,f17465]) ).
fof(f67452,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_75
| ~ spl1783_77 ),
inference(forward_subsumption_resolution,[],[f67412,f17473]) ).
fof(f67460,plain,
( $false
| spl1783_75
| ~ spl1783_77 ),
inference(forward_subsumption_resolution,[],[f67452,f15325]) ).
fof(f67461,plain,
( spl1783_75
| ~ spl1783_77 ),
inference(avatar_contradiction_clause,[],[f67460]) ).
fof(f67488,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1758)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_73 ),
inference(forward_subsumption_resolution,[],[f65352,f17456]) ).
fof(f67529,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_73
| ~ spl1783_75 ),
inference(forward_subsumption_resolution,[],[f67488,f17464]) ).
fof(f67538,plain,
( $false
| spl1783_73
| ~ spl1783_75 ),
inference(forward_subsumption_resolution,[],[f67529,f15325]) ).
fof(f67539,plain,
( spl1783_73
| ~ spl1783_75 ),
inference(avatar_contradiction_clause,[],[f67538]) ).
fof(f67567,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1759)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_71 ),
inference(forward_subsumption_resolution,[],[f65353,f17447]) ).
fof(f67608,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_71
| ~ spl1783_73 ),
inference(forward_subsumption_resolution,[],[f67567,f17455]) ).
fof(f67617,plain,
( $false
| spl1783_71
| ~ spl1783_73 ),
inference(forward_subsumption_resolution,[],[f67608,f15325]) ).
fof(f67618,plain,
( spl1783_71
| ~ spl1783_73 ),
inference(avatar_contradiction_clause,[],[f67617]) ).
fof(f67646,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1760)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_69 ),
inference(forward_subsumption_resolution,[],[f65354,f17438]) ).
fof(f67687,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_69
| ~ spl1783_71 ),
inference(forward_subsumption_resolution,[],[f67646,f17446]) ).
fof(f67696,plain,
( $false
| spl1783_69
| ~ spl1783_71 ),
inference(forward_subsumption_resolution,[],[f67687,f15325]) ).
fof(f67697,plain,
( spl1783_69
| ~ spl1783_71 ),
inference(avatar_contradiction_clause,[],[f67696]) ).
fof(f67724,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1761)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_67 ),
inference(forward_subsumption_resolution,[],[f65355,f17429]) ).
fof(f67764,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_67
| ~ spl1783_69 ),
inference(forward_subsumption_resolution,[],[f67724,f17437]) ).
fof(f67772,plain,
( $false
| spl1783_67
| ~ spl1783_69 ),
inference(forward_subsumption_resolution,[],[f67764,f15325]) ).
fof(f67773,plain,
( spl1783_67
| ~ spl1783_69 ),
inference(avatar_contradiction_clause,[],[f67772]) ).
fof(f67799,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1762)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_65 ),
inference(forward_subsumption_resolution,[],[f65356,f17420]) ).
fof(f67839,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_65
| ~ spl1783_67 ),
inference(forward_subsumption_resolution,[],[f67799,f17428]) ).
fof(f67847,plain,
( $false
| spl1783_65
| ~ spl1783_67 ),
inference(forward_subsumption_resolution,[],[f67839,f15325]) ).
fof(f67848,plain,
( spl1783_65
| ~ spl1783_67 ),
inference(avatar_contradiction_clause,[],[f67847]) ).
fof(f67874,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1763)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_63 ),
inference(forward_subsumption_resolution,[],[f65357,f17411]) ).
fof(f67914,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_63
| ~ spl1783_65 ),
inference(forward_subsumption_resolution,[],[f67874,f17419]) ).
fof(f67922,plain,
( $false
| spl1783_63
| ~ spl1783_65 ),
inference(forward_subsumption_resolution,[],[f67914,f15325]) ).
fof(f67923,plain,
( spl1783_63
| ~ spl1783_65 ),
inference(avatar_contradiction_clause,[],[f67922]) ).
fof(f67950,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1764)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_61 ),
inference(forward_subsumption_resolution,[],[f65358,f17402]) ).
fof(f67991,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_61
| ~ spl1783_63 ),
inference(forward_subsumption_resolution,[],[f67950,f17410]) ).
fof(f68000,plain,
( $false
| spl1783_61
| ~ spl1783_63 ),
inference(forward_subsumption_resolution,[],[f67991,f15325]) ).
fof(f68001,plain,
( spl1783_61
| ~ spl1783_63 ),
inference(avatar_contradiction_clause,[],[f68000]) ).
fof(f68028,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1765)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_59 ),
inference(forward_subsumption_resolution,[],[f65359,f17393]) ).
fof(f68068,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_59
| ~ spl1783_61 ),
inference(forward_subsumption_resolution,[],[f68028,f17401]) ).
fof(f68076,plain,
( $false
| spl1783_59
| ~ spl1783_61 ),
inference(forward_subsumption_resolution,[],[f68068,f15325]) ).
fof(f68077,plain,
( spl1783_59
| ~ spl1783_61 ),
inference(avatar_contradiction_clause,[],[f68076]) ).
fof(f68104,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1766)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_57 ),
inference(forward_subsumption_resolution,[],[f65360,f17384]) ).
fof(f68145,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_57
| ~ spl1783_59 ),
inference(forward_subsumption_resolution,[],[f68104,f17392]) ).
fof(f68154,plain,
( $false
| spl1783_57
| ~ spl1783_59 ),
inference(forward_subsumption_resolution,[],[f68145,f15325]) ).
fof(f68155,plain,
( spl1783_57
| ~ spl1783_59 ),
inference(avatar_contradiction_clause,[],[f68154]) ).
fof(f68183,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1767)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_55 ),
inference(forward_subsumption_resolution,[],[f65361,f17375]) ).
fof(f68224,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_55
| ~ spl1783_57 ),
inference(forward_subsumption_resolution,[],[f68183,f17383]) ).
fof(f68233,plain,
( $false
| spl1783_55
| ~ spl1783_57 ),
inference(forward_subsumption_resolution,[],[f68224,f15325]) ).
fof(f68234,plain,
( spl1783_55
| ~ spl1783_57 ),
inference(avatar_contradiction_clause,[],[f68233]) ).
fof(f68262,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1768)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_53 ),
inference(forward_subsumption_resolution,[],[f65362,f17366]) ).
fof(f68303,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_53
| ~ spl1783_55 ),
inference(forward_subsumption_resolution,[],[f68262,f17374]) ).
fof(f68312,plain,
( $false
| spl1783_53
| ~ spl1783_55 ),
inference(forward_subsumption_resolution,[],[f68303,f15325]) ).
fof(f68313,plain,
( spl1783_53
| ~ spl1783_55 ),
inference(avatar_contradiction_clause,[],[f68312]) ).
fof(f68340,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1769)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_51 ),
inference(forward_subsumption_resolution,[],[f65363,f17357]) ).
fof(f68380,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_51
| ~ spl1783_53 ),
inference(forward_subsumption_resolution,[],[f68340,f17365]) ).
fof(f68388,plain,
( $false
| spl1783_51
| ~ spl1783_53 ),
inference(forward_subsumption_resolution,[],[f68380,f15325]) ).
fof(f68389,plain,
( spl1783_51
| ~ spl1783_53 ),
inference(avatar_contradiction_clause,[],[f68388]) ).
fof(f68415,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1770)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_49 ),
inference(forward_subsumption_resolution,[],[f65364,f17348]) ).
fof(f68455,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_49
| ~ spl1783_51 ),
inference(forward_subsumption_resolution,[],[f68415,f17356]) ).
fof(f68463,plain,
( $false
| spl1783_49
| ~ spl1783_51 ),
inference(forward_subsumption_resolution,[],[f68455,f15325]) ).
fof(f68464,plain,
( spl1783_49
| ~ spl1783_51 ),
inference(avatar_contradiction_clause,[],[f68463]) ).
fof(f68491,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1771)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_47 ),
inference(forward_subsumption_resolution,[],[f65365,f17339]) ).
fof(f68532,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_47
| ~ spl1783_49 ),
inference(forward_subsumption_resolution,[],[f68491,f17347]) ).
fof(f68541,plain,
( $false
| spl1783_47
| ~ spl1783_49 ),
inference(forward_subsumption_resolution,[],[f68532,f15325]) ).
fof(f68542,plain,
( spl1783_47
| ~ spl1783_49 ),
inference(avatar_contradiction_clause,[],[f68541]) ).
fof(f68570,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1772)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_45 ),
inference(forward_subsumption_resolution,[],[f65366,f17330]) ).
fof(f68611,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_45
| ~ spl1783_47 ),
inference(forward_subsumption_resolution,[],[f68570,f17338]) ).
fof(f68620,plain,
( $false
| spl1783_45
| ~ spl1783_47 ),
inference(forward_subsumption_resolution,[],[f68611,f15325]) ).
fof(f68621,plain,
( spl1783_45
| ~ spl1783_47 ),
inference(avatar_contradiction_clause,[],[f68620]) ).
fof(f68648,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1773)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_43 ),
inference(forward_subsumption_resolution,[],[f65367,f17321]) ).
fof(f68688,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_43
| ~ spl1783_45 ),
inference(forward_subsumption_resolution,[],[f68648,f17329]) ).
fof(f68696,plain,
( $false
| spl1783_43
| ~ spl1783_45 ),
inference(forward_subsumption_resolution,[],[f68688,f15325]) ).
fof(f68697,plain,
( spl1783_43
| ~ spl1783_45 ),
inference(avatar_contradiction_clause,[],[f68696]) ).
fof(f68724,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1774)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_41 ),
inference(forward_subsumption_resolution,[],[f65368,f17312]) ).
fof(f68765,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_41
| ~ spl1783_43 ),
inference(forward_subsumption_resolution,[],[f68724,f17320]) ).
fof(f68772,plain,
( $false
| spl1783_41
| ~ spl1783_43 ),
inference(forward_subsumption_resolution,[],[f68765,f15325]) ).
fof(f68773,plain,
( spl1783_41
| ~ spl1783_43 ),
inference(avatar_contradiction_clause,[],[f68772]) ).
fof(f68800,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sF1775)
| ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| spl1783_123 ),
inference(forward_subsumption_resolution,[],[f65369,f17682]) ).
fof(f68839,plain,
( ~ c_24__type__7___24t(cCoq_2eInit_2eDatatypes_2eS)
| ~ spl1783_41
| spl1783_123 ),
inference(forward_subsumption_resolution,[],[f68800,f17311]) ).
fof(f68845,plain,
( $false
| ~ spl1783_41
| spl1783_123 ),
inference(forward_subsumption_resolution,[],[f68839,f15325]) ).
fof(f68846,plain,
( ~ spl1783_41
| spl1783_123 ),
inference(avatar_contradiction_clause,[],[f68845]) ).
fof(f68848,plain,
( ! [X0] :
( ~ p(happ(sF1781,X0))
| p(sF1778(sF1776))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0) )
| ~ spl1783_123 ),
inference(forward_subsumption_resolution,[],[f17982,f17681]) ).
fof(f68858,plain,
( ! [X0] :
( p(sF1777)
| ~ p(happ(sF1781,X0))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0) )
| ~ spl1783_123 ),
inference(forward_demodulation,[],[f68848,f17246]) ).
fof(f68867,plain,
( ! [X0] :
( ~ p(happ(sF1781,X0))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X0) )
| ~ spl1783_123 ),
inference(forward_subsumption_resolution,[],[f68858,f16502]) ).
fof(f68879,plain,
( ~ p(sF1782)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK1734)
| ~ spl1783_123 ),
inference(superposition,[],[f68867,f16513]) ).
fof(f68882,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK1734)
| ~ spl1783_123 ),
inference(forward_subsumption_resolution,[],[f68879,f16514]) ).
fof(f68885,plain,
( $false
| ~ spl1783_123 ),
inference(forward_subsumption_resolution,[],[f68882,f13545]) ).
fof(f68886,plain,
~ spl1783_123,
inference(avatar_contradiction_clause,[],[f68885]) ).
cnf(s5654,plain,
spl1783_119,
inference(sat_conversion,[],[f65748]) ).
cnf(s5660,plain,
( spl1783_117
| ~ spl1783_119 ),
inference(sat_conversion,[],[f65873]) ).
cnf(s5669,plain,
( spl1783_115
| ~ spl1783_117 ),
inference(sat_conversion,[],[f65955]) ).
cnf(s5677,plain,
( spl1783_113
| ~ spl1783_115 ),
inference(sat_conversion,[],[f66032]) ).
cnf(s5685,plain,
( spl1783_111
| ~ spl1783_113 ),
inference(sat_conversion,[],[f66106]) ).
cnf(s5693,plain,
( spl1783_109
| ~ spl1783_111 ),
inference(sat_conversion,[],[f66184]) ).
cnf(s5701,plain,
( spl1783_107
| ~ spl1783_109 ),
inference(sat_conversion,[],[f66260]) ).
cnf(s5709,plain,
( spl1783_105
| ~ spl1783_107 ),
inference(sat_conversion,[],[f66338]) ).
cnf(s5717,plain,
( spl1783_103
| ~ spl1783_105 ),
inference(sat_conversion,[],[f66414]) ).
cnf(s5725,plain,
( spl1783_101
| ~ spl1783_103 ),
inference(sat_conversion,[],[f66489]) ).
cnf(s5733,plain,
( spl1783_99
| ~ spl1783_101 ),
inference(sat_conversion,[],[f66563]) ).
cnf(s5741,plain,
( spl1783_97
| ~ spl1783_99 ),
inference(sat_conversion,[],[f66638]) ).
cnf(s5749,plain,
( spl1783_95
| ~ spl1783_97 ),
inference(sat_conversion,[],[f66712]) ).
cnf(s5757,plain,
( spl1783_93
| ~ spl1783_95 ),
inference(sat_conversion,[],[f66787]) ).
cnf(s5765,plain,
( spl1783_91
| ~ spl1783_93 ),
inference(sat_conversion,[],[f66861]) ).
cnf(s5773,plain,
( spl1783_89
| ~ spl1783_91 ),
inference(sat_conversion,[],[f66935]) ).
cnf(s5781,plain,
( spl1783_87
| ~ spl1783_89 ),
inference(sat_conversion,[],[f67009]) ).
cnf(s5789,plain,
( spl1783_85
| ~ spl1783_87 ),
inference(sat_conversion,[],[f67083]) ).
cnf(s5797,plain,
( spl1783_83
| ~ spl1783_85 ),
inference(sat_conversion,[],[f67158]) ).
cnf(s5805,plain,
( spl1783_81
| ~ spl1783_83 ),
inference(sat_conversion,[],[f67236]) ).
cnf(s5813,plain,
( spl1783_79
| ~ spl1783_81 ),
inference(sat_conversion,[],[f67312]) ).
cnf(s5821,plain,
( spl1783_77
| ~ spl1783_79 ),
inference(sat_conversion,[],[f67386]) ).
cnf(s5829,plain,
( spl1783_75
| ~ spl1783_77 ),
inference(sat_conversion,[],[f67461]) ).
cnf(s5837,plain,
( spl1783_73
| ~ spl1783_75 ),
inference(sat_conversion,[],[f67539]) ).
cnf(s5845,plain,
( spl1783_71
| ~ spl1783_73 ),
inference(sat_conversion,[],[f67618]) ).
cnf(s5853,plain,
( spl1783_69
| ~ spl1783_71 ),
inference(sat_conversion,[],[f67697]) ).
cnf(s5861,plain,
( spl1783_67
| ~ spl1783_69 ),
inference(sat_conversion,[],[f67773]) ).
cnf(s5869,plain,
( spl1783_65
| ~ spl1783_67 ),
inference(sat_conversion,[],[f67848]) ).
cnf(s5877,plain,
( spl1783_63
| ~ spl1783_65 ),
inference(sat_conversion,[],[f67923]) ).
cnf(s5885,plain,
( spl1783_61
| ~ spl1783_63 ),
inference(sat_conversion,[],[f68001]) ).
cnf(s5893,plain,
( spl1783_59
| ~ spl1783_61 ),
inference(sat_conversion,[],[f68077]) ).
cnf(s5901,plain,
( spl1783_57
| ~ spl1783_59 ),
inference(sat_conversion,[],[f68155]) ).
cnf(s5909,plain,
( spl1783_55
| ~ spl1783_57 ),
inference(sat_conversion,[],[f68234]) ).
cnf(s5917,plain,
( spl1783_53
| ~ spl1783_55 ),
inference(sat_conversion,[],[f68313]) ).
cnf(s5925,plain,
( spl1783_51
| ~ spl1783_53 ),
inference(sat_conversion,[],[f68389]) ).
cnf(s5933,plain,
( spl1783_49
| ~ spl1783_51 ),
inference(sat_conversion,[],[f68464]) ).
cnf(s5941,plain,
( spl1783_47
| ~ spl1783_49 ),
inference(sat_conversion,[],[f68542]) ).
cnf(s5949,plain,
( spl1783_45
| ~ spl1783_47 ),
inference(sat_conversion,[],[f68621]) ).
cnf(s5957,plain,
( spl1783_43
| ~ spl1783_45 ),
inference(sat_conversion,[],[f68697]) ).
cnf(s5965,plain,
( spl1783_41
| ~ spl1783_43 ),
inference(sat_conversion,[],[f68773]) ).
cnf(s5973,plain,
( ~ spl1783_41
| spl1783_123 ),
inference(sat_conversion,[],[f68846]) ).
cnf(s5976,plain,
~ spl1783_123,
inference(sat_conversion,[],[f68886]) ).
cnf(s5977,plain,
~ spl1783_41,
inference(rat,[],[s5973,s5976]) ).
cnf(s5978,plain,
~ spl1783_43,
inference(rat,[],[s5965,s5977]) ).
cnf(s5979,plain,
~ spl1783_45,
inference(rat,[],[s5957,s5978]) ).
cnf(s5980,plain,
~ spl1783_47,
inference(rat,[],[s5949,s5979]) ).
cnf(s5981,plain,
~ spl1783_49,
inference(rat,[],[s5941,s5980]) ).
cnf(s5982,plain,
~ spl1783_51,
inference(rat,[],[s5933,s5981]) ).
cnf(s5983,plain,
~ spl1783_53,
inference(rat,[],[s5925,s5982]) ).
cnf(s5984,plain,
~ spl1783_55,
inference(rat,[],[s5917,s5983]) ).
cnf(s5985,plain,
~ spl1783_57,
inference(rat,[],[s5909,s5984]) ).
cnf(s5986,plain,
~ spl1783_59,
inference(rat,[],[s5901,s5985]) ).
cnf(s5987,plain,
~ spl1783_61,
inference(rat,[],[s5893,s5986]) ).
cnf(s5988,plain,
~ spl1783_63,
inference(rat,[],[s5885,s5987]) ).
cnf(s5989,plain,
~ spl1783_65,
inference(rat,[],[s5877,s5988]) ).
cnf(s5990,plain,
~ spl1783_67,
inference(rat,[],[s5869,s5989]) ).
cnf(s5991,plain,
~ spl1783_69,
inference(rat,[],[s5861,s5990]) ).
cnf(s5992,plain,
~ spl1783_71,
inference(rat,[],[s5853,s5991]) ).
cnf(s5993,plain,
~ spl1783_73,
inference(rat,[],[s5845,s5992]) ).
cnf(s5994,plain,
~ spl1783_75,
inference(rat,[],[s5837,s5993]) ).
cnf(s5995,plain,
~ spl1783_77,
inference(rat,[],[s5829,s5994]) ).
cnf(s5996,plain,
~ spl1783_79,
inference(rat,[],[s5821,s5995]) ).
cnf(s5997,plain,
~ spl1783_81,
inference(rat,[],[s5813,s5996]) ).
cnf(s5998,plain,
~ spl1783_83,
inference(rat,[],[s5805,s5997]) ).
cnf(s5999,plain,
~ spl1783_85,
inference(rat,[],[s5797,s5998]) ).
cnf(s6000,plain,
~ spl1783_87,
inference(rat,[],[s5789,s5999]) ).
cnf(s6001,plain,
~ spl1783_89,
inference(rat,[],[s5781,s6000]) ).
cnf(s6002,plain,
~ spl1783_91,
inference(rat,[],[s5773,s6001]) ).
cnf(s6003,plain,
~ spl1783_93,
inference(rat,[],[s5765,s6002]) ).
cnf(s6004,plain,
~ spl1783_95,
inference(rat,[],[s5757,s6003]) ).
cnf(s6005,plain,
~ spl1783_97,
inference(rat,[],[s5749,s6004]) ).
cnf(s6006,plain,
~ spl1783_99,
inference(rat,[],[s5741,s6005]) ).
cnf(s6007,plain,
~ spl1783_101,
inference(rat,[],[s5733,s6006]) ).
cnf(s6008,plain,
~ spl1783_103,
inference(rat,[],[s5725,s6007]) ).
cnf(s6009,plain,
~ spl1783_105,
inference(rat,[],[s5717,s6008]) ).
cnf(s6010,plain,
~ spl1783_107,
inference(rat,[],[s5709,s6009]) ).
cnf(s6011,plain,
~ spl1783_109,
inference(rat,[],[s5701,s6010]) ).
cnf(s6012,plain,
~ spl1783_111,
inference(rat,[],[s5693,s6011]) ).
cnf(s6013,plain,
~ spl1783_113,
inference(rat,[],[s5685,s6012]) ).
cnf(s6014,plain,
~ spl1783_115,
inference(rat,[],[s5677,s6013]) ).
cnf(s6015,plain,
~ spl1783_117,
inference(rat,[],[s5669,s6014]) ).
cnf(s6016,plain,
~ spl1783_119,
inference(rat,[],[s5660,s6015]) ).
cnf(s6017,plain,
$false,
inference(rat,[],[s5654,s6016]) ).
fof(f68887,plain,
$false,
inference(avatar_sat_refutation,[],[s6017]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV634+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n018.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 28 06:47:55 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.33/2.64 % (3181623)Detected formulas, will run a generic FOF schedule.
% 10.33/2.64 % (3181630)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2486135954:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 10.33/2.64 % (3181633)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1982216876:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 10.33/2.64 % (3181632)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=791642672:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 10.33/2.64 % (3181634)dis-21_1_sil=8000:lcm=predicate:random_seed=3676257323:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 10.33/2.64 % (3181631)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=397689420:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 10.33/2.64 % (3181628)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=36855848:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 10.33/2.64 % (3181629)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1586119747:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 10.33/2.64 % (3181631)Refutation not found, incomplete strategy
% 10.33/2.64 % (3181631)------------------------------
% 10.33/2.64 % (3181631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.64 % (3181631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.64 % (3181631)CaDiCaL version: 2.1.3
% 10.33/2.64 % (3181631)Termination reason: Refutation not found, incomplete strategy
% 10.33/2.64 % (3181631)Time elapsed: 0.022 s
% 10.33/2.64 % (3181631)Peak memory usage: 92 MB
% 10.33/2.64 % (3181631)Instructions burned: 46 (million)
% 10.33/2.64 % (3181633)Instruction limit reached!
% 10.33/2.64 % (3181633)------------------------------
% 10.33/2.64 % (3181633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.64 % (3181633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.64 % (3181633)CaDiCaL version: 2.1.3
% 10.33/2.64 % (3181633)Termination reason: Instruction limit
% 10.33/2.64 % (3181633)Termination phase: Naming
% 10.33/2.64 % (3181633)Time elapsed: 0.058 s
% 10.33/2.64 % (3181633)Peak memory usage: 90 MB
% 10.33/2.64 % (3181633)Instructions burned: 140 (million)
% 10.33/2.64 % (3181632)Instruction limit reached!
% 10.33/2.64 % (3181632)------------------------------
% 10.33/2.64 % (3181632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.64 % (3181632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.64 % (3181632)CaDiCaL version: 2.1.3
% 10.33/2.64 % (3181632)Termination reason: Instruction limit
% 10.33/2.64 % (3181632)Termination phase: Saturation
% 10.33/2.64 % (3181632)Time elapsed: 0.063 s
% 10.33/2.64 % (3181632)Peak memory usage: 91 MB
% 10.33/2.64 % (3181632)Instructions burned: 119 (million)
% 10.33/2.64 % (3181634)Instruction limit reached!
% 10.33/2.64 % (3181634)------------------------------
% 10.33/2.64 % (3181634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.64 % (3181634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.33/2.64 % (3181634)CaDiCaL version: 2.1.3
% 10.33/2.64 % (3181634)Termination reason: Instruction limit
% 10.33/2.64 % (3181634)Termination phase: Preprocessing 3
% 10.33/2.64 % (3181634)Time elapsed: 0.065 s
% 10.33/2.64 % (3181634)Peak memory usage: 92 MB
% 10.33/2.64 % (3181634)Instructions burned: 129 (million)
% 10.33/2.64 % (3181642)lrs+10_1_sil=8000:sp=occurrence:random_seed=1678306972:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 10.33/2.64 % (3181644)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2705034152:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 10.33/2.64 % (3181643)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3017598936:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 10.33/2.64 % (3181644)Refutation not found, incomplete strategy
% 10.33/2.64 % (3181644)------------------------------
% 10.33/2.64 % (3181644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.33/2.64 % (3181644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181644)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181644)Termination reason: Refutation not found, incomplete strategy
% 17.56/3.66 % (3181644)Time elapsed: 0.036 s
% 17.56/3.66 % (3181644)Peak memory usage: 92 MB
% 17.56/3.66 % (3181644)Instructions burned: 65 (million)
% 17.56/3.66 % (3181643)Instruction limit reached!
% 17.56/3.66 % (3181643)------------------------------
% 17.56/3.66 % (3181643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181643)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181643)Termination reason: Instruction limit
% 17.56/3.66 % (3181643)Termination phase: Saturation
% 17.56/3.66 % (3181643)Time elapsed: 0.063 s
% 17.56/3.66 % (3181643)Peak memory usage: 92 MB
% 17.56/3.66 % (3181643)Instructions burned: 157 (million)
% 17.56/3.66 % (3181631)------------------------------
% 17.56/3.66 % (3181631)------------------------------
% 17.56/3.66 % (3181642)Instruction limit reached!
% 17.56/3.66 % (3181642)------------------------------
% 17.56/3.66 % (3181642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181642)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181642)Termination reason: Instruction limit
% 17.56/3.66 % (3181642)Termination phase: Saturation
% 17.56/3.66 % (3181642)Time elapsed: 0.158 s
% 17.56/3.66 % (3181642)Peak memory usage: 94 MB
% 17.56/3.66 % (3181642)Instructions burned: 286 (million)
% 17.56/3.66 % (3181648)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3497875511:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 17.56/3.66 % (3181649)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=102220600:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 17.56/3.66 % (3181644)------------------------------
% 17.56/3.66 % (3181644)------------------------------
% 17.56/3.66 % (3181650)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4293793090:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 17.56/3.66 % (3181648)Instruction limit reached!
% 17.56/3.66 % (3181648)------------------------------
% 17.56/3.66 % (3181648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181648)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181648)Termination reason: Instruction limit
% 17.56/3.66 % (3181648)Termination phase: Property scanning
% 17.56/3.66 % (3181648)Time elapsed: 0.116 s
% 17.56/3.66 % (3181648)Peak memory usage: 94 MB
% 17.56/3.66 % (3181648)Instructions burned: 248 (million)
% 17.56/3.66 % (3181649)Instruction limit reached!
% 17.56/3.66 % (3181649)------------------------------
% 17.56/3.66 % (3181649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181649)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181649)Termination reason: Instruction limit
% 17.56/3.66 % (3181649)Termination phase: Saturation
% 17.56/3.66 % (3181649)Time elapsed: 0.138 s
% 17.56/3.66 % (3181649)Peak memory usage: 93 MB
% 17.56/3.66 % (3181649)Instructions burned: 295 (million)
% 17.56/3.66 % (3181655)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1473452505:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.56/3.66 % (3181653)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=705248620:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 17.56/3.66 % (3181655)Instruction limit reached!
% 17.56/3.66 % (3181655)------------------------------
% 17.56/3.66 % (3181655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.56/3.66 % (3181655)CaDiCaL version: 2.1.3
% 17.56/3.66 % (3181655)Termination reason: Instruction limit
% 17.56/3.66 % (3181655)Termination phase: Clausification
% 17.56/3.66 % (3181655)Time elapsed: 0.042 s
% 17.56/3.66 % (3181655)Peak memory usage: 94 MB
% 17.56/3.66 % (3181655)Instructions burned: 127 (million)
% 17.56/3.66 % (3181653)Instruction limit reached!
% 17.56/3.66 % (3181653)------------------------------
% 17.56/3.66 % (3181653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.56/3.66 % (3181653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181653)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181653)Termination reason: Instruction limit
% 36.56/6.27 % (3181653)Termination phase: Preprocessing 3
% 36.56/6.27 % (3181653)Time elapsed: 0.059 s
% 36.56/6.27 % (3181653)Peak memory usage: 91 MB
% 36.56/6.27 % (3181653)Instructions burned: 114 (million)
% 36.56/6.27 % (3181656)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1476145104:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 36.56/6.27 % (3181656)Instruction limit reached!
% 36.56/6.27 % (3181656)------------------------------
% 36.56/6.27 % (3181656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181656)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181656)Termination reason: Instruction limit
% 36.56/6.27 % (3181656)Termination phase: Property scanning
% 36.56/6.27 % (3181656)Time elapsed: 0.042 s
% 36.56/6.27 % (3181656)Peak memory usage: 88 MB
% 36.56/6.27 % (3181656)Instructions burned: 117 (million)
% 36.56/6.27 % (3181659)lrs+10_1_sil=8000:sp=occurrence:random_seed=1697469631:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 36.56/6.27 % (3181660)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2854423968:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 36.56/6.27 % (3181663)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3266123561:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 36.56/6.27 % (3181660)Instruction limit reached!
% 36.56/6.27 % (3181660)------------------------------
% 36.56/6.27 % (3181660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181660)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181660)Termination reason: Instruction limit
% 36.56/6.27 % (3181660)Termination phase: Saturation
% 36.56/6.27 % (3181660)Time elapsed: 0.189 s
% 36.56/6.27 % (3181660)Peak memory usage: 97 MB
% 36.56/6.27 % (3181660)Instructions burned: 440 (million)
% 36.56/6.27 % (3181659)Instruction limit reached!
% 36.56/6.27 % (3181659)------------------------------
% 36.56/6.27 % (3181659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181659)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181659)Termination reason: Instruction limit
% 36.56/6.27 % (3181659)Termination phase: Saturation
% 36.56/6.27 % (3181659)Time elapsed: 0.277 s
% 36.56/6.27 % (3181659)Peak memory usage: 101 MB
% 36.56/6.27 % (3181659)Instructions burned: 909 (million)
% 36.56/6.27 % (3181667)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1547820856:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 36.56/6.27 % (3181666)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=98664031:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 36.56/6.27 % (3181666)Instruction limit reached!
% 36.56/6.27 % (3181666)------------------------------
% 36.56/6.27 % (3181666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181666)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181666)Termination reason: Instruction limit
% 36.56/6.27 % (3181666)Termination phase: NewCNF
% 36.56/6.27 % (3181666)Time elapsed: 0.071 s
% 36.56/6.27 % (3181666)Peak memory usage: 93 MB
% 36.56/6.27 % (3181666)Instructions burned: 135 (million)
% 36.56/6.27 % (3181667)Instruction limit reached!
% 36.56/6.27 % (3181667)------------------------------
% 36.56/6.27 % (3181667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181667)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181667)Termination reason: Instruction limit
% 36.56/6.27 % (3181667)Termination phase: Saturation
% 36.56/6.27 % (3181667)Time elapsed: 0.169 s
% 36.56/6.27 % (3181667)Peak memory usage: 98 MB
% 36.56/6.27 % (3181667)Instructions burned: 592 (million)
% 36.56/6.27 % (3181670)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2955201130:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 36.56/6.27 % (3181671)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=4161090990:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 36.56/6.27 % (3181671)Instruction limit reached!
% 36.56/6.27 % (3181671)------------------------------
% 36.56/6.27 % (3181671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181671)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181671)Termination reason: Instruction limit
% 36.56/6.27 % (3181671)Termination phase: SInE selection
% 36.56/6.27 % (3181671)Time elapsed: 0.025 s
% 36.56/6.27 % (3181671)Peak memory usage: 88 MB
% 36.56/6.27 % (3181671)Instructions burned: 129 (million)
% 36.56/6.27 % (3181674)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2017405557:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 36.56/6.27 % (3181674)Instruction limit reached!
% 36.56/6.27 % (3181674)------------------------------
% 36.56/6.27 % (3181674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181674)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181674)Termination reason: Instruction limit
% 36.56/6.27 % (3181674)Termination phase: Property scanning
% 36.56/6.27 % (3181674)Time elapsed: 0.027 s
% 36.56/6.27 % (3181674)Peak memory usage: 88 MB
% 36.56/6.27 % (3181674)Instructions burned: 140 (million)
% 36.56/6.27 % (3181676)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1774629742:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 36.56/6.27 % (3181676)Refutation not found, incomplete strategy
% 36.56/6.27 % (3181676)------------------------------
% 36.56/6.27 % (3181676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181676)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181676)Termination reason: Refutation not found, incomplete strategy
% 36.56/6.27 % (3181676)Time elapsed: 0.011 s
% 36.56/6.27 % (3181676)Peak memory usage: 92 MB
% 36.56/6.27 % (3181676)Instructions burned: 40 (million)
% 36.56/6.27 % (3181676)------------------------------
% 36.56/6.27 % (3181676)------------------------------
% 36.56/6.27 % (3181650)Instruction limit reached!
% 36.56/6.27 % (3181650)------------------------------
% 36.56/6.27 % (3181650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181650)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181650)Termination reason: Instruction limit
% 36.56/6.27 % (3181650)Termination phase: Saturation
% 36.56/6.27 % (3181650)Time elapsed: 1.399 s
% 36.56/6.27 % (3181650)Peak memory usage: 205 MB
% 36.56/6.27 % (3181650)Instructions burned: 2353 (million)
% 36.56/6.27 % (3181678)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=146254159:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 36.56/6.27 % (3181678)Refutation not found, incomplete strategy
% 36.56/6.27 % (3181678)------------------------------
% 36.56/6.27 % (3181678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181678)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181678)Termination reason: Refutation not found, incomplete strategy
% 36.56/6.27 % (3181678)Time elapsed: 0.023 s
% 36.56/6.27 % (3181678)Peak memory usage: 92 MB
% 36.56/6.27 % (3181678)Instructions burned: 44 (million)
% 36.56/6.27 % (3181679)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3389740926:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 36.56/6.27 % (3181678)------------------------------
% 36.56/6.27 % (3181678)------------------------------
% 36.56/6.27 % (3181682)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1018482989:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 36.56/6.27 % (3181682)Instruction limit reached!
% 36.56/6.27 % (3181682)------------------------------
% 36.56/6.27 % (3181682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181682)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181682)Termination reason: Instruction limit
% 36.56/6.27 % (3181682)Termination phase: Preprocessing 3
% 36.56/6.27 % (3181682)Time elapsed: 0.076 s
% 36.56/6.27 % (3181682)Peak memory usage: 93 MB
% 36.56/6.27 % (3181682)Instructions burned: 151 (million)
% 36.56/6.27 % (3181684)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1172844772:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 36.56/6.27 % (3181663)Instruction limit reached!
% 36.56/6.27 % (3181663)------------------------------
% 36.56/6.27 % (3181663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181663)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181663)Termination reason: Instruction limit
% 36.56/6.27 % (3181663)Termination phase: Saturation
% 36.56/6.27 % (3181663)Time elapsed: 2.037 s
% 36.56/6.27 % (3181663)Peak memory usage: 211 MB
% 36.56/6.27 % (3181663)Instructions burned: 5204 (million)
% 36.56/6.27 % (3181686)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=690117172:i=667:av=off:fsr=off_2966 on theBenchmark for (2966ds/667Mi)
% 36.56/6.27 % (3181686)Instruction limit reached!
% 36.56/6.27 % (3181686)------------------------------
% 36.56/6.27 % (3181686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181686)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181686)Termination reason: Instruction limit
% 36.56/6.27 % (3181686)Termination phase: Saturation
% 36.56/6.27 % (3181686)Time elapsed: 0.154 s
% 36.56/6.27 % (3181686)Peak memory usage: 98 MB
% 36.56/6.27 % (3181686)Instructions burned: 668 (million)
% 36.56/6.27 % (3181688)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1629112976:s2a=on:i=185:s2at=1.8:fdi=4_2964 on theBenchmark for (2964ds/185Mi)
% 36.56/6.27 % (3181688)Instruction limit reached!
% 36.56/6.27 % (3181688)------------------------------
% 36.56/6.27 % (3181688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181688)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181688)Termination reason: Instruction limit
% 36.56/6.27 % (3181688)Termination phase: NewCNF
% 36.56/6.27 % (3181688)Time elapsed: 0.055 s
% 36.56/6.27 % (3181688)Peak memory usage: 93 MB
% 36.56/6.27 % (3181688)Instructions burned: 187 (million)
% 36.56/6.27 % (3181690)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2883145827:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2962 on theBenchmark for (2962ds/193Mi)
% 36.56/6.27 % (3181690)Instruction limit reached!
% 36.56/6.27 % (3181690)------------------------------
% 36.56/6.27 % (3181690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181690)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181690)Termination reason: Instruction limit
% 36.56/6.27 % (3181690)Termination phase: Saturation
% 36.56/6.27 % (3181690)Time elapsed: 0.052 s
% 36.56/6.27 % (3181690)Peak memory usage: 93 MB
% 36.56/6.27 % (3181690)Instructions burned: 195 (million)
% 36.56/6.27 % (3181692)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=846100661:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2961 on theBenchmark for (2961ds/4850Mi)
% 36.56/6.27 % (3181628)First to succeed.
% 36.56/6.27 % (3181628)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3181623"
% 36.56/6.27 % (3181692)Instruction limit reached!
% 36.56/6.27 % (3181692)------------------------------
% 36.56/6.27 % (3181692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.56/6.27 % (3181692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.56/6.27 % (3181692)CaDiCaL version: 2.1.3
% 36.56/6.27 % (3181692)Termination reason: Instruction limit
% 36.56/6.27 % (3181692)Termination phase: Saturation
% 36.56/6.27 % (3181692)Time elapsed: 1.396 s
% 36.56/6.27 % (3181692)Peak memory usage: 137 MB
% 36.56/6.27 % (3181692)Instructions burned: 4851 (million)
% 36.56/6.27 % (3181628)Refutation found. Thanks to Tanya!
% 36.56/6.27 % SZS status Theorem for theBenchmark
% 36.56/6.27 % SZS output start Proof for theBenchmark
% See solution above
% 37.20/6.46 % (3181628)------------------------------
% 37.20/6.46 % (3181628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.20/6.46 % (3181628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.20/6.46 % (3181628)CaDiCaL version: 2.1.3
% 37.20/6.46 % (3181628)Termination reason: Refutation
% 37.20/6.46 % (3181628)Time elapsed: 4.700 s
% 37.20/6.46 % (3181628)Peak memory usage: 229 MB
% 37.20/6.46 % (3181628)Instructions burned: 8212 (million)
% 37.20/6.46 % (3181628)------------------------------
% 37.20/6.46 % (3181628)------------------------------
% 37.20/6.46 % (3181623)Success in time 5.406 s
% 37.20/6.46 % Vampire exiting
%------------------------------------------------------------------------------