%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV667+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:59:38 PM UTC 2026
% Result : Theorem 29.04s 5.31s
% Output : Refutation 29.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 28
% Syntax : Number of formulae : 111 ( 65 unt; 0 def)
% Number of atoms : 273 ( 79 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 295 ( 133 ~; 125 |; 16 &)
% ( 4 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 16 con; 0-4 aty)
% Number of variables : 213 ( 207 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f163,axiom,
! [X0] : cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0) = c_24__type__2___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Coq.Sets.Ensembles.Ensemble') ).
fof(f243,axiom,
! [X0] : cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = cQuotients_2equotient__projection___24a3(cB,cS,cf___24a1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Quotients.InducedFunction2.projf') ).
fof(f244,axiom,
! [X0,X1,X2] : cQuotients_2eequiv__class___24a3(X0,X1,X2) = cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble___24a2(X0,c_24__lam__4329___24a3(X0,X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Quotients.equiv_class') ).
fof(f245,axiom,
! [X0,X1] : cQuotients_2eequiv__classes___24a2(X0,X1) = cCoq_2eSets_2eImage_2eIm___24a4(X0,cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0),cQuotients_2eequiv__class___24a2(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Quotients.equiv_classes') ).
fof(f248,axiom,
! [X0,X1,X2] : cQuotients_2equotient__projection___24a3(X0,X1,X2) = cCoq_2eInit_2eSpecif_2eexist___24a4(cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cCoq_2eSets_2eEnsembles_2eIn___24a2(cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cQuotients_2eequiv__classes___24a2(X0,X1)),cQuotients_2eequiv__class___24a3(X0,X1,X2),cQuotients_2eequiv__class__in__quotient___24a3(X0,X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Quotients.quotient_projection') ).
fof(f651,axiom,
! [X0] :
( c_24__type__163663___24t(X0)
<=> ! [X1] :
( cA___24t(X1)
=> cB___24t(happ(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_163663') ).
fof(f935,axiom,
cType___24t(cB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_B') ).
fof(f1579,axiom,
cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cB,cS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_S') ).
fof(f1580,axiom,
c_24__type__163663___24t(cf),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_f') ).
fof(f1873,axiom,
! [X0] :
( cType___24t(X0)
=> ! [X1] :
( cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
=> ( cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
=> ! [X2] :
( t(X2,X0)
=> ! [X3] :
( t(X3,X0)
=> ( p(happ(happ(X1,X2),X3))
=> cQuotients_2equotient__projection___24a3(X0,X1,X2) = cQuotients_2equotient__projection___24a3(X0,X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Quotients.quotient_projection_collapses_R') ).
fof(f1880,axiom,
cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(cB,cS),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivS) ).
fof(f1881,axiom,
! [X0] :
( cA___24t(X0)
=> ! [X1] :
( cA___24t(X1)
=> ( cR___24a2(X0,X1)
=> cS___24a2(cf___24a1(X0),cf___24a1(X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_defined2) ).
fof(f1916,axiom,
! [X0,X1] : happ(happ(cQuotients_2eequiv__class,X0),X1) = cQuotients_2eequiv__class___24a2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.equiv_class_$a2') ).
fof(f1927,axiom,
! [X0,X1,X2] : happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2) = cQuotients_2equotient__projection___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.quotient_projection_$a3') ).
fof(f1942,axiom,
! [X0,X1] : happ(happ(cQuotients_2eequiv__classes,X0),X1) = cQuotients_2eequiv__classes___24a2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.equiv_classes_$a2') ).
fof(f2018,axiom,
! [X0,X1,X2,X3] : happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,X0),X1),X2),X3) = cCoq_2eInit_2eSpecif_2eexist___24a4(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Coq.Init.Specif.exist_$a4') ).
fof(f2038,axiom,
! [X0,X1,X2] : happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2) = cQuotients_2eequiv__class___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.equiv_class_$a3') ).
fof(f2111,axiom,
! [X0] : happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0) = cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Coq.Sets.Ensembles.Full_set_$a1') ).
fof(f2191,axiom,
! [X0] : happ(cQuotients_2eInducedFunction2_2eprojf,X0) = cQuotients_2eInducedFunction2_2eprojf___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.InducedFunction2.projf_$a1') ).
fof(f2246,axiom,
! [X0,X1] :
( p(happ(happ(cS,X0),X1))
<=> cS___24a2(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_S_$a2') ).
fof(f2322,axiom,
! [X0] : happ(cf,X0) = cf___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_f_$a1') ).
fof(f2323,axiom,
! [X0,X1,X2] : happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2) = cQuotients_2eequiv__class__in__quotient___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Quotients.equiv_class_in_quotient_$a3') ).
fof(f2348,axiom,
! [X0,X1,X2,X3] : happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),X1),X2),X3) = cCoq_2eSets_2eImage_2eIm___24a4(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Coq.Sets.Image.Im_$a4') ).
fof(f2360,axiom,
! [X0,X1,X2] : happ(happ(happ(c_24__lam__4329,X0),X1),X2) = c_24__lam__4329___24a3(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_$_lam_4329_$a3') ).
fof(f2405,axiom,
! [X0,X1] : happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),X1) = cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble___24a2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_ZornsLemma.EnsemblesSpec.characteristic_function_to_ensemble_$a2') ).
fof(f2432,axiom,
! [X0,X1] : happ(happ(cCoq_2eSets_2eEnsembles_2eIn,X0),X1) = cCoq_2eSets_2eEnsembles_2eIn___24a2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Coq.Sets.Ensembles.In_$a2') ).
fof(f2657,axiom,
! [X0] :
( cB___24t(X0)
<=> t(X0,cB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$tdef_B') ).
fof(f2863,conjecture,
! [X0] :
( cA___24t(X0)
=> ! [X1] :
( cA___24t(X1)
=> ( cR___24a2(X0,X1)
=> cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = cQuotients_2eInducedFunction2_2eprojf___24a1(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f2864,negated_conjecture,
~ ! [X0] :
( cA___24t(X0)
=> ! [X1] :
( cA___24t(X1)
=> ( cR___24a2(X0,X1)
=> cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = cQuotients_2eInducedFunction2_2eprojf___24a1(X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f2863]) ).
fof(f2904,plain,
! [X0,X1] :
( cS___24a2(X0,X1)
=> p(happ(happ(cS,X0),X1)) ),
inference(unused_predicate_definition_removal,[],[f2246]) ).
fof(f3734,plain,
! [X0] :
( c_24__type__163663___24t(X0)
<=> ! [X1] :
( cB___24t(happ(X0,X1))
| ~ cA___24t(X1) ) ),
inference(ennf_transformation,[],[f651]) ).
fof(f4491,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( cQuotients_2equotient__projection___24a3(X0,X1,X2) = cQuotients_2equotient__projection___24a3(X0,X1,X3)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0) )
| ~ t(X2,X0) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1) )
| ~ cType___24t(X0) ),
inference(ennf_transformation,[],[f1873]) ).
fof(f4492,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( cQuotients_2equotient__projection___24a3(X0,X1,X2) = cQuotients_2equotient__projection___24a3(X0,X1,X3)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0) )
| ~ t(X2,X0) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1) )
| ~ cType___24t(X0) ),
inference(flattening,[],[f4491]) ).
fof(f4501,plain,
! [X0] :
( ! [X1] :
( cS___24a2(cf___24a1(X0),cf___24a1(X1))
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1) )
| ~ cA___24t(X0) ),
inference(ennf_transformation,[],[f1881]) ).
fof(f4502,plain,
! [X0] :
( ! [X1] :
( cS___24a2(cf___24a1(X0),cf___24a1(X1))
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1) )
| ~ cA___24t(X0) ),
inference(flattening,[],[f4501]) ).
fof(f4529,plain,
! [X0,X1] :
( p(happ(happ(cS,X0),X1))
| ~ cS___24a2(X0,X1) ),
inference(ennf_transformation,[],[f2904]) ).
fof(f4569,plain,
? [X0] :
( ? [X1] :
( cQuotients_2eInducedFunction2_2eprojf___24a1(X0) != cQuotients_2eInducedFunction2_2eprojf___24a1(X1)
& cR___24a2(X0,X1)
& cA___24t(X1) )
& cA___24t(X0) ),
inference(ennf_transformation,[],[f2864]) ).
fof(f4570,plain,
? [X0] :
( ? [X1] :
( cQuotients_2eInducedFunction2_2eprojf___24a1(X0) != cQuotients_2eInducedFunction2_2eprojf___24a1(X1)
& cR___24a2(X0,X1)
& cA___24t(X1) )
& cA___24t(X0) ),
inference(flattening,[],[f4569]) ).
fof(f8256,plain,
! [X0] :
( ( c_24__type__163663___24t(X0)
| ? [X1] :
( ~ cB___24t(happ(X0,X1))
& cA___24t(X1) ) )
& ( ! [X1] :
( cB___24t(happ(X0,X1))
| ~ cA___24t(X1) )
| ~ c_24__type__163663___24t(X0) ) ),
inference(nnf_transformation,[],[f3734]) ).
fof(f8257,plain,
! [X0] :
( ( c_24__type__163663___24t(X0)
| ? [X1] :
( ~ cB___24t(happ(X0,X1))
& cA___24t(X1) ) )
& ( ! [X2] :
( cB___24t(happ(X0,X2))
| ~ cA___24t(X2) )
| ~ c_24__type__163663___24t(X0) ) ),
inference(rectify,[],[f8256]) ).
fof(f8258,plain,
! [X0] :
( ( c_24__type__163663___24t(X0)
| ( ~ cB___24t(happ(X0,sK1701(X0)))
& cA___24t(sK1701(X0)) ) )
& ( ! [X2] :
( cB___24t(happ(X0,X2))
| ~ cA___24t(X2) )
| ~ c_24__type__163663___24t(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1701]),skolemize(X1,sK1701(X0))],[f8257]) ).
fof(f9916,plain,
! [X0] :
( ( cB___24t(X0)
| ~ t(X0,cB) )
& ( t(X0,cB)
| ~ cB___24t(X0) ) ),
inference(nnf_transformation,[],[f2657]) ).
fof(f10109,plain,
( cQuotients_2eInducedFunction2_2eprojf___24a1(sK2429) != cQuotients_2eInducedFunction2_2eprojf___24a1(sK2430)
& cR___24a2(sK2429,sK2430)
& cA___24t(sK2430)
& cA___24t(sK2429) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2429,sK2430]),skolemize(X0,sK2429),skolemize(X1,sK2430)],[f4570]) ).
fof(f11148,plain,
! [X0] : cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0) = c_24__type__2___24a1(X0),
inference(cnf_transformation,[],[f163]) ).
fof(f11743,plain,
! [X0] : cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = cQuotients_2equotient__projection___24a3(cB,cS,cf___24a1(X0)),
inference(cnf_transformation,[],[f243]) ).
fof(f11744,plain,
! [X2,X0,X1] : cQuotients_2eequiv__class___24a3(X0,X1,X2) = cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble___24a2(X0,c_24__lam__4329___24a3(X0,X1,X2)),
inference(cnf_transformation,[],[f244]) ).
fof(f11745,plain,
! [X0,X1] : cQuotients_2eequiv__classes___24a2(X0,X1) = cCoq_2eSets_2eImage_2eIm___24a4(X0,cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0),cQuotients_2eequiv__class___24a2(X0,X1)),
inference(cnf_transformation,[],[f245]) ).
fof(f11748,plain,
! [X2,X0,X1] : cQuotients_2equotient__projection___24a3(X0,X1,X2) = cCoq_2eInit_2eSpecif_2eexist___24a4(cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cCoq_2eSets_2eEnsembles_2eIn___24a2(cCoq_2eSets_2eEnsembles_2eEnsemble___24a1(X0),cQuotients_2eequiv__classes___24a2(X0,X1)),cQuotients_2eequiv__class___24a3(X0,X1,X2),cQuotients_2eequiv__class__in__quotient___24a3(X0,X1,X2)),
inference(cnf_transformation,[],[f248]) ).
fof(f13544,plain,
! [X2,X0] :
( ~ c_24__type__163663___24t(X0)
| ~ cA___24t(X2)
| cB___24t(happ(X0,X2)) ),
inference(cnf_transformation,[],[f8258]) ).
fof(f14693,plain,
cType___24t(cB),
inference(cnf_transformation,[],[f935]) ).
fof(f15337,plain,
cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cB,cS),
inference(cnf_transformation,[],[f1579]) ).
fof(f15338,plain,
c_24__type__163663___24t(cf),
inference(cnf_transformation,[],[f1580]) ).
fof(f16107,plain,
! [X2,X3,X0,X1] :
( cQuotients_2equotient__projection___24a3(X0,X1,X2) = cQuotients_2equotient__projection___24a3(X0,X1,X3)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(cnf_transformation,[],[f4492]) ).
fof(f16115,plain,
cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(cB,cS),
inference(cnf_transformation,[],[f1880]) ).
fof(f16116,plain,
! [X0,X1] :
( cS___24a2(cf___24a1(X0),cf___24a1(X1))
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(cnf_transformation,[],[f4502]) ).
fof(f16160,plain,
! [X0,X1] : cQuotients_2eequiv__class___24a2(X0,X1) = happ(happ(cQuotients_2eequiv__class,X0),X1),
inference(cnf_transformation,[],[f1916]) ).
fof(f16173,plain,
! [X2,X0,X1] : cQuotients_2equotient__projection___24a3(X0,X1,X2) = happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2),
inference(cnf_transformation,[],[f1927]) ).
fof(f16193,plain,
! [X0,X1] : cQuotients_2eequiv__classes___24a2(X0,X1) = happ(happ(cQuotients_2eequiv__classes,X0),X1),
inference(cnf_transformation,[],[f1942]) ).
fof(f16288,plain,
! [X2,X3,X0,X1] : happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,X0),X1),X2),X3) = cCoq_2eInit_2eSpecif_2eexist___24a4(X0,X1,X2,X3),
inference(cnf_transformation,[],[f2018]) ).
fof(f16315,plain,
! [X2,X0,X1] : cQuotients_2eequiv__class___24a3(X0,X1,X2) = happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2),
inference(cnf_transformation,[],[f2038]) ).
fof(f16404,plain,
! [X0] : cCoq_2eSets_2eEnsembles_2eFull__set___24a1(X0) = happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0),
inference(cnf_transformation,[],[f2111]) ).
fof(f16498,plain,
! [X0] : cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = happ(cQuotients_2eInducedFunction2_2eprojf,X0),
inference(cnf_transformation,[],[f2191]) ).
fof(f16566,plain,
! [X0,X1] :
( p(happ(happ(cS,X0),X1))
| ~ cS___24a2(X0,X1) ),
inference(cnf_transformation,[],[f4529]) ).
fof(f16663,plain,
! [X0] : cf___24a1(X0) = happ(cf,X0),
inference(cnf_transformation,[],[f2322]) ).
fof(f16664,plain,
! [X2,X0,X1] : cQuotients_2eequiv__class__in__quotient___24a3(X0,X1,X2) = happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2),
inference(cnf_transformation,[],[f2323]) ).
fof(f16694,plain,
! [X2,X3,X0,X1] : cCoq_2eSets_2eImage_2eIm___24a4(X0,X1,X2,X3) = happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),X1),X2),X3),
inference(cnf_transformation,[],[f2348]) ).
fof(f16707,plain,
! [X2,X0,X1] : c_24__lam__4329___24a3(X0,X1,X2) = happ(happ(happ(c_24__lam__4329,X0),X1),X2),
inference(cnf_transformation,[],[f2360]) ).
fof(f16761,plain,
! [X0,X1] : happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),X1) = cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble___24a2(X0,X1),
inference(cnf_transformation,[],[f2405]) ).
fof(f16795,plain,
! [X0,X1] : happ(happ(cCoq_2eSets_2eEnsembles_2eIn,X0),X1) = cCoq_2eSets_2eEnsembles_2eIn___24a2(X0,X1),
inference(cnf_transformation,[],[f2432]) ).
fof(f17228,plain,
! [X0] :
( ~ cB___24t(X0)
| t(X0,cB) ),
inference(cnf_transformation,[],[f9916]) ).
fof(f17627,plain,
cA___24t(sK2429),
inference(cnf_transformation,[],[f10109]) ).
fof(f17628,plain,
cA___24t(sK2430),
inference(cnf_transformation,[],[f10109]) ).
fof(f17629,plain,
cR___24a2(sK2429,sK2430),
inference(cnf_transformation,[],[f10109]) ).
fof(f17630,plain,
cQuotients_2eInducedFunction2_2eprojf___24a1(sK2429) != cQuotients_2eInducedFunction2_2eprojf___24a1(sK2430),
inference(cnf_transformation,[],[f10109]) ).
fof(f17649,plain,
! [X0,X1] : cQuotients_2eequiv__classes___24a2(X0,X1) = happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)),
inference(definition_unfolding,[],[f11745,f16694,f11148,f16404,f16160]) ).
fof(f17650,plain,
! [X2,X0,X1] : cQuotients_2eequiv__class___24a3(X0,X1,X2) = happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2)),
inference(definition_unfolding,[],[f11744,f16761,f16707]) ).
fof(f17651,plain,
! [X2,X0,X1] : cQuotients_2equotient__projection___24a3(X0,X1,X2) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)),
inference(definition_unfolding,[],[f11748,f16288,f11148,f16795,f11148,f17649,f17650,f16664]) ).
fof(f17652,plain,
! [X0] : cQuotients_2eInducedFunction2_2eprojf___24a1(X0) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,cB),happ(happ(happ(c_24__lam__4329,cB),cS),happ(cf,X0)))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,X0))),
inference(definition_unfolding,[],[f11743,f17651,f16663]) ).
fof(f18860,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X3))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X3))
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(definition_unfolding,[],[f16107,f17651,f17651]) ).
fof(f18866,plain,
! [X0,X1] :
( cS___24a2(happ(cf,X0),happ(cf,X1))
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(definition_unfolding,[],[f16116,f16663,f16663]) ).
fof(f18871,plain,
! [X2,X0,X1] : happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)),
inference(definition_unfolding,[],[f16173,f17651]) ).
fof(f18872,plain,
! [X0,X1] : happ(happ(cQuotients_2eequiv__classes,X0),X1) = happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)),
inference(definition_unfolding,[],[f16193,f17649]) ).
fof(f18877,plain,
! [X2,X0,X1] : happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2) = happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2)),
inference(definition_unfolding,[],[f16315,f17650]) ).
fof(f18884,plain,
! [X0] : happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,cB),happ(happ(happ(c_24__lam__4329,cB),cS),happ(cf,X0)))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,X0))),
inference(definition_unfolding,[],[f16498,f17652]) ).
fof(f18957,plain,
happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,cB),happ(happ(happ(c_24__lam__4329,cB),cS),happ(cf,sK2429)))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,sK2429))) != happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,cB),happ(happ(happ(c_24__lam__4329,cB),cS),happ(cf,sK2430)))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,sK2430))),
inference(definition_unfolding,[],[f17630,f17652,f17652]) ).
fof(f19082,plain,
! [X2,X0,X1] : happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2)),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)),
inference(forward_demodulation,[],[f18871,f18877]) ).
fof(f19086,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,X0),c_24__type__2___24a1(X0)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,X0)),happ(happ(cQuotients_2eequiv__class,X0),X1)))),happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X3)),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X3))
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(forward_demodulation,[],[f18860,f18877]) ).
fof(f19903,plain,
! [X2,X0,X1] : happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(cQuotients_2eequiv__classes,X0),X1))),happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2)),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)),
inference(forward_demodulation,[],[f19082,f18872]) ).
fof(f19907,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(cQuotients_2eequiv__classes,X0),X1))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(cQuotients_2eequiv__classes,X0),X1))),happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X3)),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X3))
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(forward_demodulation,[],[f19086,f18872]) ).
fof(f19927,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(cQuotients_2eequiv__classes,X0),X1))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,X0),happ(happ(happ(c_24__lam__4329,X0),X1),X2))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)) = happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X3)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(forward_demodulation,[],[f19907,f19903]) ).
fof(f19938,plain,
! [X2,X3,X0,X1] :
( happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(X0)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(X0)),happ(happ(cQuotients_2eequiv__classes,X0),X1))),happ(happ(happ(cQuotients_2eequiv__class,X0),X1),X2)),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,X0),X1),X2)) = happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X3)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(forward_demodulation,[],[f19927,f18877]) ).
fof(f19943,plain,
! [X2,X3,X0,X1] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2eequivalence___24a2(X0,X1)
| ~ p(happ(happ(X1,X2),X3))
| ~ t(X3,X0)
| ~ t(X2,X0)
| happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X2) = happ(happ(happ(cQuotients_2equotient__projection,X0),X1),X3)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(X0,X1)
| ~ cType___24t(X0) ),
inference(forward_demodulation,[],[f19938,f19903]) ).
fof(f19946,plain,
! [X0] :
( cB___24t(happ(cf,X0))
| ~ cA___24t(X0) ),
inference(resolution,[],[f15338,f13544]) ).
fof(f19948,plain,
happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(cZornsLemma_2eEnsemblesSpec_2echaracteristic__function__to__ensemble,cB),happ(happ(happ(c_24__lam__4329,cB),cS),happ(cf,sK2429)))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,sK2429))) != happ(cQuotients_2eInducedFunction2_2eprojf,sK2430),
inference(superposition,[],[f18957,f18884]) ).
fof(f19951,plain,
happ(cQuotients_2eInducedFunction2_2eprojf,sK2430) != happ(cQuotients_2eInducedFunction2_2eprojf,sK2429),
inference(forward_demodulation,[],[f19948,f18884]) ).
fof(f19973,plain,
! [X0,X1] :
( ~ p(happ(happ(cS,X0),X1))
| ~ t(X1,cB)
| ~ t(X0,cB)
| happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X0) = happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X1)
| ~ cCoq_2eRelations_2eRelation__Definitions_2erelation___24t(cB,cS)
| ~ cType___24t(cB) ),
inference(resolution,[],[f19943,f16115]) ).
fof(f19976,plain,
! [X0,X1] :
( ~ p(happ(happ(cS,X0),X1))
| ~ t(X1,cB)
| ~ t(X0,cB)
| happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X0) = happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X1) ),
inference(global_subsumption,[],[f19973,f14693,f15337]) ).
fof(f19983,plain,
! [X0] :
( t(happ(cf,X0),cB)
| ~ cA___24t(X0) ),
inference(resolution,[],[f19946,f17228]) ).
fof(f20028,plain,
! [X0,X1] :
( ~ cS___24a2(X1,X0)
| ~ t(X1,cB)
| happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X0) = happ(happ(happ(cQuotients_2equotient__projection,cB),cS),X1)
| ~ t(X0,cB) ),
inference(resolution,[],[f19976,f16566]) ).
fof(f20387,plain,
! [X0] : happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(happ(happ(cCoq_2eSets_2eImage_2eIm,cB),c_24__type__2___24a1(cB)),happ(cCoq_2eSets_2eEnsembles_2eFull__set,cB)),happ(happ(cQuotients_2eequiv__class,cB),cS)))),happ(happ(happ(cQuotients_2eequiv__class,cB),cS),happ(cf,X0))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,X0))),
inference(superposition,[],[f18884,f18877]) ).
fof(f20389,plain,
! [X0] : happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(happ(happ(happ(cCoq_2eInit_2eSpecif_2eexist,c_24__type__2___24a1(cB)),happ(happ(cCoq_2eSets_2eEnsembles_2eIn,c_24__type__2___24a1(cB)),happ(happ(cQuotients_2eequiv__classes,cB),cS))),happ(happ(happ(cQuotients_2eequiv__class,cB),cS),happ(cf,X0))),happ(happ(happ(cQuotients_2eequiv__class__in__quotient,cB),cS),happ(cf,X0))),
inference(forward_demodulation,[],[f20387,f18872]) ).
fof(f20391,plain,
! [X0] : happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(happ(happ(cQuotients_2equotient__projection,cB),cS),happ(cf,X0)),
inference(forward_demodulation,[],[f20389,f19903]) ).
fof(f20432,plain,
! [X0,X1] :
( ~ t(happ(cf,X0),cB)
| happ(happ(happ(cQuotients_2equotient__projection,cB),cS),happ(cf,X0)) = happ(happ(happ(cQuotients_2equotient__projection,cB),cS),happ(cf,X1))
| ~ t(happ(cf,X1),cB)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(resolution,[],[f20028,f18866]) ).
fof(f20433,plain,
! [X0,X1] :
( happ(happ(happ(cQuotients_2equotient__projection,cB),cS),happ(cf,X0)) = happ(cQuotients_2eInducedFunction2_2eprojf,X1)
| ~ t(happ(cf,X0),cB)
| ~ t(happ(cf,X1),cB)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(forward_demodulation,[],[f20432,f20391]) ).
fof(f20434,plain,
! [X0,X1] :
( happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(cQuotients_2eInducedFunction2_2eprojf,X1)
| ~ t(happ(cf,X0),cB)
| ~ t(happ(cf,X1),cB)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(forward_demodulation,[],[f20433,f20391]) ).
fof(f20435,plain,
! [X0,X1] :
( ~ t(happ(cf,X1),cB)
| happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(cQuotients_2eInducedFunction2_2eprojf,X1)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0) ),
inference(global_subsumption,[],[f20434,f19983]) ).
fof(f21240,plain,
! [X0,X1] :
( happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(cQuotients_2eInducedFunction2_2eprojf,X1)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| ~ cA___24t(X0)
| ~ cA___24t(X1) ),
inference(resolution,[],[f20435,f19983]) ).
fof(f21241,plain,
! [X0,X1] :
( ~ cA___24t(X0)
| ~ cR___24a2(X0,X1)
| ~ cA___24t(X1)
| happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(cQuotients_2eInducedFunction2_2eprojf,X1) ),
inference(duplicate_literal_removal,[],[f21240]) ).
fof(f23130,plain,
! [X0] :
( ~ cR___24a2(sK2429,X0)
| ~ cA___24t(X0)
| happ(cQuotients_2eInducedFunction2_2eprojf,X0) = happ(cQuotients_2eInducedFunction2_2eprojf,sK2429) ),
inference(resolution,[],[f21241,f17627]) ).
fof(f23654,plain,
( ~ cA___24t(sK2430)
| happ(cQuotients_2eInducedFunction2_2eprojf,sK2430) = happ(cQuotients_2eInducedFunction2_2eprojf,sK2429) ),
inference(resolution,[],[f23130,f17629]) ).
fof(f23658,plain,
$false,
inference(global_subsumption,[],[f23654,f19951,f17628]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV667+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n001.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 06:57:18 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.64/2.28 % (169225)Will run a generic schedule for satisfiability detection.
% 11.64/2.28 % (169232)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1306729900:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 11.64/2.28 % (169231)% WARNING: option uhcvi not known.
% 11.64/2.28 % (169230)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2359840954_2998 on theBenchmark for (2998ds/0Mi)
% 11.64/2.28 % (169233)dis+10_1_sil=32000:sp=arity:random_seed=1032757724:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 11.64/2.28 % (169231)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1958867106:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 11.64/2.28 % (169234)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1028217037:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 11.64/2.28 % (169235)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3878503712:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 11.64/2.28 % (169236)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=893459177:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 11.64/2.28 % (169233)Instruction limit reached!
% 11.64/2.28 % (169233)------------------------------
% 11.64/2.28 % (169233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/2.28 % (169233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.28 % (169233)CaDiCaL version: 2.1.3
% 11.64/2.28 % (169233)Termination reason: Instruction limit
% 11.64/2.28 % (169233)Termination phase: Preprocessing 3
% 11.64/2.28 % (169233)Time elapsed: 0.063 s
% 11.64/2.28 % (169233)Peak memory usage: 19 MB
% 11.64/2.28 % (169233)Instructions burned: 103 (million)
% 11.64/2.28 % (169234)Instruction limit reached!
% 11.64/2.28 % (169234)------------------------------
% 11.64/2.28 % (169234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/2.28 % (169234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.28 % (169234)CaDiCaL version: 2.1.3
% 11.64/2.28 % (169234)Termination reason: Instruction limit
% 11.64/2.28 % (169234)Termination phase: NewCNF
% 11.64/2.28 % (169234)Time elapsed: 0.071 s
% 11.64/2.28 % (169234)Peak memory usage: 19 MB
% 11.64/2.28 % (169234)Instructions burned: 117 (million)
% 11.64/2.28 % (169235)Instruction limit reached!
% 11.64/2.28 % (169235)------------------------------
% 11.64/2.28 % (169235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/2.28 % (169235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.28 % (169235)CaDiCaL version: 2.1.3
% 11.64/2.28 % (169235)Termination reason: Instruction limit
% 11.64/2.28 % (169235)Termination phase: Property scanning
% 11.64/2.28 % (169235)Time elapsed: 0.080 s
% 11.64/2.28 % (169235)Peak memory usage: 21 MB
% 11.64/2.28 % (169235)Instructions burned: 132 (million)
% 11.64/2.28 % (169244)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=995535566:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 11.64/2.28 % (169236)Instruction limit reached!
% 11.64/2.28 % (169236)------------------------------
% 11.64/2.28 % (169236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/2.28 % (169236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.28 % (169236)CaDiCaL version: 2.1.3
% 11.64/2.29 % (169236)Termination reason: Instruction limit
% 11.64/2.29 % (169236)Termination phase: Property scanning
% 11.64/2.29 % (169236)Time elapsed: 0.090 s
% 11.64/2.29 % (169236)Peak memory usage: 21 MB
% 11.64/2.29 % (169236)Instructions burned: 159 (million)
% 11.64/2.29 % (169245)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=853103404:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 11.64/2.29 % (169246)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=398121986:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 11.64/2.29 % (169249)ott-21_1_sil=16000:fs=off:random_seed=3893702550:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 11.64/2.29 % (169245)Instruction limit reached!
% 11.64/2.29 % (169245)------------------------------
% 11.64/2.29 % (169245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.64/2.29 % (169245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.64/2.29 % (169245)CaDiCaL version: 2.1.3
% 11.64/2.29 % (169245)Termination reason: Instruction limit
% 26.10/4.29 % (169245)Termination phase: Property scanning
% 26.10/4.29 % (169245)Time elapsed: 0.080 s
% 26.10/4.29 % (169245)Peak memory usage: 21 MB
% 26.10/4.29 % (169245)Instructions burned: 134 (million)
% 26.10/4.29 % (169252)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4219641805:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 26.10/4.29 % (169249)Instruction limit reached!
% 26.10/4.29 % (169249)------------------------------
% 26.10/4.29 % (169249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169249)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169249)Termination reason: Instruction limit
% 26.10/4.29 % (169249)Termination phase: Property scanning
% 26.10/4.29 % (169249)Time elapsed: 0.096 s
% 26.10/4.29 % (169249)Peak memory usage: 21 MB
% 26.10/4.29 % (169249)Instructions burned: 181 (million)
% 26.10/4.29 % (169254)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2452092112:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 26.10/4.29 % (169246)Instruction limit reached!
% 26.10/4.29 % (169246)------------------------------
% 26.10/4.29 % (169246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169246)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169246)Termination reason: Instruction limit
% 26.10/4.29 % (169246)Termination phase: Saturation
% 26.10/4.29 % (169246)Time elapsed: 0.304 s
% 26.10/4.29 % (169246)Peak memory usage: 25 MB
% 26.10/4.29 % (169246)Instructions burned: 685 (million)
% 26.10/4.29 % (169244)Instruction limit reached!
% 26.10/4.29 % (169244)------------------------------
% 26.10/4.29 % (169244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169244)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169244)Termination reason: Instruction limit
% 26.10/4.29 % (169244)Termination phase: Finite model building preprocessing
% 26.10/4.29 % (169244)Time elapsed: 0.339 s
% 26.10/4.29 % (169244)Peak memory usage: 30 MB
% 26.10/4.29 % (169244)Instructions burned: 716 (million)
% 26.10/4.29 % (169252)Instruction limit reached!
% 26.10/4.29 % (169252)------------------------------
% 26.10/4.29 % (169252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169252)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169252)Termination reason: Instruction limit
% 26.10/4.29 % (169252)Termination phase: Saturation
% 26.10/4.29 % (169252)Time elapsed: 0.230 s
% 26.10/4.29 % (169252)Peak memory usage: 25 MB
% 26.10/4.29 % (169252)Instructions burned: 479 (million)
% 26.10/4.29 % (169256)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1487534194:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 26.10/4.29 % (169257)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2708394166:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 26.10/4.29 % (169258)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=297695866:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 26.10/4.29 % (169254)Instruction limit reached!
% 26.10/4.29 % (169254)------------------------------
% 26.10/4.29 % (169254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169254)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169254)Termination reason: Instruction limit
% 26.10/4.29 % (169254)Termination phase: Finite model building preprocessing
% 26.10/4.29 % (169254)Time elapsed: 0.421 s
% 26.10/4.29 % (169254)Peak memory usage: 27 MB
% 26.10/4.29 % (169254)Instructions burned: 866 (million)
% 26.10/4.29 % (169262)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3853930385:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 26.10/4.29 % (169258)Instruction limit reached!
% 26.10/4.29 % (169258)------------------------------
% 26.10/4.29 % (169258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.10/4.29 % (169258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.10/4.29 % (169258)CaDiCaL version: 2.1.3
% 26.10/4.29 % (169258)Termination reason: Instruction limit
% 29.04/5.31 % (169258)Termination phase: Saturation
% 29.04/5.31 % (169258)Time elapsed: 0.328 s
% 29.04/5.31 % (169258)Peak memory usage: 28 MB
% 29.04/5.31 % (169258)Instructions burned: 693 (million)
% 29.04/5.31 % (169264)fmb+10_1_sil=64000:random_seed=929114928:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 29.04/5.31 % (169257)Instruction limit reached!
% 29.04/5.31 % (169257)------------------------------
% 29.04/5.31 % (169257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169257)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169257)Termination reason: Instruction limit
% 29.04/5.31 % (169257)Termination phase: Finite model building preprocessing
% 29.04/5.31 % (169257)Time elapsed: 0.427 s
% 29.04/5.31 % (169257)Peak memory usage: 28 MB
% 29.04/5.31 % (169257)Instructions burned: 889 (million)
% 29.04/5.31 % (169266)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1157295556:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 29.04/5.31 % (169256)Instruction limit reached!
% 29.04/5.31 % (169256)------------------------------
% 29.04/5.31 % (169256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169256)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169256)Termination reason: Instruction limit
% 29.04/5.31 % (169256)Termination phase: Saturation
% 29.04/5.31 % (169256)Time elapsed: 0.609 s
% 29.04/5.31 % (169256)Peak memory usage: 37 MB
% 29.04/5.31 % (169256)Instructions burned: 1180 (million)
% 29.04/5.31 % (169268)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2782667236:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 29.04/5.31 % (169262)Instruction limit reached!
% 29.04/5.31 % (169262)------------------------------
% 29.04/5.31 % (169262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169262)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169262)Termination reason: Instruction limit
% 29.04/5.31 % (169262)Termination phase: Saturation
% 29.04/5.31 % (169262)Time elapsed: 0.397 s
% 29.04/5.31 % (169262)Peak memory usage: 32 MB
% 29.04/5.31 % (169262)Instructions burned: 879 (million)
% 29.04/5.31 % (169270)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=81339368:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 29.04/5.31 % TRYING [1]
% 29.04/5.31 % (169230)Cannot represent all propositional literals internally
% 29.04/5.31 % (169230)Refutation not found, incomplete strategy
% 29.04/5.31 % (169230)------------------------------
% 29.04/5.31 % (169230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169230)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169230)Termination reason: Refutation not found, incomplete strategy
% 29.04/5.31 % (169230)Time elapsed: 1.441 s
% 29.04/5.31 % (169230)Peak memory usage: 65 MB
% 29.04/5.31 % (169230)Instructions burned: 2971 (million)
% 29.04/5.31 % (169230)------------------------------
% 29.04/5.31 % (169230)------------------------------
% 29.04/5.31 % (169272)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1444934998:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 29.04/5.31 % (169268)Instruction limit reached!
% 29.04/5.31 % (169268)------------------------------
% 29.04/5.31 % (169268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169268)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169268)Termination reason: Instruction limit
% 29.04/5.31 % (169268)Termination phase: Finite model building preprocessing
% 29.04/5.31 % (169268)Time elapsed: 0.446 s
% 29.04/5.31 % (169268)Peak memory usage: 28 MB
% 29.04/5.31 % (169268)Instructions burned: 920 (million)
% 29.04/5.31 % (169274)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3704453310:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 29.04/5.31 % TRYING [1]
% 29.04/5.31 % (169264)Cannot represent all propositional literals internally
% 29.04/5.31 % (169264)Refutation not found, incomplete strategy
% 29.04/5.31 % (169264)------------------------------
% 29.04/5.31 % (169264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169264)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169264)Termination reason: Refutation not found, incomplete strategy
% 29.04/5.31 % (169264)Time elapsed: 0.920 s
% 29.04/5.31 % (169264)Peak memory usage: 46 MB
% 29.04/5.31 % (169264)Instructions burned: 1905 (million)
% 29.04/5.31 % (169264)------------------------------
% 29.04/5.31 % (169264)------------------------------
% 29.04/5.31 % (169276)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2760370350:fmbsr=2.30978:i=2174_2981 on theBenchmark for (2981ds/2174Mi)
% 29.04/5.31 % (169266)Cannot represent all propositional literals internally
% 29.04/5.31 % (169266)Refutation not found, incomplete strategy
% 29.04/5.31 % (169266)------------------------------
% 29.04/5.31 % (169266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169266)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169266)Termination reason: Refutation not found, incomplete strategy
% 29.04/5.31 % (169266)Time elapsed: 0.957 s
% 29.04/5.31 % (169266)Peak memory usage: 45 MB
% 29.04/5.31 % (169266)Instructions burned: 1996 (million)
% 29.04/5.31 % (169266)------------------------------
% 29.04/5.31 % (169266)------------------------------
% 29.04/5.31 % (169278)ott-2_1_sil=16000:newcnf=on:random_seed=449757508:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2979 on theBenchmark for (2979ds/869Mi)
% 29.04/5.31 % (169272)Instruction limit reached!
% 29.04/5.31 % (169272)------------------------------
% 29.04/5.31 % (169272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169272)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169272)Termination reason: Instruction limit
% 29.04/5.31 % (169272)Termination phase: Saturation
% 29.04/5.31 % (169272)Time elapsed: 0.570 s
% 29.04/5.31 % (169272)Peak memory usage: 27 MB
% 29.04/5.31 % (169272)Instructions burned: 1473 (million)
% 29.04/5.31 % (169280)ott+10_1_sil=32000:tgt=ground:random_seed=484510925:i=5114:av=off_2978 on theBenchmark for (2978ds/5114Mi)
% 29.04/5.31 % (169278)Instruction limit reached!
% 29.04/5.31 % (169278)------------------------------
% 29.04/5.31 % (169278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169278)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169278)Termination reason: Instruction limit
% 29.04/5.31 % (169278)Termination phase: Saturation
% 29.04/5.31 % (169278)Time elapsed: 0.389 s
% 29.04/5.31 % (169278)Peak memory usage: 27 MB
% 29.04/5.31 % (169278)Instructions burned: 870 (million)
% 29.04/5.31 % (169282)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3231465760:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 29.04/5.31 % (169276)Instruction limit reached!
% 29.04/5.31 % (169276)------------------------------
% 29.04/5.31 % (169276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169276)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169276)Termination reason: Instruction limit
% 29.04/5.31 % (169276)Termination phase: Finite model building preprocessing
% 29.04/5.31 % (169276)Time elapsed: 1.141 s
% 29.04/5.31 % (169276)Peak memory usage: 45 MB
% 29.04/5.31 % (169276)Instructions burned: 2175 (million)
% 29.04/5.31 % (169274)Cannot represent all propositional literals internally
% 29.04/5.31 % (169274)Refutation not found, incomplete strategy
% 29.04/5.31 % (169274)------------------------------
% 29.04/5.31 % (169274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169274)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169274)Termination reason: Refutation not found, incomplete strategy
% 29.04/5.31 % (169274)Time elapsed: 1.361 s
% 29.04/5.31 % (169274)Peak memory usage: 59 MB
% 29.04/5.31 % (169274)Instructions burned: 2845 (million)
% 29.04/5.31 % (169274)------------------------------
% 29.04/5.31 % (169274)------------------------------
% 29.04/5.31 % (169284)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1817514368:i=3512:aac=none_2969 on theBenchmark for (2969ds/3512Mi)
% 29.04/5.31 % (169285)dis+21_1_sil=32000:sas=cadical:random_seed=4026874124:i=3773:amm=off_2969 on theBenchmark for (2969ds/3773Mi)
% 29.04/5.31 % TRYING [1]
% 29.04/5.31 % (169282)Cannot represent all propositional literals internally
% 29.04/5.31 % (169282)Refutation not found, incomplete strategy
% 29.04/5.31 % (169282)------------------------------
% 29.04/5.31 % (169282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169282)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169282)Termination reason: Refutation not found, incomplete strategy
% 29.04/5.31 % (169282)Time elapsed: 1.422 s
% 29.04/5.31 % (169282)Peak memory usage: 65 MB
% 29.04/5.31 % (169282)Instructions burned: 2970 (million)
% 29.04/5.31 % (169282)------------------------------
% 29.04/5.31 % (169282)------------------------------
% 29.04/5.31 % (169288)ott+11_1_sil=16000:gs=on:random_seed=1977138230:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2961 on theBenchmark for (2961ds/2251Mi)
% 29.04/5.31 % (169270)Instruction limit reached!
% 29.04/5.31 % (169270)------------------------------
% 29.04/5.31 % (169270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.31 % (169270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.31 % (169270)CaDiCaL version: 2.1.3
% 29.04/5.31 % (169270)Termination reason: Instruction limit
% 29.04/5.31 % (169270)Termination phase: Saturation
% 29.04/5.31 % (169270)Time elapsed: 2.742 s
% 29.04/5.31 % (169270)Peak memory usage: 110 MB
% 29.04/5.31 % (169270)Instructions burned: 5133 (million)
% 29.04/5.31 % (169290)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2338006949:fmbsr=1.6:i=67534_2960 on theBenchmark for (2960ds/67534Mi)
% 29.04/5.31 % (169288) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-169225-169288"...
% 29.04/5.31 % (169288)...printing done.
% 29.04/5.31 % (169288)Refutation found. Thanks to Tanya!
% 29.04/5.31 % SZS status Theorem for theBenchmark
% 29.04/5.31 % SZS output start Proof for theBenchmark
% See solution above
% 29.04/5.32 % (169288)------------------------------
% 29.04/5.32 % (169288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.04/5.32 % (169288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.04/5.32 % (169288)CaDiCaL version: 2.1.3
% 29.04/5.32 % (169288)Termination reason: Refutation
% 29.04/5.32 % (169288)Time elapsed: 0.924 s
% 29.04/5.32 % (169288)Peak memory usage: 53 MB
% 29.04/5.32 % (169288)Instructions burned: 1546 (million)
% 29.04/5.32 % (169225)Success in time 4.891 s
% 29.04/5.32 % Vampire exiting
%------------------------------------------------------------------------------