%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT018-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:36:45 PM UTC 2026
% Result : Unsatisfiable 153.96s 26.20s
% Output : Refutation 179.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 80
% Syntax : Number of formulae : 468 ( 74 unt; 46 def)
% Number of atoms : 1139 ( 127 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1240 ( 569 ~; 632 |; 0 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 40 prp; 0-3 aty)
% Number of functors : 32 ( 32 usr; 14 con; 0-5 aty)
% Number of variables : 1032 ( 0 sgn1032 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0,X1] : ~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f26,axiom,
! [X2,X0,X1] :
( ~ c_in(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singletonE_0) ).
fof(f48,axiom,
! [X2,X3,X0,X1] :
( c_Set_Oimage(c_COMBK(X0,X1,X2),X3,X2,X1) = c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)
| X3 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__constant__conv_1) ).
fof(f49,plain,
! [X2,X3,X0,X1] :
( c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1) = c_Set_Oimage(c_COMBK(X0,X1,X2),X3,X2,X1)
| c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = X3 ),
inference(reorient_equations,[],[f48]) ).
fof(f59,axiom,
! [X0,X1] :
( X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))
| ~ c_lessequals(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subset__empty_0) ).
fof(f60,plain,
! [X0,X1] :
( ~ c_lessequals(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool))
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X0 ),
inference(reorient_equations,[],[f59]) ).
fof(f62,axiom,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f65,axiom,
! [X2,X3,X0,X1] :
( c_Set_Oimage(X0,X1,X2,X3) != c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__is__empty_0) ).
fof(f66,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) != c_Set_Oimage(X0,X1,X2,X3)
| c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = X1 ),
inference(reorient_equations,[],[f65]) ).
fof(f105,axiom,
! [X2,X0,X1] : c_in(X0,c_Set_Oinsert(X0,X1,X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insertCI_1) ).
fof(f109,axiom,
! [X2,X0,X1] :
( c_Set_Oinsert(X0,X1,X2) = X1
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f159,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(hAPP(c_Hilbert__Choice_Oinv__into(X0,X1,X2,X3),X4),X0,X2)
| ~ c_in(X4,c_Set_Oimage(X1,X0,X2,X3),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inv__into__into_0) ).
fof(f166,axiom,
! [X0,X1] : c_Set_Oimage(c_COMBI(X0),X1,X0,X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__ident_0) ).
fof(f192,axiom,
! [X2,X3,X0,X1,X4] :
( hAPP(X0,hAPP(c_Hilbert__Choice_Oinv__into(X1,X0,X2,X3),X4)) = X4
| ~ c_in(X4,c_Set_Oimage(X0,X1,X2,X3),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_f__inv__into__f_0) ).
fof(f208,axiom,
! [X2,X0,X1] : hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f257,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X4,tc_fun(X3,tc_bool),X2),X2,X3),tc_fun(X2,X3))
| c_lessequals(c_Set_Oimage(X0,X1,X2,X3),X4,tc_fun(X3,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_funcset__image_0) ).
fof(f298,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| X3 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X0 = X3
| c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_in__above_9) ).
fof(f299,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| X1 = X3
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X0 = X3
| c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(reorient_equations,[],[f298]) ).
fof(f305,axiom,
! [X2,X0,X1] :
( X0 = X1
| X0 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X0 = X1
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_in__above_5) ).
fof(f312,axiom,
! [X2,X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_above__Lin_0) ).
fof(f339,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_fun(X2,tc_bool))
| X0 = X1
| ~ c_lessequals(X0,X1,tc_fun(X2,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_equalityI_0) ).
fof(f497,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(c_FuncSet_Orestrict(X0,X1,X2,X3),c_FuncSet_OPi(X1,c_COMBK(X4,tc_fun(X3,tc_bool),X2),X2,X3),tc_fun(X2,X3))
| c_in(c_FuncSet_Osko__FuncSet__Xrestrict__in__funcset__1__1(X1,X4,X0,X2,X3),X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_restrict__in__funcset_0) ).
fof(f539,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(X0,c_FuncSet_OPi(X1,X2,X3,X4),tc_fun(X3,X4))
| c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,X3,X4),X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Pi__I_0) ).
fof(f541,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,X3,X4)),hAPP(X2,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,X3,X4)),X4)
| c_in(X0,c_FuncSet_OPi(X1,X2,X3,X4),tc_fun(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Pi__I_1) ).
fof(f542,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XPi__I_H__1__1(X1,X2,X0,X3,X4)),hAPP(X2,c_FuncSet_Osko__FuncSet__XPi__I_H__1__1(X1,X2,X0,X3,X4)),X4)
| c_in(X0,c_FuncSet_OPi(X1,X2,X3,X4),tc_fun(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Pi__I_H_1) ).
fof(f548,axiom,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| X1 = X0
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_notin__Lin__iff_0) ).
fof(f549,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| X0 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
inference(reorient_equations,[],[f548]) ).
fof(f550,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Lin__irrefl_0) ).
fof(f551,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,tc_fun(X3,tc_bool),X4),X4,X3),tc_fun(X4,X3))
| ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,X4,X3)),X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_funcsetI_1) ).
fof(f552,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,tc_fun(X3,tc_bool),X4),X4,X3),tc_fun(X4,X3))
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,X4,X3),X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_funcsetI_0) ).
fof(f553,axiom,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X0,X1)
| c_in(v_sko__Arrow__Order__Mirabelle__Xdictator__def__1(X0,X1),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dictator__def_1) ).
fof(f558,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X3,c_FuncSet_OPi(X1,X4,X2,X5),tc_fun(X2,X5))
| c_in(hAPP(X3,X0),hAPP(X4,X0),X5)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_PiE_0) ).
fof(f559,axiom,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X0,c_FuncSet_OPi(X4,c_COMBK(X2,tc_fun(X3,tc_bool),X5),X5,X3),tc_fun(X5,X3))
| ~ c_in(X1,X4,X5)
| c_in(hAPP(X0,X1),X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_funcset__mem_0) ).
fof(f560,axiom,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| ~ hBOOL(hAPP(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f561,axiom,
! [X2,X0,X1] :
( ~ c_in(X1,X0,X2)
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f563,negated_conjecture,
c_in(v_F,c_FuncSet_OPi(c_Arrow__Order__Mirabelle_OProf,c_COMBK(c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f564,negated_conjecture,
~ c_Arrow__Order__Mirabelle_Odictator(v_F,v_i),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f583,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBK__def_0) ).
fof(f584,axiom,
! [X0,X1] : hAPP(c_COMBI(X0),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_OCOMBI__def_0) ).
fof(f646,definition,
sF0 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f647,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f646]) ).
fof(f648,definition,
sF1 = tc_fun(sF0,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f649,plain,
tc_fun(sF0,tc_bool) = sF1,
inference(reorient_equations,[],[f648]) ).
fof(f650,definition,
sF2 = tc_fun(sF1,tc_bool),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f651,plain,
tc_fun(sF1,tc_bool) = sF2,
inference(reorient_equations,[],[f650]) ).
fof(f652,definition,
sF3 = tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f653,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1) = sF3,
inference(reorient_equations,[],[f652]) ).
fof(f654,definition,
sF4 = c_COMBK(c_Arrow__Order__Mirabelle_OLin,sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f655,plain,
c_COMBK(c_Arrow__Order__Mirabelle_OLin,sF2,sF3) = sF4,
inference(reorient_equations,[],[f654]) ).
fof(f656,definition,
sF5 = c_FuncSet_OPi(c_Arrow__Order__Mirabelle_OProf,sF4,sF3,sF1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f657,plain,
c_FuncSet_OPi(c_Arrow__Order__Mirabelle_OProf,sF4,sF3,sF1) = sF5,
inference(reorient_equations,[],[f656]) ).
fof(f658,definition,
sF6 = tc_fun(sF3,sF1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f659,plain,
tc_fun(sF3,sF1) = sF6,
inference(reorient_equations,[],[f658]) ).
fof(f660,plain,
c_in(v_F,sF5,sF6),
inference(definition_folding,[],[f563,f659,f649,f647,f653,f649,f647,f657,f649,f647,f653,f649,f647,f655,f653,f649,f647,f651,f649,f647]) ).
fof(f667,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(duplicate_literal_removal,[],[f305]) ).
fof(f744,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X1 = X3
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X0 = X3
| c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(backward_demodulation,[],[f299,f647]) ).
fof(f748,plain,
! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X1 = X2 ),
inference(backward_demodulation,[],[f312,f647]) ).
fof(f762,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| X0 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
inference(backward_demodulation,[],[f549,f647]) ).
fof(f763,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
inference(backward_demodulation,[],[f550,f647]) ).
fof(f764,plain,
! [X0,X1] :
( c_in(v_sko__Arrow__Order__Mirabelle__Xdictator__def__1(X0,X1),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(sF0,tc_bool)))
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) ),
inference(backward_demodulation,[],[f553,f647]) ).
fof(f770,plain,
! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| X0 = X1
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(backward_demodulation,[],[f667,f647]) ).
fof(f792,plain,
! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f770,f649]) ).
fof(f796,plain,
! [X0,X1] :
( c_in(v_sko__Arrow__Order__Mirabelle__Xdictator__def__1(X0,X1),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1))
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) ),
inference(forward_demodulation,[],[f764,f649]) ).
fof(f797,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
inference(forward_demodulation,[],[f763,f647]) ).
fof(f798,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X0 = X1
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) ),
inference(forward_demodulation,[],[f762,f647]) ).
fof(f810,plain,
! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| X1 = X2 ),
inference(forward_demodulation,[],[f748,f649]) ).
fof(f814,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X1 = X3
| X0 = X3
| c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f744,f647]) ).
fof(f836,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X1),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1 ),
inference(forward_demodulation,[],[f792,f647]) ).
fof(f840,plain,
! [X0,X1] :
( c_in(v_sko__Arrow__Order__Mirabelle__Xdictator__def__1(X0,X1),c_Arrow__Order__Mirabelle_OProf,sF3)
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) ),
inference(forward_demodulation,[],[f796,f653]) ).
fof(f841,plain,
! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0) ),
inference(forward_demodulation,[],[f797,f647]) ).
fof(f842,plain,
! [X2,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X0 = X1 ),
inference(forward_demodulation,[],[f798,f647]) ).
fof(f848,plain,
! [X2,X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,tc_fun(sF0,tc_bool))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(forward_demodulation,[],[f810,f647]) ).
fof(f852,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X1 = X3
| X0 = X3
| c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(forward_demodulation,[],[f814,f649]) ).
fof(f873,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0) ),
inference(forward_demodulation,[],[f841,f649]) ).
fof(f874,plain,
! [X2,X0,X1] :
( c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X0 = X1 ),
inference(forward_demodulation,[],[f842,f649]) ).
fof(f879,plain,
! [X2,X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(forward_demodulation,[],[f848,f649]) ).
fof(f883,plain,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X3,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X2,X0,X3),sF0)
| ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0)
| X1 = X3
| X0 = X3 ),
inference(forward_demodulation,[],[f852,f647]) ).
fof(f906,plain,
! [X2,X3,X0,X1] :
( c_in(hAPP(X0,X3),hAPP(X2,X3),tc_bool)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,sF0,tc_bool),sF1)
| ~ c_in(X3,X1,sF0) ),
inference(superposition,[],[f558,f649]) ).
fof(f908,plain,
! [X2,X3,X0,X1] :
( c_in(hAPP(X0,X3),hAPP(X2,X3),sF1)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ c_in(X3,X1,tc_Arrow__Order__Mirabelle_Oindi) ),
inference(superposition,[],[f558,f653]) ).
fof(f909,plain,
! [X2,X3,X0,X1] :
( c_in(hAPP(X0,X3),hAPP(X2,X3),sF1)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,sF3,sF1),sF6)
| ~ c_in(X3,X1,sF3) ),
inference(superposition,[],[f558,f659]) ).
fof(f910,plain,
! [X0,X1] :
( ~ c_in(X0,sF5,tc_fun(sF3,sF1))
| c_in(hAPP(X0,X1),hAPP(sF4,X1),sF1)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF3) ),
inference(superposition,[],[f558,f657]) ).
fof(f911,plain,
! [X0,X1] :
( c_in(hAPP(X0,X1),hAPP(sF4,X1),sF1)
| ~ c_in(X0,sF5,sF6)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF3) ),
inference(forward_demodulation,[],[f910,f659]) ).
fof(f926,plain,
! [X2,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,tc_fun(sF1,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,tc_Arrow__Order__Mirabelle_Oindi,sF1)),X2,sF1) ),
inference(superposition,[],[f551,f653]) ).
fof(f929,plain,
! [X2,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,tc_Arrow__Order__Mirabelle_Oindi,sF1)),X2,sF1) ),
inference(forward_demodulation,[],[f926,f651]) ).
fof(f941,plain,
! [X0] : c_Arrow__Order__Mirabelle_OLin = hAPP(sF4,X0),
inference(superposition,[],[f583,f655]) ).
fof(f946,plain,
! [X0,X1] :
( c_in(hAPP(X0,X1),c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(X0,sF5,sF6)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF3) ),
inference(backward_demodulation,[],[f911,f941]) ).
fof(f948,definition,
( spl7_3
<=> ! [X3] : ~ c_in(X3,c_Arrow__Order__Mirabelle_OProf,sF3) ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f949,plain,
( ! [X3] : ~ c_in(X3,c_Arrow__Order__Mirabelle_OProf,sF3)
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f971,plain,
! [X2,X0,X1] :
( ~ c_in(sF4,c_FuncSet_OPi(X2,X1,sF3,sF1),sF6)
| c_in(c_Arrow__Order__Mirabelle_OLin,hAPP(X1,X0),sF1)
| ~ c_in(X0,X2,sF3) ),
inference(superposition,[],[f909,f941]) ).
fof(f1005,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,X3),X3,sF1),tc_fun(X3,sF1))
| ~ c_in(X4,X1,X3)
| c_in(hAPP(X0,X4),X2,sF1) ),
inference(superposition,[],[f559,f651]) ).
fof(f1016,plain,
! [X2,X3,X0,X1,X4] :
( c_in(X0,c_FuncSet_OPi(X1,X2,X3,sF1),tc_fun(X3,sF1))
| ~ c_in(X0,c_FuncSet_OPi(X4,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,X3,sF1),X4,tc_Arrow__Order__Mirabelle_Oindi) ),
inference(resolution,[],[f541,f908]) ).
fof(f1021,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X2,c_COMBK(X0,X3,X4),X1,X5,X6)),X0,X6)
| c_in(X1,c_FuncSet_OPi(X2,c_COMBK(X0,X3,X4),X5,X6),tc_fun(X5,X6)) ),
inference(superposition,[],[f541,f583]) ).
fof(f1031,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I_H__1__1(X2,c_COMBK(X0,X3,X4),X1,X5,X6)),X0,X6)
| c_in(X1,c_FuncSet_OPi(X2,c_COMBK(X0,X3,X4),X5,X6),tc_fun(X5,X6)) ),
inference(superposition,[],[f542,f583]) ).
fof(f1038,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(c_COMBK(X0,X1,X2),c_FuncSet_OPi(X5,X4,sF0,tc_bool),sF1)
| c_in(X0,hAPP(X4,X3),tc_bool)
| ~ c_in(X3,X5,sF0) ),
inference(superposition,[],[f906,f583]) ).
fof(f1041,plain,
! [X2,X0,X1] :
( ~ c_in(sF4,c_FuncSet_OPi(X2,X1,sF0,tc_bool),sF1)
| c_in(c_Arrow__Order__Mirabelle_OLin,hAPP(X1,X0),tc_bool)
| ~ c_in(X0,X2,sF0) ),
inference(superposition,[],[f906,f941]) ).
fof(f1048,plain,
! [X0] : ~ c_in(X0,c_Orderings_Obot__class_Obot(sF1),sF0),
inference(superposition,[],[f7,f649]) ).
fof(f1049,plain,
! [X0] : ~ c_in(X0,c_Orderings_Obot__class_Obot(sF2),sF1),
inference(superposition,[],[f7,f651]) ).
fof(f1050,plain,
( ! [X0,X1] : c_Arrow__Order__Mirabelle_Odictator(X0,X1)
| ~ spl7_3 ),
inference(resolution,[],[f949,f840]) ).
fof(f1051,plain,
( $false
| ~ spl7_3 ),
inference(resolution,[],[f1050,f564]) ).
fof(f1052,plain,
~ spl7_3,
inference(avatar_contradiction_clause,[],[f1051]) ).
fof(f1075,plain,
! [X2,X0,X1] :
( ~ c_in(c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(resolution,[],[f873,f836]) ).
fof(f1078,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Oabove(X0,X1,X2),sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(forward_subsumption_resolution,[],[f1075,f879]) ).
fof(f1084,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_in(c_COMBI(X4),c_FuncSet_OPi(X0,c_COMBK(X1,X2,X3),X5,X6),tc_fun(X5,X6))
| ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,X2,X3),c_COMBI(X4),X5,X6),X1,X6) ),
inference(superposition,[],[f1021,f584]) ).
fof(f1124,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X0,X1,X2,X3,X4),X0,X3)
| ~ c_in(X5,X0,X3)
| c_in(hAPP(X2,X5),X1,X4) ),
inference(resolution,[],[f552,f559]) ).
fof(f1129,plain,
! [X2,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,tc_fun(tc_bool,tc_bool),sF0),sF0,tc_bool),sF1)
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,sF0,tc_bool),X1,sF0) ),
inference(superposition,[],[f552,f649]) ).
fof(f1132,plain,
! [X2,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,tc_fun(sF1,tc_bool),sF3),sF3,sF1),sF6)
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,sF3,sF1),X1,sF3) ),
inference(superposition,[],[f552,f659]) ).
fof(f1133,plain,
! [X2,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,sF3),sF3,sF1),sF6)
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,X0,sF3,sF1),X1,sF3) ),
inference(forward_demodulation,[],[f1132,f651]) ).
fof(f1141,plain,
! [X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(X0,X1)))
| ~ c_in(X0,sF5,sF6)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF3) ),
inference(resolution,[],[f561,f946]) ).
fof(f1177,plain,
! [X2,X3,X0,X1,X4] :
( c_lessequals(c_Set_Oimage(X0,X1,X2,X3),X4,tc_fun(X3,tc_bool))
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X4,X0,X2,X3),X1,X2) ),
inference(resolution,[],[f257,f552]) ).
fof(f1440,plain,
! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X4,X3,X2,X5)))
| c_in(hAPP(X3,X0),X4,X5)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[],[f1124,f561]) ).
fof(f1600,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ hBOOL(hAPP(X0,hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I_H__1__1(X2,c_COMBK(X0,X3,X4),X1,X5,X6))))
| c_in(X1,c_FuncSet_OPi(X2,c_COMBK(X0,X3,X4),X5,X6),tc_fun(X5,X6)) ),
inference(resolution,[],[f560,f1031]) ).
fof(f1602,plain,
! [X0] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X0)),
inference(resolution,[],[f560,f1048]) ).
fof(f1603,plain,
! [X0] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF2),X0)),
inference(resolution,[],[f560,f1049]) ).
fof(f2026,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(X0,c_Set_Oimage(c_COMBK(X1,X2,X3),X4,X5,X6),X6)
| X0 = X1 ),
inference(superposition,[],[f583,f192]) ).
fof(f2045,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Set_Oinsert(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0),sF0)
| ~ c_in(c_Set_Oinsert(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,sF0),c_Arrow__Order__Mirabelle_OLin,sF1) ),
inference(resolution,[],[f105,f873]) ).
fof(f2103,plain,
! [X2,X3,X0,X1,X4] :
( c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,sF2,X2),X3,X2,sF1),X0,X2)
| ~ c_in(X4,X0,X2)
| c_in(hAPP(X3,X4),X1,sF1) ),
inference(resolution,[],[f539,f1005]) ).
fof(f2107,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,tc_fun(X2,tc_bool),X3),X4,X3,X2),X0,X3)
| ~ c_in(X5,X0,X3)
| c_in(hAPP(X4,X5),X1,X2) ),
inference(resolution,[],[f539,f559]) ).
fof(f2113,plain,
! [X2,X0,X1] :
( c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,sF0,tc_bool),X1,sF0)
| c_in(X0,c_FuncSet_OPi(X1,X2,sF0,tc_bool),sF1) ),
inference(superposition,[],[f539,f649]) ).
fof(f2431,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,tc_Arrow__Order__Mirabelle_Oindi,sF1),X3,tc_Arrow__Order__Mirabelle_Oindi)
| ~ c_in(X0,c_FuncSet_OPi(X3,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(X0,c_FuncSet_OPi(X1,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3) ),
inference(superposition,[],[f1016,f653]) ).
fof(f2432,plain,
! [X2,X3,X0,X1] :
( ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,sF3,sF1),X3,tc_Arrow__Order__Mirabelle_Oindi)
| ~ c_in(X0,c_FuncSet_OPi(X3,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(X0,c_FuncSet_OPi(X1,X2,sF3,sF1),sF6) ),
inference(superposition,[],[f1016,f659]) ).
fof(f2538,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(X7,c_COMBK(X0,X1,X2),X5)
| c_in(hAPP(X4,X7),X3,X6)
| hBOOL(X0) ),
inference(superposition,[],[f1440,f583]) ).
fof(f2544,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(c_Arrow__Order__Mirabelle_OLin)
| c_in(hAPP(X1,X4),X0,X3)
| ~ c_in(X4,sF4,X2) ),
inference(superposition,[],[f1440,f941]) ).
fof(f2546,definition,
( spl7_36
<=> ! [X2,X4,X0,X3,X1] :
( c_in(hAPP(X1,X4),X0,X3)
| ~ c_in(X4,sF4,X2) ) ),
introduced(definition,[new_symbols(definition,[spl7_36])],[avatar_definition]) ).
fof(f2547,plain,
( ! [X2,X3,X0,X1,X4] :
( c_in(hAPP(X1,X4),X0,X3)
| ~ c_in(X4,sF4,X2) )
| ~ spl7_36 ),
inference(avatar_component_clause,[],[f2546]) ).
fof(f2549,definition,
( spl7_37
<=> hBOOL(c_Arrow__Order__Mirabelle_OLin) ),
introduced(definition,[new_symbols(definition,[spl7_37])],[avatar_definition]) ).
fof(f2550,plain,
( ~ hBOOL(c_Arrow__Order__Mirabelle_OLin)
| spl7_37 ),
inference(avatar_component_clause,[],[f2549]) ).
fof(f2551,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OLin)
| ~ spl7_37 ),
inference(avatar_component_clause,[],[f2549]) ).
fof(f2552,plain,
( spl7_36
| spl7_37 ),
inference(avatar_split_clause,[],[f2544,f2549,f2546]) ).
fof(f2687,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ c_in(c_COMBK(X0,X1,X2),sF5,sF6)
| ~ c_in(X3,c_Arrow__Order__Mirabelle_OProf,sF3) ),
inference(superposition,[],[f1141,f583]) ).
fof(f2702,definition,
( spl7_38
<=> ! [X2,X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ c_in(c_COMBK(X0,X1,X2),sF5,sF6) ) ),
introduced(definition,[new_symbols(definition,[spl7_38])],[avatar_definition]) ).
fof(f2703,plain,
( ! [X2,X0,X1] :
( ~ c_in(c_COMBK(X0,X1,X2),sF5,sF6)
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) )
| ~ spl7_38 ),
inference(avatar_component_clause,[],[f2702]) ).
fof(f2704,plain,
( spl7_3
| spl7_38 ),
inference(avatar_split_clause,[],[f2687,f2702,f948]) ).
fof(f2716,plain,
( ! [X0,X1] : ~ c_in(X0,sF4,X1)
| ~ spl7_36 ),
inference(resolution,[],[f2547,f1049]) ).
fof(f2756,definition,
( spl7_39
<=> ! [X0,X3] : ~ c_in(X0,sF4,X3) ),
introduced(definition,[new_symbols(definition,[spl7_39])],[avatar_definition]) ).
fof(f2757,plain,
( ! [X3,X0] : ~ c_in(X0,sF4,X3)
| ~ spl7_39 ),
inference(avatar_component_clause,[],[f2756]) ).
fof(f2774,plain,
( spl7_39
| ~ spl7_36 ),
inference(avatar_split_clause,[],[f2716,f2546,f2756]) ).
fof(f2959,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,X2,X0,sF0,tc_bool)))
| c_in(X0,c_FuncSet_OPi(X1,X2,sF0,tc_bool),sF1) ),
inference(resolution,[],[f2113,f561]) ).
fof(f3082,plain,
! [X0,X1] :
( ~ c_in(c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),c_Arrow__Order__Mirabelle_OLin,sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),sF0)
| X0 = X1 ),
inference(resolution,[],[f874,f7]) ).
fof(f3100,plain,
! [X0,X1] :
( ~ c_in(c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)),c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f3082,f7]) ).
fof(f3102,plain,
! [X0,X1] :
( ~ c_in(c_Orderings_Obot__class_Obot(sF1),c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1 ),
inference(forward_demodulation,[],[f3100,f649]) ).
fof(f3104,definition,
( spl7_45
<=> ! [X0,X1] : X0 = X1 ),
introduced(definition,[new_symbols(definition,[spl7_45])],[avatar_definition]) ).
fof(f3105,plain,
( ! [X0,X1] : X0 = X1
| ~ spl7_45 ),
inference(avatar_component_clause,[],[f3104]) ).
fof(f3107,definition,
( spl7_46
<=> c_in(c_Orderings_Obot__class_Obot(sF1),c_Arrow__Order__Mirabelle_OLin,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_46])],[avatar_definition]) ).
fof(f3109,plain,
( ~ c_in(c_Orderings_Obot__class_Obot(sF1),c_Arrow__Order__Mirabelle_OLin,sF1)
| spl7_46 ),
inference(avatar_component_clause,[],[f3107]) ).
fof(f3111,plain,
( spl7_45
| ~ spl7_46 ),
inference(avatar_split_clause,[],[f3102,f3107,f3104]) ).
fof(f3113,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Obot__class_Obot(sF1)))
| spl7_46 ),
inference(resolution,[],[f3109,f560]) ).
fof(f3307,plain,
! [X0] :
( c_Set_Oinsert(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Obot__class_Obot(tc_fun(sF2,tc_bool)),sF2) = c_Set_Oimage(sF4,X0,sF3,sF2)
| c_Orderings_Obot__class_Obot(tc_fun(sF3,tc_bool)) = X0 ),
inference(superposition,[],[f49,f655]) ).
fof(f3362,plain,
! [X0] :
( c_in(c_Arrow__Order__Mirabelle_OLin,c_Set_Oimage(sF4,X0,sF3,sF2),sF2)
| c_Orderings_Obot__class_Obot(tc_fun(sF3,tc_bool)) = X0 ),
inference(superposition,[],[f105,f3307]) ).
fof(f3366,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(sF5,c_COMBK(X0,X1,X2)))
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) )
| ~ spl7_38 ),
inference(resolution,[],[f2703,f560]) ).
fof(f3654,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( c_in(c_FuncSet_Orestrict(X1,X2,X3,X4),c_FuncSet_OPi(X2,c_COMBK(X5,tc_fun(X4,tc_bool),X3),X3,X4),X0)
| c_in(c_FuncSet_Osko__FuncSet__Xrestrict__in__funcset__1__1(X2,X5,X1,X3,X4),X2,X3) )
| ~ spl7_45 ),
inference(superposition,[],[f497,f3105]) ).
fof(f4845,plain,
( ! [X2,X0,X1] : ~ c_in(X1,X0,X2)
| ~ spl7_45 ),
inference(superposition,[],[f7,f3105]) ).
fof(f5839,definition,
( spl7_58
<=> ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
introduced(definition,[new_symbols(definition,[spl7_58])],[avatar_definition]) ).
fof(f5840,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl7_58 ),
inference(avatar_component_clause,[],[f5839]) ).
fof(f6088,plain,
( ! [X2,X3,X0,X1,X4,X5] : c_in(c_FuncSet_Orestrict(X1,X2,X3,X4),c_FuncSet_OPi(X2,c_COMBK(X5,tc_fun(X4,tc_bool),X3),X3,X4),X0)
| ~ spl7_45 ),
inference(forward_subsumption_resolution,[],[f3654,f4845]) ).
fof(f6204,plain,
( $false
| ~ spl7_45 ),
inference(forward_subsumption_resolution,[],[f6088,f4845]) ).
fof(f6205,plain,
~ spl7_45,
inference(avatar_contradiction_clause,[],[f6204]) ).
fof(f6723,plain,
! [X2,X0,X1] :
( ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ c_in(c_Pair(X1,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,sF0)
| X1 = X2
| X1 = X2
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(resolution,[],[f883,f1078]) ).
fof(f6730,plain,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X1,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1)
| X1 = X2 ),
inference(duplicate_literal_removal,[],[f6723]) ).
fof(f6745,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,c_Pair(X1,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| X1 = X2
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1) ),
inference(resolution,[],[f6730,f560]) ).
fof(f7069,definition,
( spl7_79
<=> ! [X2,X1] : c_in(X1,c_FuncSet_OPi(X2,sF4,sF3,sF1),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_79])],[avatar_definition]) ).
fof(f7070,plain,
( ! [X2,X1] : c_in(X1,c_FuncSet_OPi(X2,sF4,sF3,sF1),sF6)
| ~ spl7_79 ),
inference(avatar_component_clause,[],[f7069]) ).
fof(f7164,plain,
( ! [X0] : c_in(X0,sF5,sF6)
| ~ spl7_79 ),
inference(superposition,[],[f7070,f657]) ).
fof(f7238,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl7_38
| ~ spl7_79 ),
inference(resolution,[],[f7164,f2703]) ).
fof(f7251,plain,
( spl7_58
| ~ spl7_38
| ~ spl7_79 ),
inference(avatar_split_clause,[],[f7238,f7069,f2702,f5839]) ).
fof(f7463,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X3,X2,X0,tc_Arrow__Order__Mirabelle_Oindi,sF1)))
| c_in(X0,c_FuncSet_OPi(X3,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3) ),
inference(resolution,[],[f2431,f560]) ).
fof(f7801,plain,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) != X0
| ~ c_in(X2,X0,X1) ),
inference(superposition,[],[f62,f109]) ).
fof(f7805,plain,
! [X0,X1] :
( ~ c_in(X1,X0,sF1)
| c_Orderings_Obot__class_Obot(sF2) != X0 ),
inference(superposition,[],[f7801,f651]) ).
fof(f7852,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| c_Orderings_Obot__class_Obot(sF2) != X0 ),
inference(resolution,[],[f7805,f560]) ).
fof(f7886,definition,
( spl7_98
<=> ! [X0] : ~ c_in(X0,sF5,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_98])],[avatar_definition]) ).
fof(f7887,plain,
( ! [X0] : ~ c_in(X0,sF5,sF6)
| ~ spl7_98 ),
inference(avatar_component_clause,[],[f7886]) ).
fof(f8025,plain,
( $false
| spl7_46
| ~ spl7_58 ),
inference(resolution,[],[f5840,f3113]) ).
fof(f8035,plain,
( spl7_46
| ~ spl7_58 ),
inference(avatar_contradiction_clause,[],[f8025]) ).
fof(f9186,definition,
( spl7_121
<=> ! [X3] : c_Orderings_Obot__class_Obot(sF2) != X3 ),
introduced(definition,[new_symbols(definition,[spl7_121])],[avatar_definition]) ).
fof(f9187,plain,
( ! [X3] : c_Orderings_Obot__class_Obot(sF2) != X3
| ~ spl7_121 ),
inference(avatar_component_clause,[],[f9186]) ).
fof(f10070,plain,
! [X2,X3,X0,X1] :
( c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X2,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,X3,X0),X2,X3)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Set_Oimage(X1,X2,X3,X0) ),
inference(resolution,[],[f60,f1177]) ).
fof(f10855,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ hBOOL(hAPP(c_Set_Oimage(c_COMBK(X1,X2,X3),X4,X5,X6),X0))
| X0 = X1 ),
inference(resolution,[],[f2026,f560]) ).
fof(f10890,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(c_Set_Oimage(sF4,X0,X1,X2),X3))
| c_Arrow__Order__Mirabelle_OLin = X3 ),
inference(superposition,[],[f10855,f655]) ).
fof(f11045,definition,
( spl7_165
<=> ! [X2,X1] : ~ c_in(X2,X1,sF3) ),
introduced(definition,[new_symbols(definition,[spl7_165])],[avatar_definition]) ).
fof(f11046,plain,
( ! [X2,X1] : ~ c_in(X2,X1,sF3)
| ~ spl7_165 ),
inference(avatar_component_clause,[],[f11045]) ).
fof(f11148,definition,
( spl7_166
<=> ! [X3] : c_in(c_Arrow__Order__Mirabelle_OLin,X3,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_166])],[avatar_definition]) ).
fof(f11149,plain,
( ! [X3] : c_in(c_Arrow__Order__Mirabelle_OLin,X3,sF1)
| ~ spl7_166 ),
inference(avatar_component_clause,[],[f11148]) ).
fof(f11166,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF2) != X0
| ~ spl7_166 ),
inference(resolution,[],[f11149,f7805]) ).
fof(f11176,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin = X0
| ~ spl7_166 ),
inference(resolution,[],[f11149,f26]) ).
fof(f11185,definition,
( spl7_171
<=> ! [X3] : hBOOL(X3) ),
introduced(definition,[new_symbols(definition,[spl7_171])],[avatar_definition]) ).
fof(f11186,plain,
( ! [X3] : hBOOL(X3)
| ~ spl7_171 ),
inference(avatar_component_clause,[],[f11185]) ).
fof(f11196,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin != X0
| ~ spl7_166 ),
inference(forward_demodulation,[],[f11166,f11176]) ).
fof(f11201,plain,
( $false
| ~ spl7_166 ),
inference(forward_subsumption_resolution,[],[f11196,f11176]) ).
fof(f11202,plain,
~ spl7_166,
inference(avatar_contradiction_clause,[],[f11201]) ).
fof(f11639,plain,
! [X0,X1] : ~ c_in(c_Set_Oinsert(c_Pair(X0,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1,sF0),c_Arrow__Order__Mirabelle_OLin,sF1),
inference(resolution,[],[f2045,f105]) ).
fof(f11651,plain,
! [X0,X1] :
( ~ c_in(c_Pair(X1,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0,sF0)
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1) ),
inference(superposition,[],[f11639,f109]) ).
fof(f11671,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,c_Pair(X1,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))
| ~ c_in(X0,c_Arrow__Order__Mirabelle_OLin,sF1) ),
inference(resolution,[],[f11651,f560]) ).
fof(f11691,plain,
! [X2,X0,X1] :
( ~ c_in(c_COMBK(X0,X1,X2),c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ hBOOL(X0) ),
inference(superposition,[],[f11671,f583]) ).
fof(f11708,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_COMBK(X0,X1,X2)))
| ~ hBOOL(X0) ),
inference(resolution,[],[f11691,f560]) ).
fof(f12277,plain,
! [X2,X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_OLin,hAPP(c_COMBK(X0,sF2,sF3),X1),sF1)
| ~ c_in(X1,X2,sF3)
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X2,X0,sF4,sF3,sF1),X2,sF3) ),
inference(resolution,[],[f971,f1133]) ).
fof(f12288,plain,
! [X2,X0,X1] :
( c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X2,X0,sF4,sF3,sF1),X2,sF3)
| ~ c_in(X1,X2,sF3)
| c_in(c_Arrow__Order__Mirabelle_OLin,X0,sF1) ),
inference(forward_demodulation,[],[f12277,f583]) ).
fof(f12293,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,sF4,sF3,sF1)))
| c_in(c_Arrow__Order__Mirabelle_OLin,X2,sF1)
| ~ c_in(X0,X1,sF3) ),
inference(resolution,[],[f12288,f561]) ).
fof(f12304,plain,
! [X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_OLin,X0,sF1)
| ~ c_in(X1,c_Orderings_Obot__class_Obot(sF1),sF3) ),
inference(resolution,[],[f12293,f1602]) ).
fof(f12353,definition,
( spl7_197
<=> ! [X1] : ~ c_in(X1,c_Orderings_Obot__class_Obot(sF1),sF3) ),
introduced(definition,[new_symbols(definition,[spl7_197])],[avatar_definition]) ).
fof(f12354,plain,
( ! [X1] : ~ c_in(X1,c_Orderings_Obot__class_Obot(sF1),sF3)
| ~ spl7_197 ),
inference(avatar_component_clause,[],[f12353]) ).
fof(f12355,plain,
( spl7_197
| spl7_166 ),
inference(avatar_split_clause,[],[f12304,f11148,f12353]) ).
fof(f12591,plain,
! [X2,X3,X0,X1,X4] :
( c_in(X4,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X3,sF0,tc_bool),sF1)
| hBOOL(X0) ),
inference(superposition,[],[f2959,f583]) ).
fof(f12623,definition,
( spl7_199
<=> ! [X1] : ~ hBOOL(X1) ),
introduced(definition,[new_symbols(definition,[spl7_199])],[avatar_definition]) ).
fof(f12624,plain,
( ! [X1] : ~ hBOOL(X1)
| ~ spl7_199 ),
inference(avatar_component_clause,[],[f12623]) ).
fof(f12662,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X5,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X4,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(X5,c_FuncSet_OPi(X3,X4,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(X0) ),
inference(superposition,[],[f7463,f583]) ).
fof(f12944,plain,
( $false
| ~ spl7_199 ),
inference(resolution,[],[f12624,f208]) ).
fof(f12972,plain,
~ spl7_199,
inference(avatar_contradiction_clause,[],[f12944]) ).
fof(f13032,plain,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(sF2),
inference(resolution,[],[f7852,f208]) ).
fof(f13087,plain,
! [X2,X0,X1] :
( ~ c_in(X1,X0,X2)
| c_Orderings_Obot__class_Obot(sF2) != X0 ),
inference(superposition,[],[f13032,f109]) ).
fof(f14764,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,c_COMBK(X4,sF2,X2),X3,X2,sF1)))
| c_in(hAPP(X3,X0),X4,sF1)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[],[f2103,f561]) ).
fof(f16280,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(c_COMBK(X3,X4,X5),X2,X0,tc_Arrow__Order__Mirabelle_Oindi,sF1)),X2,sF1)
| ~ hBOOL(X3)
| c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3) ),
inference(resolution,[],[f12662,f929]) ).
fof(f16876,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( c_in(c_COMBK(X0,X2,X3),c_FuncSet_OPi(X4,c_COMBK(X1,X5,X6),X7,X8),tc_fun(X7,X8))
| ~ hBOOL(hAPP(X1,X0)) ),
inference(superposition,[],[f1600,f583]) ).
fof(f16891,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( c_in(X3,c_FuncSet_OPi(X4,c_COMBK(c_COMBK(X0,X1,X2),X5,X6),X7,X8),tc_fun(X7,X8))
| ~ hBOOL(X0) ),
inference(superposition,[],[f1600,f583]) ).
fof(f16899,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(c_Arrow__Order__Mirabelle_OLin)
| c_in(X0,c_FuncSet_OPi(X1,c_COMBK(sF4,X2,X3),X4,X5),tc_fun(X4,X5)) ),
inference(superposition,[],[f1600,f941]) ).
fof(f16918,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_COMBK(X0,X1,X2),c_FuncSet_OPi(X3,sF4,X4,X5),tc_fun(X4,X5))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
inference(superposition,[],[f16876,f655]) ).
fof(f16932,plain,
! [X2,X0,X1] :
( c_in(c_COMBK(X0,X1,X2),sF5,tc_fun(sF3,sF1))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
inference(superposition,[],[f16918,f657]) ).
fof(f16937,plain,
! [X2,X0,X1] :
( c_in(c_COMBK(X0,X1,X2),sF5,sF6)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
inference(forward_demodulation,[],[f16932,f659]) ).
fof(f16943,definition,
( spl7_256
<=> ! [X0] : ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
introduced(definition,[new_symbols(definition,[spl7_256])],[avatar_definition]) ).
fof(f16944,plain,
( ! [X0] : ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl7_256 ),
inference(avatar_component_clause,[],[f16943]) ).
fof(f16952,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(sF5,c_COMBK(X0,X1,X2)))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ),
inference(resolution,[],[f16937,f561]) ).
fof(f17294,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_lessequals(c_Set_Oimage(X1,X2,X3,X4),c_COMBK(X0,X5,X6),tc_fun(X4,tc_bool))
| ~ hBOOL(X0) ),
inference(resolution,[],[f16891,f257]) ).
fof(f17311,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(c_COMBK(X2,X3,X4),X5,X6),sF0,tc_bool),sF1)
| ~ hBOOL(X2) ),
inference(superposition,[],[f16891,f649]) ).
fof(f17313,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(c_COMBK(X2,X3,X4),X5,X6),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(X2) ),
inference(superposition,[],[f16891,f653]) ).
fof(f17314,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(c_COMBK(X2,X3,X4),X5,X6),sF3,sF1),sF6)
| ~ hBOOL(X2) ),
inference(superposition,[],[f16891,f659]) ).
fof(f18279,plain,
( ! [X0,X1] :
( ~ c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sF4,sF0)
| X0 = X1 )
| ~ spl7_39 ),
inference(resolution,[],[f2757,f874]) ).
fof(f18304,plain,
( ! [X0,X1] :
( ~ c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1 )
| ~ spl7_39 ),
inference(forward_subsumption_resolution,[],[f18279,f2757]) ).
fof(f18307,definition,
( spl7_295
<=> c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_295])],[avatar_definition]) ).
fof(f18308,plain,
( c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1)
| ~ spl7_295 ),
inference(avatar_component_clause,[],[f18307]) ).
fof(f18309,plain,
( ~ c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1)
| spl7_295 ),
inference(avatar_component_clause,[],[f18307]) ).
fof(f18310,plain,
( spl7_45
| ~ spl7_295
| ~ spl7_39 ),
inference(avatar_split_clause,[],[f18304,f2756,f18307,f3104]) ).
fof(f18415,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,sF4))
| spl7_295 ),
inference(resolution,[],[f18309,f560]) ).
fof(f18708,plain,
! [X2,X3,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(sF4,X2,X3),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(c_Arrow__Order__Mirabelle_OLin) ),
inference(superposition,[],[f17313,f655]) ).
fof(f19579,plain,
( ! [X0,X1] :
( ~ c_in(X0,sF5,sF6)
| ~ c_in(X1,c_Arrow__Order__Mirabelle_OProf,sF3) )
| ~ spl7_256 ),
inference(resolution,[],[f16944,f1141]) ).
fof(f19668,plain,
( $false
| ~ spl7_98 ),
inference(resolution,[],[f7887,f660]) ).
fof(f19669,plain,
~ spl7_98,
inference(avatar_contradiction_clause,[],[f19668]) ).
fof(f19671,plain,
( spl7_3
| spl7_98
| ~ spl7_256 ),
inference(avatar_split_clause,[],[f19579,f16943,f7886,f948]) ).
fof(f19983,definition,
( spl7_314
<=> hBOOL(sF4) ),
introduced(definition,[new_symbols(definition,[spl7_314])],[avatar_definition]) ).
fof(f19984,plain,
( hBOOL(sF4)
| ~ spl7_314 ),
inference(avatar_component_clause,[],[f19983]) ).
fof(f19985,plain,
( ~ hBOOL(sF4)
| spl7_314 ),
inference(avatar_component_clause,[],[f19983]) ).
fof(f21581,plain,
! [X0,X1] :
( ~ hBOOL(c_Arrow__Order__Mirabelle_OLin)
| X0 = X1
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1) ),
inference(superposition,[],[f6745,f941]) ).
fof(f21915,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,X2,X3),c_COMBI(X4),X5,X6),X1,X6)
| c_in(hAPP(c_COMBI(X4),X7),hAPP(c_COMBK(X1,X2,X3),X7),X6)
| ~ c_in(X7,X0,X5) ),
inference(resolution,[],[f1084,f558]) ).
fof(f21942,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_in(hAPP(c_COMBI(X4),X7),X1,X6)
| ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,X2,X3),c_COMBI(X4),X5,X6),X1,X6)
| ~ c_in(X7,X0,X5) ),
inference(forward_demodulation,[],[f21915,f583]) ).
fof(f21943,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(c_FuncSet_Osko__FuncSet__XPi__I__1__1(X0,c_COMBK(X1,X2,X3),c_COMBI(X4),X5,X6),X1,X6)
| c_in(X7,X1,X6)
| ~ c_in(X7,X0,X5) ),
inference(forward_demodulation,[],[f21942,f584]) ).
fof(f32179,plain,
! [X2,X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_OLin,hAPP(c_COMBK(X0,tc_fun(tc_bool,tc_bool),sF0),X1),tc_bool)
| ~ c_in(X1,X2,sF0)
| c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X2,X0,sF4,sF0,tc_bool),X2,sF0) ),
inference(resolution,[],[f1041,f1129]) ).
fof(f32194,plain,
! [X2,X0,X1] :
( c_in(c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X2,X0,sF4,sF0,tc_bool),X2,sF0)
| ~ c_in(X1,X2,sF0)
| c_in(c_Arrow__Order__Mirabelle_OLin,X0,tc_bool) ),
inference(forward_demodulation,[],[f32179,f583]) ).
fof(f32215,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XfuncsetI__1__1(X1,X2,sF4,sF0,tc_bool)))
| c_in(c_Arrow__Order__Mirabelle_OLin,X2,tc_bool)
| ~ c_in(X0,X1,sF0) ),
inference(resolution,[],[f32194,f561]) ).
fof(f32235,plain,
! [X0,X1] :
( c_in(c_Arrow__Order__Mirabelle_OLin,X0,tc_bool)
| ~ c_in(X1,c_Orderings_Obot__class_Obot(sF2),sF0) ),
inference(resolution,[],[f32215,f1603]) ).
fof(f32267,definition,
( spl7_345
<=> ! [X3] : c_in(c_Arrow__Order__Mirabelle_OLin,X3,tc_bool) ),
introduced(definition,[new_symbols(definition,[spl7_345])],[avatar_definition]) ).
fof(f32268,plain,
( ! [X3] : c_in(c_Arrow__Order__Mirabelle_OLin,X3,tc_bool)
| ~ spl7_345 ),
inference(avatar_component_clause,[],[f32267]) ).
fof(f32307,definition,
( spl7_356
<=> ! [X1] : ~ c_in(X1,c_Orderings_Obot__class_Obot(sF2),sF0) ),
introduced(definition,[new_symbols(definition,[spl7_356])],[avatar_definition]) ).
fof(f32308,plain,
( ! [X1] : ~ c_in(X1,c_Orderings_Obot__class_Obot(sF2),sF0)
| ~ spl7_356 ),
inference(avatar_component_clause,[],[f32307]) ).
fof(f32309,plain,
( spl7_356
| spl7_345 ),
inference(avatar_split_clause,[],[f32235,f32267,f32307]) ).
fof(f32310,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF2) != X0
| ~ spl7_345 ),
inference(resolution,[],[f32268,f13087]) ).
fof(f32323,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin = X0
| ~ spl7_345 ),
inference(resolution,[],[f32268,f26]) ).
fof(f32339,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin != X0
| ~ spl7_345 ),
inference(forward_demodulation,[],[f32310,f32323]) ).
fof(f32350,plain,
( $false
| ~ spl7_345 ),
inference(forward_subsumption_resolution,[],[f32339,f32323]) ).
fof(f32351,plain,
~ spl7_345,
inference(avatar_contradiction_clause,[],[f32350]) ).
fof(f32438,plain,
( ! [X0,X1] :
( ~ c_in(c_Orderings_Obot__class_Obot(sF2),c_Arrow__Order__Mirabelle_OLin,sF1)
| c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Orderings_Obot__class_Obot(sF2),sF0)
| X0 = X1 )
| ~ spl7_356 ),
inference(resolution,[],[f32308,f874]) ).
fof(f32453,plain,
( ! [X0,X1] :
( ~ c_in(c_Orderings_Obot__class_Obot(sF2),c_Arrow__Order__Mirabelle_OLin,sF1)
| X0 = X1 )
| ~ spl7_356 ),
inference(forward_subsumption_resolution,[],[f32438,f32308]) ).
fof(f32455,definition,
( spl7_358
<=> c_in(c_Orderings_Obot__class_Obot(sF2),c_Arrow__Order__Mirabelle_OLin,sF1) ),
introduced(definition,[new_symbols(definition,[spl7_358])],[avatar_definition]) ).
fof(f32457,plain,
( ~ c_in(c_Orderings_Obot__class_Obot(sF2),c_Arrow__Order__Mirabelle_OLin,sF1)
| spl7_358 ),
inference(avatar_component_clause,[],[f32455]) ).
fof(f32458,plain,
( spl7_45
| ~ spl7_358
| ~ spl7_356 ),
inference(avatar_split_clause,[],[f32453,f32307,f32455,f3104]) ).
fof(f32471,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Obot__class_Obot(sF2)))
| spl7_358 ),
inference(resolution,[],[f32457,f560]) ).
fof(f32852,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ hBOOL(X0)
| c_in(X1,c_FuncSet_OPi(X2,c_COMBK(c_FuncSet_OPi(X3,c_COMBK(c_COMBK(X4,X5,X6),X7,X8),sF0,tc_bool),sF2,tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(X4) ),
inference(resolution,[],[f16280,f17311]) ).
fof(f32891,definition,
( spl7_365
<=> ! [X5,X3,X4,X2,X7,X6,X8,X1] :
( c_in(X1,c_FuncSet_OPi(X2,c_COMBK(c_FuncSet_OPi(X3,c_COMBK(c_COMBK(X4,X5,X6),X7,X8),sF0,tc_bool),sF2,tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(X4) ) ),
introduced(definition,[new_symbols(definition,[spl7_365])],[avatar_definition]) ).
fof(f32892,plain,
( ! [X2,X3,X1,X8,X6,X7,X4,X5] :
( c_in(X1,c_FuncSet_OPi(X2,c_COMBK(c_FuncSet_OPi(X3,c_COMBK(c_COMBK(X4,X5,X6),X7,X8),sF0,tc_bool),sF2,tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ hBOOL(X4) )
| ~ spl7_365 ),
inference(avatar_component_clause,[],[f32891]) ).
fof(f32893,plain,
( spl7_365
| spl7_199 ),
inference(avatar_split_clause,[],[f32852,f12623,f32891]) ).
fof(f32901,plain,
( ! [X4] : ~ hBOOL(X4)
| ~ spl7_165
| ~ spl7_365 ),
inference(forward_subsumption_resolution,[],[f32892,f11046]) ).
fof(f32921,plain,
( spl7_199
| ~ spl7_165
| ~ spl7_365 ),
inference(avatar_split_clause,[],[f32901,f32891,f11045,f12623]) ).
fof(f33623,plain,
! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,c_COMBK(X4,tc_fun(X5,tc_bool),X2),X3,X2,X5)))
| c_in(hAPP(X3,X0),X4,X5)
| ~ c_in(X0,X1,X2) ),
inference(resolution,[],[f2107,f561]) ).
fof(f45827,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(hAPP(X7,hAPP(c_Hilbert__Choice_Oinv__into(c_COMBK(X2,X3,X4),X1,X5,X6),X0)),X8,X9)
| ~ c_in(X0,c_Set_Oimage(X1,c_COMBK(X2,X3,X4),X5,X6),X6)
| hBOOL(X2) ),
inference(resolution,[],[f159,f2538]) ).
fof(f47222,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(X0,c_Set_Oimage(X1,c_COMBK(X2,X3,X4),X5,X6),X6)
| hBOOL(X2)
| c_Orderings_Obot__class_Obot(sF2) != X7 ),
inference(resolution,[],[f45827,f13087]) ).
fof(f47347,definition,
( spl7_403
<=> ! [X3,X4,X0,X6,X5,X2,X1] :
( ~ c_in(X6,c_Set_Oimage(X3,c_COMBK(X0,X1,X2),X4,X5),X5)
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_403])],[avatar_definition]) ).
fof(f47348,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(X6,c_Set_Oimage(X3,c_COMBK(X0,X1,X2),X4,X5),X5)
| hBOOL(X0) )
| ~ spl7_403 ),
inference(avatar_component_clause,[],[f47347]) ).
fof(f47395,plain,
( spl7_121
| spl7_403 ),
inference(avatar_split_clause,[],[f47222,f47347,f9186]) ).
fof(f60977,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X3,c_COMBK(X1,X5,X6),c_COMBI(X7),X4,X2)))
| ~ c_in(X0,X3,X4)
| c_in(X0,X1,X2) ),
inference(resolution,[],[f21943,f560]) ).
fof(f61067,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_in(X0,X1,X2)
| c_in(X0,X1,X3)
| c_in(hAPP(c_COMBI(X4),X5),X1,X3)
| ~ c_in(X5,X1,X2) ),
inference(resolution,[],[f60977,f33623]) ).
fof(f61094,plain,
! [X2,X3,X0,X1,X5] :
( c_in(X5,X1,X3)
| ~ c_in(X0,X1,X2)
| c_in(X0,X1,X3)
| ~ c_in(X5,X1,X2) ),
inference(forward_demodulation,[],[f61067,f584]) ).
fof(f61346,plain,
! [X2,X3,X0,X1] :
( c_in(X0,X1,X2)
| ~ c_in(X0,X1,X3)
| ~ c_in(X0,X1,X3) ),
inference(factoring,[],[f61094]) ).
fof(f61347,plain,
! [X2,X3,X0,X1] :
( c_in(X0,X1,X2)
| ~ c_in(X0,X1,X3) ),
inference(duplicate_literal_removal,[],[f61346]) ).
fof(f61382,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_in(hAPP(X0,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X1,c_COMBK(X2,X3,X4),X0,X5,X6)),X2,X7)
| c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,X3,X4),X5,X6),tc_fun(X5,X6)) ),
inference(resolution,[],[f61347,f1021]) ).
fof(f61435,plain,
( ! [X0,X1] : ~ c_in(X0,c_Orderings_Obot__class_Obot(sF1),X1)
| ~ spl7_197 ),
inference(resolution,[],[f61347,f12354]) ).
fof(f61528,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_in(hAPP(X0,X6),hAPP(X2,X6),X4)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,X3,X4),X5)
| ~ c_in(X6,X1,X3) ),
inference(resolution,[],[f61347,f558]) ).
fof(f61574,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_in(c_COMBK(X0,X1,X2),c_FuncSet_OPi(X3,X4,sF0,tc_bool),X5)
| c_in(X0,hAPP(X4,X6),tc_bool)
| ~ c_in(X6,X3,sF0) ),
inference(resolution,[],[f61347,f1038]) ).
fof(f61862,plain,
( ! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(sF1),X2,X0)
| ~ spl7_197 ),
inference(resolution,[],[f61435,f10070]) ).
fof(f62949,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(c_FuncSet_OPi(c_COMBK(X2,X3,X4),X5,sF0,tc_bool),X6,X7),X8,X9),tc_fun(X8,X9))
| hBOOL(X2) ),
inference(resolution,[],[f61382,f12591]) ).
fof(f62972,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_lessequals(c_Set_Oimage(X1,X2,X3,X4),c_FuncSet_OPi(c_COMBK(X0,X5,X6),X7,sF0,tc_bool),tc_fun(X4,tc_bool))
| hBOOL(X0) ),
inference(resolution,[],[f62949,f257]) ).
fof(f63019,definition,
( spl7_432
<=> ! [X8,X7] : ~ c_in(X7,X8,sF0) ),
introduced(definition,[new_symbols(definition,[spl7_432])],[avatar_definition]) ).
fof(f63020,plain,
( ! [X8,X7] : ~ c_in(X7,X8,sF0)
| ~ spl7_432 ),
inference(avatar_component_clause,[],[f63019]) ).
fof(f63291,plain,
( $false
| ~ spl7_432 ),
inference(resolution,[],[f63020,f105]) ).
fof(f63351,plain,
~ spl7_432,
inference(avatar_contradiction_clause,[],[f63291]) ).
fof(f63492,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF2) != X0
| ~ spl7_171 ),
inference(resolution,[],[f11186,f7852]) ).
fof(f63528,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin = X0
| ~ spl7_171 ),
inference(resolution,[],[f11186,f10890]) ).
fof(f63650,plain,
( ! [X0] : c_Arrow__Order__Mirabelle_OLin != X0
| ~ spl7_171 ),
inference(forward_demodulation,[],[f63492,f63528]) ).
fof(f63663,plain,
( $false
| ~ spl7_171 ),
inference(forward_subsumption_resolution,[],[f63650,f63528]) ).
fof(f63664,plain,
~ spl7_171,
inference(avatar_contradiction_clause,[],[f63663]) ).
fof(f66461,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( c_in(hAPP(X1,X2),X0,X5)
| ~ c_in(X1,c_FuncSet_OPi(X6,c_COMBK(X0,X3,X4),X7,X5),X8)
| ~ c_in(X2,X6,X7) ),
inference(superposition,[],[f61528,f583]) ).
fof(f67039,definition,
( spl7_521
<=> ! [X0] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl7_521])],[avatar_definition]) ).
fof(f67040,plain,
( ! [X0] :
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ hBOOL(X0) )
| ~ spl7_521 ),
inference(avatar_component_clause,[],[f67039]) ).
fof(f74207,plain,
( ! [X0,X1] : c_Orderings_Obot__class_Obot(sF2) = c_Set_Oimage(X0,c_Orderings_Obot__class_Obot(sF1),X1,sF1)
| ~ spl7_197 ),
inference(superposition,[],[f61862,f651]) ).
fof(f74280,plain,
( ! [X2,X0] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Orderings_Obot__class_Obot(sF1) )
| ~ spl7_197 ),
inference(superposition,[],[f66,f61862]) ).
fof(f74335,plain,
( ! [X2] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Orderings_Obot__class_Obot(sF1)
| ~ spl7_197 ),
inference(trivial_inequality_removal,[],[f74280]) ).
fof(f74955,plain,
( ! [X2,X0,X1] : c_Orderings_Obot__class_Obot(sF1) = c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(sF1),X2,X0)
| ~ spl7_197 ),
inference(backward_demodulation,[],[f61862,f74335]) ).
fof(f75170,plain,
( ! [X0] :
( c_Orderings_Obot__class_Obot(sF1) = X0
| c_in(c_Arrow__Order__Mirabelle_OLin,c_Set_Oimage(sF4,X0,sF3,sF2),sF2) )
| ~ spl7_197 ),
inference(backward_demodulation,[],[f3362,f74335]) ).
fof(f75484,plain,
( c_Orderings_Obot__class_Obot(sF1) = c_Orderings_Obot__class_Obot(sF2)
| ~ spl7_197 ),
inference(backward_demodulation,[],[f74207,f74955]) ).
fof(f77382,plain,
( ! [X0] :
( c_in(c_Arrow__Order__Mirabelle_OLin,c_Set_Oimage(sF4,X0,sF3,sF2),sF2)
| c_Orderings_Obot__class_Obot(sF2) = X0 )
| ~ spl7_197 ),
inference(backward_demodulation,[],[f75170,f75484]) ).
fof(f80837,definition,
( spl7_696
<=> hBOOL(c_Orderings_Obot__class_Obot(sF2)) ),
introduced(definition,[new_symbols(definition,[spl7_696])],[avatar_definition]) ).
fof(f80838,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF2))
| ~ spl7_696 ),
inference(avatar_component_clause,[],[f80837]) ).
fof(f80839,plain,
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF2))
| spl7_696 ),
inference(avatar_component_clause,[],[f80837]) ).
fof(f84610,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X1,c_FuncSet_Osko__FuncSet__XPi__I__1__1(X3,X2,X0,sF3,sF1)))
| c_in(X0,c_FuncSet_OPi(X3,X2,sF3,sF1),sF6)
| ~ c_in(X0,c_FuncSet_OPi(X1,X2,tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3) ),
inference(resolution,[],[f2432,f560]) ).
fof(f91556,plain,
( ! [X2,X3,X0,X1,X4,X5] : c_in(X0,c_FuncSet_OPi(X1,c_COMBK(sF4,X2,X3),X4,X5),tc_fun(X4,X5))
| ~ spl7_37 ),
inference(forward_subsumption_resolution,[],[f16899,f2551]) ).
fof(f91559,plain,
( ! [X2,X3,X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_COMBK(sF4,X2,X3),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ spl7_37 ),
inference(forward_subsumption_resolution,[],[f18708,f2551]) ).
fof(f92569,plain,
( ! [X2,X3,X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_COMBK(sF4,X2,X3),sF3,sF1),sF6)
| ~ spl7_37 ),
inference(superposition,[],[f91556,f659]) ).
fof(f94046,plain,
( ! [X2,X0,X1] :
( hBOOL(X0)
| c_COMBK(X0,X1,X2) = c_Orderings_Obot__class_Obot(sF2) )
| ~ spl7_197
| ~ spl7_403 ),
inference(resolution,[],[f47348,f77382]) ).
fof(f94088,definition,
( spl7_867
<=> ! [X2,X1,X3] :
( hBOOL(X1)
| c_COMBK(X1,X2,X3) = c_Orderings_Obot__class_Obot(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl7_867])],[avatar_definition]) ).
fof(f94089,plain,
( ! [X2,X3,X1] :
( c_COMBK(X1,X2,X3) = c_Orderings_Obot__class_Obot(sF2)
| hBOOL(X1) )
| ~ spl7_867 ),
inference(avatar_component_clause,[],[f94088]) ).
fof(f94098,plain,
( spl7_867
| ~ spl7_197
| ~ spl7_403 ),
inference(avatar_split_clause,[],[f94046,f47347,f12353,f94088]) ).
fof(f94170,plain,
( ! [X3,X0] :
( hAPP(c_Orderings_Obot__class_Obot(sF2),X3) = X0
| hBOOL(X0) )
| ~ spl7_867 ),
inference(superposition,[],[f583,f94089]) ).
fof(f94243,plain,
( ! [X0] :
( ~ c_in(c_Orderings_Obot__class_Obot(sF2),sF5,sF6)
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| hBOOL(X0) )
| ~ spl7_38
| ~ spl7_867 ),
inference(superposition,[],[f2703,f94089]) ).
fof(f94344,plain,
( ! [X0] :
( c_in(c_Orderings_Obot__class_Obot(sF2),sF5,sF6)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| hBOOL(X0) )
| ~ spl7_867 ),
inference(superposition,[],[f16937,f94089]) ).
fof(f94543,plain,
( sF4 = c_Orderings_Obot__class_Obot(sF2)
| hBOOL(c_Arrow__Order__Mirabelle_OLin)
| ~ spl7_867 ),
inference(superposition,[],[f655,f94089]) ).
fof(f94567,plain,
( ! [X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| hBOOL(sF4) )
| ~ spl7_37
| ~ spl7_867 ),
inference(superposition,[],[f91559,f94089]) ).
fof(f94736,plain,
( ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ spl7_37
| spl7_314
| ~ spl7_867 ),
inference(forward_subsumption_resolution,[],[f94567,f19985]) ).
fof(f94763,definition,
( spl7_877
<=> ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3) ),
introduced(definition,[new_symbols(definition,[spl7_877])],[avatar_definition]) ).
fof(f94764,plain,
( ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| ~ spl7_877 ),
inference(avatar_component_clause,[],[f94763]) ).
fof(f94800,definition,
( spl7_885
<=> ! [X2,X3,X4] :
( ~ hBOOL(X2)
| hBOOL(c_COMBK(X2,X3,X4)) ) ),
introduced(definition,[new_symbols(definition,[spl7_885])],[avatar_definition]) ).
fof(f94801,plain,
( ! [X2,X3,X4] :
( hBOOL(c_COMBK(X2,X3,X4))
| ~ hBOOL(X2) )
| ~ spl7_885 ),
inference(avatar_component_clause,[],[f94800]) ).
fof(f94963,definition,
( spl7_921
<=> ! [X0] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_921])],[avatar_definition]) ).
fof(f94964,plain,
( ! [X0] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| hBOOL(X0) )
| ~ spl7_921 ),
inference(avatar_component_clause,[],[f94963]) ).
fof(f94975,plain,
( ! [X0] :
( c_in(c_Orderings_Obot__class_Obot(sF2),sF5,sF6)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0)) )
| ~ spl7_521
| ~ spl7_867 ),
inference(forward_subsumption_resolution,[],[f94344,f67040]) ).
fof(f94999,definition,
( spl7_926
<=> c_in(c_Orderings_Obot__class_Obot(sF2),sF5,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_926])],[avatar_definition]) ).
fof(f95002,plain,
( spl7_921
| ~ spl7_926
| ~ spl7_38
| ~ spl7_867 ),
inference(avatar_split_clause,[],[f94243,f94088,f2702,f94999,f94963]) ).
fof(f95029,plain,
( spl7_877
| ~ spl7_37
| spl7_314
| ~ spl7_867 ),
inference(avatar_split_clause,[],[f94736,f94088,f19983,f2549,f94763]) ).
fof(f95079,plain,
( spl7_256
| spl7_926
| ~ spl7_521
| ~ spl7_867 ),
inference(avatar_split_clause,[],[f94975,f94088,f67039,f94999,f16943]) ).
fof(f95187,plain,
( hBOOL(sF4)
| spl7_295
| ~ spl7_921 ),
inference(resolution,[],[f94964,f18415]) ).
fof(f95230,plain,
( $false
| spl7_295
| spl7_314
| ~ spl7_921 ),
inference(forward_subsumption_resolution,[],[f95187,f19985]) ).
fof(f95231,plain,
( spl7_295
| spl7_314
| ~ spl7_921 ),
inference(avatar_contradiction_clause,[],[f95230]) ).
fof(f95241,plain,
( ! [X0,X1] :
( X0 = X1
| ~ c_in(sF4,c_Arrow__Order__Mirabelle_OLin,sF1) )
| ~ spl7_37 ),
inference(forward_subsumption_resolution,[],[f21581,f2551]) ).
fof(f95263,plain,
( ! [X0,X1] : X0 = X1
| ~ spl7_37
| ~ spl7_295 ),
inference(forward_subsumption_resolution,[],[f95241,f18308]) ).
fof(f95272,plain,
( spl7_45
| ~ spl7_37
| ~ spl7_295 ),
inference(avatar_split_clause,[],[f95263,f18307,f2549,f3104]) ).
fof(f101149,plain,
( ! [X2,X3,X0,X1,X4] :
( c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),sF3,sF1),sF6)
| ~ hBOOL(X2)
| hBOOL(c_COMBK(X2,X3,X4)) )
| ~ spl7_867 ),
inference(superposition,[],[f17314,f94089]) ).
fof(f103024,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_lessequals(X0,c_FuncSet_OPi(c_COMBK(X2,X3,X4),X5,sF0,tc_bool),tc_fun(X1,tc_bool))
| hBOOL(X2) ),
inference(superposition,[],[f62972,f166]) ).
fof(f104539,plain,
( $false
| ~ spl7_121 ),
inference(equality_resolution,[],[f9187]) ).
fof(f104540,plain,
~ spl7_121,
inference(avatar_contradiction_clause,[],[f104539]) ).
fof(f107484,plain,
! [X2,X3,X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,sF3),sF3,sF1),sF6)
| ~ c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,sF3),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(hAPP(X0,X3),X2,sF1)
| ~ c_in(X3,X1,sF3) ),
inference(resolution,[],[f84610,f14764]) ).
fof(f107517,plain,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_FuncSet_OPi(X1,c_COMBK(X2,sF2,sF3),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(hAPP(X0,X3),X2,sF1)
| ~ c_in(X3,X1,sF3) ),
inference(forward_subsumption_resolution,[],[f107484,f66461]) ).
fof(f107960,plain,
( ! [X2,X3,X0,X1] :
( ~ c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),tc_Arrow__Order__Mirabelle_Oindi,sF1),sF3)
| c_in(hAPP(X0,X3),X2,sF1)
| ~ c_in(X3,X1,sF3)
| hBOOL(X2) )
| ~ spl7_867 ),
inference(superposition,[],[f107517,f94089]) ).
fof(f107962,plain,
( ! [X2,X3,X0,X1] :
( c_in(hAPP(X0,X3),X2,sF1)
| ~ c_in(X3,X1,sF3)
| hBOOL(X2) )
| ~ spl7_867
| ~ spl7_877 ),
inference(forward_subsumption_resolution,[],[f107960,f94764]) ).
fof(f108134,plain,
( ! [X2,X3,X0,X1] :
( c_in(X0,X2,sF1)
| ~ c_in(X1,X3,sF3)
| hBOOL(X2)
| hBOOL(X0) )
| ~ spl7_867
| ~ spl7_877 ),
inference(superposition,[],[f107962,f94170]) ).
fof(f108158,definition,
( spl7_1149
<=> ! [X4,X0] :
( c_in(X0,X4,sF1)
| hBOOL(X0)
| hBOOL(X4) ) ),
introduced(definition,[new_symbols(definition,[spl7_1149])],[avatar_definition]) ).
fof(f108159,plain,
( ! [X0,X4] :
( c_in(X0,X4,sF1)
| hBOOL(X0)
| hBOOL(X4) )
| ~ spl7_1149 ),
inference(avatar_component_clause,[],[f108158]) ).
fof(f108162,plain,
( spl7_165
| spl7_1149
| ~ spl7_867
| ~ spl7_877 ),
inference(avatar_split_clause,[],[f108134,f94763,f94088,f108158,f11045]) ).
fof(f135707,definition,
( spl7_1468
<=> ! [X1] :
( ~ hBOOL(X1)
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl7_1468])],[avatar_definition]) ).
fof(f135708,plain,
( ! [X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X1))
| ~ hBOOL(X1) )
| ~ spl7_1468 ),
inference(avatar_component_clause,[],[f135707]) ).
fof(f170277,plain,
! [X2,X3,X0,X1,X4] :
( c_lessequals(X0,c_COMBK(X2,X3,X4),tc_fun(X1,tc_bool))
| ~ hBOOL(X2) ),
inference(superposition,[],[f17294,f166]) ).
fof(f170300,plain,
! [X2,X3,X0,X1,X4] :
( ~ c_lessequals(c_COMBK(X0,X1,X2),X3,tc_fun(X4,tc_bool))
| c_COMBK(X0,X1,X2) = X3
| ~ hBOOL(X0) ),
inference(resolution,[],[f170277,f339]) ).
fof(f170304,plain,
! [X0,X1] :
( c_lessequals(X0,sF4,tc_fun(X1,tc_bool))
| ~ hBOOL(c_Arrow__Order__Mirabelle_OLin) ),
inference(superposition,[],[f170277,f655]) ).
fof(f170314,plain,
( ! [X0,X1] : c_lessequals(X0,sF4,tc_fun(X1,tc_bool))
| ~ spl7_37 ),
inference(forward_subsumption_resolution,[],[f170304,f2551]) ).
fof(f170504,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_COMBK(X0,X1,X2) = c_COMBK(X3,X4,X5)
| ~ hBOOL(X0)
| ~ hBOOL(X3) ),
inference(resolution,[],[f170300,f170277]) ).
fof(f170505,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_COMBK(X0,X1,X2) = c_FuncSet_OPi(c_COMBK(X3,X4,X5),X6,sF0,tc_bool)
| ~ hBOOL(X0)
| hBOOL(X3) ),
inference(resolution,[],[f170300,f103024]) ).
fof(f170509,plain,
( ! [X2,X0,X1] :
( c_COMBK(X0,X1,X2) = sF4
| ~ hBOOL(X0) )
| ~ spl7_37 ),
inference(resolution,[],[f170300,f170314]) ).
fof(f170683,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(sF5,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X3,sF0,tc_bool)))
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X4))
| ~ hBOOL(X4)
| hBOOL(X0) )
| ~ spl7_38 ),
inference(superposition,[],[f3366,f170505]) ).
fof(f170796,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(sF5,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X3,sF0,tc_bool)))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X4))
| ~ hBOOL(X4)
| hBOOL(X0) ),
inference(superposition,[],[f16952,f170505]) ).
fof(f171689,definition,
( spl7_2268
<=> ! [X0,X3,X2,X1] :
( hBOOL(hAPP(sF5,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X3,sF0,tc_bool)))
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_2268])],[avatar_definition]) ).
fof(f171690,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(sF5,c_FuncSet_OPi(c_COMBK(X0,X1,X2),X3,sF0,tc_bool)))
| hBOOL(X0) )
| ~ spl7_2268 ),
inference(avatar_component_clause,[],[f171689]) ).
fof(f171691,plain,
( spl7_521
| spl7_2268 ),
inference(avatar_split_clause,[],[f170796,f171689,f67039]) ).
fof(f171856,plain,
( ! [X0,X4] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X4))
| ~ hBOOL(X4)
| hBOOL(X0) )
| ~ spl7_38
| ~ spl7_2268 ),
inference(forward_subsumption_resolution,[],[f170683,f171690]) ).
fof(f171937,plain,
( spl7_171
| spl7_1468
| ~ spl7_38
| ~ spl7_2268 ),
inference(avatar_split_clause,[],[f171856,f171689,f2702,f135707,f11185]) ).
fof(f172128,plain,
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF2))
| spl7_358
| ~ spl7_1468 ),
inference(resolution,[],[f135708,f32471]) ).
fof(f172135,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(c_COMBK(X0,X1,X2))
| ~ hBOOL(X0) )
| ~ spl7_1468 ),
inference(resolution,[],[f135708,f11708]) ).
fof(f172195,plain,
( ! [X0] : ~ hBOOL(X0)
| ~ spl7_885
| ~ spl7_1468 ),
inference(forward_subsumption_resolution,[],[f172135,f94801]) ).
fof(f172198,plain,
( $false
| spl7_358
| ~ spl7_696
| ~ spl7_1468 ),
inference(forward_subsumption_resolution,[],[f172128,f80838]) ).
fof(f172199,plain,
( spl7_358
| ~ spl7_696
| ~ spl7_1468 ),
inference(avatar_contradiction_clause,[],[f172198]) ).
fof(f172204,plain,
( spl7_199
| ~ spl7_885
| ~ spl7_1468 ),
inference(avatar_split_clause,[],[f172195,f135707,f94800,f12623]) ).
fof(f175440,definition,
( spl7_2340
<=> ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),sF3,sF1),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_2340])],[avatar_definition]) ).
fof(f175441,plain,
( ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,c_Orderings_Obot__class_Obot(sF2),sF3,sF1),sF6)
| ~ spl7_2340 ),
inference(avatar_component_clause,[],[f175440]) ).
fof(f175442,plain,
( spl7_885
| spl7_2340
| ~ spl7_867 ),
inference(avatar_split_clause,[],[f101149,f94088,f175440,f94800]) ).
fof(f178366,plain,
( ! [X0] :
( hBOOL(X0)
| hBOOL(c_Orderings_Obot__class_Obot(sF2)) )
| ~ spl7_1149 ),
inference(resolution,[],[f108159,f1049]) ).
fof(f180438,plain,
! [X2,X3,X10,X0,X11,X1,X6,X7,X4,X5] :
( c_in(X3,c_FuncSet_OPi(X4,c_COMBK(X0,X1,X2),X10,X11),tc_fun(X10,X11))
| ~ hBOOL(X5)
| ~ hBOOL(c_COMBK(X5,X6,X7))
| ~ hBOOL(X0) ),
inference(superposition,[],[f16891,f170504]) ).
fof(f182838,plain,
( ! [X0,X1] :
( c_in(X0,c_FuncSet_OPi(X1,sF4,sF3,sF1),sF6)
| ~ hBOOL(sF4) )
| ~ spl7_37 ),
inference(superposition,[],[f92569,f170509]) ).
fof(f183213,plain,
( ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,sF4,sF3,sF1),sF6)
| ~ spl7_37
| ~ spl7_314 ),
inference(forward_subsumption_resolution,[],[f182838,f19984]) ).
fof(f183285,plain,
( spl7_79
| ~ spl7_37
| ~ spl7_314 ),
inference(avatar_split_clause,[],[f183213,f19983,f2549,f7069]) ).
fof(f183513,plain,
( ! [X0] : hBOOL(X0)
| spl7_696
| ~ spl7_1149 ),
inference(forward_subsumption_resolution,[],[f178366,f80839]) ).
fof(f183750,plain,
( spl7_171
| spl7_696
| ~ spl7_1149 ),
inference(avatar_split_clause,[],[f183513,f108158,f80837,f11185]) ).
fof(f184139,plain,
( sF4 = c_Orderings_Obot__class_Obot(sF2)
| spl7_37
| ~ spl7_867 ),
inference(forward_subsumption_resolution,[],[f94543,f2550]) ).
fof(f184171,definition,
( spl7_2481
<=> sF4 = c_Orderings_Obot__class_Obot(sF2) ),
introduced(definition,[new_symbols(definition,[spl7_2481])],[avatar_definition]) ).
fof(f184172,plain,
( sF4 = c_Orderings_Obot__class_Obot(sF2)
| ~ spl7_2481 ),
inference(avatar_component_clause,[],[f184171]) ).
fof(f184349,plain,
( spl7_2481
| spl7_37
| ~ spl7_867 ),
inference(avatar_split_clause,[],[f184139,f94088,f2549,f184171]) ).
fof(f188181,plain,
( ! [X0,X1] : c_in(X0,c_FuncSet_OPi(X1,sF4,sF3,sF1),sF6)
| ~ spl7_2340
| ~ spl7_2481 ),
inference(backward_demodulation,[],[f175441,f184172]) ).
fof(f188573,plain,
( spl7_79
| ~ spl7_2340
| ~ spl7_2481 ),
inference(avatar_split_clause,[],[f188181,f184171,f175440,f7069]) ).
fof(f190068,plain,
( ! [X2,X3,X10,X0,X11,X1,X4,X5] :
( c_in(X3,c_FuncSet_OPi(X4,c_COMBK(X0,X1,X2),X10,X11),tc_fun(X10,X11))
| ~ hBOOL(X5)
| ~ hBOOL(X0) )
| ~ spl7_885 ),
inference(forward_subsumption_resolution,[],[f180438,f94801]) ).
fof(f190287,definition,
( spl7_2526
<=> ! [X3,X4,X11,X0,X12,X2,X1] :
( c_in(X3,c_FuncSet_OPi(X4,c_COMBK(X0,X1,X2),X11,X12),tc_fun(X11,X12))
| ~ hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_2526])],[avatar_definition]) ).
fof(f190288,plain,
( ! [X2,X3,X0,X11,X1,X4,X12] :
( c_in(X3,c_FuncSet_OPi(X4,c_COMBK(X0,X1,X2),X11,X12),tc_fun(X11,X12))
| ~ hBOOL(X0) )
| ~ spl7_2526 ),
inference(avatar_component_clause,[],[f190287]) ).
fof(f190296,plain,
( spl7_199
| spl7_2526
| ~ spl7_885 ),
inference(avatar_split_clause,[],[f190068,f94800,f190287,f12623]) ).
fof(f242460,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(X0)
| c_in(X1,hAPP(c_COMBK(X0,X2,X3),X4),tc_bool)
| ~ c_in(X4,X5,sF0) )
| ~ spl7_2526 ),
inference(resolution,[],[f190288,f61574]) ).
fof(f242505,plain,
( ! [X0,X1,X4,X5] :
( c_in(X1,X0,tc_bool)
| ~ hBOOL(X0)
| ~ c_in(X4,X5,sF0) )
| ~ spl7_2526 ),
inference(forward_demodulation,[],[f242460,f583]) ).
fof(f242512,definition,
( spl7_4998
<=> ! [X0,X1] :
( c_in(X1,X0,tc_bool)
| ~ hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_4998])],[avatar_definition]) ).
fof(f242513,plain,
( ! [X0,X1] :
( c_in(X1,X0,tc_bool)
| ~ hBOOL(X0) )
| ~ spl7_4998 ),
inference(avatar_component_clause,[],[f242512]) ).
fof(f242514,plain,
( spl7_432
| spl7_4998
| ~ spl7_2526 ),
inference(avatar_split_clause,[],[f242505,f190287,f242512,f63019]) ).
fof(f242579,plain,
( ~ hBOOL(sF4)
| ~ spl7_39
| ~ spl7_4998 ),
inference(resolution,[],[f242513,f2757]) ).
fof(f242594,plain,
( $false
| ~ spl7_39
| ~ spl7_314
| ~ spl7_4998 ),
inference(forward_subsumption_resolution,[],[f242579,f19984]) ).
fof(f242595,plain,
( ~ spl7_39
| ~ spl7_314
| ~ spl7_4998 ),
inference(avatar_contradiction_clause,[],[f242594]) ).
cnf(s3,plain,
~ spl7_3,
inference(sat_conversion,[],[f1052]) ).
cnf(s24,plain,
( spl7_36
| spl7_37 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s25,plain,
( spl7_3
| spl7_38 ),
inference(sat_conversion,[],[f2704]) ).
cnf(s29,plain,
( ~ spl7_36
| spl7_39 ),
inference(sat_conversion,[],[f2774]) ).
cnf(s34,plain,
( spl7_45
| ~ spl7_46 ),
inference(sat_conversion,[],[f3111]) ).
cnf(s190,plain,
~ spl7_45,
inference(sat_conversion,[],[f6205]) ).
cnf(s231,plain,
( ~ spl7_38
| spl7_58
| ~ spl7_79 ),
inference(sat_conversion,[],[f7251]) ).
cnf(s245,plain,
( spl7_46
| ~ spl7_58 ),
inference(sat_conversion,[],[f8035]) ).
cnf(s408,plain,
~ spl7_166,
inference(sat_conversion,[],[f11202]) ).
cnf(s435,plain,
( spl7_166
| spl7_197 ),
inference(sat_conversion,[],[f12355]) ).
cnf(s454,plain,
~ spl7_199,
inference(sat_conversion,[],[f12972]) ).
cnf(s697,plain,
( ~ spl7_39
| spl7_45
| ~ spl7_295 ),
inference(sat_conversion,[],[f18310]) ).
cnf(s751,plain,
~ spl7_98,
inference(sat_conversion,[],[f19669]) ).
cnf(s753,plain,
( spl7_3
| spl7_98
| ~ spl7_256 ),
inference(sat_conversion,[],[f19671]) ).
cnf(s836,plain,
( spl7_345
| spl7_356 ),
inference(sat_conversion,[],[f32309]) ).
cnf(s842,plain,
~ spl7_345,
inference(sat_conversion,[],[f32351]) ).
cnf(s848,plain,
( spl7_45
| ~ spl7_356
| ~ spl7_358 ),
inference(sat_conversion,[],[f32458]) ).
cnf(s857,plain,
( spl7_199
| spl7_365 ),
inference(sat_conversion,[],[f32893]) ).
cnf(s860,plain,
( ~ spl7_165
| spl7_199
| ~ spl7_365 ),
inference(sat_conversion,[],[f32921]) ).
cnf(s959,plain,
( spl7_121
| spl7_403 ),
inference(sat_conversion,[],[f47395]) ).
cnf(s1009,plain,
~ spl7_432,
inference(sat_conversion,[],[f63351]) ).
cnf(s1098,plain,
~ spl7_171,
inference(sat_conversion,[],[f63664]) ).
cnf(s2102,plain,
( ~ spl7_197
| ~ spl7_403
| spl7_867 ),
inference(sat_conversion,[],[f94098]) ).
cnf(s2163,plain,
( ~ spl7_38
| ~ spl7_867
| spl7_921
| ~ spl7_926 ),
inference(sat_conversion,[],[f95002]) ).
cnf(s2171,plain,
( ~ spl7_37
| spl7_314
| ~ spl7_867
| spl7_877 ),
inference(sat_conversion,[],[f95029]) ).
cnf(s2189,plain,
( spl7_256
| ~ spl7_521
| ~ spl7_867
| spl7_926 ),
inference(sat_conversion,[],[f95079]) ).
cnf(s2243,plain,
( spl7_295
| spl7_314
| ~ spl7_921 ),
inference(sat_conversion,[],[f95231]) ).
cnf(s2261,plain,
( ~ spl7_37
| spl7_45
| ~ spl7_295 ),
inference(sat_conversion,[],[f95272]) ).
cnf(s2618,plain,
~ spl7_121,
inference(sat_conversion,[],[f104540]) ).
cnf(s2697,plain,
( spl7_165
| ~ spl7_867
| ~ spl7_877
| spl7_1149 ),
inference(sat_conversion,[],[f108162]) ).
cnf(s6240,plain,
( spl7_521
| spl7_2268 ),
inference(sat_conversion,[],[f171691]) ).
cnf(s6336,plain,
( ~ spl7_38
| spl7_171
| spl7_1468
| ~ spl7_2268 ),
inference(sat_conversion,[],[f171937]) ).
cnf(s6365,plain,
( spl7_358
| ~ spl7_696
| ~ spl7_1468 ),
inference(sat_conversion,[],[f172199]) ).
cnf(s6368,plain,
( spl7_199
| ~ spl7_885
| ~ spl7_1468 ),
inference(sat_conversion,[],[f172204]) ).
cnf(s6516,plain,
( ~ spl7_867
| spl7_885
| spl7_2340 ),
inference(sat_conversion,[],[f175442]) ).
cnf(s7068,plain,
( ~ spl7_37
| spl7_79
| ~ spl7_314 ),
inference(sat_conversion,[],[f183285]) ).
cnf(s7168,plain,
( spl7_171
| spl7_696
| ~ spl7_1149 ),
inference(sat_conversion,[],[f183750]) ).
cnf(s7320,plain,
( spl7_37
| ~ spl7_867
| spl7_2481 ),
inference(sat_conversion,[],[f184349]) ).
cnf(s7340,plain,
( spl7_79
| ~ spl7_2340
| ~ spl7_2481 ),
inference(sat_conversion,[],[f188573]) ).
cnf(s7448,plain,
( spl7_199
| ~ spl7_885
| spl7_2526 ),
inference(sat_conversion,[],[f190296]) ).
cnf(s11598,plain,
( spl7_432
| ~ spl7_2526
| spl7_4998 ),
inference(sat_conversion,[],[f242514]) ).
cnf(s11602,plain,
( ~ spl7_39
| ~ spl7_314
| ~ spl7_4998 ),
inference(sat_conversion,[],[f242595]) ).
cnf(s11741,plain,
spl7_403,
inference(rat,[],[s959,s2618]) ).
cnf(s11750,plain,
spl7_356,
inference(rat,[],[s836,s842]) ).
cnf(s11863,plain,
spl7_365,
inference(rat,[],[s857,s454]) ).
cnf(s11883,plain,
~ spl7_165,
inference(rat,[],[s860,s454,s11863]) ).
cnf(s11900,plain,
spl7_197,
inference(rat,[],[s435,s408]) ).
cnf(s11918,plain,
spl7_867,
inference(rat,[],[s2102,s11741,s11900]) ).
cnf(s12195,plain,
~ spl7_358,
inference(rat,[],[s848,s11750,s190]) ).
cnf(s12208,plain,
~ spl7_46,
inference(rat,[],[s34,s190]) ).
cnf(s12209,plain,
~ spl7_58,
inference(rat,[],[s245,s12208]) ).
cnf(s12230,plain,
~ spl7_256,
inference(rat,[],[s753,s751,s3]) ).
cnf(s12237,plain,
spl7_38,
inference(rat,[],[s25,s3]) ).
cnf(s12275,plain,
~ spl7_79,
inference(rat,[],[s231,s12209,s12237]) ).
cnf(s12320,plain,
spl7_37,
inference(rat,[],[s2163,s2189,s2243,s6240,s11602,s6336,s11598,s6368,s7448,s697,s6516,s29,s7340,s24,s7320,s11918,s12237,s12230,s1098,s1009,s454,s190,s12275]) ).
cnf(s12323,plain,
~ spl7_314,
inference(rat,[],[s7068,s12275,s12320]) ).
cnf(s12329,plain,
~ spl7_295,
inference(rat,[],[s2261,s190,s12320]) ).
cnf(s12359,plain,
spl7_877,
inference(rat,[],[s2171,s12320,s11918,s12323]) ).
cnf(s12363,plain,
~ spl7_921,
inference(rat,[],[s2243,s12329,s12323]) ).
cnf(s12409,plain,
spl7_1149,
inference(rat,[],[s2697,s11918,s11883,s12359]) ).
cnf(s12416,plain,
~ spl7_926,
inference(rat,[],[s2163,s12237,s11918,s12363]) ).
cnf(s12494,plain,
spl7_696,
inference(rat,[],[s7168,s1098,s12409]) ).
cnf(s12501,plain,
~ spl7_521,
inference(rat,[],[s2189,s12230,s11918,s12416]) ).
cnf(s12533,plain,
~ spl7_1468,
inference(rat,[],[s6365,s12195,s12494]) ).
cnf(s12561,plain,
spl7_2268,
inference(rat,[],[s6240,s12501]) ).
cnf(s12595,plain,
$false,
inference(rat,[],[s6336,s12237,s1098,s12561,s12533]) ).
fof(f242616,plain,
$false,
inference(avatar_sat_refutation,[],[s12595]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT018-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n018.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 23:31:40 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.24/2.35 % (2851558)Input is clausal, will run a generic CNF schedule.
% 10.24/2.35 % (2851567)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=81327336:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.24/2.35 % (2851566)lrs+10_1_sil=8000:sp=occurrence:random_seed=524402031:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.24/2.35 % (2851565)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=707203201:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.24/2.35 % (2851564)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3981271003:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.24/2.35 % (2851563)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=439119800:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.24/2.35 % (2851568)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3213829579:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.24/2.35 % (2851569)dis-21_1_sil=8000:lcm=predicate:random_seed=3228517260:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.24/2.35 % (2851567)Instruction limit reached!
% 10.24/2.35 % (2851567)------------------------------
% 10.24/2.35 % (2851567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.35 % (2851567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.35 % (2851567)CaDiCaL version: 2.1.3
% 10.24/2.35 % (2851567)Termination reason: Instruction limit
% 10.24/2.35 % (2851567)Termination phase: Saturation
% 10.24/2.35 % (2851567)Time elapsed: 0.044 s
% 10.24/2.35 % (2851567)Peak memory usage: 89 MB
% 10.24/2.35 % (2851567)Instructions burned: 116 (million)
% 10.24/2.35 % (2851566)Instruction limit reached!
% 10.24/2.35 % (2851566)------------------------------
% 10.24/2.35 % (2851566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.35 % (2851566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.35 % (2851566)CaDiCaL version: 2.1.3
% 10.24/2.35 % (2851566)Termination reason: Instruction limit
% 10.24/2.35 % (2851566)Termination phase: Saturation
% 10.24/2.35 % (2851566)Time elapsed: 0.071 s
% 10.24/2.35 % (2851566)Peak memory usage: 89 MB
% 10.24/2.35 % (2851566)Instructions burned: 108 (million)
% 10.24/2.35 % (2851569)Instruction limit reached!
% 10.24/2.35 % (2851569)------------------------------
% 10.24/2.35 % (2851569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.35 % (2851569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.35 % (2851569)CaDiCaL version: 2.1.3
% 10.24/2.35 % (2851569)Termination reason: Instruction limit
% 10.24/2.35 % (2851569)Termination phase: Saturation
% 10.24/2.35 % (2851569)Time elapsed: 0.070 s
% 10.24/2.35 % (2851569)Peak memory usage: 89 MB
% 10.24/2.35 % (2851569)Instructions burned: 117 (million)
% 10.24/2.35 % (2851577)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1386980008:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.24/2.35 % (2851568)Instruction limit reached!
% 10.24/2.35 % (2851568)------------------------------
% 10.24/2.35 % (2851568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.35 % (2851568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.35 % (2851568)CaDiCaL version: 2.1.3
% 10.24/2.35 % (2851568)Termination reason: Instruction limit
% 10.24/2.35 % (2851568)Termination phase: Saturation
% 10.24/2.35 % (2851568)Time elapsed: 0.129 s
% 10.24/2.35 % (2851568)Peak memory usage: 90 MB
% 10.24/2.35 % (2851568)Instructions burned: 181 (million)
% 10.24/2.35 % (2851577)Instruction limit reached!
% 10.24/2.35 % (2851577)------------------------------
% 10.24/2.35 % (2851577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.24/2.35 % (2851577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.24/2.35 % (2851577)CaDiCaL version: 2.1.3
% 10.24/2.35 % (2851577)Termination reason: Instruction limit
% 10.24/2.35 % (2851577)Termination phase: Saturation
% 10.24/2.35 % (2851577)Time elapsed: 0.046 s
% 10.24/2.35 % (2851577)Peak memory usage: 89 MB
% 10.24/2.35 % (2851577)Instructions burned: 146 (million)
% 10.24/2.35 % (2851578)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=348023492:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 16.89/3.28 % (2851579)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3211556173:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.89/3.28 % (2851582)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=337401586:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 16.89/3.28 % (2851581)lrs+10_64_to=lpo:sil=8000:random_seed=2301628051:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 16.89/3.28 % (2851578)Instruction limit reached!
% 16.89/3.28 % (2851578)------------------------------
% 16.89/3.28 % (2851578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.89/3.28 % (2851578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.28 % (2851578)CaDiCaL version: 2.1.3
% 16.89/3.28 % (2851578)Termination reason: Instruction limit
% 16.89/3.28 % (2851578)Termination phase: Saturation
% 16.89/3.28 % (2851578)Time elapsed: 0.103 s
% 16.89/3.28 % (2851578)Peak memory usage: 91 MB
% 16.89/3.28 % (2851578)Instructions burned: 190 (million)
% 16.89/3.28 % (2851582)Instruction limit reached!
% 16.89/3.28 % (2851582)------------------------------
% 16.89/3.28 % (2851582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.89/3.28 % (2851582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.28 % (2851582)CaDiCaL version: 2.1.3
% 16.89/3.28 % (2851582)Termination reason: Instruction limit
% 16.89/3.28 % (2851582)Termination phase: Saturation
% 16.89/3.28 % (2851582)Time elapsed: 0.065 s
% 16.89/3.28 % (2851582)Peak memory usage: 90 MB
% 16.89/3.28 % (2851582)Instructions burned: 194 (million)
% 16.89/3.28 % (2851581)Instruction limit reached!
% 16.89/3.28 % (2851581)------------------------------
% 16.89/3.28 % (2851581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.89/3.28 % (2851581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.28 % (2851581)CaDiCaL version: 2.1.3
% 16.89/3.28 % (2851581)Termination reason: Instruction limit
% 16.89/3.28 % (2851581)Termination phase: Saturation
% 16.89/3.28 % (2851581)Time elapsed: 0.077 s
% 16.89/3.28 % (2851581)Peak memory usage: 89 MB
% 16.89/3.28 % (2851581)Instructions burned: 126 (million)
% 16.89/3.28 % (2851579)Instruction limit reached!
% 16.89/3.28 % (2851579)------------------------------
% 16.89/3.28 % (2851579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.89/3.28 % (2851579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.28 % (2851579)CaDiCaL version: 2.1.3
% 16.89/3.28 % (2851579)Termination reason: Instruction limit
% 16.89/3.28 % (2851579)Termination phase: Saturation
% 16.89/3.28 % (2851579)Time elapsed: 0.132 s
% 16.89/3.28 % (2851579)Peak memory usage: 90 MB
% 16.89/3.28 % (2851579)Instructions burned: 220 (million)
% 16.89/3.28 % (2851588)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1313070027:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 16.89/3.28 % (2851587)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1513111747:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 16.89/3.28 % (2851590)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1174423914:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 16.89/3.28 % (2851589)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=169425123:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 16.89/3.28 % (2851587)Instruction limit reached!
% 16.89/3.28 % (2851587)------------------------------
% 16.89/3.28 % (2851587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.89/3.28 % (2851587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.89/3.28 % (2851587)CaDiCaL version: 2.1.3
% 16.89/3.28 % (2851587)Termination reason: Instruction limit
% 16.89/3.28 % (2851587)Termination phase: Saturation
% 16.89/3.28 % (2851587)Time elapsed: 0.105 s
% 16.89/3.28 % (2851587)Peak memory usage: 90 MB
% 16.89/3.28 % (2851587)Instructions burned: 158 (million)
% 16.89/3.28 % (2851589)Instruction limit reached!
% 16.89/3.28 % (2851589)------------------------------
% 16.89/3.28 % (2851589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851589)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851589)Termination reason: Instruction limit
% 33.90/5.62 % (2851589)Termination phase: Saturation
% 33.90/5.62 % (2851589)Time elapsed: 0.059 s
% 33.90/5.62 % (2851589)Peak memory usage: 89 MB
% 33.90/5.62 % (2851589)Instructions burned: 107 (million)
% 33.90/5.62 % (2851590)Instruction limit reached!
% 33.90/5.62 % (2851590)------------------------------
% 33.90/5.62 % (2851590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851590)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851590)Termination reason: Instruction limit
% 33.90/5.62 % (2851590)Termination phase: Saturation
% 33.90/5.62 % (2851590)Time elapsed: 0.069 s
% 33.90/5.62 % (2851590)Peak memory usage: 90 MB
% 33.90/5.62 % (2851590)Instructions burned: 108 (million)
% 33.90/5.62 % (2851595)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1776128017:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 33.90/5.62 % (2851597)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1632957978:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 33.90/5.62 % (2851596)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4045938296:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 33.90/5.62 % (2851597)Instruction limit reached!
% 33.90/5.62 % (2851597)------------------------------
% 33.90/5.62 % (2851597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851597)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851597)Termination reason: Instruction limit
% 33.90/5.62 % (2851597)Termination phase: Saturation
% 33.90/5.62 % (2851597)Time elapsed: 0.094 s
% 33.90/5.62 % (2851597)Peak memory usage: 89 MB
% 33.90/5.62 % (2851597)Instructions burned: 134 (million)
% 33.90/5.62 % (2851595)Instruction limit reached!
% 33.90/5.62 % (2851595)------------------------------
% 33.90/5.62 % (2851595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851595)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851595)Termination reason: Instruction limit
% 33.90/5.62 % (2851595)Termination phase: Saturation
% 33.90/5.62 % (2851595)Time elapsed: 0.149 s
% 33.90/5.62 % (2851595)Peak memory usage: 90 MB
% 33.90/5.62 % (2851595)Instructions burned: 243 (million)
% 33.90/5.62 % (2851601)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=385715245:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 33.90/5.62 % (2851602)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2085196322:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 33.90/5.62 % (2851602)Instruction limit reached!
% 33.90/5.62 % (2851602)------------------------------
% 33.90/5.62 % (2851602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851602)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851602)Termination reason: Instruction limit
% 33.90/5.62 % (2851602)Termination phase: Saturation
% 33.90/5.62 % (2851602)Time elapsed: 0.121 s
% 33.90/5.62 % (2851602)Peak memory usage: 91 MB
% 33.90/5.62 % (2851602)Instructions burned: 191 (million)
% 33.90/5.62 % (2851605)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2865336404:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 33.90/5.62 % (2851601)Instruction limit reached!
% 33.90/5.62 % (2851601)------------------------------
% 33.90/5.62 % (2851601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.62 % (2851601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.62 % (2851601)CaDiCaL version: 2.1.3
% 33.90/5.62 % (2851601)Termination reason: Instruction limit
% 33.90/5.62 % (2851601)Termination phase: Saturation
% 33.90/5.62 % (2851601)Time elapsed: 0.319 s
% 33.90/5.62 % (2851601)Peak memory usage: 95 MB
% 33.90/5.62 % (2851601)Instructions burned: 499 (million)
% 33.90/5.62 % (2851607)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4117874019:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 48.22/7.74 % (2851605)Instruction limit reached!
% 48.22/7.74 % (2851605)------------------------------
% 48.22/7.74 % (2851605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851605)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851605)Termination reason: Instruction limit
% 48.22/7.74 % (2851605)Termination phase: Saturation
% 48.22/7.74 % (2851605)Time elapsed: 0.168 s
% 48.22/7.74 % (2851605)Peak memory usage: 91 MB
% 48.22/7.74 % (2851605)Instructions burned: 264 (million)
% 48.22/7.74 % (2851607)Instruction limit reached!
% 48.22/7.74 % (2851607)------------------------------
% 48.22/7.74 % (2851607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851607)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851607)Termination reason: Instruction limit
% 48.22/7.74 % (2851607)Termination phase: Saturation
% 48.22/7.74 % (2851607)Time elapsed: 0.101 s
% 48.22/7.74 % (2851607)Peak memory usage: 90 MB
% 48.22/7.74 % (2851607)Instructions burned: 157 (million)
% 48.22/7.74 % (2851609)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1377633840:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 48.22/7.74 % (2851588)Instruction limit reached!
% 48.22/7.74 % (2851588)------------------------------
% 48.22/7.74 % (2851588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851588)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851588)Termination reason: Instruction limit
% 48.22/7.74 % (2851588)Termination phase: Saturation
% 48.22/7.74 % (2851588)Time elapsed: 1.082 s
% 48.22/7.74 % (2851588)Peak memory usage: 151 MB
% 48.22/7.74 % (2851588)Instructions burned: 3397 (million)
% 48.22/7.74 % (2851612)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3803787736:i=180:bd=preordered:av=off_2983 on theBenchmark for (2983ds/180Mi)
% 48.22/7.74 % (2851610)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2042293912:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 48.22/7.74 % (2851612)Instruction limit reached!
% 48.22/7.74 % (2851612)------------------------------
% 48.22/7.74 % (2851612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851612)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851612)Termination reason: Instruction limit
% 48.22/7.74 % (2851612)Termination phase: Saturation
% 48.22/7.74 % (2851612)Time elapsed: 0.050 s
% 48.22/7.74 % (2851612)Peak memory usage: 91 MB
% 48.22/7.74 % (2851612)Instructions burned: 183 (million)
% 48.22/7.74 % (2851615)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1164619609:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/10307Mi)
% 48.22/7.74 % (2851610)Instruction limit reached!
% 48.22/7.74 % (2851610)------------------------------
% 48.22/7.74 % (2851610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851610)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851610)Termination reason: Instruction limit
% 48.22/7.74 % (2851610)Termination phase: Saturation
% 48.22/7.74 % (2851610)Time elapsed: 0.337 s
% 48.22/7.74 % (2851610)Peak memory usage: 92 MB
% 48.22/7.74 % (2851610)Instructions burned: 537 (million)
% 48.22/7.74 % (2851617)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2730427140:i=412:gtgl=4:gtg=exists_all_2979 on theBenchmark for (2979ds/412Mi)
% 48.22/7.74 % (2851617)Instruction limit reached!
% 48.22/7.74 % (2851617)------------------------------
% 48.22/7.74 % (2851617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.22/7.74 % (2851617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.22/7.74 % (2851617)CaDiCaL version: 2.1.3
% 48.22/7.74 % (2851617)Termination reason: Instruction limit
% 48.22/7.74 % (2851617)Termination phase: Saturation
% 73.64/11.22 % (2851617)Time elapsed: 0.229 s
% 73.64/11.22 % (2851617)Peak memory usage: 93 MB
% 73.64/11.22 % (2851617)Instructions burned: 413 (million)
% 73.64/11.22 % (2851619)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1283936678:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 73.64/11.22 % (2851609)Instruction limit reached!
% 73.64/11.22 % (2851609)------------------------------
% 73.64/11.22 % (2851609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.64/11.22 % (2851609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.64/11.22 % (2851609)CaDiCaL version: 2.1.3
% 73.64/11.22 % (2851609)Termination reason: Instruction limit
% 73.64/11.22 % (2851609)Termination phase: Saturation
% 73.64/11.22 % (2851609)Time elapsed: 1.292 s
% 73.64/11.22 % (2851609)Peak memory usage: 151 MB
% 73.64/11.22 % (2851609)Instructions burned: 3260 (million)
% 73.64/11.22 % (2851621)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=193372200:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 73.64/11.22 % (2851621)Instruction limit reached!
% 73.64/11.22 % (2851621)------------------------------
% 73.64/11.22 % (2851621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.64/11.22 % (2851621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.64/11.22 % (2851621)CaDiCaL version: 2.1.3
% 73.64/11.22 % (2851621)Termination reason: Instruction limit
% 73.64/11.22 % (2851621)Termination phase: Saturation
% 73.64/11.22 % (2851621)Time elapsed: 0.090 s
% 73.64/11.22 % (2851621)Peak memory usage: 92 MB
% 73.64/11.22 % (2851621)Instructions burned: 305 (million)
% 73.64/11.22 % (2851623)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3679643647:st=4:i=720:sd=3:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/720Mi)
% 73.64/11.22 % (2851623)Instruction limit reached!
% 73.64/11.22 % (2851623)------------------------------
% 73.64/11.22 % (2851623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.64/11.22 % (2851623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.64/11.22 % (2851623)CaDiCaL version: 2.1.3
% 73.64/11.22 % (2851623)Termination reason: Instruction limit
% 73.64/11.22 % (2851623)Termination phase: Saturation
% 73.64/11.22 % (2851623)Time elapsed: 0.197 s
% 73.64/11.22 % (2851623)Peak memory usage: 93 MB
% 73.64/11.22 % (2851623)Instructions burned: 722 (million)
% 73.64/11.22 % (2851625)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=147837071:i=598:bs=on:bd=preordered:av=off:ss=axioms_2966 on theBenchmark for (2966ds/598Mi)
% 73.64/11.22 % (2851625)Instruction limit reached!
% 73.64/11.22 % (2851625)------------------------------
% 73.64/11.22 % (2851625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.64/11.22 % (2851625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.64/11.22 % (2851625)CaDiCaL version: 2.1.3
% 73.64/11.22 % (2851625)Termination reason: Instruction limit
% 73.64/11.22 % (2851625)Termination phase: Saturation
% 73.64/11.22 % (2851625)Time elapsed: 0.209 s
% 73.64/11.22 % (2851625)Peak memory usage: 94 MB
% 73.64/11.22 % (2851625)Instructions burned: 601 (million)
% 73.64/11.22 % (2851627)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=167856109:i=2989:sd=3:ss=axioms:sgt=60_2962 on theBenchmark for (2962ds/2989Mi)
% 73.64/11.22 % (2851596)Instruction limit reached!
% 73.64/11.22 % (2851596)------------------------------
% 73.64/11.22 % (2851596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.64/11.22 % (2851596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.64/11.22 % (2851596)CaDiCaL version: 2.1.3
% 73.64/11.22 % (2851596)Termination reason: Instruction limit
% 73.64/11.22 % (2851596)Termination phase: Saturation
% 73.64/11.22 % (2851596)Time elapsed: 3.141 s
% 73.64/11.22 % (2851596)Peak memory usage: 151 MB
% 73.64/11.22 % (2851596)Instructions burned: 5208 (million)
% 73.64/11.22 % (2851629)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2402383664:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2960 on theBenchmark for (2960ds/1997Mi)
% 73.64/11.22 % (2851627)Instruction limit reached!
% 73.64/11.22 % (2851627)------------------------------
% 95.53/14.39 % (2851627)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851627)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851627)Termination reason: Instruction limit
% 95.53/14.39 % (2851627)Termination phase: Saturation
% 95.53/14.39 % (2851627)Time elapsed: 0.983 s
% 95.53/14.39 % (2851627)Peak memory usage: 145 MB
% 95.53/14.39 % (2851627)Instructions burned: 2991 (million)
% 95.53/14.39 % (2851631)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1227785736:i=2088:bd=preordered:av=off_2952 on theBenchmark for (2952ds/2088Mi)
% 95.53/14.39 % (2851629)Instruction limit reached!
% 95.53/14.39 % (2851629)------------------------------
% 95.53/14.39 % (2851629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851629)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851629)Termination reason: Instruction limit
% 95.53/14.39 % (2851629)Termination phase: Saturation
% 95.53/14.39 % (2851629)Time elapsed: 1.297 s
% 95.53/14.39 % (2851629)Peak memory usage: 138 MB
% 95.53/14.39 % (2851629)Instructions burned: 1998 (million)
% 95.53/14.39 % (2851633)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3347642255:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi)
% 95.53/14.39 % (2851631)Instruction limit reached!
% 95.53/14.39 % (2851631)------------------------------
% 95.53/14.39 % (2851631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851631)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851631)Termination reason: Instruction limit
% 95.53/14.39 % (2851631)Termination phase: Saturation
% 95.53/14.39 % (2851631)Time elapsed: 0.699 s
% 95.53/14.39 % (2851631)Peak memory usage: 140 MB
% 95.53/14.39 % (2851631)Instructions burned: 2089 (million)
% 95.53/14.39 % (2851635)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1192202900:i=433:bd=preordered_2944 on theBenchmark for (2944ds/433Mi)
% 95.53/14.39 % (2851635)Instruction limit reached!
% 95.53/14.39 % (2851635)------------------------------
% 95.53/14.39 % (2851635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851635)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851635)Termination reason: Instruction limit
% 95.53/14.39 % (2851635)Termination phase: Saturation
% 95.53/14.39 % (2851635)Time elapsed: 0.148 s
% 95.53/14.39 % (2851635)Peak memory usage: 95 MB
% 95.53/14.39 % (2851635)Instructions burned: 436 (million)
% 95.53/14.39 % (2851637)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3853862230:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2941 on theBenchmark for (2941ds/2942Mi)
% 95.53/14.39 % (2851633)Instruction limit reached!
% 95.53/14.39 % (2851633)------------------------------
% 95.53/14.39 % (2851633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851633)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851633)Termination reason: Instruction limit
% 95.53/14.39 % (2851633)Termination phase: Saturation
% 95.53/14.39 % (2851633)Time elapsed: 0.698 s
% 95.53/14.39 % (2851633)Peak memory usage: 100 MB
% 95.53/14.39 % (2851633)Instructions burned: 1099 (million)
% 95.53/14.39 % (2851639)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1541136592:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2937 on theBenchmark for (2937ds/6922Mi)
% 95.53/14.39 % (2851637)Instruction limit reached!
% 95.53/14.39 % (2851637)------------------------------
% 95.53/14.39 % (2851637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.53/14.39 % (2851637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.53/14.39 % (2851637)CaDiCaL version: 2.1.3
% 95.53/14.39 % (2851637)Termination reason: Instruction limit
% 95.53/14.39 % (2851637)Termination phase: Saturation
% 95.53/14.39 % (2851637)Time elapsed: 0.995 s
% 95.53/14.39 % (2851637)Peak memory usage: 145 MB
% 95.53/14.39 % (2851637)Instructions burned: 2945 (million)
% 112.77/16.90 % (2851641)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=709835756:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi)
% 112.77/16.90 % (2851619)Instruction limit reached!
% 112.77/16.90 % (2851619)------------------------------
% 112.77/16.90 % (2851619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.77/16.90 % (2851619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.77/16.90 % (2851619)CaDiCaL version: 2.1.3
% 112.77/16.90 % (2851619)Termination reason: Instruction limit
% 112.77/16.90 % (2851619)Termination phase: Saturation
% 112.77/16.90 % (2851619)Time elapsed: 4.550 s
% 112.77/16.90 % (2851619)Peak memory usage: 187 MB
% 112.77/16.90 % (2851619)Instructions burned: 8478 (million)
% 112.77/16.90 % (2851641)Instruction limit reached!
% 112.77/16.90 % (2851641)------------------------------
% 112.77/16.90 % (2851641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.77/16.90 % (2851641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.77/16.90 % (2851641)CaDiCaL version: 2.1.3
% 112.77/16.90 % (2851641)Termination reason: Instruction limit
% 112.77/16.90 % (2851641)Termination phase: Saturation
% 112.77/16.90 % (2851641)Time elapsed: 0.190 s
% 112.77/16.90 % (2851641)Peak memory usage: 95 MB
% 112.77/16.90 % (2851641)Instructions burned: 596 (million)
% 112.77/16.90 % (2851644)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3574967832:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2928 on theBenchmark for (2928ds/16411Mi)
% 112.77/16.90 % (2851643)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=588207586:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2928 on theBenchmark for (2928ds/4123Mi)
% 112.77/16.90 % (2851615)Instruction limit reached!
% 112.77/16.90 % (2851615)------------------------------
% 112.77/16.90 % (2851615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.77/16.90 % (2851615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.77/16.90 % (2851615)CaDiCaL version: 2.1.3
% 112.77/16.90 % (2851615)Termination reason: Instruction limit
% 112.77/16.90 % (2851615)Termination phase: Saturation
% 112.77/16.90 % (2851615)Time elapsed: 6.165 s
% 112.77/16.90 % (2851615)Peak memory usage: 173 MB
% 112.77/16.90 % (2851615)Instructions burned: 10308 (million)
% 112.77/16.90 % (2851647)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=126209575:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2919 on theBenchmark for (2919ds/1670Mi)
% 112.77/16.90 % (2851647)Instruction limit reached!
% 112.77/16.90 % (2851647)------------------------------
% 112.77/16.90 % (2851647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.77/16.90 % (2851647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.77/16.90 % (2851647)CaDiCaL version: 2.1.3
% 112.77/16.90 % (2851647)Termination reason: Instruction limit
% 112.77/16.90 % (2851647)Termination phase: Saturation
% 112.77/16.90 % (2851647)Time elapsed: 1.037 s
% 112.77/16.90 % (2851647)Peak memory usage: 137 MB
% 112.77/16.90 % (2851647)Instructions burned: 1670 (million)
% 112.77/16.90 % (2851649)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3145778359:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2908 on theBenchmark for (2908ds/1722Mi)
% 112.77/16.90 % (2851643)Instruction limit reached!
% 112.77/16.90 % (2851643)------------------------------
% 112.77/16.90 % (2851643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.77/16.90 % (2851643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.77/16.90 % (2851643)CaDiCaL version: 2.1.3
% 112.77/16.90 % (2851643)Termination reason: Instruction limit
% 112.77/16.90 % (2851643)Termination phase: Saturation
% 112.77/16.90 % (2851643)Time elapsed: 2.485 s
% 112.77/16.90 % (2851643)Peak memory usage: 159 MB
% 112.77/16.90 % (2851643)Instructions burned: 4124 (million)
% 112.77/16.90 % (2851651)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=642753271:cts=off:cond=on:i=9530:bs=on:fsd=on_2902 on theBenchmark for (2902ds/9530Mi)
% 112.77/16.90 % (2851649)Instruction limit reached!
% 112.77/16.90 % (2851649)------------------------------
% 136.26/20.11 % (2851649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851649)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851649)Termination reason: Instruction limit
% 136.26/20.11 % (2851649)Termination phase: Saturation
% 136.26/20.11 % (2851649)Time elapsed: 1.057 s
% 136.26/20.11 % (2851649)Peak memory usage: 137 MB
% 136.26/20.11 % (2851649)Instructions burned: 1722 (million)
% 136.26/20.11 % (2851639)Instruction limit reached!
% 136.26/20.11 % (2851639)------------------------------
% 136.26/20.11 % (2851639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851639)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851639)Termination reason: Instruction limit
% 136.26/20.11 % (2851639)Termination phase: Saturation
% 136.26/20.11 % (2851639)Time elapsed: 4.051 s
% 136.26/20.11 % (2851639)Peak memory usage: 179 MB
% 136.26/20.11 % (2851639)Instructions burned: 6924 (million)
% 136.26/20.11 % (2851653)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=857662066:st=2:i=4495:sd=10:ss=included_2896 on theBenchmark for (2896ds/4495Mi)
% 136.26/20.11 % (2851654)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3125082721:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 136.26/20.11 % (2851644)Instruction limit reached!
% 136.26/20.11 % (2851644)------------------------------
% 136.26/20.11 % (2851644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851644)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851644)Termination reason: Instruction limit
% 136.26/20.11 % (2851644)Termination phase: Saturation
% 136.26/20.11 % (2851644)Time elapsed: 5.256 s
% 136.26/20.11 % (2851644)Peak memory usage: 245 MB
% 136.26/20.11 % (2851644)Instructions burned: 16414 (million)
% 136.26/20.11 % (2851657)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1921364664:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2874 on theBenchmark for (2874ds/2083Mi)
% 136.26/20.11 % (2851653)Instruction limit reached!
% 136.26/20.11 % (2851653)------------------------------
% 136.26/20.11 % (2851653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851653)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851653)Termination reason: Instruction limit
% 136.26/20.11 % (2851653)Termination phase: Saturation
% 136.26/20.11 % (2851653)Time elapsed: 2.620 s
% 136.26/20.11 % (2851653)Peak memory usage: 160 MB
% 136.26/20.11 % (2851653)Instructions burned: 4496 (million)
% 136.26/20.11 % (2851659)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1750100536:i=4629:av=off:gsp=on_2868 on theBenchmark for (2868ds/4629Mi)
% 136.26/20.11 % (2851657)Instruction limit reached!
% 136.26/20.11 % (2851657)------------------------------
% 136.26/20.11 % (2851657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851657)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851657)Termination reason: Instruction limit
% 136.26/20.11 % (2851657)Termination phase: Saturation
% 136.26/20.11 % (2851657)Time elapsed: 0.708 s
% 136.26/20.11 % (2851657)Peak memory usage: 139 MB
% 136.26/20.11 % (2851657)Instructions burned: 2085 (million)
% 136.26/20.11 % (2851661)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1930754366:i=1258:av=off_2866 on theBenchmark for (2866ds/1258Mi)
% 136.26/20.11 % (2851654)Instruction limit reached!
% 136.26/20.11 % (2851654)------------------------------
% 136.26/20.11 % (2851654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.26/20.11 % (2851654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.26/20.11 % (2851654)CaDiCaL version: 2.1.3
% 136.26/20.11 % (2851654)Termination reason: Instruction limit
% 136.26/20.11 % (2851654)Termination phase: Saturation
% 136.26/20.11 % (2851654)Time elapsed: 2.990 s
% 136.26/20.11 % (2851654)Peak memory usage: 162 MB
% 136.26/20.11 % (2851654)Instructions burned: 4920 (million)
% 153.78/22.65 % (2851663)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4186482209:i=7343:av=off:ss=included_2864 on theBenchmark for (2864ds/7343Mi)
% 153.78/22.65 % (2851661)Instruction limit reached!
% 153.78/22.65 % (2851661)------------------------------
% 153.78/22.65 % (2851661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851661)CaDiCaL version: 2.1.3
% 153.78/22.65 % (2851661)Termination reason: Instruction limit
% 153.78/22.65 % (2851661)Termination phase: Saturation
% 153.78/22.65 % (2851661)Time elapsed: 0.372 s
% 153.78/22.65 % (2851661)Peak memory usage: 94 MB
% 153.78/22.65 % (2851661)Instructions burned: 1260 (million)
% 153.78/22.65 % (2851665)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1585850225:i=1325:sd=2:ss=axioms:sgt=16_2861 on theBenchmark for (2861ds/1325Mi)
% 153.78/22.65 % (2851665)Instruction limit reached!
% 153.78/22.65 % (2851665)------------------------------
% 153.78/22.65 % (2851665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851665)CaDiCaL version: 2.1.3
% 153.78/22.65 % (2851665)Termination reason: Instruction limit
% 153.78/22.65 % (2851665)Termination phase: Saturation
% 153.78/22.65 % (2851665)Time elapsed: 0.410 s
% 153.78/22.65 % (2851665)Peak memory usage: 97 MB
% 153.78/22.65 % (2851665)Instructions burned: 1327 (million)
% 153.78/22.65 % (2851667)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=77812821:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2856 on theBenchmark for (2856ds/2646Mi)
% 153.78/22.65 % (2851667)Instruction limit reached!
% 153.78/22.65 % (2851667)------------------------------
% 153.78/22.65 % (2851667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851667)CaDiCaL version: 2.1.3
% 153.78/22.65 % (2851667)Termination reason: Instruction limit
% 153.78/22.65 % (2851667)Termination phase: Saturation
% 153.78/22.65 % (2851667)Time elapsed: 1.024 s
% 153.78/22.65 % (2851667)Peak memory usage: 142 MB
% 153.78/22.65 % (2851667)Instructions burned: 2650 (million)
% 153.78/22.65 % (2851651)Instruction limit reached!
% 153.78/22.65 % (2851651)------------------------------
% 153.78/22.65 % (2851651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851651)CaDiCaL version: 2.1.3
% 153.78/22.65 % (2851651)Termination reason: Instruction limit
% 153.78/22.65 % (2851651)Termination phase: Saturation
% 153.78/22.65 % (2851651)Time elapsed: 5.614 s
% 153.78/22.65 % (2851651)Peak memory usage: 163 MB
% 153.78/22.65 % (2851651)Instructions burned: 9531 (million)
% 153.78/22.65 % (2851669)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3058907175:i=1489:sd=2:ep=R:ss=axioms_2845 on theBenchmark for (2845ds/1489Mi)
% 153.78/22.65 % (2851671)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2917917114:i=1503_2844 on theBenchmark for (2844ds/1503Mi)
% 153.78/22.65 % (2851659)Instruction limit reached!
% 153.78/22.65 % (2851659)------------------------------
% 153.78/22.65 % (2851659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851659)CaDiCaL version: 2.1.3
% 153.78/22.65 % (2851659)Termination reason: Instruction limit
% 153.78/22.65 % (2851659)Termination phase: Saturation
% 153.78/22.65 % (2851659)Time elapsed: 2.637 s
% 153.78/22.65 % (2851659)Peak memory usage: 149 MB
% 153.78/22.65 % (2851659)Instructions burned: 4630 (million)
% 153.78/22.65 % (2851673)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=4067696795:i=13942:kws=frequency_2840 on theBenchmark for (2840ds/13942Mi)
% 153.78/22.65 % (2851669)Instruction limit reached!
% 153.78/22.65 % (2851669)------------------------------
% 153.78/22.65 % (2851669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.78/22.65 % (2851669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.78/22.65 % (2851669)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851669)Termination reason: Instruction limit
% 176.73/25.86 % (2851669)Termination phase: Saturation
% 176.73/25.86 % (2851669)Time elapsed: 0.549 s
% 176.73/25.86 % (2851669)Peak memory usage: 131 MB
% 176.73/25.86 % (2851669)Instructions burned: 1492 (million)
% 176.73/25.86 % (2851675)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=1882124605:i=3604:fsr=off:er=filter_2839 on theBenchmark for (2839ds/3604Mi)
% 176.73/25.86 % (2851671)Instruction limit reached!
% 176.73/25.86 % (2851671)------------------------------
% 176.73/25.86 % (2851671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.73/25.86 % (2851671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.73/25.86 % (2851671)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851671)Termination reason: Instruction limit
% 176.73/25.86 % (2851671)Termination phase: Saturation
% 176.73/25.86 % (2851671)Time elapsed: 0.906 s
% 176.73/25.86 % (2851671)Peak memory usage: 136 MB
% 176.73/25.86 % (2851671)Instructions burned: 1504 (million)
% 176.73/25.86 % (2851677)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2451237884:i=1876:sd=1:ss=included:sgt=32_2834 on theBenchmark for (2834ds/1876Mi)
% 176.73/25.86 % (2851677)Instruction limit reached!
% 176.73/25.86 % (2851677)------------------------------
% 176.73/25.86 % (2851677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.73/25.86 % (2851677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.73/25.86 % (2851677)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851677)Termination reason: Instruction limit
% 176.73/25.86 % (2851677)Termination phase: Saturation
% 176.73/25.86 % (2851677)Time elapsed: 1.143 s
% 176.73/25.86 % (2851677)Peak memory usage: 138 MB
% 176.73/25.86 % (2851677)Instructions burned: 1877 (million)
% 176.73/25.86 % (2851663)Instruction limit reached!
% 176.73/25.86 % (2851663)------------------------------
% 176.73/25.86 % (2851663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.73/25.86 % (2851663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.73/25.86 % (2851663)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851663)Termination reason: Instruction limit
% 176.73/25.86 % (2851663)Termination phase: Saturation
% 176.73/25.86 % (2851663)Time elapsed: 4.250 s
% 176.73/25.86 % (2851663)Peak memory usage: 183 MB
% 176.73/25.86 % (2851663)Instructions burned: 7343 (million)
% 176.73/25.86 % (2851679)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3966154170:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2821 on theBenchmark for (2821ds/1932Mi)
% 176.73/25.86 % (2851680)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=4074863235:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2820 on theBenchmark for (2820ds/1980Mi)
% 176.73/25.86 % (2851675)Instruction limit reached!
% 176.73/25.86 % (2851675)------------------------------
% 176.73/25.86 % (2851675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.73/25.86 % (2851675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.73/25.86 % (2851675)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851675)Termination reason: Instruction limit
% 176.73/25.86 % (2851675)Termination phase: Saturation
% 176.73/25.86 % (2851675)Time elapsed: 1.952 s
% 176.73/25.86 % (2851675)Peak memory usage: 147 MB
% 176.73/25.86 % (2851675)Instructions burned: 3606 (million)
% 176.73/25.86 % (2851683)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1361891335:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2818 on theBenchmark for (2818ds/3902Mi)
% 176.73/25.86 % (2851679)Instruction limit reached!
% 176.73/25.86 % (2851679)------------------------------
% 176.73/25.86 % (2851679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.73/25.86 % (2851679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.73/25.86 % (2851679)CaDiCaL version: 2.1.3
% 176.73/25.86 % (2851679)Termination reason: Instruction limit
% 176.73/25.86 % (2851679)Termination phase: Saturation
% 176.73/25.86 % (2851679)Time elapsed: 1.169 s
% 176.73/25.86 % (2851679)Peak memory usage: 137 MB
% 176.73/25.86 % (2851679)Instructions burned: 1933 (million)
% 176.73/25.86 % (2851685)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2055794487:avsq=on:i=3916:aac=none:amm=off_2808 on theBenchmark for (2808ds/3916Mi)
% 153.96/26.20 % (2851680)Instruction limit reached!
% 153.96/26.20 % (2851680)------------------------------
% 153.96/26.20 % (2851680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851680)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851680)Termination reason: Instruction limit
% 153.96/26.20 % (2851680)Termination phase: Saturation
% 153.96/26.20 % (2851680)Time elapsed: 1.257 s
% 153.96/26.20 % (2851680)Peak memory usage: 138 MB
% 153.96/26.20 % (2851680)Instructions burned: 1981 (million)
% 153.96/26.20 % (2851687)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3480711725:cond=on:i=3940:av=off:er=known_2806 on theBenchmark for (2806ds/3940Mi)
% 153.96/26.20 % (2851683)Instruction limit reached!
% 153.96/26.20 % (2851683)------------------------------
% 153.96/26.20 % (2851683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851683)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851683)Termination reason: Instruction limit
% 153.96/26.20 % (2851683)Termination phase: Saturation
% 153.96/26.20 % (2851683)Time elapsed: 2.204 s
% 153.96/26.20 % (2851683)Peak memory usage: 150 MB
% 153.96/26.20 % (2851683)Instructions burned: 3903 (million)
% 153.96/26.20 % (2851673)Instruction limit reached!
% 153.96/26.20 % (2851673)------------------------------
% 153.96/26.20 % (2851673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851673)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851673)Termination reason: Instruction limit
% 153.96/26.20 % (2851673)Termination phase: Saturation
% 153.96/26.20 % (2851673)Time elapsed: 4.462 s
% 153.96/26.20 % (2851673)Peak memory usage: 236 MB
% 153.96/26.20 % (2851673)Instructions burned: 13946 (million)
% 153.96/26.20 % (2851690)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1305698321:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2795 on theBenchmark for (2795ds/2087Mi)
% 153.96/26.20 % (2851689)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2515114004:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2795 on theBenchmark for (2795ds/3980Mi)
% 153.96/26.20 % (2851690)Instruction limit reached!
% 153.96/26.20 % (2851690)------------------------------
% 153.96/26.20 % (2851690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851690)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851690)Termination reason: Instruction limit
% 153.96/26.20 % (2851690)Termination phase: Saturation
% 153.96/26.20 % (2851690)Time elapsed: 0.762 s
% 153.96/26.20 % (2851690)Peak memory usage: 140 MB
% 153.96/26.20 % (2851690)Instructions burned: 2087 (million)
% 153.96/26.20 % (2851685)Instruction limit reached!
% 153.96/26.20 % (2851685)------------------------------
% 153.96/26.20 % (2851685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851685)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851685)Termination reason: Instruction limit
% 153.96/26.20 % (2851685)Termination phase: Saturation
% 153.96/26.20 % (2851685)Time elapsed: 2.166 s
% 153.96/26.20 % (2851685)Peak memory usage: 121 MB
% 153.96/26.20 % (2851685)Instructions burned: 3917 (million)
% 153.96/26.20 % (2851693)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3904840670:cts=off:cond=on:i=4272:bs=on:fsd=on_2786 on theBenchmark for (2786ds/4272Mi)
% 153.96/26.20 % (2851694)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1915961945:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2785 on theBenchmark for (2785ds/2197Mi)
% 153.96/26.20 % (2851687)Instruction limit reached!
% 153.96/26.20 % (2851687)------------------------------
% 153.96/26.20 % (2851687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851687)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851687)Termination reason: Instruction limit
% 153.96/26.20 % (2851687)Termination phase: Saturation
% 153.96/26.20 % (2851687)Time elapsed: 2.336 s
% 153.96/26.20 % (2851687)Peak memory usage: 151 MB
% 153.96/26.20 % (2851687)Instructions burned: 3940 (million)
% 153.96/26.20 % (2851697)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1819976674:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2781 on theBenchmark for (2781ds/6508Mi)
% 153.96/26.20 % (2851689)Instruction limit reached!
% 153.96/26.20 % (2851689)------------------------------
% 153.96/26.20 % (2851689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851689)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851689)Termination reason: Instruction limit
% 153.96/26.20 % (2851689)Termination phase: Saturation
% 153.96/26.20 % (2851689)Time elapsed: 2.354 s
% 153.96/26.20 % (2851689)Peak memory usage: 156 MB
% 153.96/26.20 % (2851689)Instructions burned: 3980 (million)
% 153.96/26.20 % (2851694)Instruction limit reached!
% 153.96/26.20 % (2851694)------------------------------
% 153.96/26.20 % (2851694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851694)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851694)Termination reason: Instruction limit
% 153.96/26.20 % (2851694)Termination phase: Saturation
% 153.96/26.20 % (2851694)Time elapsed: 1.372 s
% 153.96/26.20 % (2851694)Peak memory usage: 141 MB
% 153.96/26.20 % (2851694)Instructions burned: 2198 (million)
% 153.96/26.20 % (2851693)Instruction limit reached!
% 153.96/26.20 % (2851693)------------------------------
% 153.96/26.20 % (2851693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851693)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851693)Termination reason: Instruction limit
% 153.96/26.20 % (2851693)Termination phase: Saturation
% 153.96/26.20 % (2851693)Time elapsed: 1.500 s
% 153.96/26.20 % (2851693)Peak memory usage: 153 MB
% 153.96/26.20 % (2851693)Instructions burned: 4275 (million)
% 153.96/26.20 % (2851701)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=1029972106:i=2693:kws=precedence:ins=1:av=off_2770 on theBenchmark for (2770ds/2693Mi)
% 153.96/26.20 % (2851699)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=581061812:i=2330:fgj=on:av=off:fsr=off_2770 on theBenchmark for (2770ds/2330Mi)
% 153.96/26.20 % (2851700)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2398538678:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2770 on theBenchmark for (2770ds/7592Mi)
% 153.96/26.20 % (2851701)Instruction limit reached!
% 153.96/26.20 % (2851701)------------------------------
% 153.96/26.20 % (2851701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851701)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851701)Termination reason: Instruction limit
% 153.96/26.20 % (2851701)Termination phase: Saturation
% 153.96/26.20 % (2851701)Time elapsed: 0.928 s
% 153.96/26.20 % (2851701)Peak memory usage: 148 MB
% 153.96/26.20 % (2851701)Instructions burned: 2693 (million)
% 153.96/26.20 % (2851705)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=403159757:i=28651:sd=4:ss=included:sgt=64_2760 on theBenchmark for (2760ds/28651Mi)
% 153.96/26.20 % (2851699)Instruction limit reached!
% 153.96/26.20 % (2851699)------------------------------
% 153.96/26.20 % (2851699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 153.96/26.20 % (2851699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 153.96/26.20 % (2851699)CaDiCaL version: 2.1.3
% 153.96/26.20 % (2851699)Termination reason: Instruction limit
% 153.96/26.20 % (2851699)Termination phase: Saturation
% 153.96/26.20 % (2851699)Time elapsed: 1.432 s
% 153.96/26.20 % (2851699)Peak memory usage: 140 MB
% 153.96/26.20 % (2851699)Instructions burned: 2330 (million)
% 153.96/26.20 % (2851707)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3351193718:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2754 on theBenchmark for (2754ds/2700Mi)
% 153.96/26.20 % (2851565)First to succeed.
% 153.96/26.20 % (2851565)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2851558"
% 153.96/26.20 % (2851565)Refutation found. Thanks to Tanya!
% 153.96/26.20 % SZS status Unsatisfiable for theBenchmark
% 153.96/26.20 % SZS output start Proof for theBenchmark
% See solution above
% 179.89/26.40 % (2851565)------------------------------
% 179.89/26.40 % (2851565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.89/26.40 % (2851565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.89/26.40 % (2851565)CaDiCaL version: 2.1.3
% 179.89/26.40 % (2851565)Termination reason: Refutation
% 179.89/26.40 % (2851565)Time elapsed: 24.857 s
% 179.89/26.40 % (2851565)Peak memory usage: 324 MB
% 179.89/26.40 % (2851565)Instructions burned: 37406 (million)
% 179.89/26.40 % (2851565)------------------------------
% 179.89/26.40 % (2851565)------------------------------
% 179.89/26.40 % (2851558)Success in time 25.348 s
% 179.89/26.40 % Vampire exiting
%------------------------------------------------------------------------------