%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV630+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:27 PM UTC 2026
% Result : Theorem 2.49s 1.96s
% Output : Refutation 6.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 20
% Syntax : Number of formulae : 127 ( 28 unt; 6 def)
% Number of atoms : 421 ( 103 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 509 ( 215 ~; 233 |; 40 &)
% ( 8 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 7 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-3 aty)
% Number of variables : 192 ( 0 sgn 174 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f171,axiom,
! [X0,X1,X2] :
( cType___24t(X0)
=> ( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
=> ( ( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) )
| ? [X3] :
( t(X3,X0)
& ? [X4] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X4)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X3,X4)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cHahnTotalExt_2eone__ext___24a3(X0,X3,cHahnTotalExt_2etot__ext___24a3(X0,X4,X2)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_HahnTotalExt.tot_ext') ).
fof(f230,axiom,
! [X0,X1,X2,X3] : cCoq_2eInit_2eDatatypes_2enil___24a1(X0) != cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_discrim_Coq.Init.Datatypes.nil$Coq.Init.Datatypes.cons') ).
fof(f251,axiom,
! [X0,X1,X2,X3,X4,X5] :
( cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X4) = cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X3,X5)
=> ( X4 = X5
& X2 = X3
& X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_inj_Coq.Init.Datatypes.cons') ).
fof(f311,axiom,
! [X0,X1] :
( cType___24t(X0)
=> ( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
=> ( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
| ? [X2] :
( t(X2,X0)
& ? [X3] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X3)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_inversion_Coq.Init.Datatypes.list') ).
fof(f595,axiom,
! [X0] :
( c_24__type__32274___24t(X0)
<=> ! [X1] :
( cType___24t(X1)
=> ! [X2] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X1,X2)
=> ! [X3] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,X3)
=> cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,happ(happ(happ(X0,X1),X2),X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_32274') ).
fof(f738,axiom,
cType___24t(cA),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_A') ).
fof(f974,axiom,
c_24__type__32274___24t(cHahnTotalExt_2etot__ext),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_HahnTotalExt.tot_ext') ).
fof(f975,axiom,
cCoq_2eInit_2eDatatypes_2elist___24t(cA,cdom),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_dom') ).
fof(f1029,axiom,
cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,cr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_r') ).
fof(f1403,axiom,
! [X0] :
( cType___24t(X0)
=> ! [X1] :
( t(X1,X0)
=> ! [X2] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X2)
=> cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cHahnTotalExt_2eone__ext___24a3(X0,X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','HahnTotalExt.one_ext_trans') ).
fof(f1689,axiom,
! [X0] :
( cType___24t(X0)
=> ! [X1] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
=> cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','hahn.HahnRelationsBasic.transitive_ct') ).
fof(f1794,axiom,
! [X0,X1,X2] : happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2) = cHahnTotalExt_2etot__ext___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_HahnTotalExt.tot_ext_$a3') ).
fof(f1993,axiom,
! [X0,X1,X2] : happ(happ(happ(cHahnTotalExt_2eone__ext,X0),X1),X2) = cHahnTotalExt_2eone__ext___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_HahnTotalExt.one_ext_$a3') ).
fof(f2560,conjecture,
cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,cHahnTotalExt_2etot__ext___24a3(cA,cdom,cr)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f2561,negated_conjecture,
~ cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,cHahnTotalExt_2etot__ext___24a3(cA,cdom,cr)),
inference(negated_conjecture,[status(cth)],[f2560]) ).
fof(f2562,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,cHahnTotalExt_2etot__ext___24a3(cA,cdom,cr)),
inference(flattening,[],[f2561]) ).
fof(f2577,plain,
! [X0,X1,X2] :
( ( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) )
| ? [X3] :
( t(X3,X0)
& ? [X4] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X4)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X3,X4)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cHahnTotalExt_2eone__ext___24a3(X0,X3,cHahnTotalExt_2etot__ext___24a3(X0,X4,X2)) ) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(ennf_transformation,[],[f171]) ).
fof(f2578,plain,
! [X0,X1,X2] :
( ( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) )
| ? [X3] :
( t(X3,X0)
& ? [X4] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X4)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X3,X4)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cHahnTotalExt_2eone__ext___24a3(X0,X3,cHahnTotalExt_2etot__ext___24a3(X0,X4,X2)) ) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(flattening,[],[f2577]) ).
fof(f2615,plain,
! [X0,X1] :
( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
| ? [X2] :
( t(X2,X0)
& ? [X3] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X3)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X3) ) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(ennf_transformation,[],[f311]) ).
fof(f2616,plain,
! [X0,X1] :
( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
| ? [X2] :
( t(X2,X0)
& ? [X3] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,X3)
& X1 = cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X3) ) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(flattening,[],[f2615]) ).
fof(f2618,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( X4 = X5
& X2 = X3
& X0 = X1 )
| cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X4) != cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X3,X5) ),
inference(ennf_transformation,[],[f251]) ).
fof(f2619,plain,
! [X0] :
( ! [X1] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X1))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1) )
| ~ cType___24t(X0) ),
inference(ennf_transformation,[],[f1689]) ).
fof(f2642,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cHahnTotalExt_2eone__ext___24a3(X0,X1,X2))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X2) )
| ~ t(X1,X0) )
| ~ cType___24t(X0) ),
inference(ennf_transformation,[],[f1403]) ).
fof(f2644,plain,
! [X0] :
( c_24__type__32274___24t(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,happ(happ(happ(X0,X1),X2),X3))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,X3) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X1,X2) )
| ~ cType___24t(X1) ) ),
inference(ennf_transformation,[],[f595]) ).
fof(f2664,plain,
! [X0,X1,X2] :
( ( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) )
| ( t(sK4(X0,X1,X2),X0)
& cCoq_2eInit_2eDatatypes_2elist___24t(X0,sK5(X0,X1,X2))
& cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK4(X0,X1,X2),sK5(X0,X1,X2)) = X1
& cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cHahnTotalExt_2eone__ext___24a3(X0,sK4(X0,X1,X2),cHahnTotalExt_2etot__ext___24a3(X0,sK5(X0,X1,X2),X2)) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X0,X1,X2)),skolemize(X4,sK5(X0,X1,X2))],[f2578]) ).
fof(f2671,plain,
! [X0,X1] :
( X1 = cCoq_2eInit_2eDatatypes_2enil___24a1(X0)
| ( t(sK8(X0,X1),X0)
& cCoq_2eInit_2eDatatypes_2elist___24t(X0,sK9(X0,X1))
& cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK8(X0,X1),sK9(X0,X1)) = X1 )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X2,sK8(X0,X1)),skolemize(X3,sK9(X0,X1))],[f2616]) ).
fof(f2674,plain,
! [X0] :
( ( c_24__type__32274___24t(X0)
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,happ(happ(happ(X0,X1),X2),X3))
& cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,X3) )
& cCoq_2eInit_2eDatatypes_2elist___24t(X1,X2) )
& cType___24t(X1) ) )
& ( ! [X1] :
( ! [X2] :
( ! [X3] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,happ(happ(happ(X0,X1),X2),X3))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,X3) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X1,X2) )
| ~ cType___24t(X1) )
| ~ c_24__type__32274___24t(X0) ) ),
inference(nnf_transformation,[],[f2644]) ).
fof(f2675,plain,
! [X0] :
( ( c_24__type__32274___24t(X0)
| ? [X1] :
( ? [X2] :
( ? [X3] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,happ(happ(happ(X0,X1),X2),X3))
& cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X1,X3) )
& cCoq_2eInit_2eDatatypes_2elist___24t(X1,X2) )
& cType___24t(X1) ) )
& ( ! [X4] :
( ! [X5] :
( ! [X6] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,happ(happ(happ(X0,X4),X5),X6))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,X6) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X4,X5) )
| ~ cType___24t(X4) )
| ~ c_24__type__32274___24t(X0) ) ),
inference(rectify,[],[f2674]) ).
fof(f2676,plain,
! [X0] :
( ( c_24__type__32274___24t(X0)
| ( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(sK10(X0),happ(happ(happ(X0,sK10(X0)),sK11(X0)),sK12(X0)))
& cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(sK10(X0),sK12(X0))
& cCoq_2eInit_2eDatatypes_2elist___24t(sK10(X0),sK11(X0))
& cType___24t(sK10(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ! [X6] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,happ(happ(happ(X0,X4),X5),X6))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,X6) )
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X4,X5) )
| ~ cType___24t(X4) )
| ~ c_24__type__32274___24t(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X1,sK10(X0)),skolemize(X2,sK11(X0)),skolemize(X3,sK12(X0))],[f2675]) ).
fof(f2683,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,cHahnTotalExt_2etot__ext___24a3(cA,cdom,cr)),
inference(cnf_transformation,[],[f2562]) ).
fof(f2697,plain,
! [X2,X0,X1] : cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2),
inference(cnf_transformation,[],[f1794]) ).
fof(f2700,plain,
! [X2,X0,X1] :
( cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2)
| cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK4(X0,X1,X2),sK5(X0,X1,X2)) = X1
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2664]) ).
fof(f2701,plain,
! [X2,X0,X1] :
( cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2)
| cCoq_2eInit_2eDatatypes_2elist___24t(X0,sK5(X0,X1,X2))
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2664]) ).
fof(f2702,plain,
! [X2,X0,X1] :
( cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2)
| t(sK4(X0,X1,X2),X0)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2664]) ).
fof(f2703,plain,
! [X2,X0,X1] :
( cCoq_2eInit_2eDatatypes_2enil___24a1(X0) = X1
| cHahnTotalExt_2etot__ext___24a3(X0,X1,X2) = cHahnTotalExt_2eone__ext___24a3(X0,sK4(X0,X1,X2),cHahnTotalExt_2etot__ext___24a3(X0,sK5(X0,X1,X2),X2))
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2664]) ).
fof(f2704,plain,
! [X2,X0,X1] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK4(X0,X1,X2),sK5(X0,X1,X2)) = X1
| cCoq_2eInit_2eDatatypes_2enil___24a1(X0) = X1
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2664]) ).
fof(f2707,plain,
cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,cr),
inference(cnf_transformation,[],[f1029]) ).
fof(f2708,plain,
cCoq_2eInit_2eDatatypes_2elist___24t(cA,cdom),
inference(cnf_transformation,[],[f975]) ).
fof(f2709,plain,
cType___24t(cA),
inference(cnf_transformation,[],[f738]) ).
fof(f2737,plain,
c_24__type__32274___24t(cHahnTotalExt_2etot__ext),
inference(cnf_transformation,[],[f974]) ).
fof(f2739,plain,
! [X0,X1] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK8(X0,X1),sK9(X0,X1)) = X1
| cCoq_2eInit_2eDatatypes_2enil___24a1(X0) = X1
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2671]) ).
fof(f2743,plain,
! [X2,X3,X0,X1] : cCoq_2eInit_2eDatatypes_2enil___24a1(X0) != cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X2,X3),
inference(cnf_transformation,[],[f230]) ).
fof(f2745,plain,
! [X2,X3,X0,X1,X4,X5] :
( cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X4) != cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X3,X5)
| X2 = X3 ),
inference(cnf_transformation,[],[f2618]) ).
fof(f2746,plain,
! [X2,X3,X0,X1,X4,X5] :
( cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X2,X4) != cCoq_2eInit_2eDatatypes_2econs___24a3(X1,X3,X5)
| X4 = X5 ),
inference(cnf_transformation,[],[f2618]) ).
fof(f2747,plain,
! [X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X1))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2619]) ).
fof(f2763,plain,
! [X2,X0,X1] : cHahnTotalExt_2eone__ext___24a3(X0,X1,X2) = happ(happ(happ(cHahnTotalExt_2eone__ext,X0),X1),X2),
inference(cnf_transformation,[],[f1993]) ).
fof(f2764,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,cHahnTotalExt_2eone__ext___24a3(X0,X1,X2))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X2)
| ~ t(X1,X0)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f2642]) ).
fof(f2768,plain,
! [X0,X6,X4,X5] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,happ(happ(happ(X0,X4),X5),X6))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X4,X6)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X4,X5)
| ~ cType___24t(X4)
| ~ c_24__type__32274___24t(X0) ),
inference(cnf_transformation,[],[f2676]) ).
fof(f2790,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),cr)),
inference(definition_unfolding,[],[f2683,f2697]) ).
fof(f2792,plain,
! [X2,X0,X1] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2) = happ(happ(happ(cHahnTotalExt_2eone__ext,X0),sK4(X0,X1,X2)),happ(happ(happ(cHahnTotalExt_2etot__ext,X0),sK5(X0,X1,X2)),X2))
| cCoq_2eInit_2eDatatypes_2enil___24a1(X0) = X1
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f2703,f2697,f2763,f2697]) ).
fof(f2793,plain,
! [X2,X0,X1] :
( t(sK4(X0,X1,X2),X0)
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) = happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f2702,f2697]) ).
fof(f2794,plain,
! [X2,X0,X1] :
( cCoq_2eInit_2eDatatypes_2elist___24t(X0,sK5(X0,X1,X2))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) = happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f2701,f2697]) ).
fof(f2795,plain,
! [X2,X0,X1] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(X0,X1)
| cCoq_2eInit_2eDatatypes_2econs___24a3(X0,sK4(X0,X1,X2),sK5(X0,X1,X2)) = X1
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(X0,X2) = happ(happ(happ(cHahnTotalExt_2etot__ext,X0),X1),X2)
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f2700,f2697]) ).
fof(f2797,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(X0,happ(happ(happ(cHahnTotalExt_2eone__ext,X0),X1),X2))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X2)
| ~ t(X1,X0)
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f2764,f2763]) ).
fof(f2889,plain,
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK8(cA,cdom),sK9(cA,cdom))
| cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA)
| ~ cType___24t(cA) ),
inference(resolution,[],[f2739,f2708]) ).
fof(f2896,plain,
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK8(cA,cdom),sK9(cA,cdom))
| cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA) ),
inference(forward_subsumption_resolution,[],[f2889,f2709]) ).
fof(f2898,definition,
( spl18_3
<=> cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA) ),
introduced(definition,[new_symbols(definition,[spl18_3])],[avatar_definition]) ).
fof(f2900,plain,
( cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA)
| ~ spl18_3 ),
inference(avatar_component_clause,[],[f2898]) ).
fof(f2902,definition,
( spl18_4
<=> cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK8(cA,cdom),sK9(cA,cdom)) ),
introduced(definition,[new_symbols(definition,[spl18_4])],[avatar_definition]) ).
fof(f2904,plain,
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK8(cA,cdom),sK9(cA,cdom))
| ~ spl18_4 ),
inference(avatar_component_clause,[],[f2902]) ).
fof(f2905,plain,
( spl18_3
| spl18_4 ),
inference(avatar_split_clause,[],[f2896,f2902,f2898]) ).
fof(f2912,plain,
! [X0] :
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK4(cA,cdom,X0),sK5(cA,cdom,X0))
| cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA)
| ~ cType___24t(cA) ),
inference(resolution,[],[f2704,f2708]) ).
fof(f3070,plain,
! [X0] :
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK4(cA,cdom,X0),sK5(cA,cdom,X0))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)
| ~ cType___24t(cA) ),
inference(resolution,[],[f2795,f2708]) ).
fof(f3079,plain,
! [X0] :
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK4(cA,cdom,X0),sK5(cA,cdom,X0))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) ),
inference(forward_subsumption_resolution,[],[f3070,f2709]) ).
fof(f3080,plain,
! [X0,X1] :
( cCoq_2eInit_2eDatatypes_2enil___24a1(X0) != cdom
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X1) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X1) ),
inference(superposition,[],[f2743,f3079]) ).
fof(f3088,definition,
( spl18_5
<=> ! [X3] : cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X3) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X3) ),
introduced(definition,[new_symbols(definition,[spl18_5])],[avatar_definition]) ).
fof(f3089,plain,
( ! [X3] : cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X3) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X3)
| ~ spl18_5 ),
inference(avatar_component_clause,[],[f3088]) ).
fof(f3096,definition,
( spl18_7
<=> ! [X0] : cCoq_2eInit_2eDatatypes_2enil___24a1(X0) != cdom ),
introduced(definition,[new_symbols(definition,[spl18_7])],[avatar_definition]) ).
fof(f3097,plain,
( ! [X0] : cCoq_2eInit_2eDatatypes_2enil___24a1(X0) != cdom
| ~ spl18_7 ),
inference(avatar_component_clause,[],[f3096]) ).
fof(f3098,plain,
( spl18_5
| spl18_7 ),
inference(avatar_split_clause,[],[f3080,f3096,f3088]) ).
fof(f3116,plain,
( ~ cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,cr))
| ~ spl18_5 ),
inference(superposition,[],[f2790,f3089]) ).
fof(f3166,plain,
( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,cr)
| ~ cType___24t(cA)
| ~ spl18_5 ),
inference(resolution,[],[f3116,f2747]) ).
fof(f3167,plain,
( ~ cType___24t(cA)
| ~ spl18_5 ),
inference(forward_subsumption_resolution,[],[f3166,f2707]) ).
fof(f3168,plain,
( $false
| ~ spl18_5 ),
inference(forward_subsumption_resolution,[],[f3167,f2709]) ).
fof(f3169,plain,
~ spl18_5,
inference(avatar_contradiction_clause,[],[f3168]) ).
fof(f3178,plain,
( cdom != cdom
| ~ spl18_3
| ~ spl18_7 ),
inference(superposition,[],[f3097,f2900]) ).
fof(f3179,plain,
( $false
| ~ spl18_3
| ~ spl18_7 ),
inference(trivial_inequality_removal,[],[f3178]) ).
fof(f3180,plain,
( ~ spl18_3
| ~ spl18_7 ),
inference(avatar_contradiction_clause,[],[f3179]) ).
fof(f3181,plain,
( ! [X0] :
( cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK4(cA,cdom,X0),sK5(cA,cdom,X0))
| ~ cType___24t(cA) )
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f2912,f3097]) ).
fof(f3182,plain,
( ! [X0] : cdom = cCoq_2eInit_2eDatatypes_2econs___24a3(cA,sK4(cA,cdom,X0),sK5(cA,cdom,X0))
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3181,f2709]) ).
fof(f3231,plain,
( ! [X2,X0,X1] :
( cdom != cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X1,X2)
| sK8(cA,cdom) = X1 )
| ~ spl18_4 ),
inference(superposition,[],[f2745,f2904]) ).
fof(f3233,plain,
( ! [X2,X0,X1] :
( cdom != cCoq_2eInit_2eDatatypes_2econs___24a3(X0,X1,X2)
| sK9(cA,cdom) = X2 )
| ~ spl18_4 ),
inference(superposition,[],[f2746,f2904]) ).
fof(f3267,plain,
( ! [X0] :
( cdom != cdom
| sK8(cA,cdom) = sK4(cA,cdom,X0) )
| ~ spl18_4
| ~ spl18_7 ),
inference(superposition,[],[f3231,f3182]) ).
fof(f3268,plain,
( ! [X0] :
( cdom != cdom
| sK9(cA,cdom) = sK5(cA,cdom,X0) )
| ~ spl18_4
| ~ spl18_7 ),
inference(superposition,[],[f3233,f3182]) ).
fof(f3269,plain,
( ! [X0] : sK9(cA,cdom) = sK5(cA,cdom,X0)
| ~ spl18_4
| ~ spl18_7 ),
inference(trivial_inequality_removal,[],[f3268]) ).
fof(f3270,plain,
( ! [X0] : sK8(cA,cdom) = sK4(cA,cdom,X0)
| ~ spl18_4
| ~ spl18_7 ),
inference(trivial_inequality_removal,[],[f3267]) ).
fof(f3287,plain,
( ! [X0] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cA,cdom)
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7 ),
inference(superposition,[],[f2794,f3269]) ).
fof(f3289,plain,
( ! [X0] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3287,f2708]) ).
fof(f3292,plain,
( ! [X0] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom))
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) )
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3289,f2709]) ).
fof(f3294,definition,
( spl18_17
<=> cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom)) ),
introduced(definition,[new_symbols(definition,[spl18_17])],[avatar_definition]) ).
fof(f3296,plain,
( cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom))
| ~ spl18_17 ),
inference(avatar_component_clause,[],[f3294]) ).
fof(f3297,plain,
( spl18_5
| spl18_17
| ~ spl18_4
| ~ spl18_7 ),
inference(avatar_split_clause,[],[f3292,f3096,f2902,f3294,f3088]) ).
fof(f3317,plain,
! [X0] :
( happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) = happ(happ(happ(cHahnTotalExt_2eone__ext,cA),sK4(cA,cdom,X0)),happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK5(cA,cdom,X0)),X0))
| cdom = cCoq_2eInit_2eDatatypes_2enil___24a1(cA)
| ~ cType___24t(cA) ),
inference(resolution,[],[f2792,f2708]) ).
fof(f3327,plain,
( ! [X0] :
( happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) = happ(happ(happ(cHahnTotalExt_2eone__ext,cA),sK4(cA,cdom,X0)),happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK5(cA,cdom,X0)),X0))
| ~ cType___24t(cA) )
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3317,f3097]) ).
fof(f3328,plain,
( ! [X0] : happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) = happ(happ(happ(cHahnTotalExt_2eone__ext,cA),sK4(cA,cdom,X0)),happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK5(cA,cdom,X0)),X0))
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3327,f2709]) ).
fof(f3329,plain,
( ! [X0] : happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) = happ(happ(happ(cHahnTotalExt_2eone__ext,cA),sK4(cA,cdom,X0)),happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK9(cA,cdom)),X0))
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_demodulation,[],[f3328,f3269]) ).
fof(f3353,plain,
( ! [X0] :
( t(sK8(cA,cdom),cA)
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cA,cdom)
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7 ),
inference(superposition,[],[f2793,f3270]) ).
fof(f3355,plain,
( ! [X0] :
( t(sK8(cA,cdom),cA)
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3353,f2708]) ).
fof(f3358,plain,
( ! [X0] :
( t(sK8(cA,cdom),cA)
| cCoq_2eRelations_2eRelation__Operators_2eclos__trans___24a2(cA,X0) = happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) )
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_subsumption_resolution,[],[f3355,f2709]) ).
fof(f3360,definition,
( spl18_21
<=> t(sK8(cA,cdom),cA) ),
introduced(definition,[new_symbols(definition,[spl18_21])],[avatar_definition]) ).
fof(f3362,plain,
( t(sK8(cA,cdom),cA)
| ~ spl18_21 ),
inference(avatar_component_clause,[],[f3360]) ).
fof(f3363,plain,
( spl18_5
| spl18_21
| ~ spl18_4
| ~ spl18_7 ),
inference(avatar_split_clause,[],[f3358,f3096,f2902,f3360,f3088]) ).
fof(f3662,plain,
( ! [X0] : happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0) = happ(happ(happ(cHahnTotalExt_2eone__ext,cA),sK8(cA,cdom)),happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK9(cA,cdom)),X0))
| ~ spl18_4
| ~ spl18_7 ),
inference(forward_demodulation,[],[f3329,f3270]) ).
fof(f3666,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK9(cA,cdom)),X0))
| ~ t(sK8(cA,cdom),cA)
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7 ),
inference(superposition,[],[f2797,f3662]) ).
fof(f3682,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK9(cA,cdom)),X0))
| ~ cType___24t(cA) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f3666,f3362]) ).
fof(f3684,plain,
( ! [X0] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),sK9(cA,cdom)),X0))
| cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0)) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f3682,f2709]) ).
fof(f4670,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,X0)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cA,sK9(cA,cdom))
| ~ cType___24t(cA)
| ~ c_24__type__32274___24t(cHahnTotalExt_2etot__ext) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_21 ),
inference(resolution,[],[f3684,f2768]) ).
fof(f4671,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,X0)
| ~ cType___24t(cA)
| ~ c_24__type__32274___24t(cHahnTotalExt_2etot__ext) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f4670,f3296]) ).
fof(f4672,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,X0)
| ~ c_24__type__32274___24t(cHahnTotalExt_2etot__ext) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f4671,f2709]) ).
fof(f4673,plain,
( ! [X0] :
( cCoq_2eRelations_2eRelation__Definitions_2etransitive___24a2(cA,happ(happ(happ(cHahnTotalExt_2etot__ext,cA),cdom),X0))
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,X0) )
| ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f4672,f2737]) ).
fof(f4682,plain,
( ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cA,cr)
| ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(resolution,[],[f4673,f2790]) ).
fof(f4685,plain,
( $false
| ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(forward_subsumption_resolution,[],[f4682,f2707]) ).
fof(f4686,plain,
( ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(avatar_contradiction_clause,[],[f4685]) ).
cnf(s2,plain,
( spl18_3
| spl18_4 ),
inference(sat_conversion,[],[f2905]) ).
cnf(s5,plain,
( spl18_5
| spl18_7 ),
inference(sat_conversion,[],[f3098]) ).
cnf(s9,plain,
~ spl18_5,
inference(sat_conversion,[],[f3169]) ).
cnf(s10,plain,
( ~ spl18_3
| ~ spl18_7 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s13,plain,
( ~ spl18_4
| spl18_5
| ~ spl18_7
| spl18_17 ),
inference(sat_conversion,[],[f3297]) ).
cnf(s16,plain,
( ~ spl18_4
| spl18_5
| ~ spl18_7
| spl18_21 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s44,plain,
( ~ spl18_4
| ~ spl18_7
| ~ spl18_17
| ~ spl18_21 ),
inference(sat_conversion,[],[f4686]) ).
cnf(s45,plain,
spl18_7,
inference(rat,[],[s5,s9]) ).
cnf(s46,plain,
~ spl18_3,
inference(rat,[],[s10,s45]) ).
cnf(s48,plain,
spl18_4,
inference(rat,[],[s2,s46]) ).
cnf(s49,plain,
spl18_21,
inference(rat,[],[s16,s45,s9,s48]) ).
cnf(s50,plain,
spl18_17,
inference(rat,[],[s13,s45,s9,s48]) ).
cnf(s51,plain,
$false,
inference(rat,[],[s44,s48,s45,s49,s50]) ).
fof(f4687,plain,
$false,
inference(avatar_sat_refutation,[],[s51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV630+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.48 % Computer : n006.cluster.edu
% 0.20/0.48 % Model : x86_64 x86_64
% 0.20/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.48 % Memory : 8046.5625MB
% 0.20/0.48 % OS : Linux 6.8.0-71-generic
% 0.20/0.48 % CPULimit : 300
% 0.20/0.48 % WCLimit : 300
% 0.20/0.48 % DateTime : Mon Sep 28 06:44:25 UTC 2026
% 0.20/0.48 % CPUTime :
% 0.20/0.48 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.55 Running first-order theorem proving
% 0.25/0.55 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.49/1.96 % (3777469)Detected formulas, will run a generic FOF schedule.
% 2.49/1.96 % (3777479)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4120916762:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 2.49/1.96 % (3777478)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3996237483:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 2.49/1.96 % (3777477)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3040056294:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 2.49/1.96 % (3777475)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=2139434585:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 2.49/1.96 % (3777474)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=4230248868:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 2.49/1.96 % (3777476)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=1149724709:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 2.49/1.96 % (3777477)Refutation not found, incomplete strategy
% 2.49/1.96 % (3777477)------------------------------
% 2.49/1.96 % (3777477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777477)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777477)Termination reason: Refutation not found, incomplete strategy
% 2.49/1.96 % (3777477)Time elapsed: 0.017 s
% 2.49/1.96 % (3777477)Peak memory usage: 92 MB
% 2.49/1.96 % (3777477)Instructions burned: 13 (million)
% 2.49/1.96 % (3777480)dis-21_1_sil=8000:lcm=predicate:random_seed=4163302803:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 2.49/1.96 % (3777479)Instruction limit reached!
% 2.49/1.96 % (3777479)------------------------------
% 2.49/1.96 % (3777479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777479)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777479)Termination reason: Instruction limit
% 2.49/1.96 % (3777479)Termination phase: Preprocessing 3
% 2.49/1.96 % (3777479)Time elapsed: 0.079 s
% 2.49/1.96 % (3777479)Peak memory usage: 94 MB
% 2.49/1.96 % (3777479)Instructions burned: 139 (million)
% 2.49/1.96 % (3777478)Instruction limit reached!
% 2.49/1.96 % (3777478)------------------------------
% 2.49/1.96 % (3777478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777478)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777478)Termination reason: Instruction limit
% 2.49/1.96 % (3777478)Termination phase: Saturation
% 2.49/1.96 % (3777478)Time elapsed: 0.108 s
% 2.49/1.96 % (3777478)Peak memory usage: 92 MB
% 2.49/1.96 % (3777478)Instructions burned: 120 (million)
% 2.49/1.96 % (3777480)Instruction limit reached!
% 2.49/1.96 % (3777480)------------------------------
% 2.49/1.96 % (3777480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777480)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777480)Termination reason: Instruction limit
% 2.49/1.96 % (3777480)Termination phase: Clausification
% 2.49/1.96 % (3777480)Time elapsed: 0.130 s
% 2.49/1.96 % (3777480)Peak memory usage: 95 MB
% 2.49/1.96 % (3777480)Instructions burned: 129 (million)
% 2.49/1.96 % (3777488)lrs+10_1_sil=8000:sp=occurrence:random_seed=1979362206:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 2.49/1.96 % (3777489)lrs+10_1_sil=32000:urr=on:br=off:random_seed=349236673:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 2.49/1.96 % (3777488)First to succeed.
% 2.49/1.96 % (3777488)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3777469"
% 2.49/1.96 % (3777489)Refutation not found, incomplete strategy
% 2.49/1.96 % (3777489)------------------------------
% 2.49/1.96 % (3777489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777489)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777489)Termination reason: Refutation not found, incomplete strategy
% 2.49/1.96 % (3777489)Time elapsed: 0.044 s
% 2.49/1.96 % (3777489)Peak memory usage: 92 MB
% 2.49/1.96 % (3777489)Instructions burned: 44 (million)
% 2.49/1.96 % (3777477)------------------------------
% 2.49/1.96 % (3777477)------------------------------
% 2.49/1.96 % (3777490)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1161809215:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 2.49/1.96 % (3777490)Refutation not found, incomplete strategy
% 2.49/1.96 % (3777490)------------------------------
% 2.49/1.96 % (3777490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.49/1.96 % (3777490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/1.96 % (3777490)CaDiCaL version: 2.1.3
% 2.49/1.96 % (3777490)Termination reason: Refutation not found, incomplete strategy
% 2.49/1.96 % (3777490)Time elapsed: 0.020 s
% 2.49/1.96 % (3777490)Peak memory usage: 92 MB
% 2.49/1.96 % (3777490)Instructions burned: 13 (million)
% 2.49/1.96 % (3777488)Refutation found. Thanks to Tanya!
% 2.49/1.96 % SZS status Theorem for theBenchmark
% 2.49/1.96 % SZS output start Proof for theBenchmark
% See solution above
% 6.68/2.28 % (3777488)------------------------------
% 6.68/2.28 % (3777488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.68/2.28 % (3777488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/2.28 % (3777488)CaDiCaL version: 2.1.3
% 6.68/2.28 % (3777488)Termination reason: Refutation
% 6.68/2.28 % (3777488)Time elapsed: 0.077 s
% 6.68/2.28 % (3777488)Peak memory usage: 95 MB
% 6.68/2.28 % (3777488)Instructions burned: 138 (million)
% 6.68/2.28 % (3777488)------------------------------
% 6.68/2.28 % (3777488)------------------------------
% 6.68/2.28 % (3777469)Success in time 0.938 s
% 6.68/2.28 % Vampire exiting
%------------------------------------------------------------------------------