%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT084-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:53 PM UTC 2026
% Result : Unsatisfiable 139.76s 29.41s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 45
% Syntax : Number of formulae : 249 ( 107 unt; 27 def)
% Number of atoms : 435 ( 166 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 327 ( 141 ~; 182 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-3 aty)
% Number of functors : 50 ( 50 usr; 33 con; 0-5 aty)
% Number of variables : 213 ( 0 sgn 213 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0,X1] : hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),X0) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Diff__cancel_0) ).
fof(f8,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),X0),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Compl__eq__Diff__UNIV_0) ).
fof(f21,axiom,
! [X0,X1] : hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__Diff_0) ).
fof(f22,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X1),
inference(reorient_equations,[],[f21]) ).
fof(f125,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X2,tc_fun(X1,tc_bool))
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,tc_fun(X1,tc_bool)),X2) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Int__absorb2_0) ).
fof(f133,axiom,
! [X2,X0,X1] : c_lessequals(hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),X2),X0,tc_fun(X1,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Diff__subset_0) ).
fof(f173,axiom,
! [X0,X1] : hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Diff__UNIV_0) ).
fof(f174,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool))),
inference(reorient_equations,[],[f173]) ).
fof(f205,axiom,
! [X0,X1] : hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,tc_fun(X1,tc_bool)),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Int__absorb_0) ).
fof(f475,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBK__def_0) ).
fof(f594,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f618,axiom,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_double__complement_0) ).
fof(f630,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2)))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplI_0) ).
fof(f631,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f771,negated_conjecture,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X1,X0)),X1))
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_UNIV__eq__I_0) ).
fof(f850,axiom,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_top1I_0) ).
fof(f859,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f860,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f864,axiom,
hBOOL(hAPP(hAPP(c_in(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),v_Lab____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f869,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(v_F,hAPP(c_COMBC(hAPP(c_COMBC(c_COMBB(c_HOL_OIf(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),hAPP(c_COMBC(c_COMBB(c_HOL_Oord__class_Oless(tc_nat),v_h____,tc_nat,tc_fun(tc_nat,tc_bool),tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,tc_nat,tc_bool),c_Finite__Set_Ocard(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool)),tc_Arrow__Order__Mirabelle_Oindi)),tc_bool,tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_Lab____),tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_Lba____)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f912,definition,
sF0 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f913,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f912]) ).
fof(f914,definition,
sF1 = tc_fun(sF0,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f915,plain,
tc_fun(sF0,tc_bool) = sF1,
inference(reorient_equations,[],[f914]) ).
fof(f916,definition,
sF2 = c_HOL_OIf(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f917,plain,
c_HOL_OIf(sF1) = sF2,
inference(reorient_equations,[],[f916]) ).
fof(f918,definition,
sF3 = c_HOL_Oord__class_Oless(tc_nat),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f919,plain,
c_HOL_Oord__class_Oless(tc_nat) = sF3,
inference(reorient_equations,[],[f918]) ).
fof(f924,definition,
sF6 = tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f925,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_bool) = sF6,
inference(reorient_equations,[],[f924]) ).
fof(f926,definition,
sF7 = c_Orderings_Otop__class_Otop(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f927,plain,
c_Orderings_Otop__class_Otop(sF6) = sF7,
inference(reorient_equations,[],[f926]) ).
fof(f928,definition,
sF8 = c_Finite__Set_Ocard(sF7,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f929,plain,
c_Finite__Set_Ocard(sF7,tc_Arrow__Order__Mirabelle_Oindi) = sF8,
inference(reorient_equations,[],[f928]) ).
fof(f939,definition,
sF13 = c_in(sF0),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f940,plain,
c_in(sF0) = sF13,
inference(reorient_equations,[],[f939]) ).
fof(f941,definition,
sF14 = c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f942,plain,
c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF14,
inference(reorient_equations,[],[f941]) ).
fof(f943,definition,
sF15 = hAPP(sF13,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f944,plain,
hAPP(sF13,sF14) = sF15,
inference(reorient_equations,[],[f943]) ).
fof(f945,definition,
sF16 = tc_fun(tc_nat,tc_bool),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f946,plain,
tc_fun(tc_nat,tc_bool) = sF16,
inference(reorient_equations,[],[f945]) ).
fof(f947,definition,
sF17 = c_COMBB(sF3,v_h____,tc_nat,sF16,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f948,plain,
c_COMBB(sF3,v_h____,tc_nat,sF16,tc_Arrow__Order__Mirabelle_Oindi) = sF17,
inference(reorient_equations,[],[f947]) ).
fof(f949,definition,
sF18 = c_COMBC(sF17,tc_Arrow__Order__Mirabelle_Oindi,tc_nat,tc_bool),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f950,plain,
c_COMBC(sF17,tc_Arrow__Order__Mirabelle_Oindi,tc_nat,tc_bool) = sF18,
inference(reorient_equations,[],[f949]) ).
fof(f951,definition,
sF19 = hAPP(sF18,sF8),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f952,plain,
hAPP(sF18,sF8) = sF19,
inference(reorient_equations,[],[f951]) ).
fof(f953,definition,
sF20 = tc_fun(sF1,sF1),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f954,plain,
tc_fun(sF1,sF1) = sF20,
inference(reorient_equations,[],[f953]) ).
fof(f955,definition,
sF21 = tc_fun(sF1,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f956,plain,
tc_fun(sF1,sF20) = sF21,
inference(reorient_equations,[],[f955]) ).
fof(f957,definition,
sF22 = c_COMBB(sF2,sF19,tc_bool,sF21,tc_Arrow__Order__Mirabelle_Oindi),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f958,plain,
c_COMBB(sF2,sF19,tc_bool,sF21,tc_Arrow__Order__Mirabelle_Oindi) = sF22,
inference(reorient_equations,[],[f957]) ).
fof(f959,definition,
sF23 = c_COMBC(sF22,tc_Arrow__Order__Mirabelle_Oindi,sF1,sF20),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f960,plain,
c_COMBC(sF22,tc_Arrow__Order__Mirabelle_Oindi,sF1,sF20) = sF23,
inference(reorient_equations,[],[f959]) ).
fof(f961,definition,
sF24 = hAPP(sF23,v_Lab____),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f962,plain,
hAPP(sF23,v_Lab____) = sF24,
inference(reorient_equations,[],[f961]) ).
fof(f963,definition,
sF25 = c_COMBC(sF24,tc_Arrow__Order__Mirabelle_Oindi,sF1,sF1),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f964,plain,
c_COMBC(sF24,tc_Arrow__Order__Mirabelle_Oindi,sF1,sF1) = sF25,
inference(reorient_equations,[],[f963]) ).
fof(f965,definition,
sF26 = hAPP(sF25,v_Lba____),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f966,plain,
hAPP(sF25,v_Lba____) = sF26,
inference(reorient_equations,[],[f965]) ).
fof(f967,definition,
sF27 = hAPP(v_F,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f968,plain,
hAPP(v_F,sF26) = sF27,
inference(reorient_equations,[],[f967]) ).
fof(f969,definition,
sF28 = hAPP(sF15,sF27),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f970,plain,
hAPP(sF15,sF27) = sF28,
inference(reorient_equations,[],[f969]) ).
fof(f971,plain,
~ hBOOL(sF28),
inference(definition_folding,[],[f869,f970,f968,f966,f964,f915,f913,f915,f913,f962,f960,f954,f915,f913,f915,f913,f915,f913,f958,f956,f954,f915,f913,f915,f913,f915,f913,f952,f929,f927,f925,f950,f948,f946,f919,f917,f915,f913,f944,f942,f940,f913]) ).
fof(f986,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_in(sF0),X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| hBOOL(hAPP(hAPP(c_in(sF0),X0),X1)) ),
inference(superposition,[],[f630,f915]) ).
fof(f987,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| hBOOL(hAPP(hAPP(c_in(sF0),X0),X1)) ),
inference(forward_demodulation,[],[f986,f940]) ).
fof(f988,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| hBOOL(hAPP(hAPP(sF13,X0),X1)) ),
inference(forward_demodulation,[],[f987,f940]) ).
fof(f993,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)) = X0,
inference(superposition,[],[f618,f915]) ).
fof(f1001,plain,
! [X0] : hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,sF1),X0) = X0,
inference(superposition,[],[f205,f915]) ).
fof(f1002,plain,
! [X0] : hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,sF16),X0) = X0,
inference(superposition,[],[f205,f946]) ).
fof(f1005,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| ~ hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(sF0,tc_bool)),X1))) ),
inference(superposition,[],[f631,f940]) ).
fof(f1006,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| ~ hBOOL(hAPP(hAPP(sF13,X0),X1)) ),
inference(forward_demodulation,[],[f1005,f915]) ).
fof(f1016,plain,
! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ominus__class_Ominus(X0,sF1),X0),
inference(superposition,[],[f8,f915]) ).
fof(f1045,plain,
hBOOL(hAPP(hAPP(c_in(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),sF14),v_Lab____)),
inference(forward_demodulation,[],[f864,f942]) ).
fof(f1046,plain,
hBOOL(hAPP(hAPP(c_in(sF0),sF14),v_Lab____)),
inference(forward_demodulation,[],[f1045,f913]) ).
fof(f1047,plain,
hBOOL(hAPP(hAPP(sF13,sF14),v_Lab____)),
inference(forward_demodulation,[],[f1046,f940]) ).
fof(f1048,plain,
hBOOL(hAPP(sF15,v_Lab____)),
inference(forward_demodulation,[],[f1047,f944]) ).
fof(f1087,plain,
! [X0] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X0)),
inference(superposition,[],[f594,f915]) ).
fof(f1094,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,sF1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,sF1),X1) = X0 ),
inference(superposition,[],[f125,f915]) ).
fof(f1095,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,sF16)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X0,sF16),X1) = X0 ),
inference(superposition,[],[f125,f946]) ).
fof(f1111,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF13,X0),X1))
| ~ hBOOL(hAPP(X1,X0)) ),
inference(superposition,[],[f859,f940]) ).
fof(f1112,plain,
! [X0] :
( hBOOL(hAPP(sF15,X0))
| ~ hBOOL(hAPP(X0,sF14)) ),
inference(superposition,[],[f1111,f944]) ).
fof(f1113,plain,
( hBOOL(sF28)
| ~ hBOOL(hAPP(sF27,sF14)) ),
inference(superposition,[],[f1112,f970]) ).
fof(f1114,plain,
~ hBOOL(hAPP(sF27,sF14)),
inference(forward_subsumption_resolution,[],[f1113,f971]) ).
fof(f1120,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| hBOOL(hAPP(X1,X0)) ),
inference(superposition,[],[f860,f940]) ).
fof(f1122,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1))
| hBOOL(hAPP(hAPP(sF13,X1),X0)) ),
inference(resolution,[],[f1120,f988]) ).
fof(f1124,plain,
! [X0] :
( ~ hBOOL(hAPP(sF15,X0))
| hBOOL(hAPP(X0,sF14)) ),
inference(superposition,[],[f1120,f944]) ).
fof(f1127,plain,
hBOOL(hAPP(v_Lab____,sF14)),
inference(resolution,[],[f1124,f1048]) ).
fof(f1165,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X1,X0)))
| c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X1 ),
inference(resolution,[],[f771,f859]) ).
fof(f1236,plain,
! [X0] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(sF6),X0)),
inference(superposition,[],[f850,f925]) ).
fof(f1237,plain,
! [X0] : hBOOL(hAPP(sF7,X0)),
inference(forward_demodulation,[],[f1236,f927]) ).
fof(f1238,plain,
! [X0] : c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = sF7,
inference(resolution,[],[f1237,f1165]) ).
fof(f1239,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = hAPP(c_HOL_Ominus__class_Ominus(sF7,tc_fun(X0,tc_bool)),X1),
inference(backward_demodulation,[],[f9,f1238]) ).
fof(f1240,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),sF7),
inference(backward_demodulation,[],[f174,f1238]) ).
fof(f1244,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X1,X0)),X1))
| sF7 = X1 ),
inference(backward_demodulation,[],[f771,f1238]) ).
fof(f1250,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(c_HOL_Ominus__class_Ominus(sF7,sF1),X0),
inference(superposition,[],[f1239,f915]) ).
fof(f1286,plain,
c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF7),
inference(superposition,[],[f1016,f1250]) ).
fof(f1304,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X0,X1)))
| sF7 = X0 ),
inference(resolution,[],[f1244,f859]) ).
fof(f1306,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF13,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X0,sF0)),X0))
| sF7 = X0 ),
inference(superposition,[],[f1244,f940]) ).
fof(f1307,plain,
! [X0] :
( ~ hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X0,sF0)))
| sF7 = X0 ),
inference(resolution,[],[f1306,f1111]) ).
fof(f1308,plain,
! [X0] :
( hBOOL(hAPP(hAPP(sF13,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),sF0)),X0))
| sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) ),
inference(resolution,[],[f1306,f988]) ).
fof(f1348,plain,
! [X2,X0,X1] :
( c_COMBK(X0,X1,X2) = sF7
| ~ hBOOL(X0) ),
inference(superposition,[],[f1304,f475]) ).
fof(f1357,plain,
! [X0] :
( sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),sF0))) ),
inference(resolution,[],[f1308,f1120]) ).
fof(f1364,plain,
! [X0] :
( hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X0))
| hBOOL(hAPP(hAPP(sF13,X0),sF7)) ),
inference(superposition,[],[f1122,f1286]) ).
fof(f1367,plain,
! [X0] : hBOOL(hAPP(hAPP(sF13,X0),sF7)),
inference(forward_subsumption_resolution,[],[f1364,f1087]) ).
fof(f1501,plain,
! [X3,X0] :
( ~ hBOOL(X0)
| hAPP(sF7,X3) = X0 ),
inference(superposition,[],[f475,f1348]) ).
fof(f1520,plain,
! [X0] : hAPP(v_Lab____,sF14) = hAPP(sF7,X0),
inference(resolution,[],[f1501,f1127]) ).
fof(f1555,plain,
! [X0] :
( ~ hBOOL(X0)
| hAPP(v_Lab____,sF14) = X0 ),
inference(backward_demodulation,[],[f1501,f1520]) ).
fof(f1567,plain,
! [X0,X1] :
( hAPP(hAPP(sF13,X0),X1) = hAPP(v_Lab____,sF14)
| ~ hBOOL(hAPP(X1,X0)) ),
inference(resolution,[],[f1555,f1111]) ).
fof(f1645,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),c_Orderings_Obot__class_Obot(sF1)))
| ~ hBOOL(hAPP(hAPP(sF13,X0),sF7)) ),
inference(superposition,[],[f1006,f1286]) ).
fof(f1646,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(v_Lab____,sF14))
| ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1),X0)) ),
inference(superposition,[],[f1006,f1567]) ).
fof(f1647,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1),X0))
| ~ hBOOL(hAPP(hAPP(sF13,X0),X1)) ),
inference(forward_subsumption_resolution,[],[f1646,f1127]) ).
fof(f1648,plain,
! [X0] : ~ hBOOL(hAPP(hAPP(sF13,X0),c_Orderings_Obot__class_Obot(sF1))),
inference(forward_subsumption_resolution,[],[f1645,f1367]) ).
fof(f1650,plain,
sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_Orderings_Obot__class_Obot(sF1)),
inference(resolution,[],[f1648,f1308]) ).
fof(f1652,plain,
~ hBOOL(hAPP(sF15,c_Orderings_Obot__class_Obot(sF1))),
inference(superposition,[],[f1648,f944]) ).
fof(f1794,plain,
! [X0] :
( hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF7) = X0
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),sF0))) ),
inference(superposition,[],[f993,f1357]) ).
fof(f1801,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(sF13,X1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)))
| hBOOL(hAPP(X0,X1)) ),
inference(superposition,[],[f1122,f993]) ).
fof(f1809,plain,
! [X0] :
( hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),sF0)))
| c_Orderings_Obot__class_Obot(sF1) = X0 ),
inference(forward_demodulation,[],[f1794,f1286]) ).
fof(f1826,plain,
! [X0,X1] :
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1))
| hBOOL(hAPP(X0,X1)) ),
inference(resolution,[],[f1801,f1120]) ).
fof(f1957,plain,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Orderings_Obot__class_Obot(sF1),
inference(resolution,[],[f1809,f594]) ).
fof(f1985,plain,
! [X2,X0,X1] :
( c_COMBK(X0,X1,X2) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(X0) ),
inference(superposition,[],[f1809,f475]) ).
fof(f1990,plain,
! [X0,X1] : hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),X0) = c_Orderings_Obot__class_Obot(sF1),
inference(backward_demodulation,[],[f8,f1957]) ).
fof(f1991,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(sF1),tc_fun(X0,tc_bool)),X1),
inference(backward_demodulation,[],[f22,f1957]) ).
fof(f1997,plain,
! [X0,X1] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ominus__class_Ominus(X0,tc_fun(X1,tc_bool)),sF7),
inference(backward_demodulation,[],[f1240,f1957]) ).
fof(f2046,plain,
! [X3,X0] :
( hBOOL(X0)
| hAPP(c_Orderings_Obot__class_Obot(sF1),X3) = X0 ),
inference(superposition,[],[f475,f1985]) ).
fof(f2053,plain,
! [X0,X1] : c_lessequals(c_Orderings_Obot__class_Obot(sF1),X0,tc_fun(X1,tc_bool)),
inference(superposition,[],[f133,f1997]) ).
fof(f2085,plain,
! [X0] : hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = hAPP(sF27,sF14),
inference(resolution,[],[f2046,f1114]) ).
fof(f2089,plain,
! [X0] : sF28 = hAPP(c_Orderings_Obot__class_Obot(sF1),X0),
inference(resolution,[],[f2046,f971]) ).
fof(f2090,plain,
! [X0] :
( hAPP(sF27,sF14) = X0
| hBOOL(X0) ),
inference(backward_demodulation,[],[f2046,f2085]) ).
fof(f2098,plain,
sF28 = hAPP(sF27,sF14),
inference(backward_demodulation,[],[f2085,f2089]) ).
fof(f2106,plain,
! [X0] :
( hBOOL(X0)
| sF28 = X0 ),
inference(forward_demodulation,[],[f2090,f2098]) ).
fof(f2107,plain,
! [X0] :
( sF28 = X0
| hAPP(v_Lab____,sF14) = X0 ),
inference(resolution,[],[f2106,f1555]) ).
fof(f2110,plain,
! [X0,X1] :
( sF28 = hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X0,X1))
| sF7 = X0 ),
inference(resolution,[],[f2106,f1304]) ).
fof(f2125,plain,
sF28 = hAPP(sF15,c_Orderings_Obot__class_Obot(sF1)),
inference(resolution,[],[f2106,f1652]) ).
fof(f2494,plain,
! [X0,X1] :
( hBOOL(sF28)
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1)))
| sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) ),
inference(superposition,[],[f1826,f2110]) ).
fof(f2540,plain,
! [X0,X1] :
( sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1))) ),
inference(forward_subsumption_resolution,[],[f2494,f971]) ).
fof(f2556,plain,
! [X0,X1] :
( hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF7) = X0
| hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1))) ),
inference(superposition,[],[f993,f2540]) ).
fof(f2557,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),sF7))
| ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1),X2))) ),
inference(superposition,[],[f1006,f2540]) ).
fof(f2592,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1),X2))) ),
inference(forward_subsumption_resolution,[],[f2557,f1367]) ).
fof(f2593,plain,
! [X0,X1] :
( hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1)))
| c_Orderings_Obot__class_Obot(sF1) = X0 ),
inference(forward_demodulation,[],[f2556,f1286]) ).
fof(f2600,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0)),X1)))
| hBOOL(hAPP(X0,X2)) ),
inference(resolution,[],[f2592,f1801]) ).
fof(f2616,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(X0,X1)))
| hBOOL(hAPP(X0,X2)) ),
inference(forward_demodulation,[],[f2600,f993]) ).
fof(f3187,definition,
( spl29_9
<=> ! [X0] : hBOOL(X0) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f3188,plain,
( ! [X0] : hBOOL(X0)
| ~ spl29_9 ),
inference(avatar_component_clause,[],[f3187]) ).
fof(f3206,plain,
( ! [X0,X1] : ~ hBOOL(hAPP(hAPP(sF13,X0),X1))
| ~ spl29_9 ),
inference(resolution,[],[f3188,f1647]) ).
fof(f3228,plain,
( $false
| ~ spl29_9 ),
inference(forward_subsumption_resolution,[],[f3206,f3188]) ).
fof(f3229,plain,
~ spl29_9,
inference(avatar_contradiction_clause,[],[f3228]) ).
fof(f3339,plain,
! [X0] : c_lessequals(c_Orderings_Obot__class_Obot(sF1),X0,sF1),
inference(superposition,[],[f2053,f915]) ).
fof(f3340,plain,
! [X0] : c_lessequals(c_Orderings_Obot__class_Obot(sF1),X0,sF16),
inference(superposition,[],[f2053,f946]) ).
fof(f3342,plain,
! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF1),X0),
inference(resolution,[],[f3339,f1094]) ).
fof(f3365,plain,
! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16),X0),
inference(resolution,[],[f3340,f1095]) ).
fof(f3378,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| c_Orderings_Obot__class_Obot(sF1) = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16) ),
inference(superposition,[],[f1809,f3365]) ).
fof(f3389,definition,
( spl29_11
<=> c_Orderings_Obot__class_Obot(sF1) = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f3390,plain,
( c_Orderings_Obot__class_Obot(sF1) != c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16)
| spl29_11 ),
inference(avatar_component_clause,[],[f3389]) ).
fof(f3391,plain,
( c_Orderings_Obot__class_Obot(sF1) = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16)
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f3389]) ).
fof(f3393,definition,
( spl29_12
<=> hBOOL(c_Orderings_Obot__class_Obot(sF1)) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f3395,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f3393]) ).
fof(f3396,plain,
( spl29_11
| spl29_12 ),
inference(avatar_split_clause,[],[f3378,f3393,f3389]) ).
fof(f3401,plain,
( c_Orderings_Obot__class_Obot(sF1) = hAPP(c_Orderings_Obot__class_Obot(sF1),c_Orderings_Obot__class_Obot(sF1))
| ~ spl29_11 ),
inference(superposition,[],[f1002,f3391]) ).
fof(f3402,plain,
( sF28 = c_Orderings_Obot__class_Obot(sF1)
| ~ spl29_11 ),
inference(forward_demodulation,[],[f3401,f2089]) ).
fof(f3410,plain,
( ! [X0] : ~ hBOOL(hAPP(hAPP(sF13,X0),sF28))
| ~ spl29_11 ),
inference(backward_demodulation,[],[f1648,f3402]) ).
fof(f3436,plain,
( ! [X0] : sF28 = hAPP(sF28,X0)
| ~ spl29_11 ),
inference(backward_demodulation,[],[f2089,f3402]) ).
fof(f3437,plain,
( sF28 = hAPP(sF15,sF28)
| ~ spl29_11 ),
inference(backward_demodulation,[],[f2125,f3402]) ).
fof(f3439,plain,
( ! [X0,X1] :
( hBOOL(hAPP(X0,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1)))
| sF28 = X0 )
| ~ spl29_11 ),
inference(backward_demodulation,[],[f2593,f3402]) ).
fof(f3445,plain,
( ! [X0] : sF28 = hAPP(c_Lattices_Olower__semilattice__class_Oinf(sF28,sF1),X0)
| ~ spl29_11 ),
inference(backward_demodulation,[],[f3342,f3402]) ).
fof(f3448,plain,
( ! [X0,X1] :
( hAPP(X0,X1) = X0
| hAPP(v_Lab____,sF14) = X0 )
| ~ spl29_11 ),
inference(superposition,[],[f3436,f2107]) ).
fof(f3498,plain,
( ! [X0] : sF28 = hAPP(hAPP(sF13,X0),sF28)
| ~ spl29_11 ),
inference(resolution,[],[f3410,f2106]) ).
fof(f3548,plain,
( hBOOL(sF28)
| sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF28)
| ~ spl29_11 ),
inference(superposition,[],[f1308,f3498]) ).
fof(f3561,plain,
( sF7 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF28)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f3548,f971]) ).
fof(f3567,plain,
( sF28 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),sF7)
| ~ spl29_11 ),
inference(superposition,[],[f993,f3561]) ).
fof(f3756,plain,
( hBOOL(sF28)
| sF28 = c_Lattices_Olower__semilattice__class_Oinf(sF28,sF1)
| ~ spl29_11 ),
inference(superposition,[],[f3439,f3445]) ).
fof(f3768,plain,
( sF28 = c_Lattices_Olower__semilattice__class_Oinf(sF28,sF1)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f3756,f971]) ).
fof(f4194,plain,
( ! [X2,X0] :
( hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0))
| hBOOL(hAPP(X0,X2))
| hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(v_Lab____,sF14) )
| ~ spl29_11 ),
inference(superposition,[],[f2616,f3448]) ).
fof(f4235,plain,
( hBOOL(v_Lab____)
| v_Lab____ = hAPP(v_Lab____,sF14)
| ~ spl29_11 ),
inference(superposition,[],[f1127,f3448]) ).
fof(f4261,plain,
( v_Lab____ = hAPP(v_Lab____,sF14)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4235,f1555]) ).
fof(f4267,plain,
( ! [X2,X0] :
( hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(v_Lab____,sF14)
| hBOOL(hAPP(X0,X2)) )
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4194,f1555]) ).
fof(f4456,plain,
( ! [X0] :
( sF7 = hAPP(v_Lab____,sF14)
| hBOOL(hAPP(sF28,X0)) )
| ~ spl29_11 ),
inference(superposition,[],[f3561,f4267]) ).
fof(f4459,plain,
( hBOOL(sF28)
| sF7 = hAPP(v_Lab____,sF14)
| ~ spl29_11 ),
inference(forward_demodulation,[],[f4456,f3436]) ).
fof(f4469,plain,
( sF7 = hAPP(v_Lab____,sF14)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4459,f971]) ).
fof(f4479,plain,
( ! [X0] :
( sF7 = X0
| sF28 = X0 )
| ~ spl29_11 ),
inference(backward_demodulation,[],[f2107,f4469]) ).
fof(f4498,plain,
( v_Lab____ = sF7
| ~ spl29_11 ),
inference(backward_demodulation,[],[f4469,f4261]) ).
fof(f4542,plain,
( sF28 = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),v_Lab____)
| ~ spl29_11 ),
inference(backward_demodulation,[],[f3567,f4498]) ).
fof(f4566,plain,
( ! [X0,X1] :
( hBOOL(hAPP(sF28,c_ATP__Linkup_Osko__Set__XUNIV__eq__I__1__1(v_Lab____,X0)))
| hBOOL(hAPP(v_Lab____,X1)) )
| ~ spl29_11 ),
inference(superposition,[],[f2616,f4542]) ).
fof(f4576,plain,
( ! [X1] :
( hBOOL(sF28)
| hBOOL(hAPP(v_Lab____,X1)) )
| ~ spl29_11 ),
inference(forward_demodulation,[],[f4566,f3436]) ).
fof(f4584,plain,
( ! [X1] : hBOOL(hAPP(v_Lab____,X1))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4576,f971]) ).
fof(f4600,plain,
( ! [X0] :
( v_Lab____ = X0
| sF28 = X0 )
| ~ spl29_11 ),
inference(forward_demodulation,[],[f4479,f4498]) ).
fof(f4618,plain,
( ! [X0,X1] :
( hBOOL(hAPP(X0,X1))
| sF28 = X0 )
| ~ spl29_11 ),
inference(superposition,[],[f4584,f4600]) ).
fof(f4662,plain,
( hBOOL(sF28)
| sF28 = c_HOL_Ouminus__class_Ouminus(sF1)
| ~ spl29_11 ),
inference(superposition,[],[f4618,f4542]) ).
fof(f4677,plain,
( hBOOL(sF28)
| sF15 = sF28
| ~ spl29_11 ),
inference(superposition,[],[f4618,f3437]) ).
fof(f4685,plain,
( sF15 = sF28
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4677,f971]) ).
fof(f4690,plain,
( sF28 = c_HOL_Ouminus__class_Ouminus(sF1)
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4662,f971]) ).
fof(f4723,plain,
( sF15 = c_Lattices_Olower__semilattice__class_Oinf(sF15,sF1)
| ~ spl29_11 ),
inference(backward_demodulation,[],[f3768,f4685]) ).
fof(f4785,plain,
( sF15 = c_HOL_Ouminus__class_Ouminus(sF1)
| ~ spl29_11 ),
inference(forward_demodulation,[],[f4690,f4685]) ).
fof(f4800,plain,
( ! [X0,X1] :
( hBOOL(hAPP(hAPP(sF15,X0),X1))
| hBOOL(hAPP(X0,X1)) )
| ~ spl29_11 ),
inference(backward_demodulation,[],[f1826,f4785]) ).
fof(f4812,plain,
( sF15 = hAPP(sF15,sF15)
| ~ spl29_11 ),
inference(superposition,[],[f1001,f4723]) ).
fof(f4870,plain,
( ! [X0] :
( hBOOL(hAPP(sF15,X0))
| hBOOL(hAPP(sF15,X0)) )
| ~ spl29_11 ),
inference(superposition,[],[f4800,f4812]) ).
fof(f4873,plain,
( ! [X0] : hBOOL(hAPP(sF15,X0))
| ~ spl29_11 ),
inference(duplicate_literal_removal,[],[f4870]) ).
fof(f4874,plain,
( ! [X0] : hBOOL(hAPP(X0,sF14))
| ~ spl29_11 ),
inference(resolution,[],[f4873,f1124]) ).
fof(f4985,plain,
( ! [X0] : hBOOL(X0)
| ~ spl29_11 ),
inference(superposition,[],[f4874,f475]) ).
fof(f4987,plain,
( spl29_9
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f4985,f3389,f3187]) ).
fof(f5000,plain,
! [X0] :
( hBOOL(hAPP(sF7,X0))
| hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X0)) ),
inference(superposition,[],[f1826,f1650]) ).
fof(f5129,plain,
! [X0] :
( ~ hBOOL(X0)
| hAPP(v_Lab____,sF14) = X0 ),
inference(superposition,[],[f971,f2107]) ).
fof(f5157,plain,
! [X0] :
( hBOOL(sF28)
| hBOOL(hAPP(sF7,X0)) ),
inference(backward_demodulation,[],[f5000,f2089]) ).
fof(f5162,plain,
! [X0] : hBOOL(hAPP(sF7,X0)),
inference(forward_subsumption_resolution,[],[f5157,f971]) ).
fof(f5166,plain,
! [X0] : hAPP(v_Lab____,sF14) = hAPP(sF7,X0),
inference(resolution,[],[f5162,f5129]) ).
fof(f5436,plain,
! [X0] :
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF1))
| sF7 = c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(sF1),tc_fun(X0,tc_bool)) ),
inference(superposition,[],[f1307,f1991]) ).
fof(f5454,plain,
( ! [X0] : sF7 = c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(sF1),tc_fun(X0,tc_bool))
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f5436,f3395]) ).
fof(f5516,plain,
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF1))
| sF7 = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF1) ),
inference(superposition,[],[f1307,f3342]) ).
fof(f5523,plain,
( sF7 = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF1)
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f5516,f3395]) ).
fof(f5526,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(sF7,X0)
| ~ spl29_12 ),
inference(backward_demodulation,[],[f3342,f5523]) ).
fof(f5533,plain,
( c_Orderings_Obot__class_Obot(sF1) = hAPP(v_Lab____,sF14)
| ~ spl29_12 ),
inference(backward_demodulation,[],[f5166,f5526]) ).
fof(f5545,plain,
( ! [X0] :
( sF28 = X0
| c_Orderings_Obot__class_Obot(sF1) = X0 )
| ~ spl29_12 ),
inference(backward_demodulation,[],[f2107,f5533]) ).
fof(f5853,plain,
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF1))
| sF7 = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16) ),
inference(superposition,[],[f1307,f3365]) ).
fof(f5860,plain,
( sF7 = c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(sF1),sF16)
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f5853,f3395]) ).
fof(f5864,plain,
( sF7 != c_Orderings_Obot__class_Obot(sF1)
| spl29_11
| ~ spl29_12 ),
inference(backward_demodulation,[],[f3390,f5860]) ).
fof(f6343,definition,
( spl29_13
<=> sF7 = sF13 ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f6344,plain,
( sF7 != sF13
| spl29_13 ),
inference(avatar_component_clause,[],[f6343]) ).
fof(f6345,plain,
( sF7 = sF13
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f6343]) ).
fof(f6353,plain,
( ! [X0,X1] :
( hBOOL(hAPP(hAPP(sF7,X0),X1))
| hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1))) )
| ~ spl29_13 ),
inference(backward_demodulation,[],[f988,f6345]) ).
fof(f6394,plain,
( ! [X0,X1] :
( hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X1))
| hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1))) )
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_demodulation,[],[f6353,f5526]) ).
fof(f6414,plain,
( ! [X0,X1] :
( hBOOL(sF28)
| hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1))) )
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_demodulation,[],[f6394,f2089]) ).
fof(f6423,plain,
( ! [X0,X1] : hBOOL(hAPP(hAPP(sF13,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_subsumption_resolution,[],[f6414,f971]) ).
fof(f6425,plain,
( ! [X0,X1] : hBOOL(hAPP(hAPP(sF7,X0),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_demodulation,[],[f6423,f6345]) ).
fof(f6427,plain,
( ! [X1] : hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X1)))
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_demodulation,[],[f6425,f5526]) ).
fof(f6429,plain,
( hBOOL(sF28)
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_demodulation,[],[f6427,f2089]) ).
fof(f6430,plain,
( $false
| ~ spl29_12
| ~ spl29_13 ),
inference(forward_subsumption_resolution,[],[f6429,f971]) ).
fof(f6431,plain,
( ~ spl29_12
| ~ spl29_13 ),
inference(avatar_contradiction_clause,[],[f6430]) ).
fof(f6545,plain,
( ~ hBOOL(hAPP(sF28,c_Orderings_Obot__class_Obot(sF1)))
| sF7 = sF13 ),
inference(superposition,[],[f1648,f2110]) ).
fof(f6547,plain,
( ~ hBOOL(hAPP(sF28,c_Orderings_Obot__class_Obot(sF1)))
| spl29_13 ),
inference(forward_subsumption_resolution,[],[f6545,f6344]) ).
fof(f6805,plain,
( ! [X0] :
( ~ hBOOL(hAPP(X0,c_Orderings_Obot__class_Obot(sF1)))
| c_Orderings_Obot__class_Obot(sF1) = X0 )
| ~ spl29_12
| spl29_13 ),
inference(superposition,[],[f6547,f5545]) ).
fof(f6835,plain,
( ! [X0] :
( ~ hBOOL(c_Orderings_Obot__class_Obot(sF1))
| c_Orderings_Obot__class_Obot(sF1) = c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(sF1),tc_fun(X0,tc_bool)) )
| ~ spl29_12
| spl29_13 ),
inference(superposition,[],[f6805,f1990]) ).
fof(f6912,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF1) = c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(sF1),tc_fun(X0,tc_bool))
| ~ spl29_12
| spl29_13 ),
inference(forward_subsumption_resolution,[],[f6835,f3395]) ).
fof(f6934,plain,
( sF7 = c_Orderings_Obot__class_Obot(sF1)
| ~ spl29_12
| spl29_13 ),
inference(forward_demodulation,[],[f6912,f5454]) ).
fof(f6953,plain,
( $false
| spl29_11
| ~ spl29_12
| spl29_13 ),
inference(forward_subsumption_resolution,[],[f6934,f5864]) ).
fof(f6954,plain,
( spl29_11
| ~ spl29_12
| spl29_13 ),
inference(avatar_contradiction_clause,[],[f6953]) ).
cnf(s32,plain,
~ spl29_9,
inference(sat_conversion,[],[f3229]) ).
cnf(s33,plain,
( spl29_11
| spl29_12 ),
inference(sat_conversion,[],[f3396]) ).
cnf(s34,plain,
( spl29_9
| ~ spl29_11 ),
inference(sat_conversion,[],[f4987]) ).
cnf(s36,plain,
( ~ spl29_12
| ~ spl29_13 ),
inference(sat_conversion,[],[f6431]) ).
cnf(s44,plain,
( spl29_11
| ~ spl29_12
| spl29_13 ),
inference(sat_conversion,[],[f6954]) ).
cnf(s45,plain,
~ spl29_11,
inference(rat,[],[s34,s32]) ).
cnf(s46,plain,
spl29_12,
inference(rat,[],[s33,s45]) ).
cnf(s47,plain,
spl29_13,
inference(rat,[],[s44,s45,s46]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s36,s47,s46]) ).
fof(f6955,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT084-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 23:40:02 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.06/1.89 % (1426325)Input is clausal, will run a generic CNF schedule.
% 7.06/1.89 % (1426335)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4066449725:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.06/1.89 % (1426333)lrs+10_1_sil=8000:sp=occurrence:random_seed=3116722365:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.06/1.89 % (1426330)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=1905533632:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.06/1.89 % (1426331)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=430625916:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.06/1.89 % (1426336)dis-21_1_sil=8000:lcm=predicate:random_seed=1017178628:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 7.06/1.89 % (1426334)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1389753409:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.06/1.89 % (1426332)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3513478339:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.06/1.89 % (1426336)Instruction limit reached!
% 7.06/1.89 % (1426336)------------------------------
% 7.06/1.89 % (1426336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.89 % (1426336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.89 % (1426336)CaDiCaL version: 2.1.3
% 7.06/1.89 % (1426336)Termination reason: Instruction limit
% 7.06/1.89 % (1426336)Termination phase: Saturation
% 7.06/1.89 % (1426336)Time elapsed: 0.067 s
% 7.06/1.89 % (1426336)Peak memory usage: 90 MB
% 7.06/1.89 % (1426336)Instructions burned: 117 (million)
% 7.06/1.89 % (1426333)Instruction limit reached!
% 7.06/1.89 % (1426333)------------------------------
% 7.06/1.89 % (1426333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.89 % (1426333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.89 % (1426333)CaDiCaL version: 2.1.3
% 7.06/1.89 % (1426333)Termination reason: Instruction limit
% 7.06/1.89 % (1426333)Termination phase: Saturation
% 7.06/1.89 % (1426333)Time elapsed: 0.067 s
% 7.06/1.89 % (1426333)Peak memory usage: 90 MB
% 7.06/1.89 % (1426333)Instructions burned: 107 (million)
% 7.06/1.89 % (1426334)Instruction limit reached!
% 7.06/1.89 % (1426334)------------------------------
% 7.06/1.89 % (1426334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.89 % (1426334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.89 % (1426334)CaDiCaL version: 2.1.3
% 7.06/1.89 % (1426334)Termination reason: Instruction limit
% 7.06/1.89 % (1426334)Termination phase: Saturation
% 7.06/1.89 % (1426334)Time elapsed: 0.073 s
% 7.06/1.89 % (1426334)Peak memory usage: 89 MB
% 7.06/1.89 % (1426334)Instructions burned: 114 (million)
% 7.06/1.89 % (1426335)Instruction limit reached!
% 7.06/1.89 % (1426335)------------------------------
% 7.06/1.89 % (1426335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.89 % (1426335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.89 % (1426335)CaDiCaL version: 2.1.3
% 7.06/1.89 % (1426335)Termination reason: Instruction limit
% 7.06/1.89 % (1426335)Termination phase: Saturation
% 7.06/1.89 % (1426335)Time elapsed: 0.116 s
% 7.06/1.89 % (1426335)Peak memory usage: 90 MB
% 7.06/1.89 % (1426335)Instructions burned: 181 (million)
% 7.06/1.89 % (1426344)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2572973652:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.06/1.89 % (1426346)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3311587652:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.06/1.89 % (1426345)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=704265214:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 7.06/1.89 % (1426347)lrs+10_64_to=lpo:sil=8000:random_seed=69070058:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.06/1.89 % (1426347)Instruction limit reached!
% 18.19/3.25 % (1426347)------------------------------
% 18.19/3.25 % (1426347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426347)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426347)Termination reason: Instruction limit
% 18.19/3.25 % (1426347)Termination phase: Saturation
% 18.19/3.25 % (1426347)Time elapsed: 0.045 s
% 18.19/3.25 % (1426347)Peak memory usage: 90 MB
% 18.19/3.25 % (1426347)Instructions burned: 126 (million)
% 18.19/3.25 % (1426344)Instruction limit reached!
% 18.19/3.25 % (1426344)------------------------------
% 18.19/3.25 % (1426344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426344)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426344)Termination reason: Instruction limit
% 18.19/3.25 % (1426344)Termination phase: Saturation
% 18.19/3.25 % (1426344)Time elapsed: 0.080 s
% 18.19/3.25 % (1426344)Peak memory usage: 89 MB
% 18.19/3.25 % (1426344)Instructions burned: 145 (million)
% 18.19/3.25 % (1426345)Instruction limit reached!
% 18.19/3.25 % (1426345)------------------------------
% 18.19/3.25 % (1426345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426345)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426345)Termination reason: Instruction limit
% 18.19/3.25 % (1426345)Termination phase: Saturation
% 18.19/3.25 % (1426345)Time elapsed: 0.100 s
% 18.19/3.25 % (1426345)Peak memory usage: 90 MB
% 18.19/3.25 % (1426345)Instructions burned: 190 (million)
% 18.19/3.25 % (1426346)Instruction limit reached!
% 18.19/3.25 % (1426346)------------------------------
% 18.19/3.25 % (1426346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426346)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426346)Termination reason: Instruction limit
% 18.19/3.25 % (1426346)Termination phase: Saturation
% 18.19/3.25 % (1426346)Time elapsed: 0.120 s
% 18.19/3.25 % (1426346)Peak memory usage: 90 MB
% 18.19/3.25 % (1426346)Instructions burned: 219 (million)
% 18.19/3.25 % (1426352)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3991608202:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.19/3.25 % (1426353)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3117590110:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.19/3.25 % (1426352)Instruction limit reached!
% 18.19/3.25 % (1426352)------------------------------
% 18.19/3.25 % (1426352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426352)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426352)Termination reason: Instruction limit
% 18.19/3.25 % (1426352)Termination phase: Saturation
% 18.19/3.25 % (1426352)Time elapsed: 0.071 s
% 18.19/3.25 % (1426352)Peak memory usage: 91 MB
% 18.19/3.25 % (1426352)Instructions burned: 196 (million)
% 18.19/3.25 % (1426354)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2957004924:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 18.19/3.25 % (1426355)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=76053221:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 18.19/3.25 % (1426353)Instruction limit reached!
% 18.19/3.25 % (1426353)------------------------------
% 18.19/3.25 % (1426353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426353)CaDiCaL version: 2.1.3
% 18.19/3.25 % (1426353)Termination reason: Instruction limit
% 18.19/3.25 % (1426353)Termination phase: Saturation
% 18.19/3.25 % (1426353)Time elapsed: 0.092 s
% 18.19/3.25 % (1426353)Peak memory usage: 91 MB
% 18.19/3.25 % (1426353)Instructions burned: 157 (million)
% 18.19/3.25 % (1426355)Instruction limit reached!
% 18.19/3.25 % (1426355)------------------------------
% 18.19/3.25 % (1426355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.19/3.25 % (1426355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.19/3.25 % (1426355)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426355)Termination reason: Instruction limit
% 37.42/5.98 % (1426355)Termination phase: Saturation
% 37.42/5.98 % (1426355)Time elapsed: 0.061 s
% 37.42/5.98 % (1426355)Peak memory usage: 89 MB
% 37.42/5.98 % (1426355)Instructions burned: 107 (million)
% 37.42/5.98 % (1426359)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=768455452:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 37.42/5.98 % (1426359)Instruction limit reached!
% 37.42/5.98 % (1426359)------------------------------
% 37.42/5.98 % (1426359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.42/5.98 % (1426359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.98 % (1426359)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426359)Termination reason: Instruction limit
% 37.42/5.98 % (1426359)Termination phase: Saturation
% 37.42/5.98 % (1426359)Time elapsed: 0.035 s
% 37.42/5.98 % (1426359)Peak memory usage: 90 MB
% 37.42/5.98 % (1426359)Instructions burned: 108 (million)
% 37.42/5.98 % (1426361)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4216756401:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 37.42/5.98 % (1426364)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2762772514:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 37.42/5.98 % (1426363)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1535915858:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 37.42/5.98 % (1426364)Instruction limit reached!
% 37.42/5.98 % (1426364)------------------------------
% 37.42/5.98 % (1426364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.42/5.98 % (1426364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.98 % (1426364)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426364)Termination reason: Instruction limit
% 37.42/5.98 % (1426364)Termination phase: Saturation
% 37.42/5.98 % (1426364)Time elapsed: 0.043 s
% 37.42/5.98 % (1426364)Peak memory usage: 89 MB
% 37.42/5.98 % (1426364)Instructions burned: 136 (million)
% 37.42/5.98 % (1426361)Instruction limit reached!
% 37.42/5.98 % (1426361)------------------------------
% 37.42/5.98 % (1426361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.42/5.98 % (1426361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.98 % (1426361)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426361)Termination reason: Instruction limit
% 37.42/5.98 % (1426361)Termination phase: Saturation
% 37.42/5.98 % (1426361)Time elapsed: 0.135 s
% 37.42/5.98 % (1426361)Peak memory usage: 90 MB
% 37.42/5.98 % (1426361)Instructions burned: 242 (million)
% 37.42/5.98 % (1426368)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2593751701:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 37.42/5.98 % (1426370)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1808128403:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 37.42/5.98 % (1426368)Instruction limit reached!
% 37.42/5.98 % (1426368)------------------------------
% 37.42/5.98 % (1426368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.42/5.98 % (1426368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.98 % (1426368)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426368)Termination reason: Instruction limit
% 37.42/5.98 % (1426368)Termination phase: Saturation
% 37.42/5.98 % (1426368)Time elapsed: 0.167 s
% 37.42/5.98 % (1426368)Peak memory usage: 93 MB
% 37.42/5.98 % (1426368)Instructions burned: 501 (million)
% 37.42/5.98 % (1426370)Instruction limit reached!
% 37.42/5.98 % (1426370)------------------------------
% 37.42/5.98 % (1426370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.42/5.98 % (1426370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.98 % (1426370)CaDiCaL version: 2.1.3
% 37.42/5.98 % (1426370)Termination reason: Instruction limit
% 37.42/5.98 % (1426370)Termination phase: Saturation
% 37.42/5.98 % (1426370)Time elapsed: 0.118 s
% 37.42/5.98 % (1426370)Peak memory usage: 90 MB
% 37.42/5.98 % (1426370)Instructions burned: 193 (million)
% 37.42/5.98 % (1426372)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1936622100:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 37.42/5.98 % (1426372)Instruction limit reached!
% 37.42/5.98 % (1426372)------------------------------
% 44.05/6.98 % (1426372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426372)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426372)Termination reason: Instruction limit
% 44.05/6.98 % (1426372)Termination phase: Saturation
% 44.05/6.98 % (1426372)Time elapsed: 0.090 s
% 44.05/6.98 % (1426372)Peak memory usage: 92 MB
% 44.05/6.98 % (1426372)Instructions burned: 264 (million)
% 44.05/6.98 % (1426373)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1450283503:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 44.05/6.98 % (1426375)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=4002978085:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 44.05/6.98 % (1426373)Instruction limit reached!
% 44.05/6.98 % (1426373)------------------------------
% 44.05/6.98 % (1426373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426373)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426373)Termination reason: Instruction limit
% 44.05/6.98 % (1426373)Termination phase: Saturation
% 44.05/6.98 % (1426373)Time elapsed: 0.097 s
% 44.05/6.98 % (1426373)Peak memory usage: 90 MB
% 44.05/6.98 % (1426373)Instructions burned: 157 (million)
% 44.05/6.98 % (1426378)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2560068733:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 44.05/6.98 % (1426378)Instruction limit reached!
% 44.05/6.98 % (1426378)------------------------------
% 44.05/6.98 % (1426378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426378)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426378)Termination reason: Instruction limit
% 44.05/6.98 % (1426378)Termination phase: Saturation
% 44.05/6.98 % (1426378)Time elapsed: 0.303 s
% 44.05/6.98 % (1426378)Peak memory usage: 93 MB
% 44.05/6.98 % (1426378)Instructions burned: 537 (million)
% 44.05/6.98 % (1426380)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=296049843:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 44.05/6.98 % (1426380)Instruction limit reached!
% 44.05/6.98 % (1426380)------------------------------
% 44.05/6.98 % (1426380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426380)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426380)Termination reason: Instruction limit
% 44.05/6.98 % (1426380)Termination phase: Saturation
% 44.05/6.98 % (1426380)Time elapsed: 0.093 s
% 44.05/6.98 % (1426380)Peak memory usage: 90 MB
% 44.05/6.98 % (1426380)Instructions burned: 180 (million)
% 44.05/6.98 % (1426382)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1037459533:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 44.05/6.98 % (1426375)Instruction limit reached!
% 44.05/6.98 % (1426375)------------------------------
% 44.05/6.98 % (1426375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426375)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426375)Termination reason: Instruction limit
% 44.05/6.98 % (1426375)Termination phase: Saturation
% 44.05/6.98 % (1426375)Time elapsed: 1.126 s
% 44.05/6.98 % (1426375)Peak memory usage: 151 MB
% 44.05/6.98 % (1426375)Instructions burned: 3259 (million)
% 44.05/6.98 % (1426384)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3936109441:i=412:gtgl=4:gtg=exists_all_2975 on theBenchmark for (2975ds/412Mi)
% 44.05/6.98 % (1426354)Instruction limit reached!
% 44.05/6.98 % (1426354)------------------------------
% 44.05/6.98 % (1426354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.05/6.98 % (1426354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.05/6.98 % (1426354)CaDiCaL version: 2.1.3
% 44.05/6.98 % (1426354)Termination reason: Instruction limit
% 44.05/6.98 % (1426354)Termination phase: Saturation
% 67.31/10.18 % (1426354)Time elapsed: 2.039 s
% 67.31/10.18 % (1426354)Peak memory usage: 151 MB
% 67.31/10.18 % (1426354)Instructions burned: 3394 (million)
% 67.31/10.18 % (1426384)Instruction limit reached!
% 67.31/10.18 % (1426384)------------------------------
% 67.31/10.18 % (1426384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.31/10.18 % (1426384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.31/10.18 % (1426384)CaDiCaL version: 2.1.3
% 67.31/10.18 % (1426384)Termination reason: Instruction limit
% 67.31/10.18 % (1426384)Termination phase: Saturation
% 67.31/10.18 % (1426384)Time elapsed: 0.122 s
% 67.31/10.18 % (1426384)Peak memory usage: 92 MB
% 67.31/10.18 % (1426384)Instructions burned: 415 (million)
% 67.31/10.18 % (1426386)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=156698828:s2pl=no:i=8478:s2at=4:nm=6_2973 on theBenchmark for (2973ds/8478Mi)
% 67.31/10.18 % (1426387)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3430820303:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2972 on theBenchmark for (2972ds/303Mi)
% 67.31/10.18 % (1426387)Instruction limit reached!
% 67.31/10.18 % (1426387)------------------------------
% 67.31/10.18 % (1426387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.31/10.18 % (1426387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.31/10.18 % (1426387)CaDiCaL version: 2.1.3
% 67.31/10.18 % (1426387)Termination reason: Instruction limit
% 67.31/10.18 % (1426387)Termination phase: Saturation
% 67.31/10.18 % (1426387)Time elapsed: 0.164 s
% 67.31/10.18 % (1426387)Peak memory usage: 91 MB
% 67.31/10.18 % (1426387)Instructions burned: 303 (million)
% 67.31/10.18 % (1426390)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=758011150:st=4:i=720:sd=3:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/720Mi)
% 67.31/10.18 % (1426390)Instruction limit reached!
% 67.31/10.18 % (1426390)------------------------------
% 67.31/10.18 % (1426390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.31/10.18 % (1426390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.31/10.18 % (1426390)CaDiCaL version: 2.1.3
% 67.31/10.18 % (1426390)Termination reason: Instruction limit
% 67.31/10.18 % (1426390)Termination phase: Saturation
% 67.31/10.18 % (1426390)Time elapsed: 0.370 s
% 67.31/10.18 % (1426390)Peak memory usage: 94 MB
% 67.31/10.18 % (1426390)Instructions burned: 720 (million)
% 67.31/10.18 % (1426392)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3721561084:i=598:bs=on:bd=preordered:av=off:ss=axioms_2965 on theBenchmark for (2965ds/598Mi)
% 67.31/10.18 % (1426363)Instruction limit reached!
% 67.31/10.18 % (1426363)------------------------------
% 67.31/10.18 % (1426363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.31/10.18 % (1426363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.31/10.18 % (1426363)CaDiCaL version: 2.1.3
% 67.31/10.18 % (1426363)Termination reason: Instruction limit
% 67.31/10.18 % (1426363)Termination phase: Saturation
% 67.31/10.18 % (1426363)Time elapsed: 3.179 s
% 67.31/10.18 % (1426363)Peak memory usage: 165 MB
% 67.31/10.18 % (1426363)Instructions burned: 5211 (million)
% 67.31/10.18 % (1426392)Instruction limit reached!
% 67.31/10.18 % (1426392)------------------------------
% 67.31/10.18 % (1426392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.31/10.18 % (1426392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.31/10.18 % (1426392)CaDiCaL version: 2.1.3
% 67.31/10.18 % (1426392)Termination reason: Instruction limit
% 67.31/10.18 % (1426392)Termination phase: Saturation
% 67.31/10.18 % (1426392)Time elapsed: 0.393 s
% 67.31/10.18 % (1426392)Peak memory usage: 94 MB
% 67.31/10.18 % (1426392)Instructions burned: 598 (million)
% 67.31/10.18 % (1426394)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1644889396:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 67.31/10.18 % (1426395)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=4190504380:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2959 on theBenchmark for (2959ds/1997Mi)
% 67.31/10.18 % (1426382)Instruction limit reached!
% 67.31/10.18 % (1426382)------------------------------
% 96.67/14.37 % (1426382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426382)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426382)Termination reason: Instruction limit
% 96.67/14.37 % (1426382)Termination phase: Saturation
% 96.67/14.37 % (1426382)Time elapsed: 3.190 s
% 96.67/14.37 % (1426382)Peak memory usage: 161 MB
% 96.67/14.37 % (1426382)Instructions burned: 10308 (million)
% 96.67/14.37 % (1426395)Instruction limit reached!
% 96.67/14.37 % (1426395)------------------------------
% 96.67/14.37 % (1426395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426395)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426395)Termination reason: Instruction limit
% 96.67/14.37 % (1426395)Termination phase: Saturation
% 96.67/14.37 % (1426395)Time elapsed: 1.252 s
% 96.67/14.37 % (1426395)Peak memory usage: 140 MB
% 96.67/14.37 % (1426395)Instructions burned: 1998 (million)
% 96.67/14.37 % (1426398)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2675861853:i=2088:bd=preordered:av=off_2946 on theBenchmark for (2946ds/2088Mi)
% 96.67/14.37 % (1426399)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2797155420:i=1098:nicw=on_2945 on theBenchmark for (2945ds/1098Mi)
% 96.67/14.37 % (1426394)Instruction limit reached!
% 96.67/14.37 % (1426394)------------------------------
% 96.67/14.37 % (1426394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426394)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426394)Termination reason: Instruction limit
% 96.67/14.37 % (1426394)Termination phase: Saturation
% 96.67/14.37 % (1426394)Time elapsed: 1.845 s
% 96.67/14.37 % (1426394)Peak memory usage: 146 MB
% 96.67/14.37 % (1426394)Instructions burned: 2990 (million)
% 96.67/14.37 % (1426402)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=566316552:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi)
% 96.67/14.37 % (1426398)Instruction limit reached!
% 96.67/14.37 % (1426398)------------------------------
% 96.67/14.37 % (1426398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426398)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426398)Termination reason: Instruction limit
% 96.67/14.37 % (1426398)Termination phase: Saturation
% 96.67/14.37 % (1426398)Time elapsed: 0.700 s
% 96.67/14.37 % (1426398)Peak memory usage: 140 MB
% 96.67/14.37 % (1426398)Instructions burned: 2088 (million)
% 96.67/14.37 % (1426402)Refutation not found, incomplete strategy
% 96.67/14.37 % (1426402)------------------------------
% 96.67/14.37 % (1426402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426402)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426402)Termination reason: Refutation not found, incomplete strategy
% 96.67/14.37 % (1426402)Time elapsed: 0.075 s
% 96.67/14.37 % (1426402)Peak memory usage: 90 MB
% 96.67/14.37 % (1426402)Instructions burned: 130 (million)
% 96.67/14.37 % (1426399)Instruction limit reached!
% 96.67/14.37 % (1426399)------------------------------
% 96.67/14.37 % (1426399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.67/14.37 % (1426399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.67/14.37 % (1426399)CaDiCaL version: 2.1.3
% 96.67/14.37 % (1426399)Termination reason: Instruction limit
% 96.67/14.37 % (1426399)Termination phase: Saturation
% 96.67/14.37 % (1426399)Time elapsed: 0.693 s
% 96.67/14.37 % (1426399)Peak memory usage: 100 MB
% 96.67/14.37 % (1426399)Instructions burned: 1100 (million)
% 96.67/14.37 % (1426404)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=95510255:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2938 on theBenchmark for (2938ds/2942Mi)
% 96.67/14.37 % (1426405)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=438087368:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2937 on theBenchmark for (2937ds/6922Mi)
% 114.25/16.91 % (1426402)------------------------------
% 114.25/16.91 % (1426402)------------------------------
% 114.25/16.91 % (1426408)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3584009490:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2935 on theBenchmark for (2935ds/596Mi)
% 114.25/16.91 % (1426408)Instruction limit reached!
% 114.25/16.91 % (1426408)------------------------------
% 114.25/16.91 % (1426408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.25/16.91 % (1426408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.25/16.91 % (1426408)CaDiCaL version: 2.1.3
% 114.25/16.91 % (1426408)Termination reason: Instruction limit
% 114.25/16.91 % (1426408)Termination phase: Saturation
% 114.25/16.91 % (1426408)Time elapsed: 0.329 s
% 114.25/16.91 % (1426408)Peak memory usage: 93 MB
% 114.25/16.91 % (1426408)Instructions burned: 596 (million)
% 114.25/16.91 % (1426410)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1868240883:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi)
% 114.25/16.91 % (1426404)Instruction limit reached!
% 114.25/16.91 % (1426404)------------------------------
% 114.25/16.91 % (1426404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.25/16.91 % (1426404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.25/16.91 % (1426404)CaDiCaL version: 2.1.3
% 114.25/16.91 % (1426404)Termination reason: Instruction limit
% 114.25/16.91 % (1426404)Termination phase: Saturation
% 114.25/16.91 % (1426404)Time elapsed: 0.982 s
% 114.25/16.91 % (1426404)Peak memory usage: 143 MB
% 114.25/16.91 % (1426404)Instructions burned: 2943 (million)
% 114.25/16.91 % (1426412)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4247576443:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2927 on theBenchmark for (2927ds/16411Mi)
% 114.25/16.91 % (1426386)Instruction limit reached!
% 114.25/16.91 % (1426386)------------------------------
% 114.25/16.91 % (1426386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.25/16.91 % (1426386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.25/16.91 % (1426386)CaDiCaL version: 2.1.3
% 114.25/16.91 % (1426386)Termination reason: Instruction limit
% 114.25/16.91 % (1426386)Termination phase: Saturation
% 114.25/16.91 % (1426386)Time elapsed: 4.740 s
% 114.25/16.91 % (1426386)Peak memory usage: 194 MB
% 114.25/16.91 % (1426386)Instructions burned: 8481 (million)
% 114.25/16.91 % (1426414)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2139095326:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2924 on theBenchmark for (2924ds/1670Mi)
% 114.25/16.91 % (1426414)Instruction limit reached!
% 114.25/16.91 % (1426414)------------------------------
% 114.25/16.91 % (1426414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.25/16.91 % (1426414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.25/16.91 % (1426414)CaDiCaL version: 2.1.3
% 114.25/16.91 % (1426414)Termination reason: Instruction limit
% 114.25/16.91 % (1426414)Termination phase: Saturation
% 114.25/16.91 % (1426414)Time elapsed: 1.007 s
% 114.25/16.91 % (1426414)Peak memory usage: 139 MB
% 114.25/16.91 % (1426414)Instructions burned: 1671 (million)
% 114.25/16.91 % (1426416)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3478567200:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2913 on theBenchmark for (2913ds/1722Mi)
% 114.25/16.91 % (1426410)Instruction limit reached!
% 114.25/16.91 % (1426410)------------------------------
% 114.25/16.91 % (1426410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.25/16.91 % (1426410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.25/16.91 % (1426410)CaDiCaL version: 2.1.3
% 114.25/16.91 % (1426410)Termination reason: Instruction limit
% 114.25/16.91 % (1426410)Termination phase: Saturation
% 114.25/16.91 % (1426410)Time elapsed: 2.401 s
% 114.25/16.91 % (1426410)Peak memory usage: 160 MB
% 114.25/16.91 % (1426410)Instructions burned: 4124 (million)
% 114.25/16.91 % (1426418)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2646410989:cts=off:cond=on:i=9530:bs=on:fsd=on_2905 on theBenchmark for (2905ds/9530Mi)
% 126.51/18.56 % (1426416)Instruction limit reached!
% 126.51/18.56 % (1426416)------------------------------
% 126.51/18.56 % (1426416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426416)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426416)Termination reason: Instruction limit
% 126.51/18.56 % (1426416)Termination phase: Saturation
% 126.51/18.56 % (1426416)Time elapsed: 1.102 s
% 126.51/18.56 % (1426416)Peak memory usage: 140 MB
% 126.51/18.56 % (1426416)Instructions burned: 1723 (million)
% 126.51/18.56 % (1426420)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2869442784:st=2:i=4495:sd=10:ss=included_2900 on theBenchmark for (2900ds/4495Mi)
% 126.51/18.56 % (1426405)Instruction limit reached!
% 126.51/18.56 % (1426405)------------------------------
% 126.51/18.56 % (1426405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426405)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426405)Termination reason: Instruction limit
% 126.51/18.56 % (1426405)Termination phase: Saturation
% 126.51/18.56 % (1426405)Time elapsed: 4.126 s
% 126.51/18.56 % (1426405)Peak memory usage: 187 MB
% 126.51/18.56 % (1426405)Instructions burned: 6922 (million)
% 126.51/18.56 % (1426422)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3478241994:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 126.51/18.56 % (1426412)Instruction limit reached!
% 126.51/18.56 % (1426412)------------------------------
% 126.51/18.56 % (1426412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426412)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426412)Termination reason: Instruction limit
% 126.51/18.56 % (1426412)Termination phase: Saturation
% 126.51/18.56 % (1426412)Time elapsed: 5.327 s
% 126.51/18.56 % (1426412)Peak memory usage: 263 MB
% 126.51/18.56 % (1426412)Instructions burned: 16414 (million)
% 126.51/18.56 % (1426420)Instruction limit reached!
% 126.51/18.56 % (1426420)------------------------------
% 126.51/18.56 % (1426420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426420)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426420)Termination reason: Instruction limit
% 126.51/18.56 % (1426420)Termination phase: Saturation
% 126.51/18.56 % (1426420)Time elapsed: 2.638 s
% 126.51/18.56 % (1426420)Peak memory usage: 161 MB
% 126.51/18.56 % (1426420)Instructions burned: 4496 (million)
% 126.51/18.56 % (1426424)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=490451981:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2873 on theBenchmark for (2873ds/2083Mi)
% 126.51/18.56 % (1426425)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=958334530:i=4629:av=off:gsp=on_2873 on theBenchmark for (2873ds/4629Mi)
% 126.51/18.56 % (1426424)Instruction limit reached!
% 126.51/18.56 % (1426424)------------------------------
% 126.51/18.56 % (1426424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426424)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426424)Termination reason: Instruction limit
% 126.51/18.56 % (1426424)Termination phase: Saturation
% 126.51/18.56 % (1426424)Time elapsed: 0.753 s
% 126.51/18.56 % (1426424)Peak memory usage: 139 MB
% 126.51/18.56 % (1426424)Instructions burned: 2085 (million)
% 126.51/18.56 % (1426428)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=416897486:i=1258:av=off_2865 on theBenchmark for (2865ds/1258Mi)
% 126.51/18.56 % (1426422)Instruction limit reached!
% 126.51/18.56 % (1426422)------------------------------
% 126.51/18.56 % (1426422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.51/18.56 % (1426422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.51/18.56 % (1426422)CaDiCaL version: 2.1.3
% 126.51/18.56 % (1426422)Termination reason: Instruction limit
% 126.51/18.56 % (1426422)Termination phase: Saturation
% 151.69/22.08 % (1426422)Time elapsed: 3.006 s
% 151.69/22.08 % (1426422)Peak memory usage: 166 MB
% 151.69/22.08 % (1426422)Instructions burned: 4920 (million)
% 151.69/22.08 % (1426430)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=616220304:i=7343:av=off:ss=included_2862 on theBenchmark for (2862ds/7343Mi)
% 151.69/22.08 % (1426428)Instruction limit reached!
% 151.69/22.08 % (1426428)------------------------------
% 151.69/22.08 % (1426428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426428)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426428)Termination reason: Instruction limit
% 151.69/22.08 % (1426428)Termination phase: Saturation
% 151.69/22.08 % (1426428)Time elapsed: 0.381 s
% 151.69/22.08 % (1426428)Peak memory usage: 94 MB
% 151.69/22.08 % (1426428)Instructions burned: 1259 (million)
% 151.69/22.08 % (1426432)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2293725479:i=1325:sd=2:ss=axioms:sgt=16_2860 on theBenchmark for (2860ds/1325Mi)
% 151.69/22.08 % (1426432)Instruction limit reached!
% 151.69/22.08 % (1426432)------------------------------
% 151.69/22.08 % (1426432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426432)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426432)Termination reason: Instruction limit
% 151.69/22.08 % (1426432)Termination phase: Saturation
% 151.69/22.08 % (1426432)Time elapsed: 0.720 s
% 151.69/22.08 % (1426432)Peak memory usage: 100 MB
% 151.69/22.08 % (1426432)Instructions burned: 1325 (million)
% 151.69/22.08 % (1426434)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3578927222:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2851 on theBenchmark for (2851ds/2646Mi)
% 151.69/22.08 % (1426418)Instruction limit reached!
% 151.69/22.08 % (1426418)------------------------------
% 151.69/22.08 % (1426418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426418)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426418)Termination reason: Instruction limit
% 151.69/22.08 % (1426418)Termination phase: Saturation
% 151.69/22.08 % (1426418)Time elapsed: 5.674 s
% 151.69/22.08 % (1426418)Peak memory usage: 163 MB
% 151.69/22.08 % (1426418)Instructions burned: 9531 (million)
% 151.69/22.08 % (1426425)Instruction limit reached!
% 151.69/22.08 % (1426425)------------------------------
% 151.69/22.08 % (1426425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426425)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426425)Termination reason: Instruction limit
% 151.69/22.08 % (1426425)Termination phase: Saturation
% 151.69/22.08 % (1426425)Time elapsed: 2.427 s
% 151.69/22.08 % (1426425)Peak memory usage: 151 MB
% 151.69/22.08 % (1426425)Instructions burned: 4629 (million)
% 151.69/22.08 % (1426436)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4123861869:i=1489:sd=2:ep=R:ss=axioms_2847 on theBenchmark for (2847ds/1489Mi)
% 151.69/22.08 % (1426437)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3814762259:i=1503_2847 on theBenchmark for (2847ds/1503Mi)
% 151.69/22.08 % (1426436)Instruction limit reached!
% 151.69/22.08 % (1426436)------------------------------
% 151.69/22.08 % (1426436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426436)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426436)Termination reason: Instruction limit
% 151.69/22.08 % (1426436)Termination phase: Saturation
% 151.69/22.08 % (1426436)Time elapsed: 0.904 s
% 151.69/22.08 % (1426436)Peak memory usage: 134 MB
% 151.69/22.08 % (1426436)Instructions burned: 1490 (million)
% 151.69/22.08 % (1426437)Instruction limit reached!
% 151.69/22.08 % (1426437)------------------------------
% 151.69/22.08 % (1426437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.69/22.08 % (1426437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.69/22.08 % (1426437)CaDiCaL version: 2.1.3
% 151.69/22.08 % (1426437)Termination reason: Instruction limit
% 151.69/22.08 % (1426437)Termination phase: Saturation
% 174.03/25.22 % (1426437)Time elapsed: 0.903 s
% 174.03/25.22 % (1426437)Peak memory usage: 139 MB
% 174.03/25.22 % (1426437)Instructions burned: 1505 (million)
% 174.03/25.22 % (1426430)Instruction limit reached!
% 174.03/25.22 % (1426430)------------------------------
% 174.03/25.22 % (1426430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.03/25.22 % (1426430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.03/25.22 % (1426430)CaDiCaL version: 2.1.3
% 174.03/25.22 % (1426430)Termination reason: Instruction limit
% 174.03/25.22 % (1426430)Termination phase: Saturation
% 174.03/25.22 % (1426430)Time elapsed: 2.452 s
% 174.03/25.22 % (1426430)Peak memory usage: 182 MB
% 174.03/25.22 % (1426430)Instructions burned: 7345 (million)
% 174.03/25.22 % (1426440)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2553188521:i=13942:kws=frequency_2837 on theBenchmark for (2837ds/13942Mi)
% 174.03/25.22 % (1426441)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2416661568:i=3604:fsr=off:er=filter_2837 on theBenchmark for (2837ds/3604Mi)
% 174.03/25.22 % (1426442)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3756166322:i=1876:sd=1:ss=included:sgt=32_2836 on theBenchmark for (2836ds/1876Mi)
% 174.03/25.22 % (1426434)Instruction limit reached!
% 174.03/25.22 % (1426434)------------------------------
% 174.03/25.22 % (1426434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.03/25.22 % (1426434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.03/25.22 % (1426434)CaDiCaL version: 2.1.3
% 174.03/25.22 % (1426434)Termination reason: Instruction limit
% 174.03/25.22 % (1426434)Termination phase: Saturation
% 174.03/25.22 % (1426434)Time elapsed: 1.580 s
% 174.03/25.22 % (1426434)Peak memory usage: 144 MB
% 174.03/25.22 % (1426434)Instructions burned: 2647 (million)
% 174.03/25.22 % (1426446)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1914520062:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2834 on theBenchmark for (2834ds/1932Mi)
% 174.03/25.22 % (1426442)Instruction limit reached!
% 174.03/25.22 % (1426442)------------------------------
% 174.03/25.22 % (1426442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.03/25.22 % (1426442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.03/25.22 % (1426442)CaDiCaL version: 2.1.3
% 174.03/25.22 % (1426442)Termination reason: Instruction limit
% 174.03/25.22 % (1426442)Termination phase: Saturation
% 174.03/25.22 % (1426442)Time elapsed: 0.644 s
% 174.03/25.22 % (1426442)Peak memory usage: 139 MB
% 174.03/25.22 % (1426442)Instructions burned: 1879 (million)
% 174.03/25.22 % (1426448)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=109434934:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2829 on theBenchmark for (2829ds/1980Mi)
% 174.03/25.22 % (1426446)Instruction limit reached!
% 174.03/25.22 % (1426446)------------------------------
% 174.03/25.22 % (1426446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.03/25.22 % (1426446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.03/25.22 % (1426446)CaDiCaL version: 2.1.3
% 174.03/25.22 % (1426446)Termination reason: Instruction limit
% 174.03/25.22 % (1426446)Termination phase: Saturation
% 174.03/25.22 % (1426446)Time elapsed: 1.146 s
% 174.03/25.22 % (1426446)Peak memory usage: 139 MB
% 174.03/25.22 % (1426446)Instructions burned: 1933 (million)
% 174.03/25.22 % (1426448)Instruction limit reached!
% 174.03/25.22 % (1426448)------------------------------
% 174.03/25.22 % (1426448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 174.03/25.22 % (1426448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 174.03/25.22 % (1426448)CaDiCaL version: 2.1.3
% 174.03/25.22 % (1426448)Termination reason: Instruction limit
% 174.03/25.22 % (1426448)Termination phase: Saturation
% 174.03/25.22 % (1426448)Time elapsed: 0.679 s
% 174.03/25.22 % (1426448)Peak memory usage: 141 MB
% 174.03/25.22 % (1426448)Instructions burned: 1982 (million)
% 174.03/25.22 % (1426450)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=2153945638:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2821 on theBenchmark for (2821ds/3902Mi)
% 199.67/28.88 % (1426451)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3290385377:avsq=on:i=3916:aac=none:amm=off_2821 on theBenchmark for (2821ds/3916Mi)
% 199.67/28.88 % (1426441)Instruction limit reached!
% 199.67/28.88 % (1426441)------------------------------
% 199.67/28.88 % (1426441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.67/28.88 % (1426441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.67/28.88 % (1426441)CaDiCaL version: 2.1.3
% 199.67/28.88 % (1426441)Termination reason: Instruction limit
% 199.67/28.88 % (1426441)Termination phase: Saturation
% 199.67/28.88 % (1426441)Time elapsed: 1.995 s
% 199.67/28.88 % (1426441)Peak memory usage: 143 MB
% 199.67/28.88 % (1426441)Instructions burned: 3605 (million)
% 199.67/28.88 % (1426454)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2573674050:cond=on:i=3940:av=off:er=known_2815 on theBenchmark for (2815ds/3940Mi)
% 199.67/28.88 % (1426451)Instruction limit reached!
% 199.67/28.88 % (1426451)------------------------------
% 199.67/28.88 % (1426451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.67/28.88 % (1426451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.67/28.88 % (1426451)CaDiCaL version: 2.1.3
% 199.67/28.88 % (1426451)Termination reason: Instruction limit
% 199.67/28.88 % (1426451)Termination phase: Saturation
% 199.67/28.88 % (1426451)Time elapsed: 1.262 s
% 199.67/28.88 % (1426451)Peak memory usage: 128 MB
% 199.67/28.88 % (1426451)Instructions burned: 3917 (million)
% 199.67/28.88 % (1426456)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3613365220:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2807 on theBenchmark for (2807ds/3980Mi)
% 199.67/28.88 % (1426450)Instruction limit reached!
% 199.67/28.88 % (1426450)------------------------------
% 199.67/28.88 % (1426450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.67/28.88 % (1426450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.67/28.88 % (1426450)CaDiCaL version: 2.1.3
% 199.67/28.88 % (1426450)Termination reason: Instruction limit
% 199.67/28.88 % (1426450)Termination phase: Saturation
% 199.67/28.88 % (1426450)Time elapsed: 2.089 s
% 199.67/28.88 % (1426450)Peak memory usage: 149 MB
% 199.67/28.88 % (1426450)Instructions burned: 3904 (million)
% 199.67/28.88 % (1426459)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1926725823:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2799 on theBenchmark for (2799ds/2087Mi)
% 199.67/28.88 % (1426456)Instruction limit reached!
% 199.67/28.88 % (1426456)------------------------------
% 199.67/28.88 % (1426456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.67/28.88 % (1426456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.67/28.88 % (1426456)CaDiCaL version: 2.1.3
% 199.67/28.88 % (1426456)Termination reason: Instruction limit
% 199.67/28.88 % (1426456)Termination phase: Saturation
% 199.67/28.88 % (1426456)Time elapsed: 1.303 s
% 199.67/28.88 % (1426456)Peak memory usage: 157 MB
% 199.67/28.88 % (1426456)Instructions burned: 3982 (million)
% 199.67/28.88 % (1426461)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=618155587:cts=off:cond=on:i=4272:bs=on:fsd=on_2794 on theBenchmark for (2794ds/4272Mi)
% 199.67/28.88 % (1426454)Instruction limit reached!
% 199.67/28.88 % (1426454)------------------------------
% 199.67/28.88 % (1426454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.67/28.88 % (1426454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.67/28.88 % (1426454)CaDiCaL version: 2.1.3
% 199.67/28.88 % (1426454)Termination reason: Instruction limit
% 199.67/28.88 % (1426454)Termination phase: Saturation
% 199.67/28.88 % (1426454)Time elapsed: 2.288 s
% 199.67/28.88 % (1426454)Peak memory usage: 155 MB
% 199.67/28.88 % (1426454)Instructions burned: 3941 (million)
% 199.67/28.88 % (1426463)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=738933089:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2791 on theBenchmark for (2791ds/2197Mi)
% 199.67/28.88 % (1426459)Instruction limit reached!
% 199.67/28.88 % (1426459)------------------------------
% 199.67/28.88 % (1426459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426459)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426459)Termination reason: Instruction limit
% 139.76/29.41 % (1426459)Termination phase: Saturation
% 139.76/29.41 % (1426459)Time elapsed: 1.309 s
% 139.76/29.41 % (1426459)Peak memory usage: 141 MB
% 139.76/29.41 % (1426459)Instructions burned: 2088 (million)
% 139.76/29.41 % (1426465)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1605759600:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2785 on theBenchmark for (2785ds/6508Mi)
% 139.76/29.41 % (1426461)Instruction limit reached!
% 139.76/29.41 % (1426461)------------------------------
% 139.76/29.41 % (1426461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426461)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426461)Termination reason: Instruction limit
% 139.76/29.41 % (1426461)Termination phase: Saturation
% 139.76/29.41 % (1426461)Time elapsed: 1.452 s
% 139.76/29.41 % (1426461)Peak memory usage: 157 MB
% 139.76/29.41 % (1426461)Instructions burned: 4272 (million)
% 139.76/29.41 % (1426467)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3402717855:i=2330:fgj=on:av=off:fsr=off_2778 on theBenchmark for (2778ds/2330Mi)
% 139.76/29.41 % (1426463)Instruction limit reached!
% 139.76/29.41 % (1426463)------------------------------
% 139.76/29.41 % (1426463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426463)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426463)Termination reason: Instruction limit
% 139.76/29.41 % (1426463)Termination phase: Saturation
% 139.76/29.41 % (1426463)Time elapsed: 1.335 s
% 139.76/29.41 % (1426463)Peak memory usage: 141 MB
% 139.76/29.41 % (1426463)Instructions burned: 2198 (million)
% 139.76/29.41 % (1426469)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1006241842:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2776 on theBenchmark for (2776ds/7592Mi)
% 139.76/29.41 % (1426467)Instruction limit reached!
% 139.76/29.41 % (1426467)------------------------------
% 139.76/29.41 % (1426467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426467)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426467)Termination reason: Instruction limit
% 139.76/29.41 % (1426467)Termination phase: Saturation
% 139.76/29.41 % (1426467)Time elapsed: 0.734 s
% 139.76/29.41 % (1426467)Peak memory usage: 141 MB
% 139.76/29.41 % (1426467)Instructions burned: 2332 (million)
% 139.76/29.41 % (1426471)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=2433084620:i=2693:kws=precedence:ins=1:av=off_2770 on theBenchmark for (2770ds/2693Mi)
% 139.76/29.41 % (1426471)Instruction limit reached!
% 139.76/29.41 % (1426471)------------------------------
% 139.76/29.41 % (1426471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426471)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426471)Termination reason: Instruction limit
% 139.76/29.41 % (1426471)Termination phase: Saturation
% 139.76/29.41 % (1426471)Time elapsed: 0.918 s
% 139.76/29.41 % (1426471)Peak memory usage: 149 MB
% 139.76/29.41 % (1426471)Instructions burned: 2694 (million)
% 139.76/29.41 % (1426473)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2885711994:i=28651:sd=4:ss=included:sgt=64_2760 on theBenchmark for (2760ds/28651Mi)
% 139.76/29.41 % (1426440)Instruction limit reached!
% 139.76/29.41 % (1426440)------------------------------
% 139.76/29.41 % (1426440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426440)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426440)Termination reason: Instruction limit
% 139.76/29.41 % (1426440)Termination phase: Saturation
% 139.76/29.41 % (1426440)Time elapsed: 8.043 s
% 139.76/29.41 % (1426440)Peak memory usage: 248 MB
% 139.76/29.41 % (1426440)Instructions burned: 13942 (million)
% 139.76/29.41 % (1426475)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=3398168027:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2755 on theBenchmark for (2755ds/2700Mi)
% 139.76/29.41 % (1426465)Instruction limit reached!
% 139.76/29.41 % (1426465)------------------------------
% 139.76/29.41 % (1426465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426465)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426465)Termination reason: Instruction limit
% 139.76/29.41 % (1426465)Termination phase: Saturation
% 139.76/29.41 % (1426465)Time elapsed: 3.605 s
% 139.76/29.41 % (1426465)Peak memory usage: 126 MB
% 139.76/29.41 % (1426465)Instructions burned: 6509 (million)
% 139.76/29.41 % (1426477)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3234771794:i=3196:nm=4_2747 on theBenchmark for (2747ds/3196Mi)
% 139.76/29.41 % (1426475)Instruction limit reached!
% 139.76/29.41 % (1426475)------------------------------
% 139.76/29.41 % (1426475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426475)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426475)Termination reason: Instruction limit
% 139.76/29.41 % (1426475)Termination phase: Saturation
% 139.76/29.41 % (1426475)Time elapsed: 1.633 s
% 139.76/29.41 % (1426475)Peak memory usage: 146 MB
% 139.76/29.41 % (1426475)Instructions burned: 2701 (million)
% 139.76/29.41 % (1426479)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=3099355644:cts=off:i=3254:av=off_2737 on theBenchmark for (2737ds/3254Mi)
% 139.76/29.41 % (1426469)Instruction limit reached!
% 139.76/29.41 % (1426469)------------------------------
% 139.76/29.41 % (1426469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426469)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426469)Termination reason: Instruction limit
% 139.76/29.41 % (1426469)Termination phase: Saturation
% 139.76/29.41 % (1426469)Time elapsed: 4.305 s
% 139.76/29.41 % (1426469)Peak memory usage: 117 MB
% 139.76/29.41 % (1426469)Instructions burned: 7593 (million)
% 139.76/29.41 % (1426481)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1419999760:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2732 on theBenchmark for (2732ds/3264Mi)
% 139.76/29.41 % (1426477)Instruction limit reached!
% 139.76/29.41 % (1426477)------------------------------
% 139.76/29.41 % (1426477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426477)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426477)Termination reason: Instruction limit
% 139.76/29.41 % (1426477)Termination phase: Saturation
% 139.76/29.41 % (1426477)Time elapsed: 1.764 s
% 139.76/29.41 % (1426477)Peak memory usage: 149 MB
% 139.76/29.41 % (1426477)Instructions burned: 3197 (million)
% 139.76/29.41 % (1426483)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=184547436:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2728 on theBenchmark for (2728ds/9708Mi)
% 139.76/29.41 % (1426483)Refutation not found, incomplete strategy
% 139.76/29.41 % (1426483)------------------------------
% 139.76/29.41 % (1426483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426483)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426483)Termination reason: Refutation not found, incomplete strategy
% 139.76/29.41 % (1426483)Time elapsed: 0.681 s
% 139.76/29.41 % (1426483)Peak memory usage: 138 MB
% 139.76/29.41 % (1426483)Instructions burned: 1055 (million)
% 139.76/29.41 % (1426483)------------------------------
% 139.76/29.41 % (1426483)------------------------------
% 139.76/29.41 % (1426479)Instruction limit reached!
% 139.76/29.41 % (1426479)------------------------------
% 139.76/29.41 % (1426479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.76/29.41 % (1426479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.76/29.41 % (1426479)CaDiCaL version: 2.1.3
% 139.76/29.41 % (1426479)Termination reason: Instruction limit
% 139.76/29.41 % (1426479)Termination phase: Saturation
% 139.76/29.41 % (1426479)Time elapsed: 1.888 s
% 139.76/29.41 % (1426479)Peak memory usage: 150 MB
% 139.76/29.41 % (1426479)Instructions burned: 3254 (million)
% 139.76/29.41 % (1426485)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3095034585:i=21997:s2at=5:gtg=all_2718 on theBenchmark for (2718ds/21997Mi)
% 139.76/29.41 % (1426486)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3784124686:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2717 on theBenchmark for (2717ds/7551Mi)
% 139.76/29.41 % (1426481)First to succeed.
% 139.76/29.41 % (1426481)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1426325"
% 139.76/29.41 % (1426481)Refutation found. Thanks to Tanya!
% 139.76/29.41 % SZS status Unsatisfiable for theBenchmark
% 139.76/29.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/29.60 % (1426481)------------------------------
% 0.18/29.60 % (1426481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/29.60 % (1426481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/29.60 % (1426481)CaDiCaL version: 2.1.3
% 0.18/29.60 % (1426481)Termination reason: Refutation
% 0.18/29.60 % (1426481)Time elapsed: 1.534 s
% 0.18/29.60 % (1426481)Peak memory usage: 143 MB
% 0.18/29.60 % (1426481)Instructions burned: 2419 (million)
% 0.18/29.60 % (1426481)------------------------------
% 0.18/29.60 % (1426481)------------------------------
% 0.18/29.60 % (1426325)Success in time 28.789 s
% 0.18/29.60 % Vampire exiting
%------------------------------------------------------------------------------