%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT124+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:58 PM UTC 2026
% Result : Theorem 107.85s 28.66s
% Output : Refutation 197.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 57
% Syntax : Number of formulae : 375 ( 62 unt; 37 def)
% Number of atoms : 1029 ( 66 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1162 ( 508 ~; 566 |; 28 &)
% ( 42 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 42 ( 40 usr; 38 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 6 con; 0-5 aty)
% Number of variables : 751 ( 0 sgn 732 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
<=> ! [X2] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf))
=> hAPP(X1,X2) = hAPP(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_dictator__def) ).
fof(f5,axiom,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_assms_I1_J) ).
fof(f7,axiom,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,c_COMBK(tc_fun(X4,tc_HOL_Obool),X5,X1))))
=> ( hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
=> hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_funcset__mem) ).
fof(f8,axiom,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,X1)))
=> ( hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
=> hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),hAPP(X1,X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Pi__mem) ).
fof(f12,axiom,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin))))
=> ( ! [X2] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf))
=> ! [X3,X4] :
( X3 != X4
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X2,X0)))
=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X1,X2))) ) ) )
=> c_Arrow__Order__Mirabelle_Odictator(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_dictatorI) ).
fof(f13,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
<=> hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mem__def) ).
fof(f16,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin))
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X0)),X2))
=> ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Lin__irrefl) ).
fof(f37,axiom,
! [X0,X1,X2,X3,X4] :
( ! [X5] :
( hBOOL(hAPP(hAPP(c_member(X4),X5),X3))
=> hBOOL(hAPP(hAPP(c_member(X2),hAPP(X1,X5)),X0)) )
=> hBOOL(hAPP(hAPP(c_member(tc_fun(X4,X2)),X1),c_FuncSet_OPi(X4,X2,X3,c_COMBK(tc_fun(X2,tc_HOL_Obool),X4,X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_funcsetI) ).
fof(f59,axiom,
! [X0,X1,X2] :
( ! [X3] : hBOOL(hAPP(X2,X3))
<=> ! [X4,X5] : hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X4),X5))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_split__paired__All) ).
fof(f89,axiom,
c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Prof__def) ).
fof(f91,axiom,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_top1I) ).
fof(f94,axiom,
! [X0,X1,X2] : c_FuncSet_OPi(X2,X1,X0,c_COMBK(tc_fun(X1,tc_HOL_Obool),X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X1),tc_HOL_Obool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Pi__UNIV) ).
fof(f107,axiom,
! [X0,X1] : hBOOL(hAPP(hAPP(c_member(X1),X0),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_iso__tuple__UNIV__I) ).
fof(f156,axiom,
! [X0,X1,X2] :
( X2 = X1
<=> ( c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
& c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_set__eq__subset) ).
fof(f161,axiom,
! [X0,X1] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_subset__refl) ).
fof(f170,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X2),X1))
=> ( c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1,X0)
=> hBOOL(hAPP(hAPP(c_member(X3),X2),X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_set__rev__mp) ).
fof(f175,axiom,
! [X0,X1] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_subset__UNIV) ).
fof(f264,axiom,
! [X0,X1,X2,X3] :
( ! [X4,X5] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),X4),X5)),X1))
=> hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),X4),X5)),X0)) )
=> c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X2),tc_HOL_Obool),X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_subrelI) ).
fof(f520,axiom,
! [X0,X1,X2,X3] : hAPP(c_COMBK(X3,X2,X1),X0) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBK__1) ).
fof(f529,conjecture,
? [X0] : c_Arrow__Order__Mirabelle_Odictator(v_F,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f530,negated_conjecture,
~ ? [X0] : c_Arrow__Order__Mirabelle_Odictator(v_F,X0),
inference(negated_conjecture,[status(cth)],[f529]) ).
fof(f531,plain,
! [X0] : ~ c_Arrow__Order__Mirabelle_Odictator(v_F,X0),
inference(ennf_transformation,[],[f530]) ).
fof(f532,plain,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ? [X2] :
( ? [X3,X4] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X1,X2)))
& hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X2,X0)))
& X3 != X4 )
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) )
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))) ),
inference(ennf_transformation,[],[f12]) ).
fof(f533,plain,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ? [X2] :
( ? [X3,X4] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X1,X2)))
& hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X4)),hAPP(X2,X0)))
& X3 != X4 )
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) )
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))) ),
inference(flattening,[],[f532]) ).
fof(f534,plain,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
<=> ! [X2] :
( hAPP(X1,X2) = hAPP(X2,X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f543,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X0)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f544,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X0)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin)) ),
inference(flattening,[],[f543]) ).
fof(f551,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X4,X2)),X1),c_FuncSet_OPi(X4,X2,X3,c_COMBK(tc_fun(X2,tc_HOL_Obool),X4,X0))))
| ? [X5] :
( ~ hBOOL(hAPP(hAPP(c_member(X2),hAPP(X1,X5)),X0))
& hBOOL(hAPP(hAPP(c_member(X4),X5),X3)) ) ),
inference(ennf_transformation,[],[f37]) ).
fof(f553,plain,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),hAPP(X1,X0)))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,X1))) ),
inference(ennf_transformation,[],[f8]) ).
fof(f554,plain,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),hAPP(X1,X0)))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,X1))) ),
inference(flattening,[],[f553]) ).
fof(f555,plain,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),X1))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,c_COMBK(tc_fun(X4,tc_HOL_Obool),X5,X1)))) ),
inference(ennf_transformation,[],[f7]) ).
fof(f556,plain,
! [X0,X1,X2,X3,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),X1))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,c_COMBK(tc_fun(X4,tc_HOL_Obool),X5,X1)))) ),
inference(flattening,[],[f555]) ).
fof(f561,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X2),tc_HOL_Obool),X1,X0)
| ? [X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),X4),X5)),X0))
& hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),X4),X5)),X1)) ) ),
inference(ennf_transformation,[],[f264]) ).
fof(f568,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X2),X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1,X0)
| ~ hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(ennf_transformation,[],[f170]) ).
fof(f569,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X2),X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1,X0)
| ~ hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(flattening,[],[f568]) ).
fof(f585,plain,
! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK1(X0,X1)),sK2(X0,X1))),hAPP(X1,sK0(X0,X1))))
& hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK1(X0,X1)),sK2(X0,X1))),hAPP(sK0(X0,X1),X0)))
& sK1(X0,X1) != sK2(X0,X1)
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK0(X0,X1)),c_Arrow__Order__Mirabelle_OProf)) )
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X2,sK0(X0,X1)),skolemize(X3,sK1(X0,X1)),skolemize(X4,sK2(X0,X1))],[f533]) ).
fof(f586,plain,
! [X0,X1] :
( ( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ? [X2] :
( hAPP(X1,X2) != hAPP(X2,X0)
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) ) )
& ( ! [X2] :
( hAPP(X1,X2) = hAPP(X2,X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) )
| ~ c_Arrow__Order__Mirabelle_Odictator(X1,X0) ) ),
inference(nnf_transformation,[],[f534]) ).
fof(f587,plain,
! [X0,X1] :
( ( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ? [X2] :
( hAPP(X1,X2) != hAPP(X2,X0)
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X2),c_Arrow__Order__Mirabelle_OProf)) ) )
& ( ! [X3] :
( hAPP(X3,X0) = hAPP(X1,X3)
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X3),c_Arrow__Order__Mirabelle_OProf)) )
| ~ c_Arrow__Order__Mirabelle_Odictator(X1,X0) ) ),
inference(rectify,[],[f586]) ).
fof(f588,plain,
! [X0,X1] :
( ( c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ( hAPP(X1,sK3(X0,X1)) != hAPP(sK3(X0,X1),X0)
& hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK3(X0,X1)),c_Arrow__Order__Mirabelle_OProf)) ) )
& ( ! [X3] :
( hAPP(X3,X0) = hAPP(X1,X3)
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X3),c_Arrow__Order__Mirabelle_OProf)) )
| ~ c_Arrow__Order__Mirabelle_Odictator(X1,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f587]) ).
fof(f591,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) )
& ( hBOOL(hAPP(X0,X1))
| ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0)) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f599,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X4,X2)),X1),c_FuncSet_OPi(X4,X2,X3,c_COMBK(tc_fun(X2,tc_HOL_Obool),X4,X0))))
| ( ~ hBOOL(hAPP(hAPP(c_member(X2),hAPP(X1,sK9(X0,X1,X2,X3,X4))),X0))
& hBOOL(hAPP(hAPP(c_member(X4),sK9(X0,X1,X2,X3,X4)),X3)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X5,sK9(X0,X1,X2,X3,X4))],[f551]) ).
fof(f604,plain,
! [X0,X1,X2] :
( ( ! [X3] : hBOOL(hAPP(X2,X3))
| ? [X4,X5] : ~ hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X4),X5))) )
& ( ! [X4,X5] : hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X4),X5)))
| ? [X3] : ~ hBOOL(hAPP(X2,X3)) ) ),
inference(nnf_transformation,[],[f59]) ).
fof(f605,plain,
! [X0,X1,X2] :
( ( ! [X3] : hBOOL(hAPP(X2,X3))
| ? [X4,X5] : ~ hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X4),X5))) )
& ( ! [X6,X7] : hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X6),X7)))
| ? [X8] : ~ hBOOL(hAPP(X2,X8)) ) ),
inference(rectify,[],[f604]) ).
fof(f606,plain,
! [X0,X1,X2] :
( ( ! [X3] : hBOOL(hAPP(X2,X3))
| ~ hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),sK12(X0,X1,X2)),sK13(X0,X1,X2)))) )
& ( ! [X6,X7] : hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X6),X7)))
| ~ hBOOL(hAPP(X2,sK14(X2))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X4,sK12(X0,X1,X2)),skolemize(X5,sK13(X0,X1,X2)),skolemize(X8,sK14(X2))],[f605]) ).
fof(f607,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X2),tc_HOL_Obool),X1,X0)
| ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),sK15(X0,X1,X2,X3)),sK16(X0,X1,X2,X3))),X0))
& hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),sK15(X0,X1,X2,X3)),sK16(X0,X1,X2,X3))),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X4,sK15(X0,X1,X2,X3)),skolemize(X5,sK16(X0,X1,X2,X3))],[f561]) ).
fof(f608,plain,
! [X0,X1,X2] :
( ( X2 = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
& c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) )
| X1 != X2 ) ),
inference(nnf_transformation,[],[f156]) ).
fof(f609,plain,
! [X0,X1,X2] :
( ( X2 = X1
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) )
& ( ( c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
& c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) )
| X1 != X2 ) ),
inference(flattening,[],[f608]) ).
fof(f610,plain,
! [X0] : ~ c_Arrow__Order__Mirabelle_Odictator(v_F,X0),
inference(cnf_transformation,[],[f531]) ).
fof(f611,plain,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))),
inference(cnf_transformation,[],[f5]) ).
fof(f612,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin))))
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK0(X0,X1)),c_Arrow__Order__Mirabelle_OProf))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) ),
inference(cnf_transformation,[],[f585]) ).
fof(f615,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin))))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK1(X0,X1)),sK2(X0,X1))),hAPP(X1,sK0(X0,X1))))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) ),
inference(cnf_transformation,[],[f585]) ).
fof(f616,plain,
! [X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X3),c_Arrow__Order__Mirabelle_OProf))
| hAPP(X3,X0) = hAPP(X1,X3)
| ~ c_Arrow__Order__Mirabelle_Odictator(X1,X0) ),
inference(cnf_transformation,[],[f588]) ).
fof(f617,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK3(X0,X1)),c_Arrow__Order__Mirabelle_OProf))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) ),
inference(cnf_transformation,[],[f588]) ).
fof(f618,plain,
! [X0,X1] :
( hAPP(X1,sK3(X0,X1)) != hAPP(sK3(X0,X1),X0)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) ),
inference(cnf_transformation,[],[f588]) ).
fof(f619,plain,
c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin)),
inference(cnf_transformation,[],[f89]) ).
fof(f626,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[],[f591]) ).
fof(f627,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(X2),X1),X0))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[],[f591]) ).
fof(f635,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X0)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin)) ),
inference(cnf_transformation,[],[f544]) ).
fof(f638,plain,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X3,X2,X1),X0) = X1,
inference(cnf_transformation,[],[f520]) ).
fof(f642,plain,
! [X2,X0,X1] : c_FuncSet_OPi(X2,X1,X0,c_COMBK(tc_fun(X1,tc_HOL_Obool),X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X1),tc_HOL_Obool)),
inference(cnf_transformation,[],[f94]) ).
fof(f649,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X4,X2)),X1),c_FuncSet_OPi(X4,X2,X3,c_COMBK(tc_fun(X2,tc_HOL_Obool),X4,X0))))
| hBOOL(hAPP(hAPP(c_member(X4),sK9(X0,X1,X2,X3,X4)),X3)) ),
inference(cnf_transformation,[],[f599]) ).
fof(f650,plain,
! [X2,X3,X0,X1,X4] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(X4,X2)),X1),c_FuncSet_OPi(X4,X2,X3,c_COMBK(tc_fun(X2,tc_HOL_Obool),X4,X0))))
| ~ hBOOL(hAPP(hAPP(c_member(X2),hAPP(X1,sK9(X0,X1,X2,X3,X4))),X0)) ),
inference(cnf_transformation,[],[f599]) ).
fof(f653,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,X1)))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),hAPP(X1,X0))) ),
inference(cnf_transformation,[],[f554]) ).
fof(f654,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X5,X4)),X3),c_FuncSet_OPi(X5,X4,X2,c_COMBK(tc_fun(X4,tc_HOL_Obool),X5,X1))))
| ~ hBOOL(hAPP(hAPP(c_member(X5),X0),X2))
| hBOOL(hAPP(hAPP(c_member(X4),hAPP(X3,X0)),X1)) ),
inference(cnf_transformation,[],[f556]) ).
fof(f660,plain,
! [X2,X0,X1,X6,X7] :
( hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),X6),X7)))
| ~ hBOOL(hAPP(X2,sK14(X2))) ),
inference(cnf_transformation,[],[f606]) ).
fof(f661,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X0),sK12(X0,X1,X2)),sK13(X0,X1,X2))))
| hBOOL(hAPP(X2,X3)) ),
inference(cnf_transformation,[],[f606]) ).
fof(f664,plain,
! [X0,X1] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))),
inference(cnf_transformation,[],[f175]) ).
fof(f667,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_member(X1),X0),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),
inference(cnf_transformation,[],[f107]) ).
fof(f670,plain,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X0)),
inference(cnf_transformation,[],[f91]) ).
fof(f671,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),sK15(X0,X1,X2,X3)),sK16(X0,X1,X2,X3))),X1))
| c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X2),tc_HOL_Obool),X1,X0) ),
inference(cnf_transformation,[],[f607]) ).
fof(f672,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X2)),hAPP(hAPP(c_Product__Type_OPair(X3,X2),sK15(X0,X1,X2,X3)),sK16(X0,X1,X2,X3))),X0))
| c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X2),tc_HOL_Obool),X1,X0) ),
inference(cnf_transformation,[],[f607]) ).
fof(f676,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X3),X2),X1))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1,X0)
| hBOOL(hAPP(hAPP(c_member(X3),X2),X0)) ),
inference(cnf_transformation,[],[f569]) ).
fof(f678,plain,
! [X0,X1] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X0,X0),
inference(cnf_transformation,[],[f161]) ).
fof(f681,plain,
! [X2,X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X2,X1)
| X1 = X2
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),X1,X2) ),
inference(cnf_transformation,[],[f609]) ).
fof(f714,definition,
( spl17_2
<=> c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin)) ),
introduced(definition,[new_symbols(definition,[spl17_2])],[avatar_definition]) ).
fof(f716,plain,
( c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin))
| ~ spl17_2 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f717,plain,
spl17_2,
inference(avatar_split_clause,[],[f619,f714]) ).
fof(f719,definition,
( spl17_3
<=> hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin)))) ),
introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition]) ).
fof(f721,plain,
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Arrow__Order__Mirabelle_OLin))))
| ~ spl17_3 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f722,plain,
spl17_3,
inference(avatar_split_clause,[],[f611,f719]) ).
fof(f731,plain,
( ! [X0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf))
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,X0)),c_Arrow__Order__Mirabelle_OLin)) )
| ~ spl17_3 ),
inference(resolution,[],[f654,f721]) ).
fof(f733,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP(X0,hAPP(hAPP(c_Product__Type_OPair(X1,X2),sK15(X3,X0,X2,X1)),sK16(X3,X0,X2,X1))))
| c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X1,X2),tc_HOL_Obool),X0,X3) ),
inference(resolution,[],[f626,f671]) ).
fof(f741,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(hAPP(c_Product__Type_OPair(X1,X2),sK15(X0,X3,X2,X1)),sK16(X0,X3,X2,X1))))
| c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X1,X2),tc_HOL_Obool),X3,X0) ),
inference(resolution,[],[f627,f672]) ).
fof(f744,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(c_FuncSet_OPi(X0,X1,X2,c_COMBK(tc_fun(X1,tc_HOL_Obool),X0,X3)),X4))
| ~ hBOOL(hAPP(hAPP(c_member(X0),X5),X2))
| hBOOL(hAPP(hAPP(c_member(X1),hAPP(X4,X5)),X3)) ),
inference(resolution,[],[f627,f654]) ).
fof(f755,plain,
! [X2,X3,X0,X1,X4] :
( ~ hBOOL(hAPP(hAPP(c_member(X0),hAPP(X1,sK9(X2,X1,X0,X3,X4))),X2))
| hBOOL(hAPP(c_FuncSet_OPi(X4,X0,X3,c_COMBK(tc_fun(X0,tc_HOL_Obool),X4,X2)),X1)) ),
inference(resolution,[],[f650,f626]) ).
fof(f763,plain,
( ! [X0] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK1(X0,v_F)),sK2(X0,v_F))),hAPP(v_F,sK0(X0,v_F))))
| c_Arrow__Order__Mirabelle_Odictator(v_F,X0) )
| ~ spl17_3 ),
inference(resolution,[],[f615,f721]) ).
fof(f766,plain,
( ! [X0] : ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),sK1(X0,v_F)),sK2(X0,v_F))),hAPP(v_F,sK0(X0,v_F))))
| ~ spl17_3 ),
inference(forward_subsumption_resolution,[],[f763,f610]) ).
fof(f775,plain,
! [X2,X0,X1] :
( hAPP(X2,X0) = hAPP(X0,X1)
| ~ c_Arrow__Order__Mirabelle_Odictator(X2,X1)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0)) ),
inference(resolution,[],[f616,f627]) ).
fof(f901,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK3(X1,X0)),X2))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,X2)
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) ),
inference(resolution,[],[f617,f676]) ).
fof(f1023,definition,
( spl17_21
<=> ! [X4,X2,X1] :
( ~ c_Arrow__Order__Mirabelle_Odictator(sK3(X1,X2),X4)
| c_Arrow__Order__Mirabelle_Odictator(X2,X1) ) ),
introduced(definition,[new_symbols(definition,[spl17_21])],[avatar_definition]) ).
fof(f1024,plain,
( ! [X2,X1,X4] :
( ~ c_Arrow__Order__Mirabelle_Odictator(sK3(X1,X2),X4)
| c_Arrow__Order__Mirabelle_Odictator(X2,X1) )
| ~ spl17_21 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1031,definition,
( spl17_23
<=> ! [X2,X1] : c_Arrow__Order__Mirabelle_Odictator(X2,X1) ),
introduced(definition,[new_symbols(definition,[spl17_23])],[avatar_definition]) ).
fof(f1032,plain,
( ! [X2,X1] : c_Arrow__Order__Mirabelle_Odictator(X2,X1)
| ~ spl17_23 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1037,plain,
( $false
| ~ spl17_23 ),
inference(resolution,[],[f1032,f610]) ).
fof(f1039,plain,
~ spl17_23,
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1300,definition,
( spl17_42
<=> ! [X3] : hBOOL(X3) ),
introduced(definition,[new_symbols(definition,[spl17_42])],[avatar_definition]) ).
fof(f1301,plain,
( ! [X3] : hBOOL(X3)
| ~ spl17_42 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1332,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(X1,c_COMBK(X2,X3,X0)) = X0
| ~ c_Arrow__Order__Mirabelle_Odictator(X1,X4)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_COMBK(X2,X3,X0))) ),
inference(superposition,[],[f775,f638]) ).
fof(f3016,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),c_Arrow__Order__Mirabelle_OLin)) ),
inference(resolution,[],[f667,f635]) ).
fof(f3035,plain,
~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),c_Arrow__Order__Mirabelle_OLin)),
inference(forward_subsumption_resolution,[],[f3016,f667]) ).
fof(f3037,definition,
( spl17_131
<=> hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),c_Arrow__Order__Mirabelle_OLin)) ),
introduced(definition,[new_symbols(definition,[spl17_131])],[avatar_definition]) ).
fof(f3039,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),c_Arrow__Order__Mirabelle_OLin))
| spl17_131 ),
inference(avatar_component_clause,[],[f3037]) ).
fof(f3040,plain,
~ spl17_131,
inference(avatar_split_clause,[],[f3035,f3037]) ).
fof(f3313,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X4),tc_HOL_Obool),X5,c_COMBK(X1,X2,X0))
| ~ hBOOL(X0) ),
inference(superposition,[],[f741,f638]) ).
fof(f3340,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Arrow__Order__Mirabelle_Oindi),X1),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(X0,X1)),hAPP(c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin),X1))) )
| ~ spl17_2 ),
inference(superposition,[],[f653,f716]) ).
fof(f3343,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf))
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(X0,X1)),hAPP(c_COMBK(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool),tc_Arrow__Order__Mirabelle_Oindi,c_Arrow__Order__Mirabelle_OLin),X1))) )
| ~ spl17_2 ),
inference(forward_subsumption_resolution,[],[f3340,f667]) ).
fof(f3350,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X0),c_Arrow__Order__Mirabelle_OProf))
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(X0,X1)),c_Arrow__Order__Mirabelle_OLin)) )
| ~ spl17_2 ),
inference(forward_demodulation,[],[f3343,f638]) ).
fof(f3355,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(sK3(X0,X1),X2)),c_Arrow__Order__Mirabelle_OLin))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_2 ),
inference(resolution,[],[f3350,f901]) ).
fof(f3374,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(sK3(X0,X1),X2)),c_Arrow__Order__Mirabelle_OLin))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_2 ),
inference(forward_subsumption_resolution,[],[f3355,f678]) ).
fof(f3379,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(sK3(X1,X0),X2)))
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) )
| ~ spl17_2 ),
inference(resolution,[],[f3374,f626]) ).
fof(f3535,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X4,X5),tc_HOL_Obool),c_COMBK(X0,X1,X2),X3)
| c_COMBK(X0,X1,X2) = X3
| ~ hBOOL(X2) ),
inference(resolution,[],[f681,f3313]) ).
fof(f3537,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)),X1)
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)) = X1 ),
inference(resolution,[],[f681,f664]) ).
fof(f3640,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| c_Arrow__Order__Mirabelle_Odictator(X2,X1)
| ~ c_Arrow__Order__Mirabelle_Odictator(sK3(X1,X2),X5)
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_COMBK(X3,X4,X0))) )
| ~ spl17_2 ),
inference(superposition,[],[f3379,f1332]) ).
fof(f3718,plain,
( ! [X0] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK0(X0,v_F)),c_Arrow__Order__Mirabelle_OProf))
| c_Arrow__Order__Mirabelle_Odictator(v_F,X0) )
| ~ spl17_3 ),
inference(resolution,[],[f612,f721]) ).
fof(f3751,plain,
( ! [X0] : hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),sK0(X0,v_F)),c_Arrow__Order__Mirabelle_OProf))
| ~ spl17_3 ),
inference(forward_subsumption_resolution,[],[f3718,f610]) ).
fof(f3758,plain,
( ! [X0] : hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,sK0(X0,v_F))),c_Arrow__Order__Mirabelle_OLin))
| ~ spl17_3 ),
inference(resolution,[],[f3751,f731]) ).
fof(f5795,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,sK0(X0,v_F))))
| ~ spl17_3 ),
inference(resolution,[],[f3758,f626]) ).
fof(f6097,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X3,X4),tc_HOL_Obool),c_COMBK(X1,X2,X0),X5)
| hBOOL(X0) ),
inference(superposition,[],[f733,f638]) ).
fof(f6113,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X4,X5),tc_HOL_Obool),X1,c_COMBK(X2,X3,X0))
| c_COMBK(X2,X3,X0) = X1
| hBOOL(X0) ),
inference(resolution,[],[f6097,f681]) ).
fof(f6120,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_COMBK(X0,X1,X2) = c_COMBK(X3,X4,X5)
| hBOOL(X2)
| hBOOL(X5) ),
inference(resolution,[],[f6113,f6097]) ).
fof(f6218,definition,
( spl17_180
<=> hBOOL(c_Arrow__Order__Mirabelle_OLin) ),
introduced(definition,[new_symbols(definition,[spl17_180])],[avatar_definition]) ).
fof(f6220,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OLin)
| ~ spl17_180 ),
inference(avatar_component_clause,[],[f6218]) ).
fof(f6295,definition,
( spl17_193
<=> ! [X2] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X2)) ),
introduced(definition,[new_symbols(definition,[spl17_193])],[avatar_definition]) ).
fof(f6296,plain,
( ! [X2] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X2))
| ~ spl17_193 ),
inference(avatar_component_clause,[],[f6295]) ).
fof(f6327,definition,
( spl17_196
<=> c_Arrow__Order__Mirabelle_OProf = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool)) ),
introduced(definition,[new_symbols(definition,[spl17_196])],[avatar_definition]) ).
fof(f6329,plain,
( c_Arrow__Order__Mirabelle_OProf = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool))
| ~ spl17_196 ),
inference(avatar_component_clause,[],[f6327]) ).
fof(f6442,definition,
( spl17_202
<=> ! [X6,X4,X7] : ~ hBOOL(hAPP(hAPP(c_member(X6),X4),X7)) ),
introduced(definition,[new_symbols(definition,[spl17_202])],[avatar_definition]) ).
fof(f6443,plain,
( ! [X6,X7,X4] : ~ hBOOL(hAPP(hAPP(c_member(X6),X4),X7))
| ~ spl17_202 ),
inference(avatar_component_clause,[],[f6442]) ).
fof(f6511,definition,
( spl17_220
<=> hBOOL(c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[spl17_220])],[avatar_definition]) ).
fof(f6512,plain,
( ~ hBOOL(c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)))
| spl17_220 ),
inference(avatar_component_clause,[],[f6511]) ).
fof(f6513,plain,
( hBOOL(c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)))
| ~ spl17_220 ),
inference(avatar_component_clause,[],[f6511]) ).
fof(f6519,definition,
( spl17_222
<=> ! [X3] : hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))) ),
introduced(definition,[new_symbols(definition,[spl17_222])],[avatar_definition]) ).
fof(f6520,plain,
( ! [X3] : hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))
| ~ spl17_222 ),
inference(avatar_component_clause,[],[f6519]) ).
fof(f6531,plain,
( ! [X2,X3,X0,X1,X4] : hBOOL(hAPP(hAPP(c_member(X0),sK9(X1,X2,X3,X4,X0)),X4))
| ~ spl17_202 ),
inference(resolution,[],[f6443,f649]) ).
fof(f6634,plain,
( $false
| ~ spl17_202 ),
inference(forward_subsumption_resolution,[],[f6531,f6443]) ).
fof(f6635,plain,
~ spl17_202,
inference(avatar_contradiction_clause,[],[f6634]) ).
fof(f6753,definition,
( spl17_234
<=> ! [X2,X0] :
( hBOOL(X0)
| hBOOL(hAPP(X0,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl17_234])],[avatar_definition]) ).
fof(f6754,plain,
( ! [X2,X0] :
( hBOOL(hAPP(X0,X2))
| hBOOL(X0) )
| ~ spl17_234 ),
inference(avatar_component_clause,[],[f6753]) ).
fof(f6904,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))))
| spl17_131 ),
inference(resolution,[],[f3039,f627]) ).
fof(f6910,definition,
( spl17_237
<=> hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)))) ),
introduced(definition,[new_symbols(definition,[spl17_237])],[avatar_definition]) ).
fof(f6912,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))))
| spl17_237 ),
inference(avatar_component_clause,[],[f6910]) ).
fof(f6913,plain,
( ~ spl17_237
| spl17_131 ),
inference(avatar_split_clause,[],[f6904,f3037,f6910]) ).
fof(f6954,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,sK14(X0)))
| hBOOL(hAPP(X0,X1)) ),
inference(resolution,[],[f660,f661]) ).
fof(f6955,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X1,X2),tc_HOL_Obool),X3,X0)
| ~ hBOOL(hAPP(X0,sK14(X0))) ),
inference(resolution,[],[f660,f741]) ).
fof(f7065,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin)) )
| ~ spl17_42 ),
inference(resolution,[],[f1301,f635]) ).
fof(f7113,plain,
( ! [X2,X0,X1] : ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X0),X1)),X2))
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f7065,f1301]) ).
fof(f7116,plain,
( $false
| ~ spl17_42 ),
inference(forward_subsumption_resolution,[],[f7113,f1301]) ).
fof(f7117,plain,
~ spl17_42,
inference(avatar_contradiction_clause,[],[f7116]) ).
fof(f7169,plain,
! [X2,X3,X0,X1,X4] :
( c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool)) = c_COMBK(X2,X3,X4)
| ~ hBOOL(X4) ),
inference(resolution,[],[f3537,f3313]) ).
fof(f7196,plain,
( ! [X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool)))))
| ~ hBOOL(c_Arrow__Order__Mirabelle_OLin) )
| ~ spl17_3 ),
inference(superposition,[],[f721,f7169]) ).
fof(f7197,plain,
( ! [X0,X1] :
( c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool)))
| ~ hBOOL(c_Arrow__Order__Mirabelle_OLin) )
| ~ spl17_2 ),
inference(superposition,[],[f716,f7169]) ).
fof(f7202,plain,
! [X2,X3,X0,X1,X4] :
( c_FuncSet_OPi(X2,X3,X4,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X3),tc_HOL_Obool))
| ~ hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))) ),
inference(superposition,[],[f642,f7169]) ).
fof(f7237,definition,
( spl17_243
<=> ! [X7] : ~ hBOOL(X7) ),
introduced(definition,[new_symbols(definition,[spl17_243])],[avatar_definition]) ).
fof(f7238,plain,
( ! [X7] : ~ hBOOL(X7)
| ~ spl17_243 ),
inference(avatar_component_clause,[],[f7237]) ).
fof(f7245,definition,
( spl17_245
<=> ! [X2] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin))
| ~ hBOOL(X2) ) ),
introduced(definition,[new_symbols(definition,[spl17_245])],[avatar_definition]) ).
fof(f7246,plain,
( ! [X2] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X2),c_Arrow__Order__Mirabelle_OLin))
| ~ hBOOL(X2) )
| ~ spl17_245 ),
inference(avatar_component_clause,[],[f7245]) ).
fof(f7265,plain,
( ! [X0,X1] : c_Arrow__Order__Mirabelle_OProf = c_FuncSet_OPi(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)),c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool)))
| ~ spl17_2
| ~ spl17_180 ),
inference(forward_subsumption_resolution,[],[f7197,f6220]) ).
fof(f7266,plain,
( ! [X0,X1] : hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool)))))
| ~ spl17_3
| ~ spl17_180 ),
inference(forward_subsumption_resolution,[],[f7196,f6220]) ).
fof(f7288,plain,
( ! [X2,X3,X0,X1,X4] : hBOOL(hAPP(hAPP(c_member(X0),sK9(X1,X2,X3,X4,X0)),X4))
| ~ spl17_243 ),
inference(resolution,[],[f7238,f649]) ).
fof(f7366,plain,
( $false
| ~ spl17_243 ),
inference(forward_subsumption_resolution,[],[f7288,f7238]) ).
fof(f7367,plain,
~ spl17_243,
inference(avatar_contradiction_clause,[],[f7366]) ).
fof(f7465,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(X0,X1,X2))))
| ~ hBOOL(X2) )
| ~ spl17_3
| ~ spl17_180 ),
inference(superposition,[],[f7266,f7169]) ).
fof(f7473,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(sK3(X0,X1),X2))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_2
| ~ spl17_245 ),
inference(resolution,[],[f7246,f3374]) ).
fof(f7578,definition,
( spl17_252
<=> hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,sK14(c_Arrow__Order__Mirabelle_OLin))) ),
introduced(definition,[new_symbols(definition,[spl17_252])],[avatar_definition]) ).
fof(f7579,plain,
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,sK14(c_Arrow__Order__Mirabelle_OLin)))
| ~ spl17_252 ),
inference(avatar_component_clause,[],[f7578]) ).
fof(f7580,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,sK14(c_Arrow__Order__Mirabelle_OLin)))
| spl17_252 ),
inference(avatar_component_clause,[],[f7578]) ).
fof(f7703,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_COMBK(X0,X1,X2) = c_COMBK(X3,X4,X5)
| ~ hBOOL(X2)
| ~ hBOOL(X5) ),
inference(resolution,[],[f3535,f3313]) ).
fof(f7704,plain,
! [X2,X3,X0,X1] :
( c_COMBK(X0,X1,X2) = X3
| ~ hBOOL(X2)
| ~ hBOOL(hAPP(X3,sK14(X3))) ),
inference(resolution,[],[f3535,f6955]) ).
fof(f7713,plain,
! [X3,X0,X4] :
( X0 = X4
| ~ hBOOL(X3)
| ~ hBOOL(hAPP(X4,sK14(X4)))
| ~ hBOOL(X3)
| ~ hBOOL(hAPP(X0,sK14(X0))) ),
inference(superposition,[],[f7704,f7704]) ).
fof(f7736,plain,
! [X3,X0,X4] :
( ~ hBOOL(hAPP(X0,sK14(X0)))
| ~ hBOOL(X3)
| hAPP(X0,X4) = X3 ),
inference(superposition,[],[f638,f7704]) ).
fof(f7769,plain,
! [X3,X0,X4] :
( X0 = X4
| ~ hBOOL(X3)
| ~ hBOOL(hAPP(X4,sK14(X4)))
| ~ hBOOL(hAPP(X0,sK14(X0))) ),
inference(duplicate_literal_removal,[],[f7713]) ).
fof(f7771,definition,
( spl17_254
<=> ! [X0] :
( hBOOL(X0)
| ~ hBOOL(hAPP(X0,sK14(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl17_254])],[avatar_definition]) ).
fof(f7772,plain,
( ! [X0] :
( ~ hBOOL(hAPP(X0,sK14(X0)))
| hBOOL(X0) )
| ~ spl17_254 ),
inference(avatar_component_clause,[],[f7771]) ).
fof(f7794,definition,
( spl17_257
<=> ! [X4,X0] :
( X0 = X4
| ~ hBOOL(hAPP(X0,sK14(X0)))
| ~ hBOOL(hAPP(X4,sK14(X4))) ) ),
introduced(definition,[new_symbols(definition,[spl17_257])],[avatar_definition]) ).
fof(f7795,plain,
( ! [X0,X4] :
( ~ hBOOL(hAPP(X4,sK14(X4)))
| ~ hBOOL(hAPP(X0,sK14(X0)))
| X0 = X4 )
| ~ spl17_257 ),
inference(avatar_component_clause,[],[f7794]) ).
fof(f7796,plain,
( spl17_243
| spl17_257 ),
inference(avatar_split_clause,[],[f7769,f7794,f7237]) ).
fof(f7827,definition,
( spl17_263
<=> ! [X0] : hBOOL(hAPP(v_F,sK0(X0,v_F))) ),
introduced(definition,[new_symbols(definition,[spl17_263])],[avatar_definition]) ).
fof(f7828,plain,
( ! [X0] : hBOOL(hAPP(v_F,sK0(X0,v_F)))
| ~ spl17_263 ),
inference(avatar_component_clause,[],[f7827]) ).
fof(f7954,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(c_COMBK(X0,X1,X2))
| ~ hBOOL(X2) )
| spl17_220 ),
inference(superposition,[],[f6512,f7169]) ).
fof(f8021,plain,
( ! [X0] :
( hBOOL(X0)
| hBOOL(X0) )
| ~ spl17_234
| ~ spl17_254 ),
inference(resolution,[],[f6754,f7772]) ).
fof(f8095,plain,
( ! [X0] : hBOOL(X0)
| ~ spl17_234
| ~ spl17_254 ),
inference(duplicate_literal_removal,[],[f8021]) ).
fof(f8108,plain,
( spl17_42
| ~ spl17_234
| ~ spl17_254 ),
inference(avatar_split_clause,[],[f8095,f7771,f6753,f1300]) ).
fof(f8282,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_FuncSet_OPi(X3,X4,X5,c_COMBK(X0,X1,X2)) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X3,X4),tc_HOL_Obool))
| ~ hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))
| ~ hBOOL(X2) ),
inference(superposition,[],[f642,f7703]) ).
fof(f8584,plain,
! [X2,X0,X1] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X2) = X0
| ~ hBOOL(X0) ),
inference(resolution,[],[f7736,f670]) ).
fof(f8706,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP(X2,sK14(X2)))
| c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) = X2
| ~ hBOOL(X0) )
| ~ spl17_257 ),
inference(superposition,[],[f7795,f8584]) ).
fof(f8711,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP(X2,sK14(X2)))
| c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) = X2 )
| ~ spl17_257 ),
inference(duplicate_literal_removal,[],[f8706]) ).
fof(f8716,definition,
( spl17_283
<=> ! [X2,X1] :
( ~ hBOOL(hAPP(X2,sK14(X2)))
| c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl17_283])],[avatar_definition]) ).
fof(f8717,plain,
( ! [X2,X1] :
( c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) = X2
| ~ hBOOL(hAPP(X2,sK14(X2))) )
| ~ spl17_283 ),
inference(avatar_component_clause,[],[f8716]) ).
fof(f8718,plain,
( spl17_283
| spl17_243
| ~ spl17_257 ),
inference(avatar_split_clause,[],[f8711,f7794,f7237,f8716]) ).
fof(f8772,plain,
( ! [X0] :
( hBOOL(X0)
| ~ hBOOL(hAPP(X0,sK14(X0))) )
| ~ spl17_222
| ~ spl17_283 ),
inference(superposition,[],[f6520,f8717]) ).
fof(f8776,plain,
( ! [X0] :
( hBOOL(X0)
| ~ hBOOL(hAPP(X0,sK14(X0))) )
| ~ spl17_220
| ~ spl17_283 ),
inference(superposition,[],[f6513,f8717]) ).
fof(f8861,definition,
( spl17_285
<=> ! [X4,X0,X3,X2,X1] : c_FuncSet_OPi(X2,X3,X4,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X3),tc_HOL_Obool)) ),
introduced(definition,[new_symbols(definition,[spl17_285])],[avatar_definition]) ).
fof(f8862,plain,
( ! [X2,X3,X0,X1,X4] : c_FuncSet_OPi(X2,X3,X4,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X3),tc_HOL_Obool))
| ~ spl17_285 ),
inference(avatar_component_clause,[],[f8861]) ).
fof(f9054,plain,
( spl17_254
| ~ spl17_220
| ~ spl17_283 ),
inference(avatar_split_clause,[],[f8776,f8716,f6511,f7771]) ).
fof(f9057,plain,
( spl17_254
| ~ spl17_222
| ~ spl17_283 ),
inference(avatar_split_clause,[],[f8772,f8716,f6519,f7771]) ).
fof(f9132,definition,
( spl17_329
<=> ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(X0,X1,X2))))
| ~ hBOOL(X2) ) ),
introduced(definition,[new_symbols(definition,[spl17_329])],[avatar_definition]) ).
fof(f9133,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_F),c_FuncSet_OPi(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_COMBK(X0,X1,X2))))
| ~ hBOOL(X2) )
| ~ spl17_329 ),
inference(avatar_component_clause,[],[f9132]) ).
fof(f9198,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| ~ hBOOL(X0) )
| ~ spl17_254 ),
inference(superposition,[],[f7772,f8584]) ).
fof(f9213,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) )
| ~ spl17_254 ),
inference(duplicate_literal_removal,[],[f9198]) ).
fof(f9218,plain,
( spl17_222
| spl17_243
| ~ spl17_254 ),
inference(avatar_split_clause,[],[f9213,f7771,f7237,f6519]) ).
fof(f9542,plain,
( spl17_329
| ~ spl17_3
| ~ spl17_180 ),
inference(avatar_split_clause,[],[f7465,f6218,f719,f9132]) ).
fof(f9631,plain,
( ! [X2,X3,X0,X1,X4] : c_FuncSet_OPi(X2,X3,X4,c_Orderings_Otop__class_Otop(tc_fun(tc_prod(X0,X1),tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X2,X3),tc_HOL_Obool))
| ~ spl17_222 ),
inference(forward_subsumption_resolution,[],[f7202,f6520]) ).
fof(f9632,plain,
( spl17_285
| ~ spl17_222 ),
inference(avatar_split_clause,[],[f9631,f6519,f8861]) ).
fof(f9638,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( c_FuncSet_OPi(X3,X4,X5,c_COMBK(X0,X1,X2)) = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X3,X4),tc_HOL_Obool))
| ~ hBOOL(X2) )
| ~ spl17_222 ),
inference(forward_subsumption_resolution,[],[f8282,f6520]) ).
fof(f10151,plain,
( ! [X2,X3,X0,X1,X4] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(tc_prod(X2,X3),tc_HOL_Obool),sK3(X1,X0),X4)
| c_Arrow__Order__Mirabelle_Odictator(X0,X1) )
| ~ spl17_2
| ~ spl17_245 ),
inference(resolution,[],[f7473,f733]) ).
fof(f11228,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| ~ spl17_196 ),
inference(superposition,[],[f670,f6329]) ).
fof(f11294,plain,
( ! [X2,X3,X0,X1,X4] :
( sK3(X1,X0) = c_COMBK(X2,X3,X4)
| c_Arrow__Order__Mirabelle_Odictator(X0,X1)
| hBOOL(X4) )
| ~ spl17_2
| ~ spl17_245 ),
inference(resolution,[],[f10151,f6113]) ).
fof(f11302,plain,
( ! [X2,X3,X0,X1,X6] :
( sK3(X0,X1) = sK3(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X3,X2)
| hBOOL(X6)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| hBOOL(X6) )
| ~ spl17_2
| ~ spl17_245 ),
inference(superposition,[],[f11294,f11294]) ).
fof(f11622,definition,
( spl17_423
<=> ! [X0,X3,X2,X1] :
( sK3(X0,X1) = sK3(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| c_Arrow__Order__Mirabelle_Odictator(X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl17_423])],[avatar_definition]) ).
fof(f11623,plain,
( ! [X2,X3,X0,X1] :
( sK3(X0,X1) = sK3(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| c_Arrow__Order__Mirabelle_Odictator(X3,X2) )
| ~ spl17_423 ),
inference(avatar_component_clause,[],[f11622]) ).
fof(f14937,definition,
( spl17_523
<=> ! [X2,X0,X3] :
( hBOOL(X0)
| ~ hBOOL(c_COMBK(X2,X3,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl17_523])],[avatar_definition]) ).
fof(f14938,plain,
( ! [X2,X3,X0] :
( ~ hBOOL(c_COMBK(X2,X3,X0))
| hBOOL(X0) )
| ~ spl17_523 ),
inference(avatar_component_clause,[],[f14937]) ).
fof(f15086,definition,
( spl17_532
<=> ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0)) ),
introduced(definition,[new_symbols(definition,[spl17_532])],[avatar_definition]) ).
fof(f15087,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| ~ spl17_532 ),
inference(avatar_component_clause,[],[f15086]) ).
fof(f15322,plain,
( ! [X2,X3,X0,X1,X6] :
( sK3(X0,X1) = sK3(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X3,X2)
| hBOOL(X6)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_2
| ~ spl17_245 ),
inference(duplicate_literal_removal,[],[f11302]) ).
fof(f15342,plain,
( c_Arrow__Order__Mirabelle_OProf = c_Orderings_Otop__class_Otop(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool))
| ~ spl17_2
| ~ spl17_180
| ~ spl17_285 ),
inference(forward_demodulation,[],[f7265,f8862]) ).
fof(f15349,plain,
( spl17_532
| ~ spl17_196 ),
inference(avatar_split_clause,[],[f11228,f6327,f15086]) ).
fof(f15561,definition,
( spl17_564
<=> ! [X4,X0,X3] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_COMBK(X3,X4,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl17_564])],[avatar_definition]) ).
fof(f15562,plain,
( ! [X3,X0,X4] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_COMBK(X3,X4,X0))) )
| ~ spl17_564 ),
inference(avatar_component_clause,[],[f15561]) ).
fof(f15563,plain,
( spl17_21
| spl17_564
| ~ spl17_2 ),
inference(avatar_split_clause,[],[f3640,f714,f15561,f1023]) ).
fof(f15598,plain,
( spl17_196
| ~ spl17_2
| ~ spl17_180
| ~ spl17_285 ),
inference(avatar_split_clause,[],[f15342,f8861,f6218,f714,f6327]) ).
fof(f15822,plain,
( ! [X2,X3,X0,X1] :
( hAPP(sK3(X0,X1),X3) != hAPP(X2,sK3(X0,X1))
| c_Arrow__Order__Mirabelle_Odictator(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| c_Arrow__Order__Mirabelle_Odictator(X2,X3) )
| ~ spl17_423 ),
inference(superposition,[],[f618,f11623]) ).
fof(f15937,plain,
( ! [X2,X3,X0,X1] :
( hAPP(sK3(X0,X1),X3) != hAPP(X2,sK3(X0,X1))
| c_Arrow__Order__Mirabelle_Odictator(X2,X3)
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_423 ),
inference(duplicate_literal_removal,[],[f15822]) ).
fof(f16112,plain,
( ! [X0,X1] :
( c_Arrow__Order__Mirabelle_Odictator(sK3(X0,X1),sK3(X0,X1))
| c_Arrow__Order__Mirabelle_Odictator(X1,X0) )
| ~ spl17_423 ),
inference(equality_resolution,[],[f15937]) ).
fof(f19281,plain,
( spl17_42
| spl17_423
| ~ spl17_2
| ~ spl17_245 ),
inference(avatar_split_clause,[],[f15322,f7245,f714,f11622,f1300]) ).
fof(f19311,plain,
( ! [X0,X1] : c_Arrow__Order__Mirabelle_Odictator(X1,X0)
| ~ spl17_21
| ~ spl17_423 ),
inference(forward_subsumption_resolution,[],[f16112,f1024]) ).
fof(f19637,plain,
( spl17_23
| ~ spl17_21
| ~ spl17_423 ),
inference(avatar_split_clause,[],[f19311,f11622,f1023,f1031]) ).
fof(f27171,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( hBOOL(hAPP(c_FuncSet_OPi(X6,X1,X5,c_COMBK(tc_fun(X1,tc_HOL_Obool),X6,X4)),c_COMBK(X2,X3,X0)))
| ~ hBOOL(hAPP(hAPP(c_member(X1),X0),X4)) ),
inference(superposition,[],[f755,f638]) ).
fof(f27389,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( hBOOL(hAPP(c_FuncSet_OPi(X3,X4,X5,c_COMBK(X0,X1,X2)),c_COMBK(X7,X8,X9)))
| ~ hBOOL(hAPP(hAPP(c_member(X4),X9),X6))
| hBOOL(X6)
| hBOOL(X2) ),
inference(superposition,[],[f27171,f6120]) ).
fof(f27875,plain,
( $false
| ~ spl17_193
| spl17_237 ),
inference(forward_subsumption_resolution,[],[f6912,f6296]) ).
fof(f27876,plain,
( ~ spl17_193
| spl17_237 ),
inference(avatar_contradiction_clause,[],[f27875]) ).
fof(f33493,definition,
( spl17_1179
<=> ! [X4,X1,X3] : ~ hBOOL(c_COMBK(X3,X4,X1)) ),
introduced(definition,[new_symbols(definition,[spl17_1179])],[avatar_definition]) ).
fof(f33494,plain,
( ! [X3,X1,X4] : ~ hBOOL(c_COMBK(X3,X4,X1))
| ~ spl17_1179 ),
inference(avatar_component_clause,[],[f33493]) ).
fof(f39226,definition,
( spl17_1472
<=> ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F))))
| ~ hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl17_1472])],[avatar_definition]) ).
fof(f39227,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F))))
| ~ hBOOL(X0) )
| ~ spl17_1472 ),
inference(avatar_component_clause,[],[f39226]) ).
fof(f40690,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl17_532
| ~ spl17_564 ),
inference(forward_subsumption_resolution,[],[f15562,f15087]) ).
fof(f40691,plain,
( spl17_193
| ~ spl17_532
| ~ spl17_564 ),
inference(avatar_split_clause,[],[f40690,f15561,f15086,f6295]) ).
fof(f40864,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X0))
| ~ spl17_252 ),
inference(resolution,[],[f7579,f6954]) ).
fof(f40881,plain,
( spl17_193
| ~ spl17_252 ),
inference(avatar_split_clause,[],[f40864,f7578,f6295]) ).
fof(f40882,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),X1),c_Arrow__Order__Mirabelle_OProf))
| ~ hBOOL(X0)
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,X1)),X0)) )
| ~ spl17_329 ),
inference(resolution,[],[f9133,f654]) ).
fof(f40927,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,sK3(X1,X2))),X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf)
| c_Arrow__Order__Mirabelle_Odictator(X2,X1) )
| ~ spl17_329 ),
inference(resolution,[],[f40882,f901]) ).
fof(f40975,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,sK3(X1,X2))),X0))
| ~ hBOOL(X0)
| c_Arrow__Order__Mirabelle_Odictator(X2,X1) )
| ~ spl17_329 ),
inference(forward_subsumption_resolution,[],[f40927,f678]) ).
fof(f41707,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2))
| hBOOL(X2)
| hBOOL(X3)
| ~ hBOOL(hAPP(hAPP(c_member(X4),X5),X6))
| hBOOL(hAPP(hAPP(c_member(X0),hAPP(c_COMBK(X7,X8,X1),X5)),X3)) ),
inference(resolution,[],[f27389,f744]) ).
fof(f41739,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X0),X1),X3))
| ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2))
| hBOOL(X2)
| hBOOL(X3)
| ~ hBOOL(hAPP(hAPP(c_member(X4),X5),X6)) ),
inference(forward_demodulation,[],[f41707,f638]) ).
fof(f41741,definition,
( spl17_1527
<=> ! [X0,X3,X2,X1] :
( hBOOL(hAPP(hAPP(c_member(X0),X1),X3))
| hBOOL(X3)
| hBOOL(X2)
| ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl17_1527])],[avatar_definition]) ).
fof(f41742,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2))
| hBOOL(X3)
| hBOOL(X2)
| hBOOL(hAPP(hAPP(c_member(X0),X1),X3)) )
| ~ spl17_1527 ),
inference(avatar_component_clause,[],[f41741]) ).
fof(f41743,plain,
( spl17_202
| spl17_1527 ),
inference(avatar_split_clause,[],[f41739,f41741,f6442]) ).
fof(f41775,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(X2),X3),X0))
| hBOOL(X1)
| hBOOL(X0)
| ~ hBOOL(hAPP(X1,X3)) )
| ~ spl17_1527 ),
inference(resolution,[],[f41742,f627]) ).
fof(f41931,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,X2))
| hBOOL(X1)
| hBOOL(X0)
| hBOOL(hAPP(X1,X2)) )
| ~ spl17_1527 ),
inference(resolution,[],[f41775,f626]) ).
fof(f42099,plain,
( ! [X0,X1] :
( hBOOL(X0)
| hBOOL(c_Arrow__Order__Mirabelle_OLin)
| hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F)))) )
| ~ spl17_3
| ~ spl17_1527 ),
inference(resolution,[],[f41931,f5795]) ).
fof(f42115,plain,
( ! [X2,X0,X1] :
( hBOOL(X0)
| hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| hBOOL(hAPP(X0,X2)) )
| ~ spl17_1527 ),
inference(resolution,[],[f41931,f670]) ).
fof(f42204,definition,
( spl17_1538
<=> ! [X0,X3] :
( hBOOL(X0)
| hBOOL(X3)
| hBOOL(hAPP(X0,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl17_1538])],[avatar_definition]) ).
fof(f42205,plain,
( ! [X3,X0] :
( hBOOL(hAPP(X0,X3))
| hBOOL(X3)
| hBOOL(X0) )
| ~ spl17_1538 ),
inference(avatar_component_clause,[],[f42204]) ).
fof(f42274,definition,
( spl17_1553
<=> ! [X2,X1] : hBOOL(hAPP(c_member(X1),X2)) ),
introduced(definition,[new_symbols(definition,[spl17_1553])],[avatar_definition]) ).
fof(f42275,plain,
( ! [X2,X1] : hBOOL(hAPP(c_member(X1),X2))
| ~ spl17_1553 ),
inference(avatar_component_clause,[],[f42274]) ).
fof(f45809,definition,
( spl17_1701
<=> hBOOL(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),sK14(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))))) ),
introduced(definition,[new_symbols(definition,[spl17_1701])],[avatar_definition]) ).
fof(f45810,plain,
( hBOOL(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),sK14(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))))
| ~ spl17_1701 ),
inference(avatar_component_clause,[],[f45809]) ).
fof(f45811,plain,
( ~ hBOOL(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),sK14(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)))))
| spl17_1701 ),
inference(avatar_component_clause,[],[f45809]) ).
fof(f46305,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(X0,hAPP(v_F,sK3(X2,X1))))
| c_Arrow__Order__Mirabelle_Odictator(X1,X2)
| ~ hBOOL(X0) )
| ~ spl17_329 ),
inference(resolution,[],[f40975,f626]) ).
fof(f47425,plain,
( ! [X2,X3,X0,X1,X4] :
( hBOOL(X0)
| c_Arrow__Order__Mirabelle_Odictator(X4,X3)
| ~ hBOOL(c_COMBK(X1,X2,X0)) )
| ~ spl17_329 ),
inference(superposition,[],[f46305,f638]) ).
fof(f48821,plain,
( $false
| ~ spl17_1553
| spl17_1701 ),
inference(resolution,[],[f42275,f45811]) ).
fof(f48881,plain,
( ~ spl17_1553
| spl17_1701 ),
inference(avatar_contradiction_clause,[],[f48821]) ).
fof(f61386,definition,
( spl17_2085
<=> ! [X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F)))) ) ),
introduced(definition,[new_symbols(definition,[spl17_2085])],[avatar_definition]) ).
fof(f61387,plain,
( ! [X0,X1] :
( hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F))))
| hBOOL(X0) )
| ~ spl17_2085 ),
inference(avatar_component_clause,[],[f61386]) ).
fof(f61388,plain,
( spl17_180
| spl17_2085
| ~ spl17_3
| ~ spl17_1527 ),
inference(avatar_split_clause,[],[f42099,f41741,f719,f61386,f6218]) ).
fof(f62631,plain,
( ! [X0,X1] :
( hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),X1) = X0
| ~ hBOOL(X0) )
| ~ spl17_1701 ),
inference(resolution,[],[f45810,f7736]) ).
fof(f62765,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,hAPP(v_F,sK0(X1,v_F))))
| ~ hBOOL(X0) )
| ~ spl17_3
| ~ spl17_1701 ),
inference(superposition,[],[f766,f62631]) ).
fof(f62941,plain,
( spl17_1472
| ~ spl17_3
| ~ spl17_1701 ),
inference(avatar_split_clause,[],[f62765,f45809,f719,f39226]) ).
fof(f63689,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| ~ hBOOL(X0) )
| ~ spl17_1472 ),
inference(superposition,[],[f39227,f8584]) ).
fof(f63712,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) )
| ~ spl17_1472 ),
inference(duplicate_literal_removal,[],[f63689]) ).
fof(f63716,plain,
( ! [X0] : ~ hBOOL(X0)
| ~ spl17_222
| ~ spl17_1472 ),
inference(forward_subsumption_resolution,[],[f63712,f6520]) ).
fof(f63738,plain,
( spl17_243
| ~ spl17_222
| ~ spl17_1472 ),
inference(avatar_split_clause,[],[f63716,f39226,f6519,f7237]) ).
fof(f64493,definition,
( spl17_2159
<=> ! [X2,X0,X1] :
( hBOOL(hAPP(c_member(X0),X1))
| hBOOL(hAPP(hAPP(c_member(X0),X1),X2))
| hBOOL(X2) ) ),
introduced(definition,[new_symbols(definition,[spl17_2159])],[avatar_definition]) ).
fof(f64494,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(X0),X1),X2))
| hBOOL(hAPP(c_member(X0),X1))
| hBOOL(X2) )
| ~ spl17_2159 ),
inference(avatar_component_clause,[],[f64493]) ).
fof(f64628,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(X0,X1)),X2),c_Orderings_Otop__class_Otop(tc_fun(tc_fun(X0,X1),tc_HOL_Obool))))
| ~ hBOOL(hAPP(hAPP(c_member(X0),X5),X3))
| hBOOL(hAPP(hAPP(c_member(X1),hAPP(X2,X5)),X4))
| ~ hBOOL(X4) )
| ~ spl17_222 ),
inference(superposition,[],[f654,f9638]) ).
fof(f64646,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X1),hAPP(X2,X5)),X4))
| ~ hBOOL(hAPP(hAPP(c_member(X0),X5),X3))
| ~ hBOOL(X4) )
| ~ spl17_222 ),
inference(forward_subsumption_resolution,[],[f64628,f667]) ).
fof(f64658,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_member(X0),X1))
| hBOOL(X2)
| hBOOL(hAPP(v_F,sK0(X3,v_F)))
| hBOOL(hAPP(hAPP(c_member(X0),X1),X2)) )
| ~ spl17_1527
| ~ spl17_2085 ),
inference(resolution,[],[f61387,f41742]) ).
fof(f65382,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_member(X0),X1))
| hBOOL(X2)
| hBOOL(X3)
| hBOOL(hAPP(c_member(X0),X1))
| hBOOL(hAPP(X3,X2)) )
| ~ spl17_1527
| ~ spl17_2159 ),
inference(resolution,[],[f64494,f41931]) ).
fof(f65476,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(c_member(X0),X1))
| hBOOL(X2)
| hBOOL(X3)
| hBOOL(hAPP(X3,X2)) )
| ~ spl17_1527
| ~ spl17_2159 ),
inference(duplicate_literal_removal,[],[f65382]) ).
fof(f65750,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_member(X0),sK2(X1,v_F)),X2))
| ~ hBOOL(hAPP(v_F,sK0(X1,v_F))) )
| ~ spl17_3
| ~ spl17_222 ),
inference(resolution,[],[f64646,f766]) ).
fof(f65821,plain,
( ! [X0,X1,X6,X7,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X1),X0),X5))
| ~ hBOOL(hAPP(hAPP(c_member(X6),X4),X7))
| ~ hBOOL(X5) )
| ~ spl17_222 ),
inference(superposition,[],[f64646,f638]) ).
fof(f65893,definition,
( spl17_2186
<=> ! [X5,X0,X1] :
( hBOOL(hAPP(hAPP(c_member(X1),X0),X5))
| ~ hBOOL(X5) ) ),
introduced(definition,[new_symbols(definition,[spl17_2186])],[avatar_definition]) ).
fof(f65894,plain,
( ! [X0,X1,X5] :
( hBOOL(hAPP(hAPP(c_member(X1),X0),X5))
| ~ hBOOL(X5) )
| ~ spl17_2186 ),
inference(avatar_component_clause,[],[f65893]) ).
fof(f65895,plain,
( spl17_202
| spl17_2186
| ~ spl17_222 ),
inference(avatar_split_clause,[],[f65821,f6519,f65893,f6442]) ).
fof(f65907,plain,
( ! [X2,X0,X1] : ~ hBOOL(hAPP(hAPP(c_member(X0),sK2(X1,v_F)),X2))
| ~ spl17_3
| ~ spl17_222
| ~ spl17_263 ),
inference(forward_subsumption_resolution,[],[f65750,f7828]) ).
fof(f65984,plain,
( $false
| ~ spl17_3
| ~ spl17_222
| ~ spl17_263 ),
inference(resolution,[],[f65907,f667]) ).
fof(f66044,plain,
( ~ spl17_3
| ~ spl17_222
| ~ spl17_263 ),
inference(avatar_contradiction_clause,[],[f65984]) ).
fof(f66051,plain,
( spl17_263
| spl17_2159
| ~ spl17_1527
| ~ spl17_2085 ),
inference(avatar_split_clause,[],[f64658,f61386,f41741,f64493,f7827]) ).
fof(f66087,plain,
( spl17_1538
| spl17_1553
| ~ spl17_1527
| ~ spl17_2159 ),
inference(avatar_split_clause,[],[f65476,f64493,f41741,f42274,f42204]) ).
fof(f66327,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),X0))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0),c_Arrow__Order__Mirabelle_OLin)) )
| ~ spl17_2186 ),
inference(resolution,[],[f65894,f635]) ).
fof(f66350,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(X0)
| hBOOL(X1)
| hBOOL(hAPP(c_member(X2),X3))
| hBOOL(hAPP(X1,X0)) )
| ~ spl17_1527
| ~ spl17_2186 ),
inference(resolution,[],[f65894,f41931]) ).
fof(f66444,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X1)
| hBOOL(hAPP(c_member(X2),X3))
| hBOOL(hAPP(X1,X0)) )
| ~ spl17_1527
| ~ spl17_1538
| ~ spl17_2186 ),
inference(forward_subsumption_resolution,[],[f66350,f42205]) ).
fof(f66454,plain,
( ! [X0] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X0),c_Arrow__Order__Mirabelle_OLin)) )
| ~ spl17_2186 ),
inference(forward_subsumption_resolution,[],[f66327,f65894]) ).
fof(f66456,plain,
( spl17_1553
| spl17_234
| ~ spl17_1527
| ~ spl17_1538
| ~ spl17_2186 ),
inference(avatar_split_clause,[],[f66444,f65893,f42204,f41741,f6753,f42274]) ).
fof(f66461,plain,
( spl17_245
| ~ spl17_2186 ),
inference(avatar_split_clause,[],[f66454,f65893,f7245]) ).
fof(f68105,plain,
( spl17_23
| spl17_523
| ~ spl17_329 ),
inference(avatar_split_clause,[],[f47425,f9132,f14937,f1031]) ).
fof(f68320,definition,
( spl17_2331
<=> ! [X2,X0,X1] :
( hBOOL(X0)
| hBOOL(c_COMBK(X1,X2,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl17_2331])],[avatar_definition]) ).
fof(f68321,plain,
( ! [X2,X0,X1] :
( hBOOL(X0)
| hBOOL(c_COMBK(X1,X2,X0)) )
| ~ spl17_2331 ),
inference(avatar_component_clause,[],[f68320]) ).
fof(f68480,plain,
( spl17_222
| spl17_234
| ~ spl17_1527 ),
inference(avatar_split_clause,[],[f42115,f41741,f6753,f6519]) ).
fof(f69987,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OLin)
| ~ spl17_234
| spl17_252 ),
inference(resolution,[],[f6754,f7580]) ).
fof(f70032,plain,
( ! [X2,X0,X1] :
( hBOOL(X0)
| hBOOL(c_COMBK(X1,X2,X0)) )
| ~ spl17_234 ),
inference(superposition,[],[f6754,f638]) ).
fof(f70059,plain,
( spl17_2331
| ~ spl17_234 ),
inference(avatar_split_clause,[],[f70032,f6753,f68320]) ).
fof(f70068,plain,
( spl17_180
| ~ spl17_234
| spl17_252 ),
inference(avatar_split_clause,[],[f69987,f7578,f6753,f6218]) ).
fof(f70081,plain,
( ! [X2,X3,X0] : ~ hBOOL(c_COMBK(X2,X3,X0))
| spl17_220
| ~ spl17_523 ),
inference(forward_subsumption_resolution,[],[f14938,f7954]) ).
fof(f70082,plain,
( spl17_1179
| spl17_220
| ~ spl17_523 ),
inference(avatar_split_clause,[],[f70081,f14937,f6511,f33493]) ).
fof(f70224,plain,
( ! [X0] : hBOOL(X0)
| ~ spl17_1179
| ~ spl17_2331 ),
inference(forward_subsumption_resolution,[],[f68321,f33494]) ).
fof(f70225,plain,
( spl17_42
| ~ spl17_1179
| ~ spl17_2331 ),
inference(avatar_split_clause,[],[f70224,f68320,f33493,f1300]) ).
cnf(s2,plain,
spl17_2,
inference(sat_conversion,[],[f717]) ).
cnf(s3,plain,
spl17_3,
inference(sat_conversion,[],[f722]) ).
cnf(s18,plain,
~ spl17_23,
inference(sat_conversion,[],[f1039]) ).
cnf(s108,plain,
~ spl17_131,
inference(sat_conversion,[],[f3040]) ).
cnf(s238,plain,
~ spl17_202,
inference(sat_conversion,[],[f6635]) ).
cnf(s253,plain,
( spl17_131
| ~ spl17_237 ),
inference(sat_conversion,[],[f6913]) ).
cnf(s275,plain,
~ spl17_42,
inference(sat_conversion,[],[f7117]) ).
cnf(s309,plain,
~ spl17_243,
inference(sat_conversion,[],[f7367]) ).
cnf(s324,plain,
( spl17_243
| spl17_257 ),
inference(sat_conversion,[],[f7796]) ).
cnf(s358,plain,
( spl17_42
| ~ spl17_234
| ~ spl17_254 ),
inference(sat_conversion,[],[f8108]) ).
cnf(s390,plain,
( spl17_243
| ~ spl17_257
| spl17_283 ),
inference(sat_conversion,[],[f8718]) ).
cnf(s452,plain,
( ~ spl17_220
| spl17_254
| ~ spl17_283 ),
inference(sat_conversion,[],[f9054]) ).
cnf(s455,plain,
( ~ spl17_222
| spl17_254
| ~ spl17_283 ),
inference(sat_conversion,[],[f9057]) ).
cnf(s500,plain,
( spl17_222
| spl17_243
| ~ spl17_254 ),
inference(sat_conversion,[],[f9218]) ).
cnf(s563,plain,
( ~ spl17_3
| ~ spl17_180
| spl17_329 ),
inference(sat_conversion,[],[f9542]) ).
cnf(s578,plain,
( ~ spl17_222
| spl17_285 ),
inference(sat_conversion,[],[f9632]) ).
cnf(s1098,plain,
( ~ spl17_196
| spl17_532 ),
inference(sat_conversion,[],[f15349]) ).
cnf(s1199,plain,
( ~ spl17_2
| spl17_21
| spl17_564 ),
inference(sat_conversion,[],[f15563]) ).
cnf(s1208,plain,
( ~ spl17_2
| ~ spl17_180
| spl17_196
| ~ spl17_285 ),
inference(sat_conversion,[],[f15598]) ).
cnf(s1642,plain,
( ~ spl17_2
| spl17_42
| ~ spl17_245
| spl17_423 ),
inference(sat_conversion,[],[f19281]) ).
cnf(s1688,plain,
( ~ spl17_21
| spl17_23
| ~ spl17_423 ),
inference(sat_conversion,[],[f19637]) ).
cnf(s2443,plain,
( ~ spl17_193
| spl17_237 ),
inference(sat_conversion,[],[f27876]) ).
cnf(s4020,plain,
( spl17_193
| ~ spl17_532
| ~ spl17_564 ),
inference(sat_conversion,[],[f40691]) ).
cnf(s4028,plain,
( spl17_193
| ~ spl17_252 ),
inference(sat_conversion,[],[f40881]) ).
cnf(s4054,plain,
( spl17_202
| spl17_1527 ),
inference(sat_conversion,[],[f41743]) ).
cnf(s4719,plain,
( ~ spl17_1553
| spl17_1701 ),
inference(sat_conversion,[],[f48881]) ).
cnf(s5680,plain,
( ~ spl17_3
| spl17_180
| ~ spl17_1527
| spl17_2085 ),
inference(sat_conversion,[],[f61388]) ).
cnf(s5809,plain,
( ~ spl17_3
| spl17_1472
| ~ spl17_1701 ),
inference(sat_conversion,[],[f62941]) ).
cnf(s5873,plain,
( ~ spl17_222
| spl17_243
| ~ spl17_1472 ),
inference(sat_conversion,[],[f63738]) ).
cnf(s5965,plain,
( spl17_202
| ~ spl17_222
| spl17_2186 ),
inference(sat_conversion,[],[f65895]) ).
cnf(s5999,plain,
( ~ spl17_3
| ~ spl17_222
| ~ spl17_263 ),
inference(sat_conversion,[],[f66044]) ).
cnf(s6001,plain,
( spl17_263
| ~ spl17_1527
| ~ spl17_2085
| spl17_2159 ),
inference(sat_conversion,[],[f66051]) ).
cnf(s6019,plain,
( ~ spl17_1527
| spl17_1538
| spl17_1553
| ~ spl17_2159 ),
inference(sat_conversion,[],[f66087]) ).
cnf(s6043,plain,
( spl17_234
| ~ spl17_1527
| ~ spl17_1538
| spl17_1553
| ~ spl17_2186 ),
inference(sat_conversion,[],[f66456]) ).
cnf(s6046,plain,
( spl17_245
| ~ spl17_2186 ),
inference(sat_conversion,[],[f66461]) ).
cnf(s6412,plain,
( spl17_23
| ~ spl17_329
| spl17_523 ),
inference(sat_conversion,[],[f68105]) ).
cnf(s6547,plain,
( spl17_222
| spl17_234
| ~ spl17_1527 ),
inference(sat_conversion,[],[f68480]) ).
cnf(s7122,plain,
( ~ spl17_234
| spl17_2331 ),
inference(sat_conversion,[],[f70059]) ).
cnf(s7128,plain,
( spl17_180
| ~ spl17_234
| spl17_252 ),
inference(sat_conversion,[],[f70068]) ).
cnf(s7139,plain,
( spl17_220
| ~ spl17_523
| spl17_1179 ),
inference(sat_conversion,[],[f70082]) ).
cnf(s7167,plain,
( spl17_42
| ~ spl17_1179
| ~ spl17_2331 ),
inference(sat_conversion,[],[f70225]) ).
cnf(s7179,plain,
spl17_257,
inference(rat,[],[s324,s309]) ).
cnf(s7184,plain,
spl17_283,
inference(rat,[],[s390,s309,s7179]) ).
cnf(s7192,plain,
spl17_1527,
inference(rat,[],[s4054,s238]) ).
cnf(s7197,plain,
~ spl17_237,
inference(rat,[],[s253,s108]) ).
cnf(s7198,plain,
~ spl17_193,
inference(rat,[],[s2443,s7197]) ).
cnf(s7199,plain,
~ spl17_252,
inference(rat,[],[s4028,s7198]) ).
cnf(s7255,plain,
spl17_222,
inference(rat,[],[s6412,s7139,s7167,s563,s452,s7122,s7128,s500,s6547,s18,s275,s3,s7184,s7199,s309,s7192]) ).
cnf(s7256,plain,
~ spl17_263,
inference(rat,[],[s5999,s3,s7255]) ).
cnf(s7257,plain,
spl17_2186,
inference(rat,[],[s5965,s238,s7255]) ).
cnf(s7260,plain,
~ spl17_1472,
inference(rat,[],[s5873,s309,s7255]) ).
cnf(s7264,plain,
spl17_285,
inference(rat,[],[s578,s7255]) ).
cnf(s7265,plain,
spl17_254,
inference(rat,[],[s455,s7184,s7255]) ).
cnf(s7267,plain,
spl17_245,
inference(rat,[],[s6046,s7257]) ).
cnf(s7273,plain,
~ spl17_1701,
inference(rat,[],[s5809,s3,s7260]) ).
cnf(s7280,plain,
~ spl17_234,
inference(rat,[],[s358,s275,s7265]) ).
cnf(s7285,plain,
spl17_423,
inference(rat,[],[s1642,s2,s275,s7267]) ).
cnf(s7313,plain,
~ spl17_1553,
inference(rat,[],[s4719,s7273]) ).
cnf(s7316,plain,
~ spl17_1538,
inference(rat,[],[s6043,s7257,s7313,s7192,s7280]) ).
cnf(s7320,plain,
~ spl17_21,
inference(rat,[],[s1688,s18,s7285]) ).
cnf(s7344,plain,
~ spl17_2159,
inference(rat,[],[s6019,s7313,s7192,s7316]) ).
cnf(s7351,plain,
spl17_564,
inference(rat,[],[s1199,s2,s7320]) ).
cnf(s7357,plain,
~ spl17_2085,
inference(rat,[],[s6001,s7256,s7192,s7344]) ).
cnf(s7359,plain,
~ spl17_532,
inference(rat,[],[s4020,s7198,s7351]) ).
cnf(s7366,plain,
spl17_180,
inference(rat,[],[s5680,s3,s7192,s7357]) ).
cnf(s7369,plain,
~ spl17_196,
inference(rat,[],[s1098,s7359]) ).
cnf(s7398,plain,
$false,
inference(rat,[],[s1208,s7264,s2,s7369,s7366]) ).
fof(f70226,plain,
$false,
inference(avatar_sat_refutation,[],[s7398]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT124+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n004.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 23:45:37 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.40 Running first-order theorem proving
% 0.15/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.72/2.55 % (4006678)Detected formulas, will run a generic FOF schedule.
% 11.72/2.55 % (4006684)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4147498371:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.72/2.55 % (4006686)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2078837568:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.72/2.55 % (4006683)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=113102331:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.72/2.55 % (4006687)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2212495826:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.72/2.55 % (4006685)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3623167501:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.72/2.55 % (4006689)dis-21_1_sil=8000:lcm=predicate:random_seed=3099479993:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.72/2.55 % (4006686)Refutation not found, incomplete strategy
% 11.72/2.55 % (4006686)------------------------------
% 11.72/2.55 % (4006686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.55 % (4006686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.55 % (4006686)CaDiCaL version: 2.1.3
% 11.72/2.55 % (4006686)Termination reason: Refutation not found, incomplete strategy
% 11.72/2.55 % (4006686)Time elapsed: 0.004 s
% 11.72/2.55 % (4006686)Peak memory usage: 88 MB
% 11.72/2.55 % (4006686)Instructions burned: 4 (million)
% 11.72/2.55 % (4006688)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2754447851:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.72/2.55 % (4006689)Instruction limit reached!
% 11.72/2.55 % (4006689)------------------------------
% 11.72/2.55 % (4006689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.55 % (4006689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.55 % (4006689)CaDiCaL version: 2.1.3
% 11.72/2.55 % (4006689)Termination reason: Instruction limit
% 11.72/2.55 % (4006689)Termination phase: Saturation
% 11.72/2.55 % (4006689)Time elapsed: 0.070 s
% 11.72/2.55 % (4006689)Peak memory usage: 90 MB
% 11.72/2.55 % (4006689)Instructions burned: 130 (million)
% 11.72/2.55 % (4006687)Instruction limit reached!
% 11.72/2.55 % (4006687)------------------------------
% 11.72/2.55 % (4006687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.55 % (4006687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.55 % (4006687)CaDiCaL version: 2.1.3
% 11.72/2.55 % (4006687)Termination reason: Instruction limit
% 11.72/2.55 % (4006687)Termination phase: Saturation
% 11.72/2.55 % (4006687)Time elapsed: 0.072 s
% 11.72/2.55 % (4006687)Peak memory usage: 89 MB
% 11.72/2.55 % (4006687)Instructions burned: 120 (million)
% 11.72/2.55 % (4006688)Instruction limit reached!
% 11.72/2.55 % (4006688)------------------------------
% 11.72/2.55 % (4006688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.55 % (4006688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.55 % (4006688)CaDiCaL version: 2.1.3
% 11.72/2.55 % (4006688)Termination reason: Instruction limit
% 11.72/2.55 % (4006688)Termination phase: Saturation
% 11.72/2.55 % (4006688)Time elapsed: 0.079 s
% 11.72/2.55 % (4006688)Peak memory usage: 90 MB
% 11.72/2.55 % (4006688)Instructions burned: 139 (million)
% 11.72/2.55 % (4006697)lrs+10_1_sil=8000:sp=occurrence:random_seed=755302910:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.72/2.55 % (4006698)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1566287066:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.72/2.55 % (4006698)Refutation not found, incomplete strategy
% 11.72/2.55 % (4006698)------------------------------
% 11.72/2.55 % (4006698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.55 % (4006698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.55 % (4006698)CaDiCaL version: 2.1.3
% 11.72/2.55 % (4006698)Termination reason: Refutation not found, incomplete strategy
% 19.20/3.64 % (4006698)Time elapsed: 0.008 s
% 19.20/3.64 % (4006698)Peak memory usage: 89 MB
% 19.20/3.64 % (4006698)Instructions burned: 15 (million)
% 19.20/3.64 % (4006699)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1802102766:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 19.20/3.64 % (4006699)Refutation not found, incomplete strategy
% 19.20/3.64 % (4006699)------------------------------
% 19.20/3.64 % (4006699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/3.64 % (4006699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.64 % (4006699)CaDiCaL version: 2.1.3
% 19.20/3.64 % (4006699)Termination reason: Refutation not found, incomplete strategy
% 19.20/3.64 % (4006699)Time elapsed: 0.004 s
% 19.20/3.64 % (4006699)Peak memory usage: 89 MB
% 19.20/3.64 % (4006699)Instructions burned: 4 (million)
% 19.20/3.64 % (4006686)------------------------------
% 19.20/3.64 % (4006686)------------------------------
% 19.20/3.64 % (4006697)Instruction limit reached!
% 19.20/3.64 % (4006697)------------------------------
% 19.20/3.64 % (4006697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/3.64 % (4006697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.64 % (4006697)CaDiCaL version: 2.1.3
% 19.20/3.64 % (4006697)Termination reason: Instruction limit
% 19.20/3.64 % (4006697)Termination phase: Saturation
% 19.20/3.64 % (4006697)Time elapsed: 0.178 s
% 19.20/3.64 % (4006697)Peak memory usage: 91 MB
% 19.20/3.64 % (4006697)Instructions burned: 285 (million)
% 19.20/3.64 % (4006703)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=138019432:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.20/3.64 % (4006698)------------------------------
% 19.20/3.64 % (4006698)------------------------------
% 19.20/3.64 % (4006699)------------------------------
% 19.20/3.64 % (4006699)------------------------------
% 19.20/3.64 % (4006705)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=162140028:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 19.20/3.64 % (4006703)Instruction limit reached!
% 19.20/3.64 % (4006703)------------------------------
% 19.20/3.64 % (4006703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/3.64 % (4006703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.64 % (4006703)CaDiCaL version: 2.1.3
% 19.20/3.64 % (4006703)Termination reason: Instruction limit
% 19.20/3.64 % (4006703)Termination phase: Saturation
% 19.20/3.64 % (4006703)Time elapsed: 0.136 s
% 19.20/3.64 % (4006703)Peak memory usage: 91 MB
% 19.20/3.64 % (4006703)Instructions burned: 248 (million)
% 19.20/3.64 % (4006705)Refutation not found, incomplete strategy
% 19.20/3.64 % (4006705)------------------------------
% 19.20/3.64 % (4006705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/3.64 % (4006705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.64 % (4006705)CaDiCaL version: 2.1.3
% 19.20/3.64 % (4006705)Termination reason: Refutation not found, incomplete strategy
% 19.20/3.64 % (4006705)Time elapsed: 0.015 s
% 19.20/3.64 % (4006705)Peak memory usage: 89 MB
% 19.20/3.64 % (4006705)Instructions burned: 28 (million)
% 19.20/3.64 % (4006706)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3167759991:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.20/3.64 % (4006707)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=509966906:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 19.20/3.64 % (4006707)Instruction limit reached!
% 19.20/3.64 % (4006707)------------------------------
% 19.20/3.64 % (4006707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.20/3.64 % (4006707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.20/3.64 % (4006707)CaDiCaL version: 2.1.3
% 19.20/3.64 % (4006707)Termination reason: Instruction limit
% 19.20/3.64 % (4006707)Termination phase: Saturation
% 19.20/3.64 % (4006707)Time elapsed: 0.055 s
% 19.20/3.64 % (4006707)Peak memory usage: 89 MB
% 19.20/3.64 % (4006707)Instructions burned: 113 (million)
% 19.20/3.64 % (4006709)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2956000478:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 19.20/3.64 % (4006709)Instruction limit reached!
% 19.20/3.64 % (4006709)------------------------------
% 19.20/3.64 % (4006709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006709)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006709)Termination reason: Instruction limit
% 40.98/6.66 % (4006709)Termination phase: Saturation
% 40.98/6.66 % (4006709)Time elapsed: 0.057 s
% 40.98/6.66 % (4006709)Peak memory usage: 89 MB
% 40.98/6.66 % (4006709)Instructions burned: 127 (million)
% 40.98/6.66 % (4006705)------------------------------
% 40.98/6.66 % (4006705)------------------------------
% 40.98/6.66 % (4006713)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2013200246:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 40.98/6.66 % (4006714)lrs+10_1_sil=8000:sp=occurrence:random_seed=4082322702:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 40.98/6.66 % (4006713)Instruction limit reached!
% 40.98/6.66 % (4006713)------------------------------
% 40.98/6.66 % (4006713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006713)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006713)Termination reason: Instruction limit
% 40.98/6.66 % (4006713)Termination phase: Saturation
% 40.98/6.66 % (4006713)Time elapsed: 0.058 s
% 40.98/6.66 % (4006713)Peak memory usage: 89 MB
% 40.98/6.66 % (4006713)Instructions burned: 116 (million)
% 40.98/6.66 % (4006715)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4068822799:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 40.98/6.66 % (4006715)Refutation not found, incomplete strategy
% 40.98/6.66 % (4006715)------------------------------
% 40.98/6.66 % (4006715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006715)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006715)Termination reason: Refutation not found, incomplete strategy
% 40.98/6.66 % (4006715)Time elapsed: 0.051 s
% 40.98/6.66 % (4006715)Peak memory usage: 90 MB
% 40.98/6.66 % (4006715)Instructions burned: 102 (million)
% 40.98/6.66 % (4006718)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3434573902:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 40.98/6.66 % (4006715)------------------------------
% 40.98/6.66 % (4006715)------------------------------
% 40.98/6.66 % (4006722)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=588283090:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 40.98/6.66 % (4006722)Instruction limit reached!
% 40.98/6.66 % (4006722)------------------------------
% 40.98/6.66 % (4006722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006722)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006722)Termination reason: Instruction limit
% 40.98/6.66 % (4006722)Termination phase: Saturation
% 40.98/6.66 % (4006722)Time elapsed: 0.074 s
% 40.98/6.66 % (4006722)Peak memory usage: 90 MB
% 40.98/6.66 % (4006722)Instructions burned: 135 (million)
% 40.98/6.66 % (4006714)Instruction limit reached!
% 40.98/6.66 % (4006714)------------------------------
% 40.98/6.66 % (4006714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006714)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006714)Termination reason: Instruction limit
% 40.98/6.66 % (4006714)Termination phase: Saturation
% 40.98/6.66 % (4006714)Time elapsed: 0.541 s
% 40.98/6.66 % (4006714)Peak memory usage: 95 MB
% 40.98/6.66 % (4006714)Instructions burned: 907 (million)
% 40.98/6.66 % (4006725)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4242230520:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 40.98/6.66 % (4006724)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2153534441:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 40.98/6.66 % (4006724)Refutation not found, incomplete strategy
% 40.98/6.66 % (4006724)------------------------------
% 40.98/6.66 % (4006724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.98/6.66 % (4006724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.98/6.66 % (4006724)CaDiCaL version: 2.1.3
% 40.98/6.66 % (4006724)Termination reason: Refutation not found, incomplete strategy
% 80.27/12.14 % (4006724)Time elapsed: 0.033 s
% 80.27/12.14 % (4006724)Peak memory usage: 89 MB
% 80.27/12.14 % (4006724)Instructions burned: 71 (million)
% 80.27/12.14 % (4006724)------------------------------
% 80.27/12.14 % (4006724)------------------------------
% 80.27/12.14 % (4006728)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1848244349:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 80.27/12.14 % (4006706)Instruction limit reached!
% 80.27/12.14 % (4006706)------------------------------
% 80.27/12.14 % (4006706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.27/12.14 % (4006706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.27/12.14 % (4006706)CaDiCaL version: 2.1.3
% 80.27/12.14 % (4006706)Termination reason: Instruction limit
% 80.27/12.14 % (4006706)Termination phase: Saturation
% 80.27/12.14 % (4006706)Time elapsed: 1.350 s
% 80.27/12.14 % (4006706)Peak memory usage: 144 MB
% 80.27/12.14 % (4006706)Instructions burned: 2350 (million)
% 80.27/12.14 % (4006728)Instruction limit reached!
% 80.27/12.14 % (4006728)------------------------------
% 80.27/12.14 % (4006728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.27/12.14 % (4006728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.27/12.14 % (4006728)CaDiCaL version: 2.1.3
% 80.27/12.14 % (4006728)Termination reason: Instruction limit
% 80.27/12.14 % (4006728)Termination phase: Saturation
% 80.27/12.14 % (4006728)Time elapsed: 0.068 s
% 80.27/12.14 % (4006728)Peak memory usage: 90 MB
% 80.27/12.14 % (4006728)Instructions burned: 125 (million)
% 80.27/12.14 % (4006730)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2103502363:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 80.27/12.14 % (4006731)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=250478880:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 80.27/12.14 % (4006730)Instruction limit reached!
% 80.27/12.14 % (4006730)------------------------------
% 80.27/12.14 % (4006730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.27/12.14 % (4006730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.27/12.14 % (4006730)CaDiCaL version: 2.1.3
% 80.27/12.14 % (4006730)Termination reason: Instruction limit
% 80.27/12.14 % (4006730)Termination phase: Saturation
% 80.27/12.14 % (4006730)Time elapsed: 0.066 s
% 80.27/12.14 % (4006730)Peak memory usage: 91 MB
% 80.27/12.14 % (4006730)Instructions burned: 134 (million)
% 80.27/12.14 % (4006731)Instruction limit reached!
% 80.27/12.14 % (4006731)------------------------------
% 80.27/12.14 % (4006731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.27/12.14 % (4006731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.27/12.14 % (4006731)CaDiCaL version: 2.1.3
% 80.27/12.14 % (4006731)Termination reason: Instruction limit
% 80.27/12.14 % (4006731)Termination phase: Saturation
% 80.27/12.14 % (4006731)Time elapsed: 0.054 s
% 80.27/12.14 % (4006731)Peak memory usage: 89 MB
% 80.27/12.14 % (4006731)Instructions burned: 142 (million)
% 80.27/12.14 % (4006734)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2924961053:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 80.27/12.14 % (4006734)Refutation not found, incomplete strategy
% 80.27/12.14 % (4006734)------------------------------
% 80.27/12.14 % (4006734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.27/12.14 % (4006734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.27/12.14 % (4006734)CaDiCaL version: 2.1.3
% 80.27/12.14 % (4006734)Termination reason: Refutation not found, incomplete strategy
% 80.27/12.14 % (4006734)Time elapsed: 0.003 s
% 80.27/12.14 % (4006734)Peak memory usage: 88 MB
% 80.27/12.14 % (4006734)Instructions burned: 3 (million)
% 80.27/12.14 % (4006735)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1448959781:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 80.27/12.14 % (4006734)------------------------------
% 80.27/12.14 % (4006734)------------------------------
% 80.27/12.14 % (4006738)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2411305336:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 104.09/15.56 % (4006738)Instruction limit reached!
% 104.09/15.56 % (4006738)------------------------------
% 104.09/15.56 % (4006738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006738)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006738)Termination reason: Instruction limit
% 104.09/15.56 % (4006738)Termination phase: Saturation
% 104.09/15.56 % (4006738)Time elapsed: 0.086 s
% 104.09/15.56 % (4006738)Peak memory usage: 91 MB
% 104.09/15.56 % (4006738)Instructions burned: 150 (million)
% 104.09/15.56 % (4006740)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1083915467:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 104.09/15.56 % (4006718)Instruction limit reached!
% 104.09/15.56 % (4006718)------------------------------
% 104.09/15.56 % (4006718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006718)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006718)Termination reason: Instruction limit
% 104.09/15.56 % (4006718)Termination phase: Saturation
% 104.09/15.56 % (4006718)Time elapsed: 3.045 s
% 104.09/15.56 % (4006718)Peak memory usage: 162 MB
% 104.09/15.56 % (4006718)Instructions burned: 5203 (million)
% 104.09/15.56 % (4006742)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1126164224:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi)
% 104.09/15.56 % (4006742)Refutation not found, incomplete strategy
% 104.09/15.56 % (4006742)------------------------------
% 104.09/15.56 % (4006742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006742)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006742)Termination reason: Refutation not found, incomplete strategy
% 104.09/15.56 % (4006742)Time elapsed: 0.055 s
% 104.09/15.56 % (4006742)Peak memory usage: 90 MB
% 104.09/15.56 % (4006742)Instructions burned: 115 (million)
% 104.09/15.56 % (4006742)------------------------------
% 104.09/15.56 % (4006742)------------------------------
% 104.09/15.56 % (4006744)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1299690812:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 104.09/15.56 % (4006744)Instruction limit reached!
% 104.09/15.56 % (4006744)------------------------------
% 104.09/15.56 % (4006744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006744)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006744)Termination reason: Instruction limit
% 104.09/15.56 % (4006744)Termination phase: Saturation
% 104.09/15.56 % (4006744)Time elapsed: 0.084 s
% 104.09/15.56 % (4006744)Peak memory usage: 90 MB
% 104.09/15.56 % (4006744)Instructions burned: 187 (million)
% 104.09/15.56 % (4006746)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=930082347:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/193Mi)
% 104.09/15.56 % (4006746)Instruction limit reached!
% 104.09/15.56 % (4006746)------------------------------
% 104.09/15.56 % (4006746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006746)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006746)Termination reason: Instruction limit
% 104.09/15.56 % (4006746)Termination phase: Saturation
% 104.09/15.56 % (4006746)Time elapsed: 0.121 s
% 104.09/15.56 % (4006746)Peak memory usage: 91 MB
% 104.09/15.56 % (4006746)Instructions burned: 194 (million)
% 104.09/15.56 % (4006748)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4026240692:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2949 on theBenchmark for (2949ds/4850Mi)
% 104.09/15.56 % (4006735)Instruction limit reached!
% 104.09/15.56 % (4006735)------------------------------
% 104.09/15.56 % (4006735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.09/15.56 % (4006735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.09/15.56 % (4006735)CaDiCaL version: 2.1.3
% 104.09/15.56 % (4006735)Termination reason: Instruction limit
% 104.09/15.56 % (4006735)Termination phase: Saturation
% 137.53/20.27 % (4006735)Time elapsed: 3.370 s
% 137.53/20.27 % (4006735)Peak memory usage: 181 MB
% 137.53/20.27 % (4006735)Instructions burned: 6062 (million)
% 137.53/20.27 % (4006750)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=692649719:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 137.53/20.27 % (4006748)Instruction limit reached!
% 137.53/20.27 % (4006748)------------------------------
% 137.53/20.27 % (4006748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.53/20.27 % (4006748)CaDiCaL version: 2.1.3
% 137.53/20.27 % (4006748)Termination reason: Instruction limit
% 137.53/20.27 % (4006748)Termination phase: Saturation
% 137.53/20.27 % (4006748)Time elapsed: 2.929 s
% 137.53/20.27 % (4006748)Peak memory usage: 128 MB
% 137.53/20.27 % (4006748)Instructions burned: 4850 (million)
% 137.53/20.27 % (4006752)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3530844656:i=319:kws=precedence:fsr=off_2918 on theBenchmark for (2918ds/319Mi)
% 137.53/20.27 % (4006752)Instruction limit reached!
% 137.53/20.27 % (4006752)------------------------------
% 137.53/20.27 % (4006752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.53/20.27 % (4006752)CaDiCaL version: 2.1.3
% 137.53/20.27 % (4006752)Termination reason: Instruction limit
% 137.53/20.27 % (4006752)Termination phase: Saturation
% 137.53/20.27 % (4006752)Time elapsed: 0.189 s
% 137.53/20.27 % (4006752)Peak memory usage: 94 MB
% 137.53/20.27 % (4006752)Instructions burned: 320 (million)
% 137.53/20.27 % (4006754)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2591820655:i=2064:ep=RST_2915 on theBenchmark for (2915ds/2064Mi)
% 137.53/20.27 % (4006754)Refutation not found, incomplete strategy
% 137.53/20.27 % (4006754)------------------------------
% 137.53/20.27 % (4006754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.53/20.27 % (4006754)CaDiCaL version: 2.1.3
% 137.53/20.27 % (4006754)Termination reason: Refutation not found, incomplete strategy
% 137.53/20.27 % (4006754)Time elapsed: 0.040 s
% 137.53/20.27 % (4006754)Peak memory usage: 89 MB
% 137.53/20.27 % (4006754)Instructions burned: 87 (million)
% 137.53/20.27 % (4006754)------------------------------
% 137.53/20.27 % (4006754)------------------------------
% 137.53/20.27 % (4006756)dis-1011_128_sil=32000:random_seed=1650551084:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 137.53/20.27 % (4006725)Instruction limit reached!
% 137.53/20.27 % (4006725)------------------------------
% 137.53/20.27 % (4006725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.53/20.27 % (4006725)CaDiCaL version: 2.1.3
% 137.53/20.27 % (4006725)Termination reason: Instruction limit
% 137.53/20.27 % (4006725)Termination phase: Saturation
% 137.53/20.27 % (4006725)Time elapsed: 7.374 s
% 137.53/20.27 % (4006725)Peak memory usage: 230 MB
% 137.53/20.27 % (4006725)Instructions burned: 13194 (million)
% 137.53/20.27 % (4006758)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=968896780:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2909 on theBenchmark for (2909ds/757Mi)
% 137.53/20.27 % (4006758)Refutation not found, incomplete strategy
% 137.53/20.27 % (4006758)------------------------------
% 137.53/20.27 % (4006758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.53/20.27 % (4006758)CaDiCaL version: 2.1.3
% 137.53/20.27 % (4006758)Termination reason: Refutation not found, incomplete strategy
% 137.53/20.27 % (4006758)Time elapsed: 0.011 s
% 137.53/20.27 % (4006758)Peak memory usage: 89 MB
% 137.53/20.27 % (4006758)Instructions burned: 19 (million)
% 137.53/20.27 % (4006758)------------------------------
% 137.53/20.27 % (4006758)------------------------------
% 137.53/20.27 % (4006760)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3459740500:i=13913:ss=axioms:sgt=8_2905 on theBenchmark for (2905ds/13913Mi)
% 137.53/20.27 % (4006756)Instruction limit reached!
% 137.53/20.27 % (4006756)------------------------------
% 137.53/20.27 % (4006756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.53/20.27 % (4006756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006756)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006756)Termination reason: Instruction limit
% 155.05/22.70 % (4006756)Termination phase: Saturation
% 155.05/22.70 % (4006756)Time elapsed: 2.301 s
% 155.05/22.70 % (4006756)Peak memory usage: 122 MB
% 155.05/22.70 % (4006756)Instructions burned: 3706 (million)
% 155.05/22.70 % (4006740)Instruction limit reached!
% 155.05/22.70 % (4006740)------------------------------
% 155.05/22.70 % (4006740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.05/22.70 % (4006740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006740)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006740)Termination reason: Instruction limit
% 155.05/22.70 % (4006740)Termination phase: Saturation
% 155.05/22.70 % (4006740)Time elapsed: 8.408 s
% 155.05/22.70 % (4006740)Peak memory usage: 229 MB
% 155.05/22.70 % (4006740)Instructions burned: 14156 (million)
% 155.05/22.70 % (4006762)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2811336574:i=9925:aac=none_2886 on theBenchmark for (2886ds/9925Mi)
% 155.05/22.70 % (4006764)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3231497819:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2885 on theBenchmark for (2885ds/2479Mi)
% 155.05/22.70 % (4006764)Refutation not found, incomplete strategy
% 155.05/22.70 % (4006764)------------------------------
% 155.05/22.70 % (4006764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.05/22.70 % (4006764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006764)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006764)Termination reason: Refutation not found, incomplete strategy
% 155.05/22.70 % (4006764)Time elapsed: 0.009 s
% 155.05/22.70 % (4006764)Peak memory usage: 89 MB
% 155.05/22.70 % (4006764)Instructions burned: 12 (million)
% 155.05/22.70 % (4006764)------------------------------
% 155.05/22.70 % (4006764)------------------------------
% 155.05/22.70 % (4006766)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=373846863:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2881 on theBenchmark for (2881ds/440Mi)
% 155.05/22.70 % (4006766)Instruction limit reached!
% 155.05/22.70 % (4006766)------------------------------
% 155.05/22.70 % (4006766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.05/22.70 % (4006766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006766)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006766)Termination reason: Instruction limit
% 155.05/22.70 % (4006766)Termination phase: Saturation
% 155.05/22.70 % (4006766)Time elapsed: 0.228 s
% 155.05/22.70 % (4006766)Peak memory usage: 94 MB
% 155.05/22.70 % (4006766)Instructions burned: 440 (million)
% 155.05/22.70 % (4006768)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4206731621:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2878 on theBenchmark for (2878ds/11145Mi)
% 155.05/22.70 % (4006750)Instruction limit reached!
% 155.05/22.70 % (4006750)------------------------------
% 155.05/22.70 % (4006750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.05/22.70 % (4006750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006750)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006750)Termination reason: Instruction limit
% 155.05/22.70 % (4006750)Termination phase: Saturation
% 155.05/22.70 % (4006750)Time elapsed: 6.747 s
% 155.05/22.70 % (4006750)Peak memory usage: 236 MB
% 155.05/22.70 % (4006750)Instructions burned: 12111 (million)
% 155.05/22.70 % (4006770)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=79916588:cts=off:i=3034:av=off:er=known:fsd=on_2872 on theBenchmark for (2872ds/3034Mi)
% 155.05/22.70 % (4006770)Instruction limit reached!
% 155.05/22.70 % (4006770)------------------------------
% 155.05/22.70 % (4006770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.05/22.70 % (4006770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.05/22.70 % (4006770)CaDiCaL version: 2.1.3
% 155.05/22.70 % (4006770)Termination reason: Instruction limit
% 155.05/22.70 % (4006770)Termination phase: Saturation
% 155.05/22.70 % (4006770)Time elapsed: 1.741 s
% 155.05/22.70 % (4006770)Peak memory usage: 148 MB
% 155.05/22.70 % (4006770)Instructions burned: 3036 (million)
% 155.05/22.70 % (4006772)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1938122136:st=2:s2a=on:i=524:s2at=2:ss=axioms_2854 on theBenchmark for (2854ds/524Mi)
% 184.53/26.91 % (4006772)Instruction limit reached!
% 184.53/26.91 % (4006772)------------------------------
% 184.53/26.91 % (4006772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006772)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006772)Termination reason: Instruction limit
% 184.53/26.91 % (4006772)Termination phase: Saturation
% 184.53/26.91 % (4006772)Time elapsed: 0.270 s
% 184.53/26.91 % (4006772)Peak memory usage: 92 MB
% 184.53/26.91 % (4006772)Instructions burned: 524 (million)
% 184.53/26.91 % (4006774)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=370925647:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2850 on theBenchmark for (2850ds/1016Mi)
% 184.53/26.91 % (4006774)Refutation not found, incomplete strategy
% 184.53/26.91 % (4006774)------------------------------
% 184.53/26.91 % (4006774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006774)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006774)Termination reason: Refutation not found, incomplete strategy
% 184.53/26.91 % (4006774)Time elapsed: 0.005 s
% 184.53/26.91 % (4006774)Peak memory usage: 89 MB
% 184.53/26.91 % (4006774)Instructions burned: 5 (million)
% 184.53/26.91 % (4006774)------------------------------
% 184.53/26.91 % (4006774)------------------------------
% 184.53/26.91 % (4006776)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=728526122:i=14123:bd=preordered:ins=4_2846 on theBenchmark for (2846ds/14123Mi)
% 184.53/26.91 % (4006762)Instruction limit reached!
% 184.53/26.91 % (4006762)------------------------------
% 184.53/26.91 % (4006762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006762)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006762)Termination reason: Instruction limit
% 184.53/26.91 % (4006762)Termination phase: Saturation
% 184.53/26.91 % (4006762)Time elapsed: 5.382 s
% 184.53/26.91 % (4006762)Peak memory usage: 206 MB
% 184.53/26.91 % (4006762)Instructions burned: 9926 (million)
% 184.53/26.91 % (4006778)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=826387253:i=5781:kws=precedence:bd=all:rawr=on_2831 on theBenchmark for (2831ds/5781Mi)
% 184.53/26.91 % (4006760)Instruction limit reached!
% 184.53/26.91 % (4006760)------------------------------
% 184.53/26.91 % (4006760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006760)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006760)Termination reason: Instruction limit
% 184.53/26.91 % (4006760)Termination phase: Saturation
% 184.53/26.91 % (4006760)Time elapsed: 8.385 s
% 184.53/26.91 % (4006760)Peak memory usage: 230 MB
% 184.53/26.91 % (4006760)Instructions burned: 13914 (million)
% 184.53/26.91 % (4006780)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=305757838:i=2448:gtgl=5:bd=preordered:gtg=all_2820 on theBenchmark for (2820ds/2448Mi)
% 184.53/26.91 % (4006768)Instruction limit reached!
% 184.53/26.91 % (4006768)------------------------------
% 184.53/26.91 % (4006768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006768)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006768)Termination reason: Instruction limit
% 184.53/26.91 % (4006768)Termination phase: Saturation
% 184.53/26.91 % (4006768)Time elapsed: 6.830 s
% 184.53/26.91 % (4006768)Peak memory usage: 207 MB
% 184.53/26.91 % (4006768)Instructions burned: 11145 (million)
% 184.53/26.91 % (4006782)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=274958785:i=3223:kws=precedence:fgj=on:av=off_2808 on theBenchmark for (2808ds/3223Mi)
% 184.53/26.91 % (4006780)Instruction limit reached!
% 184.53/26.91 % (4006780)------------------------------
% 184.53/26.91 % (4006780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 184.53/26.91 % (4006780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 184.53/26.91 % (4006780)CaDiCaL version: 2.1.3
% 184.53/26.91 % (4006780)Termination reason: Instruction limit
% 184.53/26.91 % (4006780)Termination phase: Saturation
% 107.85/28.66 % (4006780)Time elapsed: 1.345 s
% 107.85/28.66 % (4006780)Peak memory usage: 146 MB
% 107.85/28.66 % (4006780)Instructions burned: 2449 (million)
% 107.85/28.66 % (4006778)Instruction limit reached!
% 107.85/28.66 % (4006778)------------------------------
% 107.85/28.66 % (4006778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006778)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006778)Termination reason: Instruction limit
% 107.85/28.66 % (4006778)Termination phase: Saturation
% 107.85/28.66 % (4006778)Time elapsed: 2.590 s
% 107.85/28.66 % (4006778)Peak memory usage: 112 MB
% 107.85/28.66 % (4006778)Instructions burned: 5781 (million)
% 107.85/28.66 % (4006784)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=282038448:st=5.6:i=2033:sd=3:ss=axioms_2805 on theBenchmark for (2805ds/2033Mi)
% 107.85/28.66 % (4006786)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3634252403:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2804 on theBenchmark for (2804ds/2055Mi)
% 107.85/28.66 % (4006784)Refutation not found, incomplete strategy
% 107.85/28.66 % (4006784)------------------------------
% 107.85/28.66 % (4006784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006784)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006784)Termination reason: Refutation not found, incomplete strategy
% 107.85/28.66 % (4006784)Time elapsed: 0.644 s
% 107.85/28.66 % (4006784)Peak memory usage: 137 MB
% 107.85/28.66 % (4006784)Instructions burned: 996 (million)
% 107.85/28.66 % (4006784)------------------------------
% 107.85/28.66 % (4006784)------------------------------
% 107.85/28.66 % (4006788)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1002650572:i=21611:sd=3:ss=axioms_2795 on theBenchmark for (2795ds/21611Mi)
% 107.85/28.66 % (4006786)Instruction limit reached!
% 107.85/28.66 % (4006786)------------------------------
% 107.85/28.66 % (4006786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006786)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006786)Termination reason: Instruction limit
% 107.85/28.66 % (4006786)Termination phase: Saturation
% 107.85/28.66 % (4006786)Time elapsed: 1.280 s
% 107.85/28.66 % (4006786)Peak memory usage: 140 MB
% 107.85/28.66 % (4006786)Instructions burned: 2055 (million)
% 107.85/28.66 % (4006782)Instruction limit reached!
% 107.85/28.66 % (4006782)------------------------------
% 107.85/28.66 % (4006782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006782)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006782)Termination reason: Instruction limit
% 107.85/28.66 % (4006782)Termination phase: Saturation
% 107.85/28.66 % (4006782)Time elapsed: 1.790 s
% 107.85/28.66 % (4006782)Peak memory usage: 154 MB
% 107.85/28.66 % (4006782)Instructions burned: 3223 (million)
% 107.85/28.66 % (4006790)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=462492943:i=4835:sd=13:ss=axioms:sgt=23_2790 on theBenchmark for (2790ds/4835Mi)
% 107.85/28.66 % (4006791)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=49476592:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2789 on theBenchmark for (2789ds/797Mi)
% 107.85/28.66 % (4006791)Instruction limit reached!
% 107.85/28.66 % (4006791)------------------------------
% 107.85/28.66 % (4006791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006791)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006791)Termination reason: Instruction limit
% 107.85/28.66 % (4006791)Termination phase: Saturation
% 107.85/28.66 % (4006791)Time elapsed: 0.433 s
% 107.85/28.66 % (4006791)Peak memory usage: 93 MB
% 107.85/28.66 % (4006791)Instructions burned: 799 (million)
% 107.85/28.66 % (4006794)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1351874560:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2783 on theBenchmark for (2783ds/2326Mi)
% 107.85/28.66 % (4006794)Refutation not found, incomplete strategy
% 107.85/28.66 % (4006794)------------------------------
% 107.85/28.66 % (4006794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006794)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006794)Termination reason: Refutation not found, incomplete strategy
% 107.85/28.66 % (4006794)Time elapsed: 0.099 s
% 107.85/28.66 % (4006794)Peak memory usage: 91 MB
% 107.85/28.66 % (4006794)Instructions burned: 181 (million)
% 107.85/28.66 % (4006794)------------------------------
% 107.85/28.66 % (4006794)------------------------------
% 107.85/28.66 % (4006796)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1243622182:i=6038:nm=6_2779 on theBenchmark for (2779ds/6038Mi)
% 107.85/28.66 % (4006790)Instruction limit reached!
% 107.85/28.66 % (4006790)------------------------------
% 107.85/28.66 % (4006790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006790)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006790)Termination reason: Instruction limit
% 107.85/28.66 % (4006790)Termination phase: Saturation
% 107.85/28.66 % (4006790)Time elapsed: 2.760 s
% 107.85/28.66 % (4006790)Peak memory usage: 119 MB
% 107.85/28.66 % (4006790)Instructions burned: 4836 (million)
% 107.85/28.66 % (4006776)Instruction limit reached!
% 107.85/28.66 % (4006776)------------------------------
% 107.85/28.66 % (4006776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006776)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006776)Termination reason: Instruction limit
% 107.85/28.66 % (4006776)Termination phase: Saturation
% 107.85/28.66 % (4006776)Time elapsed: 8.438 s
% 107.85/28.66 % (4006776)Peak memory usage: 240 MB
% 107.85/28.66 % (4006776)Instructions burned: 14124 (million)
% 107.85/28.66 % (4006798)lrs+10_1_sil=32000:sp=occurrence:random_seed=1377069656:st=2:i=33334:sd=3:ss=included:sgt=32_2761 on theBenchmark for (2761ds/33334Mi)
% 107.85/28.66 % (4006799)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3223269659:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2760 on theBenchmark for (2760ds/1008Mi)
% 107.85/28.66 % (4006799)Instruction limit reached!
% 107.85/28.66 % (4006799)------------------------------
% 107.85/28.66 % (4006799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006799)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006799)Termination reason: Instruction limit
% 107.85/28.66 % (4006799)Termination phase: Saturation
% 107.85/28.66 % (4006799)Time elapsed: 0.548 s
% 107.85/28.66 % (4006799)Peak memory usage: 98 MB
% 107.85/28.66 % (4006799)Instructions burned: 1008 (million)
% 107.85/28.66 % (4006802)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=604107102:i=8327:s2at=5:bd=preordered_2753 on theBenchmark for (2753ds/8327Mi)
% 107.85/28.66 % (4006796)Instruction limit reached!
% 107.85/28.66 % (4006796)------------------------------
% 107.85/28.66 % (4006796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006796)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006796)Termination reason: Instruction limit
% 107.85/28.66 % (4006796)Termination phase: Saturation
% 107.85/28.66 % (4006796)Time elapsed: 3.266 s
% 107.85/28.66 % (4006796)Peak memory usage: 170 MB
% 107.85/28.66 % (4006796)Instructions burned: 6040 (million)
% 107.85/28.66 % (4006804)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1670702773:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2745 on theBenchmark for (2745ds/1083Mi)
% 107.85/28.66 % (4006804)Instruction limit reached!
% 107.85/28.66 % (4006804)------------------------------
% 107.85/28.66 % (4006804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006804)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006804)Termination reason: Instruction limit
% 107.85/28.66 % (4006804)Termination phase: Saturation
% 107.85/28.66 % (4006804)Time elapsed: 0.427 s
% 107.85/28.66 % (4006804)Peak memory usage: 92 MB
% 107.85/28.66 % (4006804)Instructions burned: 1083 (million)
% 107.85/28.66 % (4006806)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1213900219:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2739 on theBenchmark for (2739ds/1084Mi)
% 107.85/28.66 % (4006806)Instruction limit reached!
% 107.85/28.66 % (4006806)------------------------------
% 107.85/28.66 % (4006806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.85/28.66 % (4006806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.85/28.66 % (4006806)CaDiCaL version: 2.1.3
% 107.85/28.66 % (4006806)Termination reason: Instruction limit
% 107.85/28.66 % (4006806)Termination phase: Saturation
% 107.85/28.66 % (4006806)Time elapsed: 0.362 s
% 107.85/28.66 % (4006806)Peak memory usage: 89 MB
% 107.85/28.66 % (4006806)Instructions burned: 1085 (million)
% 107.85/28.66 % (4006808)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2122366257:i=6995:s2at=5:gtg=all_2734 on theBenchmark for (2734ds/6995Mi)
% 107.85/28.66 % (4006788)First to succeed.
% 107.85/28.66 % (4006788)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4006678"
% 107.85/28.66 % (4006788)Refutation found. Thanks to Tanya!
% 107.85/28.66 % SZS status Theorem for theBenchmark
% 107.85/28.66 % SZS output start Proof for theBenchmark
% See solution above
% 197.42/28.85 % (4006788)------------------------------
% 197.42/28.85 % (4006788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.42/28.85 % (4006788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.42/28.85 % (4006788)CaDiCaL version: 2.1.3
% 197.42/28.85 % (4006788)Termination reason: Refutation
% 197.42/28.85 % (4006788)Time elapsed: 6.899 s
% 197.42/28.85 % (4006788)Peak memory usage: 195 MB
% 197.42/28.85 % (4006788)Instructions burned: 11760 (million)
% 197.42/28.85 % (4006788)------------------------------
% 197.42/28.85 % (4006788)------------------------------
% 197.42/28.85 % (4006678)Success in time 27.812 s
% 197.42/28.85 % Vampire exiting
%------------------------------------------------------------------------------