%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT030-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:46 PM UTC 2026
% Result : Unsatisfiable 11.54s 3.04s
% Output : Refutation 15.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 41
% Syntax : Number of formulae : 205 ( 62 unt; 19 def)
% Number of atoms : 424 ( 107 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 415 ( 196 ~; 206 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 16 ( 14 usr; 14 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 12 con; 0-5 aty)
% Number of variables : 381 ( 0 sgn 381 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f65,axiom,
! [X0,X1] : hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f102,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(c_COMBB(X0,X1,X2,X3,X4),X5) = hAPP(X0,hAPP(X1,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
fof(f211,axiom,
! [X2,X3,X0,X1] : hAPP(c_Set_Ovimage(X0,X1,X2),c_Collect(X3,X2)) = c_Collect(c_COMBB(X3,X0,X2,tc_bool,X1),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__Collect__eq_0) ).
fof(f344,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f373,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/sandbox/benchmark/theBenchmark.p',cls_Diff__cancel_0) ).
fof(f374,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,[],[f373]) ).
fof(f375,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/sandbox/benchmark/theBenchmark.p',cls_Compl__eq__Diff__UNIV_0) ).
fof(f402,axiom,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_Collect(c_COMBB(c_Not,hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),tc_bool,tc_bool,X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Compl__eq_0) ).
fof(f452,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5) = hAPP(hAPP(X0,X5),X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
fof(f453,axiom,
! [X2,X3,X0,X1] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBK__def_0) ).
fof(f565,axiom,
! [X0,X1] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f587,axiom,
! [X0,X1] : hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_top1I_0) ).
fof(f607,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Set_Ovimage(c_COMBK(X0,X1,X2),X2,X1),X3) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__const_1) ).
fof(f608,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_Set_Ovimage(c_COMBK(X0,X1,X2),X2,X1),X3)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(reorient_equations,[],[f607]) ).
fof(f627,axiom,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0)
| ~ hBOOL(hAPP(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f628,axiom,
! [X2,X0,X1] : hBOOL(hAPP(hAPP(c_Set_Oinsert(X0,X1),X2),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f662,axiom,
! [X2,X3,X0,X1] :
( hAPP(c_Set_Ovimage(c_COMBK(X0,X1,X2),X2,X1),X3) = c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__const_0) ).
fof(f663,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = hAPP(c_Set_Ovimage(c_COMBK(X0,X1,X2),X2,X1),X3)
| ~ hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(reorient_equations,[],[f662]) ).
fof(f671,axiom,
! [X0,X1] : c_Collect(hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),X0) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__mem__eq_0) ).
fof(f684,axiom,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ominus__class_Ominus(X3,tc_fun(X0,tc_bool)),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f692,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/sandbox/benchmark/theBenchmark.p',cls_ComplI_0) ).
fof(f693,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/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f747,axiom,
! [X2,X0,X1] :
( hAPP(c_Set_Oinsert(X0,X1),X2) = X2
| ~ hBOOL(hAPP(hAPP(c_in(X1),X0),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f779,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f813,axiom,
! [X0,X1] : hBOOL(hAPP(hAPP(c_fequal(X0),X1),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ATP__Linkup_Oequal__imp__fequal_0) ).
fof(f815,definition,
sF0 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f816,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(reorient_equations,[],[f815]) ).
fof(f817,definition,
sF1 = tc_fun(sF0,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f818,plain,
tc_fun(sF0,tc_bool) = sF1,
inference(reorient_equations,[],[f817]) ).
fof(f819,definition,
sF2 = tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f820,plain,
tc_fun(tc_Arrow__Order__Mirabelle_Oindi,sF1) = sF2,
inference(reorient_equations,[],[f819]) ).
fof(f821,definition,
sF3 = c_in(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f822,plain,
c_in(sF2) = sF3,
inference(reorient_equations,[],[f821]) ).
fof(f823,definition,
sF4 = hAPP(sF3,v_Q____),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f824,plain,
hAPP(sF3,v_Q____) = sF4,
inference(reorient_equations,[],[f823]) ).
fof(f825,definition,
sF5 = hAPP(sF4,c_Arrow__Order__Mirabelle_OProf),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f826,plain,
hAPP(sF4,c_Arrow__Order__Mirabelle_OProf) = sF5,
inference(reorient_equations,[],[f825]) ).
fof(f827,plain,
~ hBOOL(sF5),
inference(definition_folding,[],[f779,f826,f824,f822,f820,f818,f816]) ).
fof(f872,plain,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != X1
| ~ hBOOL(hAPP(X1,X2)) ),
inference(backward_demodulation,[],[f627,f344]) ).
fof(f876,plain,
! [X0,X1] : hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1) = X1,
inference(backward_demodulation,[],[f671,f344]) ).
fof(f879,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_COMBB(c_Not,hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1),tc_bool,tc_bool,X0),
inference(backward_demodulation,[],[f402,f344]) ).
fof(f888,plain,
! [X2,X3,X0,X1] : hAPP(c_Set_Ovimage(X0,X1,X2),c_Collect(X3,X2)) = c_COMBB(X3,X0,X2,tc_bool,X1),
inference(forward_demodulation,[],[f211,f344]) ).
fof(f938,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_COMBB(c_Not,X1,tc_bool,tc_bool,X0),
inference(backward_demodulation,[],[f879,f876]) ).
fof(f942,plain,
! [X2,X3,X0,X1] : c_COMBB(X3,X0,X2,tc_bool,X1) = hAPP(c_Set_Ovimage(X0,X1,X2),X3),
inference(forward_demodulation,[],[f888,f344]) ).
fof(f965,plain,
! [X0,X1] : hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),tc_fun(X0,tc_bool)),X1) = c_COMBB(c_Not,X1,tc_bool,tc_bool,X0),
inference(backward_demodulation,[],[f375,f938]) ).
fof(f972,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),c_COMBB(c_Not,X2,tc_bool,tc_bool,X0)))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(backward_demodulation,[],[f692,f938]) ).
fof(f973,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_COMBB(c_Not,X2,tc_bool,tc_bool,X0)))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(backward_demodulation,[],[f693,f938]) ).
fof(f1002,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_COMBB(X3,c_COMBK(X0,X1,X2),X1,tc_bool,X2)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(backward_demodulation,[],[f608,f942]) ).
fof(f1003,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = c_COMBB(X3,c_COMBK(X0,X1,X2),X1,tc_bool,X2)
| ~ hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(backward_demodulation,[],[f663,f942]) ).
fof(f1038,plain,
! [X2,X0,X1] : hAPP(X0,X2) = hAPP(hAPP(c_in(X1),X2),X0),
inference(superposition,[],[f452,f876]) ).
fof(f1103,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(X2,X1))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ominus__class_Ominus(X3,tc_fun(X0,tc_bool)),X2))) ),
inference(backward_demodulation,[],[f684,f1038]) ).
fof(f1125,plain,
! [X2,X0,X1] :
( hAPP(c_Set_Oinsert(X0,X1),X2) = X2
| ~ hBOOL(hAPP(X2,X0)) ),
inference(backward_demodulation,[],[f747,f1038]) ).
fof(f1148,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP(c_in(X0),X1),c_COMBB(c_Not,X2,tc_bool,tc_bool,X0))) ),
inference(backward_demodulation,[],[f972,f1038]) ).
fof(f1149,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X2,X1))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_COMBB(c_Not,X2,tc_bool,tc_bool,X0))) ),
inference(backward_demodulation,[],[f973,f1038]) ).
fof(f1150,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_COMBB(X3,c_COMBK(X0,X1,X2),X1,tc_bool,X2)
| hBOOL(hAPP(X3,X0)) ),
inference(backward_demodulation,[],[f1002,f1038]) ).
fof(f1151,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)) = c_COMBB(X3,c_COMBK(X0,X1,X2),X1,tc_bool,X2)
| ~ hBOOL(hAPP(X3,X0)) ),
inference(backward_demodulation,[],[f1003,f1038]) ).
fof(f1199,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_COMBB(c_Not,X2,tc_bool,tc_bool,X0),X1))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1149,f1038]) ).
fof(f1200,plain,
! [X2,X0,X1] :
( hBOOL(hAPP(c_COMBB(c_Not,X2,tc_bool,tc_bool,X0),X1))
| hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1148,f1038]) ).
fof(f1217,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Ominus__class_Ominus(X3,tc_fun(X0,tc_bool)),X2),X1))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1103,f1038]) ).
fof(f1254,plain,
! [X2,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(X2,X1)))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1199,f102]) ).
fof(f1255,plain,
! [X2,X1] :
( hBOOL(hAPP(c_Not,hAPP(X2,X1)))
| hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1200,f102]) ).
fof(f1269,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Not,X0))
| ~ hBOOL(X0) ),
inference(superposition,[],[f1254,f876]) ).
fof(f1286,plain,
( hBOOL(hAPP(c_Not,sF5))
| hBOOL(sF5) ),
inference(superposition,[],[f1255,f826]) ).
fof(f1287,plain,
hBOOL(hAPP(c_Not,sF5)),
inference(forward_subsumption_resolution,[],[f1286,f827]) ).
fof(f1298,plain,
! [X0,X1] : hAPP(X0,X1) = hAPP(hAPP(sF3,X1),X0),
inference(superposition,[],[f1038,f822]) ).
fof(f1325,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| c_Orderings_Obot__class_Obot(sF1) != X0 ),
inference(superposition,[],[f872,f818]) ).
fof(f1329,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) != c_Orderings_Obot__class_Obot(sF1),
inference(resolution,[],[f1325,f813]) ).
fof(f1330,plain,
! [X2,X0,X1] : hAPP(c_Set_Oinsert(X0,X1),X2) != c_Orderings_Obot__class_Obot(sF1),
inference(resolution,[],[f1325,f628]) ).
fof(f1364,definition,
( spl6_6
<=> ! [X0] : ~ hBOOL(X0) ),
introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition]) ).
fof(f1365,plain,
( ! [X0] : ~ hBOOL(X0)
| ~ spl6_6 ),
inference(avatar_component_clause,[],[f1364]) ).
fof(f1367,plain,
! [X0] : c_COMBB(c_Not,X0,tc_bool,tc_bool,sF0) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),
inference(superposition,[],[f938,f818]) ).
fof(f1386,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : hAPP(X1,X0) = hAPP(c_COMBB(X1,c_COMBK(X0,X2,X3),X4,X5,X6),X7),
inference(superposition,[],[f102,f453]) ).
fof(f1438,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : hAPP(c_COMBB(c_COMBK(X0,X1,X2),X3,X4,X5,X6),X7) = X0,
inference(superposition,[],[f453,f102]) ).
fof(f1442,plain,
! [X0] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X0)),
inference(superposition,[],[f565,f818]) ).
fof(f1550,plain,
! [X2,X0,X1,X4] :
( hAPP(X1,X2) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4)
| hBOOL(hAPP(X1,X2)) ),
inference(superposition,[],[f1386,f1150]) ).
fof(f1555,plain,
! [X2,X3,X0,X1,X6,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X6) = X1
| hBOOL(hAPP(c_COMBK(X1,X2,X3),X4)) ),
inference(superposition,[],[f1438,f1150]) ).
fof(f1568,plain,
! [X0,X1,X6] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X6) = X1
| hBOOL(X1) ),
inference(forward_demodulation,[],[f1555,f453]) ).
fof(f1569,plain,
! [X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = X1
| hBOOL(X1) ),
inference(superposition,[],[f1568,f818]) ).
fof(f1593,plain,
! [X2,X0,X1,X4] :
( hAPP(X1,X2) = hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X4)
| ~ hBOOL(hAPP(X1,X2)) ),
inference(superposition,[],[f1386,f1151]) ).
fof(f1596,plain,
! [X2,X3,X0,X1,X6,X4] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X6) = X1
| ~ hBOOL(hAPP(c_COMBK(X1,X2,X3),X4)) ),
inference(superposition,[],[f1438,f1151]) ).
fof(f1597,plain,
! [X0,X1,X6] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X6) = X1
| ~ hBOOL(X1) ),
inference(forward_demodulation,[],[f1596,f453]) ).
fof(f1651,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(X2,hAPP(X3,X7))
| hBOOL(hAPP(c_COMBB(X2,X3,X4,X5,X6),X7)) ),
inference(superposition,[],[f102,f1550]) ).
fof(f1666,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = X4
| ~ hBOOL(hAPP(X4,X2))
| hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4)) ),
inference(superposition,[],[f1125,f1550]) ).
fof(f1670,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(X2,X3) = hAPP(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1),X2)
| hBOOL(hAPP(c_in(X4),X3)) ),
inference(superposition,[],[f1038,f1550]) ).
fof(f1721,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4)) ),
inference(superposition,[],[f1330,f1550]) ).
fof(f1723,definition,
( spl6_9
<=> ! [X4,X2,X3] : hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4)) ),
introduced(definition,[new_symbols(definition,[spl6_9])],[avatar_definition]) ).
fof(f1724,plain,
( ! [X2,X3,X4] : hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4))
| ~ spl6_9 ),
inference(avatar_component_clause,[],[f1723]) ).
fof(f1726,definition,
( spl6_10
<=> ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1) ),
introduced(definition,[new_symbols(definition,[spl6_10])],[avatar_definition]) ).
fof(f1727,plain,
( ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_10 ),
inference(avatar_component_clause,[],[f1726]) ).
fof(f1728,plain,
( spl6_9
| spl6_10 ),
inference(avatar_split_clause,[],[f1721,f1726,f1723]) ).
fof(f1810,plain,
! [X3,X0] :
( X0 = X3
| ~ hBOOL(X3)
| ~ hBOOL(X0) ),
inference(superposition,[],[f1597,f1597]) ).
fof(f1847,plain,
! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ominus__class_Ominus(X0,sF1),X0),
inference(superposition,[],[f374,f818]) ).
fof(f1859,plain,
! [X2,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_HOL_Ominus__class_Ominus(X2,sF1),X2)) ),
inference(superposition,[],[f1847,f1550]) ).
fof(f1871,definition,
( spl6_14
<=> hBOOL(c_Orderings_Obot__class_Obot(sF1)) ),
introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition]) ).
fof(f1872,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ spl6_14 ),
inference(avatar_component_clause,[],[f1871]) ).
fof(f1875,plain,
( ! [X2] : hBOOL(hAPP(c_HOL_Ominus__class_Ominus(X2,sF1),X2))
| ~ spl6_10 ),
inference(forward_subsumption_resolution,[],[f1859,f1727]) ).
fof(f1876,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ spl6_10 ),
inference(forward_demodulation,[],[f1875,f1847]) ).
fof(f1877,plain,
( spl6_14
| ~ spl6_10 ),
inference(avatar_split_clause,[],[f1876,f1726,f1871]) ).
fof(f1880,plain,
( ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_6 ),
inference(forward_subsumption_resolution,[],[f1859,f1365]) ).
fof(f1888,plain,
( ! [X2,X3,X6,X7,X4,X5] :
( c_Orderings_Obot__class_Obot(sF1) = hAPP(X2,hAPP(X3,X7))
| hBOOL(hAPP(c_COMBB(X2,X3,X4,X5,X6),X7)) )
| ~ spl6_6 ),
inference(backward_demodulation,[],[f1651,f1880]) ).
fof(f1913,plain,
( ! [X2,X3,X7] : c_Orderings_Obot__class_Obot(sF1) = hAPP(X2,hAPP(X3,X7))
| ~ spl6_6 ),
inference(forward_subsumption_resolution,[],[f1888,f1365]) ).
fof(f2058,plain,
( ! [X2,X1] :
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| hBOOL(hAPP(X2,X1)) )
| ~ spl6_6 ),
inference(backward_demodulation,[],[f1255,f1913]) ).
fof(f2070,plain,
( hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ spl6_6 ),
inference(forward_subsumption_resolution,[],[f2058,f1365]) ).
fof(f2089,plain,
( $false
| ~ spl6_6 ),
inference(forward_subsumption_resolution,[],[f2070,f1365]) ).
fof(f2090,plain,
~ spl6_6,
inference(avatar_contradiction_clause,[],[f2089]) ).
fof(f2343,plain,
! [X0,X1] : hAPP(c_Not,hAPP(X0,X1)) = hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0),X1),
inference(superposition,[],[f102,f1367]) ).
fof(f2346,plain,
! [X0] :
( c_Orderings_Obot__class_Obot(tc_fun(sF0,tc_bool)) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X0,tc_bool,sF0))
| hBOOL(hAPP(c_Not,X0)) ),
inference(superposition,[],[f1150,f1367]) ).
fof(f2348,plain,
! [X0] :
( c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X0,tc_bool,sF0))
| hBOOL(hAPP(c_Not,X0)) ),
inference(forward_demodulation,[],[f2346,f818]) ).
fof(f2354,plain,
! [X2,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X2,tc_bool,sF0))) ),
inference(superposition,[],[f2348,f1550]) ).
fof(f2359,plain,
( ! [X2] :
( hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X2,tc_bool,sF0))) )
| ~ spl6_10 ),
inference(forward_subsumption_resolution,[],[f2354,f1727]) ).
fof(f2361,definition,
( spl6_19
<=> ! [X0] : hBOOL(hAPP(c_Not,X0)) ),
introduced(definition,[new_symbols(definition,[spl6_19])],[avatar_definition]) ).
fof(f2362,plain,
( ! [X0] : hBOOL(hAPP(c_Not,X0))
| ~ spl6_19 ),
inference(avatar_component_clause,[],[f2361]) ).
fof(f2381,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_COMBB(X0,c_COMBK(X1,X2,X3),X2,tc_bool,X3),tc_fun(X3,tc_bool)),X4) = X4
| hBOOL(hAPP(X0,X1)) ),
inference(superposition,[],[f65,f1150]) ).
fof(f3521,plain,
! [X0] : c_COMBB(c_Not,X0,tc_bool,tc_bool,sF0) = hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(sF1),sF1),X0),
inference(superposition,[],[f965,f818]) ).
fof(f3541,plain,
! [X0] : hAPP(c_HOL_Ouminus__class_Ouminus(sF1),X0) = hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(sF1),sF1),X0),
inference(forward_demodulation,[],[f3521,f1367]) ).
fof(f3550,plain,
c_Orderings_Obot__class_Obot(sF1) = hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_Orderings_Otop__class_Otop(sF1)),
inference(superposition,[],[f1847,f3541]) ).
fof(f3576,plain,
! [X0] : hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = hAPP(c_Not,hAPP(c_Orderings_Otop__class_Otop(sF1),X0)),
inference(superposition,[],[f2343,f3550]) ).
fof(f4478,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1)
| ~ hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4)) ),
inference(superposition,[],[f1330,f1593]) ).
fof(f4490,plain,
! [X2,X0,X1] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_Not,X2))
| ~ hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X2,tc_bool,sF0))) ),
inference(superposition,[],[f2348,f1593]) ).
fof(f4533,definition,
( spl6_69
<=> ! [X0,X1] : hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1) ),
introduced(definition,[new_symbols(definition,[spl6_69])],[avatar_definition]) ).
fof(f4534,plain,
( ! [X0,X1] : hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) != c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_69 ),
inference(avatar_component_clause,[],[f4533]) ).
fof(f4540,plain,
( ! [X2,X0,X1] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_Not,X2)) )
| ~ spl6_10 ),
inference(forward_subsumption_resolution,[],[f4490,f2359]) ).
fof(f4546,definition,
( spl6_70
<=> ! [X4,X2,X3] : ~ hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4)) ),
introduced(definition,[new_symbols(definition,[spl6_70])],[avatar_definition]) ).
fof(f4547,plain,
( ! [X2,X3,X4] : ~ hBOOL(hAPP(c_Set_Oinsert(X2,X3),X4))
| ~ spl6_70 ),
inference(avatar_component_clause,[],[f4546]) ).
fof(f4548,plain,
( spl6_70
| spl6_69 ),
inference(avatar_split_clause,[],[f4478,f4533,f4546]) ).
fof(f4591,definition,
( spl6_71
<=> ! [X0,X1] : hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1) ),
introduced(definition,[new_symbols(definition,[spl6_71])],[avatar_definition]) ).
fof(f4592,plain,
( ! [X0,X1] : hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_71 ),
inference(avatar_component_clause,[],[f4591]) ).
fof(f4593,plain,
( spl6_19
| spl6_71
| ~ spl6_10 ),
inference(avatar_split_clause,[],[f4540,f1726,f4591,f2361]) ).
fof(f4608,definition,
( spl6_75
<=> ! [X2] :
( hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X2,tc_bool,sF0))) ) ),
introduced(definition,[new_symbols(definition,[spl6_75])],[avatar_definition]) ).
fof(f4609,plain,
( ! [X2] :
( hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_HOL_Ouminus__class_Ouminus(sF1),c_COMBK(X2,tc_bool,sF0))) )
| ~ spl6_75 ),
inference(avatar_component_clause,[],[f4608]) ).
fof(f4611,definition,
( spl6_76
<=> ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1) ),
introduced(definition,[new_symbols(definition,[spl6_76])],[avatar_definition]) ).
fof(f4612,plain,
( ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_76 ),
inference(avatar_component_clause,[],[f4611]) ).
fof(f4613,plain,
( spl6_75
| spl6_76 ),
inference(avatar_split_clause,[],[f2354,f4611,f4608]) ).
fof(f4631,plain,
( $false
| ~ spl6_9
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f4547,f1724]) ).
fof(f4632,plain,
( ~ spl6_9
| ~ spl6_70 ),
inference(avatar_contradiction_clause,[],[f4631]) ).
fof(f4633,plain,
( ! [X0] : ~ hBOOL(X0)
| ~ spl6_19 ),
inference(resolution,[],[f2362,f1269]) ).
fof(f4644,plain,
( spl6_6
| ~ spl6_19 ),
inference(avatar_split_clause,[],[f4633,f2361,f1364]) ).
fof(f4860,plain,
( ! [X2,X0,X1] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)),X1) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_Not,X2)) )
| ~ spl6_75 ),
inference(forward_subsumption_resolution,[],[f4490,f4609]) ).
fof(f4865,plain,
( ! [X2] : hBOOL(hAPP(c_Not,X2))
| ~ spl6_69
| ~ spl6_75 ),
inference(forward_subsumption_resolution,[],[f4860,f4534]) ).
fof(f4866,plain,
( spl6_19
| ~ spl6_69
| ~ spl6_75 ),
inference(avatar_split_clause,[],[f4865,f4608,f4533,f2361]) ).
fof(f4877,plain,
( ! [X2,X3,X4] :
( hAPP(X2,X3) = hAPP(c_Orderings_Obot__class_Obot(sF1),X2)
| hBOOL(hAPP(c_in(X4),X3)) )
| ~ spl6_76 ),
inference(backward_demodulation,[],[f1670,f4612]) ).
fof(f4938,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_Orderings_Obot__class_Obot(sF1),X0)
| ~ spl6_76 ),
inference(superposition,[],[f4612,f818]) ).
fof(f4959,plain,
( ! [X2,X3,X4] :
( hAPP(X2,X3) = c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_in(X4),X3)) )
| ~ spl6_76 ),
inference(backward_demodulation,[],[f4877,f4938]) ).
fof(f5167,plain,
( ! [X2,X1] :
( c_Orderings_Obot__class_Obot(sF1) != c_Orderings_Obot__class_Obot(sF1)
| hBOOL(hAPP(c_in(X2),X1)) )
| ~ spl6_76 ),
inference(superposition,[],[f1329,f4959]) ).
fof(f5198,plain,
( ! [X2,X1] : hBOOL(hAPP(c_in(X2),X1))
| ~ spl6_76 ),
inference(trivial_inequality_removal,[],[f5167]) ).
fof(f5205,definition,
( spl6_81
<=> ! [X4,X3] : hBOOL(hAPP(c_in(X4),X3)) ),
introduced(definition,[new_symbols(definition,[spl6_81])],[avatar_definition]) ).
fof(f5206,plain,
( ! [X3,X4] : hBOOL(hAPP(c_in(X4),X3))
| ~ spl6_81 ),
inference(avatar_component_clause,[],[f5205]) ).
fof(f5214,plain,
( spl6_81
| ~ spl6_76 ),
inference(avatar_split_clause,[],[f5198,f4611,f5205]) ).
fof(f5403,plain,
( ! [X0] : hAPP(c_Orderings_Otop__class_Otop(sF1),X0) = c_Orderings_Obot__class_Obot(sF1)
| ~ spl6_71 ),
inference(superposition,[],[f4592,f818]) ).
fof(f5421,plain,
( ! [X0] : hAPP(c_Orderings_Obot__class_Obot(sF1),X0) = hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1))
| ~ spl6_71 ),
inference(backward_demodulation,[],[f3576,f5403]) ).
fof(f5464,plain,
( ! [X1] :
( hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1)) = X1
| hBOOL(X1) )
| ~ spl6_71 ),
inference(superposition,[],[f1569,f5421]) ).
fof(f5649,plain,
( ! [X2,X0,X1] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1))
| hBOOL(hAPP(c_Orderings_Obot__class_Obot(sF1),X2)) )
| ~ spl6_71 ),
inference(superposition,[],[f5421,f1550]) ).
fof(f5732,plain,
( ! [X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1))
| ~ spl6_71 ),
inference(forward_subsumption_resolution,[],[f5649,f1442]) ).
fof(f6266,plain,
( ! [X2,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = X4
| ~ hBOOL(hAPP(X4,X2)) )
| ~ spl6_70 ),
inference(forward_subsumption_resolution,[],[f1666,f4547]) ).
fof(f6304,plain,
( ! [X2,X4] :
( hAPP(c_Not,c_Orderings_Obot__class_Obot(sF1)) = X4
| ~ hBOOL(hAPP(X4,X2)) )
| ~ spl6_70
| ~ spl6_71 ),
inference(forward_demodulation,[],[f6266,f5732]) ).
fof(f6470,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(hAPP(X0,X2))
| hBOOL(X1)
| X0 = X1 )
| ~ spl6_70
| ~ spl6_71 ),
inference(superposition,[],[f5464,f6304]) ).
fof(f6473,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(c_Orderings_Obot__class_Obot(sF1))
| ~ hBOOL(hAPP(X0,X1)) )
| ~ spl6_70
| ~ spl6_71 ),
inference(superposition,[],[f1269,f6304]) ).
fof(f6478,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| ~ hBOOL(X0) )
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71 ),
inference(forward_subsumption_resolution,[],[f6473,f1872]) ).
fof(f6590,plain,
( ! [X0] :
( hBOOL(X0)
| c_Not = X0 )
| ~ spl6_70
| ~ spl6_71 ),
inference(resolution,[],[f6470,f1287]) ).
fof(f6732,definition,
( spl6_123
<=> ! [X0] :
( hBOOL(X0)
| c_Not = X0 ) ),
introduced(definition,[new_symbols(definition,[spl6_123])],[avatar_definition]) ).
fof(f6733,plain,
( ! [X0] :
( c_Not = X0
| hBOOL(X0) )
| ~ spl6_123 ),
inference(avatar_component_clause,[],[f6732]) ).
fof(f6735,plain,
( spl6_123
| ~ spl6_70
| ~ spl6_71 ),
inference(avatar_split_clause,[],[f6590,f4591,f4546,f6732]) ).
fof(f6740,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| ~ hBOOL(X1)
| hBOOL(X0) )
| ~ spl6_123 ),
inference(superposition,[],[f1269,f6733]) ).
fof(f6751,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(X0,X1))
| ~ hBOOL(X1) )
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123 ),
inference(forward_subsumption_resolution,[],[f6740,f6478]) ).
fof(f6780,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(X0)
| hBOOL(hAPP(X1,X2)) )
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123 ),
inference(superposition,[],[f6751,f2381]) ).
fof(f6853,plain,
( ! [X2,X0,X1] :
( ~ hBOOL(X0)
| hBOOL(hAPP(X1,X2)) )
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123 ),
inference(duplicate_literal_removal,[],[f6780]) ).
fof(f7050,definition,
( spl6_128
<=> ! [X2,X1] : hBOOL(hAPP(X1,X2)) ),
introduced(definition,[new_symbols(definition,[spl6_128])],[avatar_definition]) ).
fof(f7051,plain,
( ! [X2,X1] : hBOOL(hAPP(X1,X2))
| ~ spl6_128 ),
inference(avatar_component_clause,[],[f7050]) ).
fof(f7052,plain,
( spl6_128
| spl6_6
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123 ),
inference(avatar_split_clause,[],[f6853,f6732,f4591,f4546,f1871,f1364,f7050]) ).
fof(f7060,plain,
( ! [X1] :
( c_Orderings_Obot__class_Obot(sF1) = X1
| hBOOL(X1) )
| ~ spl6_76 ),
inference(forward_demodulation,[],[f1568,f4612]) ).
fof(f7205,plain,
( ! [X0] : hBOOL(hAPP(sF3,X0))
| ~ spl6_81 ),
inference(superposition,[],[f5206,f822]) ).
fof(f7330,plain,
( ! [X0] : c_Orderings_Obot__class_Obot(sF1) = hAPP(c_Orderings_Obot__class_Obot(sF1),X0)
| ~ spl6_76 ),
inference(superposition,[],[f4612,f818]) ).
fof(f7704,plain,
( ! [X0,X1] : ~ hBOOL(hAPP(X0,X1))
| ~ spl6_128 ),
inference(resolution,[],[f7051,f1217]) ).
fof(f7818,plain,
( $false
| ~ spl6_128 ),
inference(forward_subsumption_resolution,[],[f7704,f7051]) ).
fof(f7819,plain,
~ spl6_128,
inference(avatar_contradiction_clause,[],[f7818]) ).
fof(f11952,plain,
( ! [X0,X1] :
( hAPP(X0,X1) = X0
| hBOOL(X0) )
| ~ spl6_76 ),
inference(superposition,[],[f7330,f7060]) ).
fof(f12125,plain,
( ! [X2,X0] :
( c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X2
| ~ hBOOL(X2)
| hBOOL(c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool))) )
| ~ spl6_76 ),
inference(superposition,[],[f1597,f11952]) ).
fof(f12232,plain,
( ! [X2,X0] :
( c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) = X2
| ~ hBOOL(X2) )
| ~ spl6_76 ),
inference(forward_subsumption_resolution,[],[f12125,f1810]) ).
fof(f12238,plain,
( ! [X2,X0] :
( hBOOL(hAPP(X0,X2))
| ~ hBOOL(X0) )
| ~ spl6_76 ),
inference(superposition,[],[f587,f12232]) ).
fof(f12356,plain,
( ! [X0,X1] :
( hBOOL(hAPP(X0,X1))
| ~ hBOOL(hAPP(sF3,X1)) )
| ~ spl6_76 ),
inference(superposition,[],[f12238,f1298]) ).
fof(f12425,plain,
( ! [X0,X1] : hBOOL(hAPP(X0,X1))
| ~ spl6_76
| ~ spl6_81 ),
inference(forward_subsumption_resolution,[],[f12356,f7205]) ).
fof(f12453,plain,
( spl6_128
| ~ spl6_76
| ~ spl6_81 ),
inference(avatar_split_clause,[],[f12425,f5205,f4611,f7050]) ).
cnf(s19,plain,
( spl6_9
| spl6_10 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s23,plain,
( ~ spl6_10
| spl6_14 ),
inference(sat_conversion,[],[f1877]) ).
cnf(s31,plain,
~ spl6_6,
inference(sat_conversion,[],[f2090]) ).
cnf(s84,plain,
( spl6_69
| spl6_70 ),
inference(sat_conversion,[],[f4548]) ).
cnf(s85,plain,
( ~ spl6_10
| spl6_19
| spl6_71 ),
inference(sat_conversion,[],[f4593]) ).
cnf(s88,plain,
( spl6_75
| spl6_76 ),
inference(sat_conversion,[],[f4613]) ).
cnf(s93,plain,
( ~ spl6_9
| ~ spl6_70 ),
inference(sat_conversion,[],[f4632]) ).
cnf(s95,plain,
( spl6_6
| ~ spl6_19 ),
inference(sat_conversion,[],[f4644]) ).
cnf(s99,plain,
( spl6_19
| ~ spl6_69
| ~ spl6_75 ),
inference(sat_conversion,[],[f4866]) ).
cnf(s102,plain,
( ~ spl6_76
| spl6_81 ),
inference(sat_conversion,[],[f5214]) ).
cnf(s230,plain,
( ~ spl6_70
| ~ spl6_71
| spl6_123 ),
inference(sat_conversion,[],[f6735]) ).
cnf(s307,plain,
( spl6_6
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123
| spl6_128 ),
inference(sat_conversion,[],[f7052]) ).
cnf(s392,plain,
~ spl6_128,
inference(sat_conversion,[],[f7819]) ).
cnf(s578,plain,
( ~ spl6_76
| ~ spl6_81
| spl6_128 ),
inference(sat_conversion,[],[f12453]) ).
cnf(s588,plain,
( spl6_6
| ~ spl6_14
| ~ spl6_70
| ~ spl6_71
| ~ spl6_123 ),
inference(rat,[],[s307,s392]) ).
cnf(s595,plain,
~ spl6_19,
inference(rat,[],[s95,s31]) ).
cnf(s608,plain,
~ spl6_70,
inference(rat,[],[s588,s230,s23,s85,s19,s93,s31,s595]) ).
cnf(s609,plain,
spl6_69,
inference(rat,[],[s84,s608]) ).
cnf(s612,plain,
~ spl6_75,
inference(rat,[],[s99,s595,s609]) ).
cnf(s616,plain,
spl6_76,
inference(rat,[],[s88,s612]) ).
cnf(s622,plain,
~ spl6_81,
inference(rat,[],[s578,s392,s616]) ).
cnf(s643,plain,
$false,
inference(rat,[],[s102,s622,s616]) ).
fof(f12459,plain,
$false,
inference(avatar_sat_refutation,[],[s643]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT030-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n019.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 23:30:34 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.09/2.18 % (3527050)Input is clausal, will run a generic CNF schedule.
% 9.09/2.18 % (3527059)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2217893266:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.09/2.18 % (3527061)dis-21_1_sil=8000:lcm=predicate:random_seed=3624583415: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)
% 9.09/2.18 % (3527058)lrs+10_1_sil=8000:sp=occurrence:random_seed=3699713772:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.09/2.18 % (3527056)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4202121386:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.09/2.18 % (3527055)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=2930572950:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.09/2.18 % (3527060)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1830339716:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.09/2.18 % (3527057)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1100578448:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.09/2.18 % (3527058)Refutation not found, incomplete strategy
% 9.09/2.18 % (3527058)------------------------------
% 9.09/2.18 % (3527058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.09/2.18 % (3527058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.09/2.18 % (3527058)CaDiCaL version: 2.1.3
% 9.09/2.18 % (3527058)Termination reason: Refutation not found, incomplete strategy
% 9.09/2.18 % (3527058)Time elapsed: 0.003 s
% 9.09/2.18 % (3527058)Peak memory usage: 88 MB
% 9.09/2.18 % (3527058)Instructions burned: 3 (million)
% 9.09/2.18 % (3527059)Instruction limit reached!
% 9.09/2.18 % (3527059)------------------------------
% 9.09/2.18 % (3527059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.09/2.18 % (3527059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.09/2.18 % (3527059)CaDiCaL version: 2.1.3
% 9.09/2.18 % (3527059)Termination reason: Instruction limit
% 9.09/2.18 % (3527059)Termination phase: Saturation
% 9.09/2.18 % (3527059)Time elapsed: 0.041 s
% 9.09/2.18 % (3527059)Peak memory usage: 88 MB
% 9.09/2.18 % (3527059)Instructions burned: 115 (million)
% 9.09/2.18 % (3527061)Instruction limit reached!
% 9.09/2.18 % (3527061)------------------------------
% 9.09/2.18 % (3527061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.09/2.18 % (3527061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.09/2.18 % (3527061)CaDiCaL version: 2.1.3
% 9.09/2.18 % (3527061)Termination reason: Instruction limit
% 9.09/2.18 % (3527061)Termination phase: Saturation
% 9.09/2.18 % (3527061)Time elapsed: 0.071 s
% 9.09/2.18 % (3527061)Peak memory usage: 89 MB
% 9.09/2.18 % (3527061)Instructions burned: 118 (million)
% 9.09/2.18 % (3527069)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=4142973089:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.09/2.18 % (3527069)Refutation not found, incomplete strategy
% 9.09/2.18 % (3527069)------------------------------
% 9.09/2.18 % (3527069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.09/2.18 % (3527069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.09/2.18 % (3527069)CaDiCaL version: 2.1.3
% 9.09/2.18 % (3527069)Termination reason: Refutation not found, incomplete strategy
% 9.09/2.18 % (3527069)Time elapsed: 0.002 s
% 9.09/2.18 % (3527069)Peak memory usage: 88 MB
% 9.09/2.18 % (3527069)Instructions burned: 3 (million)
% 9.09/2.18 % (3527060)Instruction limit reached!
% 9.09/2.18 % (3527060)------------------------------
% 9.09/2.18 % (3527060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.09/2.18 % (3527060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.09/2.18 % (3527060)CaDiCaL version: 2.1.3
% 9.09/2.18 % (3527060)Termination reason: Instruction limit
% 9.09/2.18 % (3527060)Termination phase: Saturation
% 9.09/2.18 % (3527060)Time elapsed: 0.107 s
% 9.09/2.18 % (3527060)Peak memory usage: 89 MB
% 9.09/2.18 % (3527060)Instructions burned: 181 (million)
% 9.09/2.18 % (3527070)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1922689953: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)
% 11.54/3.04 % (3527073)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3946855899:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.54/3.04 % (3527058)------------------------------
% 11.54/3.04 % (3527058)------------------------------
% 11.54/3.04 % (3527069)------------------------------
% 11.54/3.04 % (3527069)------------------------------
% 11.54/3.04 % (3527070)Instruction limit reached!
% 11.54/3.04 % (3527070)------------------------------
% 11.54/3.04 % (3527070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527070)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527070)Termination reason: Instruction limit
% 11.54/3.04 % (3527070)Termination phase: Saturation
% 11.54/3.04 % (3527070)Time elapsed: 0.110 s
% 11.54/3.04 % (3527070)Peak memory usage: 90 MB
% 11.54/3.04 % (3527070)Instructions burned: 190 (million)
% 11.54/3.04 % (3527077)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=823517514:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.54/3.04 % (3527073)Instruction limit reached!
% 11.54/3.04 % (3527073)------------------------------
% 11.54/3.04 % (3527073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527073)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527073)Termination reason: Instruction limit
% 11.54/3.04 % (3527073)Termination phase: Saturation
% 11.54/3.04 % (3527073)Time elapsed: 0.139 s
% 11.54/3.04 % (3527073)Peak memory usage: 90 MB
% 11.54/3.04 % (3527073)Instructions burned: 220 (million)
% 11.54/3.04 % (3527076)lrs+10_64_to=lpo:sil=8000:random_seed=2649746050:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 11.54/3.04 % (3527077)Instruction limit reached!
% 11.54/3.04 % (3527077)------------------------------
% 11.54/3.04 % (3527077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527077)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527077)Termination reason: Instruction limit
% 11.54/3.04 % (3527077)Termination phase: Saturation
% 11.54/3.04 % (3527077)Time elapsed: 0.069 s
% 11.54/3.04 % (3527077)Peak memory usage: 90 MB
% 11.54/3.04 % (3527077)Instructions burned: 194 (million)
% 11.54/3.04 % (3527078)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1874176707:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 11.54/3.04 % (3527076)Instruction limit reached!
% 11.54/3.04 % (3527076)------------------------------
% 11.54/3.04 % (3527076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527076)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527076)Termination reason: Instruction limit
% 11.54/3.04 % (3527076)Termination phase: Saturation
% 11.54/3.04 % (3527076)Time elapsed: 0.086 s
% 11.54/3.04 % (3527076)Peak memory usage: 90 MB
% 11.54/3.04 % (3527076)Instructions burned: 127 (million)
% 11.54/3.04 % (3527080)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4040950984:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 11.54/3.04 % (3527082)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=1097660563:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 11.54/3.04 % (3527082)Instruction limit reached!
% 11.54/3.04 % (3527082)------------------------------
% 11.54/3.04 % (3527082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527082)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527082)Termination reason: Instruction limit
% 11.54/3.04 % (3527082)Termination phase: Saturation
% 11.54/3.04 % (3527082)Time elapsed: 0.028 s
% 11.54/3.04 % (3527082)Peak memory usage: 89 MB
% 11.54/3.04 % (3527082)Instructions burned: 109 (million)
% 11.54/3.04 % (3527078)Instruction limit reached!
% 11.54/3.04 % (3527078)------------------------------
% 11.54/3.04 % (3527078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527078)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527078)Termination reason: Instruction limit
% 11.54/3.04 % (3527078)Termination phase: Saturation
% 11.54/3.04 % (3527078)Time elapsed: 0.097 s
% 11.54/3.04 % (3527078)Peak memory usage: 90 MB
% 11.54/3.04 % (3527078)Instructions burned: 157 (million)
% 11.54/3.04 % (3527084)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=773701159:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 11.54/3.04 % (3527087)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3312943339:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 11.54/3.04 % (3527084)Instruction limit reached!
% 11.54/3.04 % (3527084)------------------------------
% 11.54/3.04 % (3527084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527084)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527084)Termination reason: Instruction limit
% 11.54/3.04 % (3527084)Termination phase: Saturation
% 11.54/3.04 % (3527084)Time elapsed: 0.064 s
% 11.54/3.04 % (3527084)Peak memory usage: 89 MB
% 11.54/3.04 % (3527084)Instructions burned: 107 (million)
% 11.54/3.04 % (3527088)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=479974086:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 11.54/3.04 % (3527087)Instruction limit reached!
% 11.54/3.04 % (3527087)------------------------------
% 11.54/3.04 % (3527087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527087)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527087)Termination reason: Instruction limit
% 11.54/3.04 % (3527087)Termination phase: Saturation
% 11.54/3.04 % (3527087)Time elapsed: 0.079 s
% 11.54/3.04 % (3527087)Peak memory usage: 90 MB
% 11.54/3.04 % (3527087)Instructions burned: 244 (million)
% 11.54/3.04 % (3527093)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2134209260:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 11.54/3.04 % (3527091)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2074848287:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 11.54/3.04 % (3527091)Instruction limit reached!
% 11.54/3.04 % (3527091)------------------------------
% 11.54/3.04 % (3527091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527091)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527091)Termination reason: Instruction limit
% 11.54/3.04 % (3527091)Termination phase: Saturation
% 11.54/3.04 % (3527091)Time elapsed: 0.075 s
% 11.54/3.04 % (3527091)Peak memory usage: 89 MB
% 11.54/3.04 % (3527091)Instructions burned: 134 (million)
% 11.54/3.04 % (3527093)Instruction limit reached!
% 11.54/3.04 % (3527093)------------------------------
% 11.54/3.04 % (3527093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527093)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527093)Termination reason: Instruction limit
% 11.54/3.04 % (3527093)Termination phase: Saturation
% 11.54/3.04 % (3527093)Time elapsed: 0.164 s
% 11.54/3.04 % (3527093)Peak memory usage: 94 MB
% 11.54/3.04 % (3527093)Instructions burned: 500 (million)
% 11.54/3.04 % (3527096)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2649546240:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 11.54/3.04 % (3527097)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3280072879:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 11.54/3.04 % (3527097)Instruction limit reached!
% 11.54/3.04 % (3527097)------------------------------
% 11.54/3.04 % (3527097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527097)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527097)Termination reason: Instruction limit
% 11.54/3.04 % (3527097)Termination phase: Saturation
% 11.54/3.04 % (3527097)Time elapsed: 0.090 s
% 11.54/3.04 % (3527097)Peak memory usage: 92 MB
% 11.54/3.04 % (3527097)Instructions burned: 266 (million)
% 11.54/3.04 % (3527096)Instruction limit reached!
% 11.54/3.04 % (3527096)------------------------------
% 11.54/3.04 % (3527096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527096)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527096)Termination reason: Instruction limit
% 11.54/3.04 % (3527096)Termination phase: Saturation
% 11.54/3.04 % (3527096)Time elapsed: 0.135 s
% 11.54/3.04 % (3527096)Peak memory usage: 91 MB
% 11.54/3.04 % (3527096)Instructions burned: 192 (million)
% 11.54/3.04 % (3527100)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4054285845:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 11.54/3.04 % (3527101)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=3604368247:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 11.54/3.04 % (3527100)Instruction limit reached!
% 11.54/3.04 % (3527100)------------------------------
% 11.54/3.04 % (3527100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527100)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527100)Termination reason: Instruction limit
% 11.54/3.04 % (3527100)Termination phase: Saturation
% 11.54/3.04 % (3527100)Time elapsed: 0.058 s
% 11.54/3.04 % (3527100)Peak memory usage: 90 MB
% 11.54/3.04 % (3527100)Instructions burned: 157 (million)
% 11.54/3.04 % (3527104)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2951401969:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 11.54/3.04 % (3527104)Instruction limit reached!
% 11.54/3.04 % (3527104)------------------------------
% 11.54/3.04 % (3527104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527104)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527104)Termination reason: Instruction limit
% 11.54/3.04 % (3527104)Termination phase: Saturation
% 11.54/3.04 % (3527104)Time elapsed: 0.157 s
% 11.54/3.04 % (3527104)Peak memory usage: 92 MB
% 11.54/3.04 % (3527104)Instructions burned: 537 (million)
% 11.54/3.04 % (3527106)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=939516521:i=180:bd=preordered:av=off_2982 on theBenchmark for (2982ds/180Mi)
% 11.54/3.04 % (3527106)Instruction limit reached!
% 11.54/3.04 % (3527106)------------------------------
% 11.54/3.04 % (3527106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.54/3.04 % (3527106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.54/3.04 % (3527106)CaDiCaL version: 2.1.3
% 11.54/3.04 % (3527106)Termination reason: Instruction limit
% 11.54/3.04 % (3527106)Termination phase: Saturation
% 11.54/3.04 % (3527106)Time elapsed: 0.061 s
% 11.54/3.04 % (3527106)Peak memory usage: 89 MB
% 11.54/3.04 % (3527106)Instructions burned: 180 (million)
% 11.54/3.04 % (3527057)First to succeed.
% 11.54/3.04 % (3527057)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3527050"
% 11.54/3.04 % (3527108)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=906824199:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2981 on theBenchmark for (2981ds/10307Mi)
% 11.54/3.04 % (3527057)Refutation found. Thanks to Tanya!
% 11.54/3.04 % SZS status Unsatisfiable for theBenchmark
% 11.54/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 15.78/3.24 % (3527057)------------------------------
% 15.78/3.24 % (3527057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.24 % (3527057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.24 % (3527057)CaDiCaL version: 2.1.3
% 15.78/3.24 % (3527057)Termination reason: Refutation
% 15.78/3.24 % (3527057)Time elapsed: 1.710 s
% 15.78/3.24 % (3527057)Peak memory usage: 144 MB
% 15.78/3.24 % (3527057)Instructions burned: 2665 (million)
% 15.78/3.24 % (3527057)------------------------------
% 15.78/3.24 % (3527057)------------------------------
% 15.78/3.24 % (3527050)Success in time 2.178 s
% 15.78/3.24 % Vampire exiting
%------------------------------------------------------------------------------