%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT044-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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:36:48 PM UTC 2026
% Result : Unsatisfiable 28.46s 7.21s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 36
% Syntax : Number of formulae : 185 ( 51 unt; 18 def)
% Number of atoms : 440 ( 77 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 411 ( 156 ~; 237 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 18 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 19 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-4 aty)
% Number of variables : 375 ( 0 sgn 375 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f45,axiom,
! [X0,X1] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f194,axiom,
! [X0,X1] : c_Collect(hAPP(c_COMBB(c_Not,tc_bool,tc_bool,X0),X1),X0) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),c_Collect(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__neg__eq_0) ).
fof(f195,axiom,
! [X2,X3,X0,X1] : c_Set_Ovimage(X0,c_Collect(X1,X2),X3,X2) = c_Collect(hAPP(c_COMBB(X1,X2,tc_bool,X3),X0),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__Collect__eq_0) ).
fof(f333,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f387,axiom,
! [X2,X3,X0,X1] : c_Set_Ovimage(X0,X1,X2,X3) = c_Collect(hAPP(c_COMBC(hAPP(c_COMBB(c_in(X3),X3,tc_fun(tc_fun(X3,tc_bool),tc_bool),X2),X0),X2,tc_fun(X3,tc_bool),tc_bool),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__def_0) ).
fof(f405,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(f473,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/sandbox/benchmark/theBenchmark.p',cls_double__complement_0) ).
fof(f567,axiom,
! [X2,X3,X0,X1] :
( c_Set_Ovimage(c_COMBK(X0,X1,X2),X3,X2,X1) = 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(f568,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Set_Ovimage(c_COMBK(X0,X1,X2),X3,X2,X1)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(reorient_equations,[],[f567]) ).
fof(f601,axiom,
! [X0,X1] : hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),X1),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Int__absorb_0) ).
fof(f624,axiom,
! [X2,X0,X1] : c_Set_Ovimage(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,X1) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_vimage__empty_0) ).
fof(f625,plain,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Set_Ovimage(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,X1),
inference(reorient_equations,[],[f624]) ).
fof(f626,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(f643,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(f644,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(f737,axiom,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ hBOOL(hAPP(X2,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f739,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(c_COMBB(X0,X1,X2,X3),X4),X5) = hAPP(X0,hAPP(X4,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
fof(f740,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(f742,axiom,
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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f743,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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_a____)),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f787,plain,
! [X2,X3,X0,X1] : c_Collect(hAPP(c_COMBB(X1,X2,tc_bool,X3),X0),X3) = c_Collect(hAPP(c_COMBC(hAPP(c_COMBB(c_in(X2),X2,tc_fun(tc_fun(X2,tc_bool),tc_bool),X3),X0),X3,tc_fun(X2,tc_bool),tc_bool),c_Collect(X1,X2)),X3),
inference(definition_unfolding,[],[f195,f387]) ).
fof(f849,plain,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Collect(hAPP(c_COMBC(hAPP(c_COMBB(c_in(X1),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X2),X0),X2,tc_fun(X1,tc_bool),tc_bool),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2),
inference(definition_unfolding,[],[f625,f387]) ).
fof(f853,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = c_Collect(hAPP(c_COMBC(hAPP(c_COMBB(c_in(X1),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X2),c_COMBK(X0,X1,X2)),X2,tc_fun(X1,tc_bool),tc_bool),X3),X2)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(definition_unfolding,[],[f568,f387]) ).
fof(f899,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = c_Collect(hAPP(c_COMBB(c_Not,tc_bool,tc_bool,X0),X1),X0),
inference(forward_demodulation,[],[f194,f333]) ).
fof(f900,plain,
! [X0,X1] : hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1) = hAPP(c_COMBB(c_Not,tc_bool,tc_bool,X0),X1),
inference(forward_demodulation,[],[f899,f333]) ).
fof(f901,plain,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_b____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_a____))),
inference(resolution,[],[f737,f743]) ).
fof(f902,plain,
! [X2,X3,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_COMBC(hAPP(c_COMBB(c_in(X1),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X2),c_COMBK(X0,X1,X2)),X2,tc_fun(X1,tc_bool),tc_bool),X3)
| hBOOL(hAPP(hAPP(c_in(X1),X0),X3)) ),
inference(forward_demodulation,[],[f853,f333]) ).
fof(f903,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(hAPP(hAPP(c_COMBB(c_in(X1),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X0),c_COMBK(X2,X1,X0)),X4),X3) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
inference(superposition,[],[f740,f902]) ).
fof(f904,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4) = hAPP(hAPP(c_in(X1),hAPP(c_COMBK(X2,X1,X0),X4)),X3)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
inference(forward_demodulation,[],[f903,f739]) ).
fof(f905,plain,
! [X0,X1] : hAPP(c_COMBC(c_in(X0),X0,tc_fun(X0,tc_bool),tc_bool),X1) = X1,
inference(forward_demodulation,[],[f626,f333]) ).
fof(f906,plain,
! [X2,X0,X1] : hAPP(X0,X2) = hAPP(hAPP(c_in(X1),X2),X0),
inference(superposition,[],[f740,f905]) ).
fof(f910,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____))),
inference(superposition,[],[f742,f906]) ).
fof(f918,plain,
! [X2,X3,X0,X1] : c_Collect(hAPP(c_COMBB(X1,X2,tc_bool,X3),X0),X3) = hAPP(c_COMBC(hAPP(c_COMBB(c_in(X2),X2,tc_fun(tc_fun(X2,tc_bool),tc_bool),X3),X0),X3,tc_fun(X2,tc_bool),tc_bool),c_Collect(X1,X2)),
inference(forward_demodulation,[],[f787,f333]) ).
fof(f919,plain,
! [X2,X3,X0,X1] : c_Collect(hAPP(c_COMBB(X1,X2,tc_bool,X3),X0),X3) = hAPP(c_COMBC(hAPP(c_COMBB(c_in(X2),X2,tc_fun(tc_fun(X2,tc_bool),tc_bool),X3),X0),X3,tc_fun(X2,tc_bool),tc_bool),X1),
inference(forward_demodulation,[],[f918,f333]) ).
fof(f920,plain,
! [X2,X3,X0,X1] : hAPP(c_COMBB(X1,X2,tc_bool,X3),X0) = hAPP(c_COMBC(hAPP(c_COMBB(c_in(X2),X2,tc_fun(tc_fun(X2,tc_bool),tc_bool),X3),X0),X3,tc_fun(X2,tc_bool),tc_bool),X1),
inference(forward_demodulation,[],[f919,f333]) ).
fof(f929,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4) = hAPP(X3,hAPP(c_COMBK(X2,X1,X0),X4))
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
inference(forward_demodulation,[],[f904,f906]) ).
fof(f930,plain,
! [X2,X3,X0,X1,X4] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X4) = hAPP(X3,hAPP(c_COMBK(X2,X1,X0),X4))
| hBOOL(hAPP(X3,X2)) ),
inference(forward_demodulation,[],[f929,f906]) ).
fof(f945,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(X2,hAPP(X6,hAPP(c_COMBK(X7,X8,X0),X1)))
| hBOOL(hAPP(hAPP(c_COMBB(X2,X3,X4,X5),X6),X7)) ),
inference(superposition,[],[f739,f930]) ).
fof(f966,plain,
! [X2,X0,X1,X8,X6,X7] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(X2,hAPP(X6,hAPP(c_COMBK(X7,X8,X0),X1)))
| hBOOL(hAPP(X2,hAPP(X6,X7))) ),
inference(forward_demodulation,[],[f945,f739]) ).
fof(f992,plain,
! [X2,X0,X1] : hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X1),X2) = hAPP(c_Not,hAPP(X1,X2)),
inference(superposition,[],[f739,f900]) ).
fof(f1019,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(X2,X1))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2))) ),
inference(forward_demodulation,[],[f644,f906]) ).
fof(f1020,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X0,tc_bool)),X2),X1))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1019,f906]) ).
fof(f1021,plain,
! [X2,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(X2,X1)))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1020,f992]) ).
fof(f1025,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Not,X0))
| ~ hBOOL(X0) ),
inference(superposition,[],[f1021,f601]) ).
fof(f1038,definition,
( spl0_1
<=> ! [X1,X3] : hBOOL(hAPP(X1,X3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f1039,plain,
( ! [X3,X1] : hBOOL(hAPP(X1,X3))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f1038]) ).
fof(f1082,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( hAPP(X0,hAPP(X1,hAPP(X2,hAPP(c_COMBK(X3,X4,X5),X6)))) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X5,tc_bool)),X6)
| hBOOL(hAPP(hAPP(c_COMBB(X0,X7,X8,X9),X1),hAPP(X2,X3))) ),
inference(superposition,[],[f966,f739]) ).
fof(f1150,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( hAPP(X0,hAPP(X1,hAPP(X2,hAPP(c_COMBK(X3,X4,X5),X6)))) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X5,tc_bool)),X6)
| hBOOL(hAPP(X0,hAPP(X1,hAPP(X2,X3)))) ),
inference(forward_demodulation,[],[f1082,f739]) ).
fof(f1319,plain,
! [X2,X0,X1] : hAPP(X0,X2) = hAPP(c_Not,hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X0),X2)),
inference(superposition,[],[f992,f473]) ).
fof(f1328,plain,
! [X2,X0] : hAPP(X0,X2) = hAPP(c_Not,hAPP(c_Not,hAPP(X0,X2))),
inference(forward_demodulation,[],[f1319,f992]) ).
fof(f1341,plain,
! [X0] : hAPP(c_Not,hAPP(c_Not,X0)) = X0,
inference(superposition,[],[f1328,f45]) ).
fof(f1435,plain,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_COMBC(hAPP(c_COMBB(c_in(X1),X1,tc_fun(tc_fun(X1,tc_bool),tc_bool),X2),X0),X2,tc_fun(X1,tc_bool),tc_bool),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),
inference(forward_demodulation,[],[f849,f333]) ).
fof(f1436,plain,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_COMBB(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,tc_bool,X2),X0),
inference(forward_demodulation,[],[f1435,f920]) ).
fof(f1437,plain,
! [X2,X3,X0,X1,X4] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)
| hBOOL(hAPP(c_COMBB(c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3,tc_bool,X2),X4)) ),
inference(superposition,[],[f1436,f930]) ).
fof(f1440,plain,
! [X2,X3,X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),hAPP(X2,X3)) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X3),
inference(superposition,[],[f739,f1436]) ).
fof(f1457,plain,
! [X2,X0,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))) ),
inference(forward_demodulation,[],[f1437,f1436]) ).
fof(f1477,definition,
( spl0_4
<=> ! [X2] : hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f1478,plain,
( ! [X2] : hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1519,plain,
! [X0,X1,X4] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X4,tc_bool)),X1),
inference(superposition,[],[f1440,f1440]) ).
fof(f1554,definition,
( spl0_9
<=> ! [X2,X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X1) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1555,plain,
( ! [X2,X0,X1] : hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X1)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1558,plain,
spl0_9,
inference(avatar_split_clause,[],[f1519,f1554]) ).
fof(f1816,definition,
( spl0_14
<=> ! [X0] : hBOOL(X0) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1817,plain,
( ! [X0] : hBOOL(X0)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1816]) ).
fof(f1872,plain,
! [X2,X3,X0,X1,X8,X7,X4,X5] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X7,tc_bool)),X8) = hAPP(X1,X0)
| hBOOL(hAPP(X1,hAPP(c_COMBK(X0,X2,X3),hAPP(X4,X5)))) ),
inference(superposition,[],[f1150,f405]) ).
fof(f1874,plain,
! [X2,X3,X0,X1,X8,X7,X4,X5] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X7,tc_bool)),X8) = X0
| hBOOL(hAPP(c_COMBK(X0,X1,X2),hAPP(X3,hAPP(X4,X5)))) ),
inference(superposition,[],[f1150,f405]) ).
fof(f1880,plain,
! [X0,X8,X7] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X7,tc_bool)),X8) = X0
| hBOOL(X0) ),
inference(forward_demodulation,[],[f1874,f405]) ).
fof(f1882,plain,
! [X0,X1,X8,X7] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X7,tc_bool)),X8) = hAPP(X1,X0)
| hBOOL(hAPP(X1,X0)) ),
inference(forward_demodulation,[],[f1872,f405]) ).
fof(f2169,definition,
( spl0_40
<=> hBOOL(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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f2274,plain,
! [X0,X1,X4] :
( hAPP(X0,X1) = X4
| hBOOL(X4)
| hBOOL(hAPP(X0,X1)) ),
inference(superposition,[],[f1880,f1882]) ).
fof(f2400,plain,
! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0)
| hBOOL(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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____))) ),
inference(superposition,[],[f742,f2274]) ).
fof(f2438,plain,
! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0)
| hBOOL(hAPP(c_Not,X1)) ),
inference(superposition,[],[f1341,f2274]) ).
fof(f2531,definition,
( spl0_66
<=> ! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f2532,plain,
( ! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0) )
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f2531]) ).
fof(f2533,plain,
( spl0_40
| spl0_66 ),
inference(avatar_split_clause,[],[f2400,f2531,f2169]) ).
fof(f2581,plain,
! [X0,X1] :
( X0 = X1
| hBOOL(hAPP(c_Not,X0))
| hBOOL(hAPP(c_Not,X1)) ),
inference(superposition,[],[f2438,f1341]) ).
fof(f2629,definition,
( spl0_74
<=> ! [X2,X0] :
( X0 = X2
| hBOOL(hAPP(c_Not,X0))
| hBOOL(hAPP(c_Not,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f2630,plain,
( ! [X2,X0] :
( hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_Not,X0))
| X0 = X2 )
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f2629]) ).
fof(f2632,plain,
spl0_74,
inference(avatar_split_clause,[],[f2581,f2629]) ).
fof(f2646,plain,
( ! [X0,X1] :
( hBOOL(hAPP(c_Not,X0))
| X0 = X1
| ~ hBOOL(X1) )
| ~ spl0_74 ),
inference(resolution,[],[f2630,f1025]) ).
fof(f2678,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0)
| ~ hBOOL(X1) )
| ~ spl0_74 ),
inference(superposition,[],[f2646,f1341]) ).
fof(f2760,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X1)
| ~ hBOOL(X0) )
| ~ spl0_74 ),
inference(superposition,[],[f1341,f2678]) ).
fof(f2809,plain,
( ! [X0,X1] : ~ hBOOL(hAPP(X0,X1))
| ~ spl0_14 ),
inference(resolution,[],[f1817,f1021]) ).
fof(f2815,plain,
( $false
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f2809,f1817]) ).
fof(f2816,plain,
~ spl0_14,
inference(avatar_contradiction_clause,[],[f2815]) ).
fof(f2818,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(c_Not,X0))
| hBOOL(X1)
| X0 = X1 )
| ~ spl0_74 ),
inference(superposition,[],[f2760,f1341]) ).
fof(f2862,plain,
( ! [X2,X0,X1] :
( X1 = X2
| X0 = X1
| hBOOL(X0)
| ~ hBOOL(X2) )
| ~ spl0_74 ),
inference(resolution,[],[f2818,f2646]) ).
fof(f3109,plain,
( ! [X2,X3,X0,X1,X4] :
( hAPP(X0,X2) = X3
| hBOOL(X3)
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X4
| hBOOL(X4)
| ~ hBOOL(X0) )
| ~ spl0_74 ),
inference(superposition,[],[f1880,f2862]) ).
fof(f3589,definition,
( spl0_163
<=> ! [X4,X1] :
( c_in(X1) = X4
| hBOOL(X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f3590,plain,
( ! [X1,X4] :
( c_in(X1) = X4
| hBOOL(X4) )
| ~ spl0_163 ),
inference(avatar_component_clause,[],[f3589]) ).
fof(f3631,definition,
( spl0_174
<=> ! [X5,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X5
| hBOOL(X5) ) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f3632,plain,
( ! [X1,X5] :
( c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X5
| hBOOL(X5) )
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f3631]) ).
fof(f3638,definition,
( spl0_176
<=> ! [X2,X0,X3] :
( hAPP(X0,X2) = X3
| ~ hBOOL(X0)
| hBOOL(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f3639,plain,
( ! [X2,X3,X0] :
( hAPP(X0,X2) = X3
| ~ hBOOL(X0)
| hBOOL(X3) )
| ~ spl0_176 ),
inference(avatar_component_clause,[],[f3638]) ).
fof(f3640,plain,
( spl0_174
| spl0_176
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f3109,f2629,f3638,f3631]) ).
fof(f4650,plain,
( ! [X0] :
( hBOOL(X0)
| hBOOL(X0) )
| ~ spl0_4
| ~ spl0_174 ),
inference(superposition,[],[f1478,f3632]) ).
fof(f4654,plain,
( ! [X2,X0,X1] :
( hAPP(X0,X2) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2)
| hBOOL(X0) )
| ~ spl0_9
| ~ spl0_174 ),
inference(superposition,[],[f1555,f3632]) ).
fof(f4660,plain,
( ! [X0] : hBOOL(X0)
| ~ spl0_4
| ~ spl0_174 ),
inference(duplicate_literal_removal,[],[f4650]) ).
fof(f4662,plain,
( spl0_14
| ~ spl0_4
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f4660,f3631,f1477,f1816]) ).
fof(f5077,definition,
( spl0_332
<=> ! [X2,X0,X1] :
( hAPP(X0,X1) = hAPP(X1,X2)
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_332])],[avatar_definition]) ).
fof(f5078,plain,
( ! [X2,X0,X1] :
( hAPP(X0,X1) = hAPP(X1,X2)
| hBOOL(X0) )
| ~ spl0_332 ),
inference(avatar_component_clause,[],[f5077]) ).
fof(f5149,definition,
( spl0_340
<=> ! [X2,X1,X3] :
( hBOOL(hAPP(X3,X2))
| ~ hBOOL(hAPP(c_in(X1),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_340])],[avatar_definition]) ).
fof(f5150,plain,
( ! [X2,X3,X1] :
( ~ hBOOL(hAPP(c_in(X1),X2))
| hBOOL(hAPP(X3,X2)) )
| ~ spl0_340 ),
inference(avatar_component_clause,[],[f5149]) ).
fof(f5554,definition,
( spl0_343
<=> ! [X4,X0,X3] :
( hAPP(X0,X4) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X4)
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_343])],[avatar_definition]) ).
fof(f5555,plain,
( ! [X3,X0,X4] :
( hAPP(X0,X4) = hAPP(c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X4)
| hBOOL(X0) )
| ~ spl0_343 ),
inference(avatar_component_clause,[],[f5554]) ).
fof(f5666,plain,
( spl0_343
| ~ spl0_9
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f4654,f3631,f1554,f5554]) ).
fof(f5930,definition,
( spl0_357
<=> ! [X1] : hBOOL(c_in(X1)) ),
introduced(definition,[new_symbols(definition,[spl0_357])],[avatar_definition]) ).
fof(f5931,plain,
( ! [X1] : hBOOL(c_in(X1))
| ~ spl0_357 ),
inference(avatar_component_clause,[],[f5930]) ).
fof(f6217,plain,
( ! [X2,X0,X1] :
( hAPP(X1,X2) = X0
| hBOOL(X1)
| hBOOL(X0) )
| ~ spl0_343 ),
inference(superposition,[],[f5555,f1880]) ).
fof(f7238,definition,
( spl0_399
<=> ! [X3] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X3)) ),
introduced(definition,[new_symbols(definition,[spl0_399])],[avatar_definition]) ).
fof(f7239,plain,
( ! [X3] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X3))
| ~ spl0_399 ),
inference(avatar_component_clause,[],[f7238]) ).
fof(f7328,plain,
( ! [X0] :
( hBOOL(X0)
| hBOOL(X0) )
| ~ spl0_163
| ~ spl0_357 ),
inference(superposition,[],[f5931,f3590]) ).
fof(f7330,plain,
( ! [X0] : hBOOL(X0)
| ~ spl0_163
| ~ spl0_357 ),
inference(duplicate_literal_removal,[],[f7328]) ).
fof(f7331,plain,
( spl0_14
| ~ spl0_163
| ~ spl0_357 ),
inference(avatar_split_clause,[],[f7330,f5930,f3589,f1816]) ).
fof(f7450,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(c_in(X1),X2))
| hBOOL(X0) )
| ~ spl0_343 ),
inference(superposition,[],[f737,f6217]) ).
fof(f7455,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| hBOOL(hAPP(c_in(X1),X2))
| hBOOL(X0) )
| ~ spl0_343 ),
inference(superposition,[],[f643,f6217]) ).
fof(f7493,plain,
( ! [X2,X3,X0,X1] :
( hAPP(X0,X1) = hAPP(X1,X2)
| hBOOL(c_in(X3))
| hBOOL(X0) )
| ~ spl0_343 ),
inference(superposition,[],[f906,f6217]) ).
fof(f7560,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_343 ),
inference(duplicate_literal_removal,[],[f7455]) ).
fof(f7561,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_343 ),
inference(duplicate_literal_removal,[],[f7450]) ).
fof(f7615,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(X3,X2))
| hBOOL(X0)
| hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_343 ),
inference(forward_demodulation,[],[f7560,f906]) ).
fof(f7648,definition,
( spl0_413
<=> ! [X2,X1,X3] :
( hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(c_in(X1),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_413])],[avatar_definition]) ).
fof(f7649,plain,
( ! [X2,X3,X1] :
( hBOOL(hAPP(c_in(X1),X2))
| hBOOL(hAPP(X3,X2)) )
| ~ spl0_413 ),
inference(avatar_component_clause,[],[f7648]) ).
fof(f7892,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| ~ hBOOL(hAPP(c_in(X1),X2))
| hBOOL(X0) )
| ~ spl0_176 ),
inference(superposition,[],[f643,f3639]) ).
fof(f7897,plain,
( ! [X0] :
( hBOOL(X0)
| ~ hBOOL(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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)))
| hBOOL(X0) )
| ~ spl0_176 ),
inference(superposition,[],[f742,f3639]) ).
fof(f7994,plain,
( ! [X0] :
( hBOOL(X0)
| ~ hBOOL(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))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____))) )
| ~ spl0_176 ),
inference(duplicate_literal_removal,[],[f7897]) ).
fof(f7996,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| ~ hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_176 ),
inference(duplicate_literal_removal,[],[f7892]) ).
fof(f8051,plain,
( ~ spl0_40
| spl0_14
| ~ spl0_176 ),
inference(avatar_split_clause,[],[f7994,f3638,f1816,f2169]) ).
fof(f8053,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(X3,X2))
| hBOOL(X0)
| ~ hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_176 ),
inference(forward_demodulation,[],[f7996,f906]) ).
fof(f8085,plain,
( spl0_14
| spl0_340
| ~ spl0_176 ),
inference(avatar_split_clause,[],[f8053,f3638,f5149,f1816]) ).
fof(f8414,plain,
( ! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0) )
| ~ spl0_332 ),
inference(superposition,[],[f910,f5078]) ).
fof(f8430,plain,
( spl0_66
| ~ spl0_332 ),
inference(avatar_split_clause,[],[f8414,f5077,f2531]) ).
fof(f9013,plain,
( ! [X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| hBOOL(hAPP(c_in(X1),X0)) )
| ~ spl0_66 ),
inference(superposition,[],[f2532,f906]) ).
fof(f9019,plain,
( ! [X0,X1] :
( hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) )
| ~ spl0_66 ),
inference(superposition,[],[f2532,f1457]) ).
fof(f9042,plain,
( ! [X0,X1] :
( hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))) )
| ~ spl0_66 ),
inference(duplicate_literal_removal,[],[f9019]) ).
fof(f9056,plain,
( spl0_4
| spl0_4
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f9042,f2531,f1477,f1477]) ).
fof(f9059,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| ~ spl0_66
| ~ spl0_340 ),
inference(forward_subsumption_resolution,[],[f9013,f5150]) ).
fof(f9064,plain,
( spl0_399
| ~ spl0_66
| ~ spl0_340 ),
inference(avatar_split_clause,[],[f9059,f5149,f2531,f7238]) ).
fof(f9111,plain,
( spl0_14
| spl0_413
| ~ spl0_343 ),
inference(avatar_split_clause,[],[f7615,f5554,f7648,f1816]) ).
fof(f9247,plain,
( $false
| ~ spl0_399 ),
inference(resolution,[],[f7239,f901]) ).
fof(f9257,plain,
~ spl0_399,
inference(avatar_contradiction_clause,[],[f9247]) ).
fof(f9267,plain,
( ! [X2,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_343
| ~ spl0_413 ),
inference(forward_subsumption_resolution,[],[f7561,f7649]) ).
fof(f9273,plain,
( spl0_357
| spl0_332
| ~ spl0_343 ),
inference(avatar_split_clause,[],[f7493,f5554,f5077,f5930]) ).
fof(f9298,definition,
( spl0_494
<=> ! [X2,X1] : hBOOL(hAPP(c_in(X1),X2)) ),
introduced(definition,[new_symbols(definition,[spl0_494])],[avatar_definition]) ).
fof(f9299,plain,
( ! [X2,X1] : hBOOL(hAPP(c_in(X1),X2))
| ~ spl0_494 ),
inference(avatar_component_clause,[],[f9298]) ).
fof(f9300,plain,
( spl0_494
| spl0_14
| ~ spl0_343
| ~ spl0_413 ),
inference(avatar_split_clause,[],[f9267,f7648,f5554,f1816,f9298]) ).
fof(f9349,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(X0,X2))
| c_in(X1) = X3
| hBOOL(X3)
| ~ hBOOL(X0) )
| ~ spl0_74
| ~ spl0_494 ),
inference(superposition,[],[f9299,f2862]) ).
fof(f9358,definition,
( spl0_496
<=> ! [X2,X0] :
( hBOOL(hAPP(X0,X2))
| ~ hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_496])],[avatar_definition]) ).
fof(f9359,plain,
( ! [X2,X0] :
( hBOOL(hAPP(X0,X2))
| ~ hBOOL(X0) )
| ~ spl0_496 ),
inference(avatar_component_clause,[],[f9358]) ).
fof(f9360,plain,
( spl0_163
| spl0_496
| ~ spl0_74
| ~ spl0_494 ),
inference(avatar_split_clause,[],[f9349,f9298,f2629,f9358,f3589]) ).
fof(f9676,plain,
( ! [X0,X1] : ~ hBOOL(hAPP(X0,X1))
| ~ spl0_1 ),
inference(resolution,[],[f1039,f1021]) ).
fof(f9738,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f9676,f1039]) ).
fof(f9739,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f9738]) ).
fof(f11142,plain,
( ! [X2,X0,X1] :
( hBOOL(hAPP(X0,X1))
| ~ hBOOL(hAPP(c_in(X2),X1)) )
| ~ spl0_496 ),
inference(superposition,[],[f9359,f906]) ).
fof(f11202,plain,
( ! [X0,X1] : hBOOL(hAPP(X0,X1))
| ~ spl0_413
| ~ spl0_496 ),
inference(forward_subsumption_resolution,[],[f11142,f7649]) ).
fof(f11213,plain,
( spl0_1
| ~ spl0_413
| ~ spl0_496 ),
inference(avatar_split_clause,[],[f11202,f9358,f7648,f1038]) ).
cnf(s11,plain,
spl0_9,
inference(sat_conversion,[],[f1558]) ).
cnf(s89,plain,
( spl0_40
| spl0_66 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s123,plain,
spl0_74,
inference(sat_conversion,[],[f2632]) ).
cnf(s137,plain,
~ spl0_14,
inference(sat_conversion,[],[f2816]) ).
cnf(s212,plain,
( ~ spl0_74
| spl0_174
| spl0_176 ),
inference(sat_conversion,[],[f3640]) ).
cnf(s404,plain,
( ~ spl0_4
| spl0_14
| ~ spl0_174 ),
inference(sat_conversion,[],[f4662]) ).
cnf(s537,plain,
( ~ spl0_9
| ~ spl0_174
| spl0_343 ),
inference(sat_conversion,[],[f5666]) ).
cnf(s823,plain,
( spl0_14
| ~ spl0_163
| ~ spl0_357 ),
inference(sat_conversion,[],[f7331]) ).
cnf(s993,plain,
( spl0_14
| ~ spl0_40
| ~ spl0_176 ),
inference(sat_conversion,[],[f8051]) ).
cnf(s1018,plain,
( spl0_14
| ~ spl0_176
| spl0_340 ),
inference(sat_conversion,[],[f8085]) ).
cnf(s1028,plain,
( spl0_66
| ~ spl0_332 ),
inference(sat_conversion,[],[f8430]) ).
cnf(s1183,plain,
( spl0_4
| spl0_4
| ~ spl0_66 ),
inference(sat_conversion,[],[f9056]) ).
cnf(s1184,plain,
( spl0_4
| ~ spl0_66 ),
inference(rat,[],[s1183]) ).
cnf(s1191,plain,
( ~ spl0_66
| ~ spl0_340
| spl0_399 ),
inference(sat_conversion,[],[f9064]) ).
cnf(s1234,plain,
( spl0_14
| ~ spl0_343
| spl0_413 ),
inference(sat_conversion,[],[f9111]) ).
cnf(s1345,plain,
~ spl0_399,
inference(sat_conversion,[],[f9257]) ).
cnf(s1361,plain,
( spl0_332
| ~ spl0_343
| spl0_357 ),
inference(sat_conversion,[],[f9273]) ).
cnf(s1386,plain,
( spl0_14
| ~ spl0_343
| ~ spl0_413
| spl0_494 ),
inference(sat_conversion,[],[f9300]) ).
cnf(s1394,plain,
( ~ spl0_74
| spl0_163
| ~ spl0_494
| spl0_496 ),
inference(sat_conversion,[],[f9360]) ).
cnf(s1458,plain,
~ spl0_1,
inference(sat_conversion,[],[f9739]) ).
cnf(s1742,plain,
( spl0_1
| ~ spl0_413
| ~ spl0_496 ),
inference(sat_conversion,[],[f11213]) ).
cnf(s1749,plain,
( ~ spl0_66
| ~ spl0_340 ),
inference(rat,[],[s1191,s1345]) ).
cnf(s1786,plain,
( ~ spl0_343
| spl0_332 ),
inference(rat,[],[s1394,s1386,s1742,s823,s1234,s1361,s1458,s137,s123]) ).
cnf(s1787,plain,
spl0_66,
inference(rat,[],[s1786,s537,s212,s993,s89,s1028,s11,s123,s137]) ).
cnf(s1788,plain,
~ spl0_340,
inference(rat,[],[s1749,s1787]) ).
cnf(s1789,plain,
spl0_4,
inference(rat,[],[s1184,s1787]) ).
cnf(s1793,plain,
~ spl0_176,
inference(rat,[],[s1018,s137,s1788]) ).
cnf(s1794,plain,
~ spl0_174,
inference(rat,[],[s404,s137,s1789]) ).
cnf(s1795,plain,
$false,
inference(rat,[],[s212,s123,s1793,s1794]) ).
fof(f11215,plain,
$false,
inference(avatar_sat_refutation,[],[s1795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT044-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n001.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 23:41:17 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.56/2.54 % (4087770)Input is clausal, will run a generic CNF schedule.
% 11.56/2.54 % (4087777)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4166666992:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.56/2.54 % (4087781)dis-21_1_sil=8000:lcm=predicate:random_seed=4171184237: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)
% 11.56/2.54 % (4087778)lrs+10_1_sil=8000:sp=occurrence:random_seed=1527262412:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.56/2.54 % (4087775)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=2131715021:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.56/2.54 % (4087780)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2390852497:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.56/2.54 % (4087776)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2824915939:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.56/2.54 % (4087779)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=90672682:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.56/2.54 % (4087781)Instruction limit reached!
% 11.56/2.54 % (4087781)------------------------------
% 11.56/2.54 % (4087781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.54 % (4087781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.54 % (4087781)CaDiCaL version: 2.1.3
% 11.56/2.54 % (4087781)Termination reason: Instruction limit
% 11.56/2.54 % (4087781)Termination phase: Saturation
% 11.56/2.54 % (4087781)Time elapsed: 0.066 s
% 11.56/2.54 % (4087781)Peak memory usage: 89 MB
% 11.56/2.54 % (4087781)Instructions burned: 119 (million)
% 11.56/2.54 % (4087778)Instruction limit reached!
% 11.56/2.54 % (4087778)------------------------------
% 11.56/2.54 % (4087778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.54 % (4087778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.54 % (4087778)CaDiCaL version: 2.1.3
% 11.56/2.54 % (4087778)Termination reason: Instruction limit
% 11.56/2.54 % (4087778)Termination phase: Saturation
% 11.56/2.54 % (4087778)Time elapsed: 0.071 s
% 11.56/2.54 % (4087778)Peak memory usage: 89 MB
% 11.56/2.54 % (4087778)Instructions burned: 108 (million)
% 11.56/2.54 % (4087779)Instruction limit reached!
% 11.56/2.54 % (4087779)------------------------------
% 11.56/2.54 % (4087779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.54 % (4087779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.54 % (4087779)CaDiCaL version: 2.1.3
% 11.56/2.54 % (4087779)Termination reason: Instruction limit
% 11.56/2.54 % (4087779)Termination phase: Saturation
% 11.56/2.54 % (4087779)Time elapsed: 0.072 s
% 11.56/2.54 % (4087779)Peak memory usage: 89 MB
% 11.56/2.54 % (4087779)Instructions burned: 115 (million)
% 11.56/2.54 % (4087780)Instruction limit reached!
% 11.56/2.54 % (4087780)------------------------------
% 11.56/2.54 % (4087780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.54 % (4087780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.54 % (4087780)CaDiCaL version: 2.1.3
% 11.56/2.54 % (4087780)Termination reason: Instruction limit
% 11.56/2.54 % (4087780)Termination phase: Saturation
% 11.56/2.54 % (4087780)Time elapsed: 0.111 s
% 11.56/2.54 % (4087780)Peak memory usage: 90 MB
% 11.56/2.54 % (4087780)Instructions burned: 182 (million)
% 11.56/2.54 % (4087789)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=3400796432:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.56/2.54 % (4087790)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1851309292: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.56/2.54 % (4087791)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1941202102:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.56/2.54 % (4087792)lrs+10_64_to=lpo:sil=8000:random_seed=3000018536:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 11.56/2.54 % (4087789)Instruction limit reached!
% 20.90/3.94 % (4087789)------------------------------
% 20.90/3.94 % (4087789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087789)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087789)Termination reason: Instruction limit
% 20.90/3.94 % (4087789)Termination phase: Saturation
% 20.90/3.94 % (4087789)Time elapsed: 0.075 s
% 20.90/3.94 % (4087789)Peak memory usage: 88 MB
% 20.90/3.94 % (4087789)Instructions burned: 145 (million)
% 20.90/3.94 % (4087790)Instruction limit reached!
% 20.90/3.94 % (4087790)------------------------------
% 20.90/3.94 % (4087790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087790)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087790)Termination reason: Instruction limit
% 20.90/3.94 % (4087790)Termination phase: Saturation
% 20.90/3.94 % (4087790)Time elapsed: 0.095 s
% 20.90/3.94 % (4087790)Peak memory usage: 89 MB
% 20.90/3.94 % (4087790)Instructions burned: 190 (million)
% 20.90/3.94 % (4087791)Instruction limit reached!
% 20.90/3.94 % (4087791)------------------------------
% 20.90/3.94 % (4087791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087791)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087791)Termination reason: Instruction limit
% 20.90/3.94 % (4087791)Termination phase: Saturation
% 20.90/3.94 % (4087791)Time elapsed: 0.116 s
% 20.90/3.94 % (4087791)Peak memory usage: 90 MB
% 20.90/3.94 % (4087791)Instructions burned: 221 (million)
% 20.90/3.94 % (4087792)Instruction limit reached!
% 20.90/3.94 % (4087792)------------------------------
% 20.90/3.94 % (4087792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087792)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087792)Termination reason: Instruction limit
% 20.90/3.94 % (4087792)Termination phase: Saturation
% 20.90/3.94 % (4087792)Time elapsed: 0.078 s
% 20.90/3.94 % (4087792)Peak memory usage: 90 MB
% 20.90/3.94 % (4087792)Instructions burned: 127 (million)
% 20.90/3.94 % (4087797)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3557414765:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.90/3.94 % (4087798)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3928721254:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.90/3.94 % (4087799)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=986750644:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 20.90/3.94 % (4087800)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=3513932014:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 20.90/3.94 % (4087800)Instruction limit reached!
% 20.90/3.94 % (4087800)------------------------------
% 20.90/3.94 % (4087800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087800)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087800)Termination reason: Instruction limit
% 20.90/3.94 % (4087800)Termination phase: Saturation
% 20.90/3.94 % (4087800)Time elapsed: 0.055 s
% 20.90/3.94 % (4087800)Peak memory usage: 89 MB
% 20.90/3.94 % (4087800)Instructions burned: 108 (million)
% 20.90/3.94 % (4087798)Instruction limit reached!
% 20.90/3.94 % (4087798)------------------------------
% 20.90/3.94 % (4087798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087798)CaDiCaL version: 2.1.3
% 20.90/3.94 % (4087798)Termination reason: Instruction limit
% 20.90/3.94 % (4087798)Termination phase: Saturation
% 20.90/3.94 % (4087798)Time elapsed: 0.098 s
% 20.90/3.94 % (4087798)Peak memory usage: 91 MB
% 20.90/3.94 % (4087798)Instructions burned: 158 (million)
% 20.90/3.94 % (4087797)Instruction limit reached!
% 20.90/3.94 % (4087797)------------------------------
% 20.90/3.94 % (4087797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.90/3.94 % (4087797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.90/3.94 % (4087797)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087797)Termination reason: Instruction limit
% 42.94/6.93 % (4087797)Termination phase: Saturation
% 42.94/6.93 % (4087797)Time elapsed: 0.126 s
% 42.94/6.93 % (4087797)Peak memory usage: 90 MB
% 42.94/6.93 % (4087797)Instructions burned: 195 (million)
% 42.94/6.93 % (4087805)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=481352645:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 42.94/6.93 % (4087806)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3906795119:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 42.94/6.93 % (4087807)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1818810711:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 42.94/6.93 % (4087805)Instruction limit reached!
% 42.94/6.93 % (4087805)------------------------------
% 42.94/6.93 % (4087805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.94/6.93 % (4087805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.94/6.93 % (4087805)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087805)Termination reason: Instruction limit
% 42.94/6.93 % (4087805)Termination phase: Saturation
% 42.94/6.93 % (4087805)Time elapsed: 0.058 s
% 42.94/6.93 % (4087805)Peak memory usage: 89 MB
% 42.94/6.93 % (4087805)Instructions burned: 107 (million)
% 42.94/6.93 % (4087806)Instruction limit reached!
% 42.94/6.93 % (4087806)------------------------------
% 42.94/6.93 % (4087806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.94/6.93 % (4087806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.94/6.93 % (4087806)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087806)Termination reason: Instruction limit
% 42.94/6.93 % (4087806)Termination phase: Saturation
% 42.94/6.93 % (4087806)Time elapsed: 0.142 s
% 42.94/6.93 % (4087806)Peak memory usage: 90 MB
% 42.94/6.93 % (4087806)Instructions burned: 242 (million)
% 42.94/6.93 % (4087811)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4010000110:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 42.94/6.93 % (4087811)Instruction limit reached!
% 42.94/6.93 % (4087811)------------------------------
% 42.94/6.93 % (4087811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.94/6.93 % (4087811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.94/6.93 % (4087811)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087811)Termination reason: Instruction limit
% 42.94/6.93 % (4087811)Termination phase: Saturation
% 42.94/6.93 % (4087811)Time elapsed: 0.086 s
% 42.94/6.93 % (4087811)Peak memory usage: 90 MB
% 42.94/6.93 % (4087811)Instructions burned: 134 (million)
% 42.94/6.93 % (4087812)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4183755280:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 42.94/6.93 % (4087814)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2498735630:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 42.94/6.93 % (4087814)Instruction limit reached!
% 42.94/6.93 % (4087814)------------------------------
% 42.94/6.93 % (4087814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.94/6.93 % (4087814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.94/6.93 % (4087814)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087814)Termination reason: Instruction limit
% 42.94/6.93 % (4087814)Termination phase: Saturation
% 42.94/6.93 % (4087814)Time elapsed: 0.125 s
% 42.94/6.93 % (4087814)Peak memory usage: 91 MB
% 42.94/6.93 % (4087814)Instructions burned: 192 (million)
% 42.94/6.93 % (4087812)Instruction limit reached!
% 42.94/6.93 % (4087812)------------------------------
% 42.94/6.93 % (4087812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.94/6.93 % (4087812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.94/6.93 % (4087812)CaDiCaL version: 2.1.3
% 42.94/6.93 % (4087812)Termination reason: Instruction limit
% 42.94/6.93 % (4087812)Termination phase: Saturation
% 42.94/6.93 % (4087812)Time elapsed: 0.289 s
% 42.94/6.93 % (4087812)Peak memory usage: 96 MB
% 42.94/6.93 % (4087812)Instructions burned: 499 (million)
% 42.94/6.93 % (4087817)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1484898592:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 42.94/6.93 % (4087818)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1616267254:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 28.46/7.20 % (4087818)Instruction limit reached!
% 28.46/7.20 % (4087818)------------------------------
% 28.46/7.20 % (4087818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087818)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087818)Termination reason: Instruction limit
% 28.46/7.20 % (4087818)Termination phase: Saturation
% 28.46/7.20 % (4087818)Time elapsed: 0.101 s
% 28.46/7.20 % (4087818)Peak memory usage: 90 MB
% 28.46/7.20 % (4087818)Instructions burned: 156 (million)
% 28.46/7.20 % (4087817)Instruction limit reached!
% 28.46/7.20 % (4087817)------------------------------
% 28.46/7.20 % (4087817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087817)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087817)Termination reason: Instruction limit
% 28.46/7.20 % (4087817)Termination phase: Saturation
% 28.46/7.20 % (4087817)Time elapsed: 0.155 s
% 28.46/7.20 % (4087817)Peak memory usage: 91 MB
% 28.46/7.20 % (4087817)Instructions burned: 267 (million)
% 28.46/7.20 % (4087821)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=4283844482:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 28.46/7.20 % (4087822)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2406611931:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 28.46/7.20 % (4087822)Instruction limit reached!
% 28.46/7.20 % (4087822)------------------------------
% 28.46/7.20 % (4087822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087822)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087822)Termination reason: Instruction limit
% 28.46/7.20 % (4087822)Termination phase: Saturation
% 28.46/7.20 % (4087822)Time elapsed: 0.302 s
% 28.46/7.20 % (4087822)Peak memory usage: 92 MB
% 28.46/7.20 % (4087822)Instructions burned: 538 (million)
% 28.46/7.20 % (4087825)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=440185195:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 28.46/7.20 % (4087825)Instruction limit reached!
% 28.46/7.20 % (4087825)------------------------------
% 28.46/7.20 % (4087825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087825)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087825)Termination reason: Instruction limit
% 28.46/7.20 % (4087825)Termination phase: Saturation
% 28.46/7.20 % (4087825)Time elapsed: 0.094 s
% 28.46/7.20 % (4087825)Peak memory usage: 90 MB
% 28.46/7.20 % (4087825)Instructions burned: 180 (million)
% 28.46/7.20 % (4087799)Instruction limit reached!
% 28.46/7.20 % (4087799)------------------------------
% 28.46/7.20 % (4087799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087799)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087799)Termination reason: Instruction limit
% 28.46/7.20 % (4087799)Termination phase: Saturation
% 28.46/7.20 % (4087799)Time elapsed: 2.007 s
% 28.46/7.20 % (4087799)Peak memory usage: 152 MB
% 28.46/7.20 % (4087799)Instructions burned: 3395 (million)
% 28.46/7.20 % (4087827)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=4037584358:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 28.46/7.20 % (4087828)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=4142544825:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 28.46/7.20 % (4087828)Instruction limit reached!
% 28.46/7.20 % (4087828)------------------------------
% 28.46/7.20 % (4087828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087828)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087828)Termination reason: Instruction limit
% 28.46/7.20 % (4087828)Termination phase: Saturation
% 28.46/7.20 % (4087828)Time elapsed: 0.194 s
% 28.46/7.20 % (4087828)Peak memory usage: 91 MB
% 28.46/7.20 % (4087828)Instructions burned: 414 (million)
% 28.46/7.20 % (4087831)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=2329876262:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 28.46/7.20 % (4087821)Instruction limit reached!
% 28.46/7.20 % (4087821)------------------------------
% 28.46/7.20 % (4087821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.20 % (4087821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.20 % (4087821)CaDiCaL version: 2.1.3
% 28.46/7.20 % (4087821)Termination reason: Instruction limit
% 28.46/7.20 % (4087821)Termination phase: Saturation
% 28.46/7.20 % (4087821)Time elapsed: 1.970 s
% 28.46/7.20 % (4087821)Peak memory usage: 147 MB
% 28.46/7.20 % (4087821)Instructions burned: 3257 (million)
% 28.46/7.20 % (4087807)Instruction limit reached!
% 28.46/7.20 % (4087807)------------------------------
% 28.46/7.20 % (4087807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.21 % (4087807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.21 % (4087807)CaDiCaL version: 2.1.3
% 28.46/7.21 % (4087807)Termination reason: Instruction limit
% 28.46/7.21 % (4087807)Termination phase: Saturation
% 28.46/7.21 % (4087807)Time elapsed: 3.074 s
% 28.46/7.21 % (4087807)Peak memory usage: 161 MB
% 28.46/7.21 % (4087807)Instructions burned: 5209 (million)
% 28.46/7.21 % (4087833)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=3741222431:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 28.46/7.21 % (4087834)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3424974133:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 28.46/7.21 % (4087833)Instruction limit reached!
% 28.46/7.21 % (4087833)------------------------------
% 28.46/7.21 % (4087833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.21 % (4087833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.21 % (4087833)CaDiCaL version: 2.1.3
% 28.46/7.21 % (4087833)Termination reason: Instruction limit
% 28.46/7.21 % (4087833)Termination phase: Saturation
% 28.46/7.21 % (4087833)Time elapsed: 0.163 s
% 28.46/7.21 % (4087833)Peak memory usage: 92 MB
% 28.46/7.21 % (4087833)Instructions burned: 303 (million)
% 28.46/7.21 % (4087837)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3851044317:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 28.46/7.21 % (4087834)Instruction limit reached!
% 28.46/7.21 % (4087834)------------------------------
% 28.46/7.21 % (4087834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.21 % (4087834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.21 % (4087834)CaDiCaL version: 2.1.3
% 28.46/7.21 % (4087834)Termination reason: Instruction limit
% 28.46/7.21 % (4087834)Termination phase: Saturation
% 28.46/7.21 % (4087834)Time elapsed: 0.376 s
% 28.46/7.21 % (4087834)Peak memory usage: 94 MB
% 28.46/7.21 % (4087834)Instructions burned: 720 (million)
% 28.46/7.21 % (4087839)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3294518713:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi)
% 28.46/7.21 % (4087837)Instruction limit reached!
% 28.46/7.21 % (4087837)------------------------------
% 28.46/7.21 % (4087837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.21 % (4087837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.21 % (4087837)CaDiCaL version: 2.1.3
% 28.46/7.21 % (4087837)Termination reason: Instruction limit
% 28.46/7.21 % (4087837)Termination phase: Saturation
% 28.46/7.21 % (4087837)Time elapsed: 0.394 s
% 28.46/7.21 % (4087837)Peak memory usage: 94 MB
% 28.46/7.21 % (4087837)Instructions burned: 599 (million)
% 28.46/7.21 % (4087841)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=2678210534:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2951 on theBenchmark for (2951ds/1997Mi)
% 28.46/7.21 % (4087839)First to succeed.
% 28.46/7.21 % (4087839)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4087770"
% 28.46/7.21 % (4087841)Instruction limit reached!
% 28.46/7.21 % (4087841)------------------------------
% 28.46/7.21 % (4087841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.46/7.21 % (4087841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.46/7.21 % (4087841)CaDiCaL version: 2.1.3
% 28.46/7.21 % (4087841)Termination reason: Instruction limit
% 28.46/7.21 % (4087841)Termination phase: Saturation
% 28.46/7.21 % (4087841)Time elapsed: 1.210 s
% 28.46/7.21 % (4087841)Peak memory usage: 140 MB
% 28.46/7.21 % (4087841)Instructions burned: 1998 (million)
% 28.46/7.21 % (4087839)Refutation found. Thanks to Tanya!
% 28.46/7.21 % SZS status Unsatisfiable for theBenchmark
% 28.46/7.21 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/7.41 % (4087839)------------------------------
% 0.16/7.41 % (4087839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/7.41 % (4087839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/7.41 % (4087839)CaDiCaL version: 2.1.3
% 0.16/7.41 % (4087839)Termination reason: Refutation
% 0.16/7.41 % (4087839)Time elapsed: 1.323 s
% 0.16/7.41 % (4087839)Peak memory usage: 142 MB
% 0.16/7.41 % (4087839)Instructions burned: 2177 (million)
% 0.16/7.41 % (4087839)------------------------------
% 0.16/7.41 % (4087839)------------------------------
% 0.16/7.41 % (4087770)Success in time 6.338 s
% 0.16/7.41 % Vampire exiting
%------------------------------------------------------------------------------