%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SCT045-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 39.37s 6.50s
% Output : Refutation 40.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 34
% Syntax : Number of formulae : 170 ( 42 unt; 18 def)
% Number of atoms : 437 ( 92 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 421 ( 154 ~; 249 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 23 ( 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 : 318 ( 0 sgn 318 !; 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_Collect__neg__eq_0) ).
fof(f333,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',cls_Int__absorb_0) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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),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/sandbox2/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),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____)),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_a____),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_c____)),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
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),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____)),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_a____),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_c____))),
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(f933,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(f934,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,[],[f933,f906]) ).
fof(f950,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,f934]) ).
fof(f973,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,[],[f950,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(f1043,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,[],[f973,f739]) ).
fof(f1110,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,[],[f1043,f739]) ).
fof(f1308,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(f1309,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,[],[f1308,f906]) ).
fof(f1310,plain,
! [X2,X1] :
( ~ hBOOL(hAPP(c_Not,hAPP(X2,X1)))
| ~ hBOOL(hAPP(X2,X1)) ),
inference(forward_demodulation,[],[f1309,f992]) ).
fof(f1314,plain,
! [X0] :
( ~ hBOOL(hAPP(c_Not,X0))
| ~ hBOOL(X0) ),
inference(superposition,[],[f1310,f601]) ).
fof(f1358,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(f1367,plain,
! [X2,X0] : hAPP(X0,X2) = hAPP(c_Not,hAPP(c_Not,hAPP(X0,X2))),
inference(forward_demodulation,[],[f1358,f992]) ).
fof(f1382,plain,
! [X0] : hAPP(c_Not,hAPP(c_Not,X0)) = X0,
inference(superposition,[],[f1367,f45]) ).
fof(f1474,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,[],[f1110,f405]) ).
fof(f1476,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,[],[f1110,f405]) ).
fof(f1479,plain,
! [X0,X8,X7] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X7,tc_bool)),X8) = X0
| hBOOL(X0) ),
inference(forward_demodulation,[],[f1476,f405]) ).
fof(f1481,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,[],[f1474,f405]) ).
fof(f1779,definition,
( spl0_35
<=> 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),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____))) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f1835,definition,
( spl0_43
<=> ! [X2] : hBOOL(X2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f1836,plain,
( ! [X2] : hBOOL(X2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f1835]) ).
fof(f1839,definition,
( spl0_44
<=> ! [X2] : ~ hBOOL(X2) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f1840,plain,
( ! [X2] : ~ hBOOL(X2)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f1839]) ).
fof(f1892,plain,
! [X0,X1,X4] :
( hAPP(X0,X1) = X4
| hBOOL(X4)
| hBOOL(hAPP(X0,X1)) ),
inference(superposition,[],[f1479,f1481]) ).
fof(f1984,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),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(superposition,[],[f742,f1892]) ).
fof(f2034,plain,
! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0)
| hBOOL(hAPP(c_Not,X1)) ),
inference(superposition,[],[f1382,f1892]) ).
fof(f2156,definition,
( spl0_69
<=> ! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f2157,plain,
( ! [X0] :
( hBOOL(hAPP(X0,c_Arrow__Order__Mirabelle_OProf))
| hBOOL(X0) )
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f2156]) ).
fof(f2158,plain,
( spl0_35
| spl0_69 ),
inference(avatar_split_clause,[],[f1984,f2156,f1779]) ).
fof(f2226,plain,
! [X0,X1] :
( X0 = X1
| hBOOL(hAPP(c_Not,X0))
| hBOOL(hAPP(c_Not,X1)) ),
inference(superposition,[],[f2034,f1382]) ).
fof(f2271,definition,
( spl0_80
<=> ! [X2,X0] :
( X0 = X2
| hBOOL(hAPP(c_Not,X0))
| hBOOL(hAPP(c_Not,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f2272,plain,
( ! [X2,X0] :
( hBOOL(hAPP(c_Not,X2))
| hBOOL(hAPP(c_Not,X0))
| X0 = X2 )
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f2271]) ).
fof(f2274,plain,
spl0_80,
inference(avatar_split_clause,[],[f2226,f2271]) ).
fof(f2288,plain,
( ! [X0,X1] :
( hBOOL(hAPP(c_Not,X0))
| X0 = X1
| ~ hBOOL(X1) )
| ~ spl0_80 ),
inference(resolution,[],[f2272,f1314]) ).
fof(f2320,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0)
| ~ hBOOL(X1) )
| ~ spl0_80 ),
inference(superposition,[],[f2288,f1382]) ).
fof(f2361,definition,
( spl0_83
<=> ! [X0,X3] :
( X0 = X3
| hBOOL(hAPP(c_Not,X3)) ) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f2362,plain,
( ! [X3,X0] :
( hBOOL(hAPP(c_Not,X3))
| X0 = X3 )
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f2361]) ).
fof(f2379,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X1)
| ~ hBOOL(X0) )
| ~ spl0_80 ),
inference(superposition,[],[f1382,f2320]) ).
fof(f2425,plain,
( ! [X0,X1] : ~ hBOOL(hAPP(X0,X1))
| ~ spl0_43 ),
inference(resolution,[],[f1836,f1310]) ).
fof(f2431,plain,
( $false
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f2425,f1836]) ).
fof(f2432,plain,
~ spl0_43,
inference(avatar_contradiction_clause,[],[f2431]) ).
fof(f2434,plain,
( ! [X0,X1] :
( ~ hBOOL(hAPP(c_Not,X0))
| hBOOL(X1)
| X0 = X1 )
| ~ spl0_80 ),
inference(superposition,[],[f2379,f1382]) ).
fof(f2475,plain,
( ! [X2,X0,X1] :
( X1 = X2
| X0 = X1
| hBOOL(X0)
| ~ hBOOL(X2) )
| ~ spl0_80 ),
inference(resolution,[],[f2434,f2288]) ).
fof(f2675,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(X0)
| hBOOL(X2)
| X1 = X2
| hAPP(c_Not,X1) = X3
| hBOOL(X3)
| ~ hBOOL(X0) )
| ~ spl0_80 ),
inference(superposition,[],[f2434,f2475]) ).
fof(f2692,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_80 ),
inference(superposition,[],[f1479,f2475]) ).
fof(f2836,plain,
( ! [X2,X3,X0,X1] :
( ~ hBOOL(X0)
| hBOOL(X2)
| X1 = X2
| hAPP(c_Not,X1) = X3
| hBOOL(X3) )
| ~ spl0_80 ),
inference(duplicate_literal_removal,[],[f2675]) ).
fof(f3076,definition,
( spl0_142
<=> ! [X3] :
( c_Not = X3
| hBOOL(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f3077,plain,
( ! [X3] :
( c_Not = X3
| hBOOL(X3) )
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f3076]) ).
fof(f3259,definition,
( spl0_187
<=> ! [X4,X1] :
( c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X4
| hBOOL(X4) ) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f3260,plain,
( ! [X1,X4] :
( c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X4
| hBOOL(X4) )
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f3259]) ).
fof(f3270,definition,
( spl0_190
<=> ! [X2,X0,X3] :
( hAPP(X0,X2) = X3
| ~ hBOOL(X0)
| hBOOL(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f3271,plain,
( ! [X2,X3,X0] :
( hAPP(X0,X2) = X3
| ~ hBOOL(X0)
| hBOOL(X3) )
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f3270]) ).
fof(f3272,plain,
( spl0_187
| spl0_190
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2692,f2271,f3270,f3259]) ).
fof(f3310,definition,
( spl0_199
<=> ! [X2,X1,X3] :
( hBOOL(X2)
| hBOOL(X3)
| hAPP(c_Not,X1) = X3
| X1 = X2 ) ),
introduced(definition,[new_symbols(definition,[spl0_199])],[avatar_definition]) ).
fof(f3311,plain,
( ! [X2,X3,X1] :
( hAPP(c_Not,X1) = X3
| hBOOL(X3)
| hBOOL(X2)
| X1 = X2 )
| ~ spl0_199 ),
inference(avatar_component_clause,[],[f3310]) ).
fof(f3312,plain,
( spl0_199
| spl0_44
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2836,f2271,f1839,f3310]) ).
fof(f4108,definition,
( spl0_320
<=> ! [X2,X0] :
( X0 = X2
| hBOOL(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_320])],[avatar_definition]) ).
fof(f4109,plain,
( ! [X2,X0] :
( X0 = X2
| hBOOL(X2) )
| ~ spl0_320 ),
inference(avatar_component_clause,[],[f4108]) ).
fof(f4159,definition,
( spl0_327
<=> ! [X0,X1] :
( ~ hBOOL(X0)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_327])],[avatar_definition]) ).
fof(f4160,plain,
( ! [X0,X1] :
( X0 = X1
| ~ hBOOL(X0) )
| ~ spl0_327 ),
inference(avatar_component_clause,[],[f4159]) ).
fof(f4264,plain,
( ! [X2,X0,X1] : hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| ~ spl0_44 ),
inference(resolution,[],[f1840,f643]) ).
fof(f4281,plain,
( $false
| ~ spl0_44 ),
inference(forward_subsumption_resolution,[],[f4264,f1840]) ).
fof(f4282,plain,
~ spl0_44,
inference(avatar_contradiction_clause,[],[f4281]) ).
fof(f4513,plain,
( ! [X2,X3,X0,X1,X4] :
( hAPP(X0,X1) = X2
| hBOOL(X2)
| hBOOL(X3)
| X1 = X3
| c_Not = X4
| hBOOL(X4)
| ~ hBOOL(X0) )
| ~ spl0_80
| ~ spl0_199 ),
inference(superposition,[],[f3311,f2475]) ).
fof(f4883,definition,
( spl0_348
<=> ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_348])],[avatar_definition]) ).
fof(f4884,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0) )
| ~ spl0_348 ),
inference(avatar_component_clause,[],[f4883]) ).
fof(f5326,definition,
( spl0_373
<=> ! [X2,X1,X3] :
( hBOOL(hAPP(X3,X2))
| ~ hBOOL(hAPP(c_in(X1),X2)) ) ),
introduced(definition,[new_symbols(definition,[spl0_373])],[avatar_definition]) ).
fof(f5327,plain,
( ! [X2,X3,X1] :
( ~ hBOOL(hAPP(c_in(X1),X2))
| hBOOL(hAPP(X3,X2)) )
| ~ spl0_373 ),
inference(avatar_component_clause,[],[f5326]) ).
fof(f5526,plain,
( ! [X0,X1] :
( hAPP(c_Not,X0) = X1
| hBOOL(X0) )
| ~ spl0_320 ),
inference(superposition,[],[f1382,f4109]) ).
fof(f5782,plain,
( spl0_348
| ~ spl0_320 ),
inference(avatar_split_clause,[],[f5526,f4108,f4883]) ).
fof(f6442,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| ~ hBOOL(hAPP(c_in(X1),X2))
| hBOOL(X0) )
| ~ spl0_190 ),
inference(superposition,[],[f643,f3271]) ).
fof(f6448,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),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____)))
| hBOOL(X0) )
| ~ spl0_190 ),
inference(superposition,[],[f742,f3271]) ).
fof(f6550,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),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____))) )
| ~ spl0_190 ),
inference(duplicate_literal_removal,[],[f6448]) ).
fof(f6553,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(X0)
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| ~ hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_190 ),
inference(duplicate_literal_removal,[],[f6442]) ).
fof(f6622,plain,
( ~ spl0_35
| spl0_43
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f6550,f3270,f1835,f1779]) ).
fof(f6625,plain,
( ! [X2,X3,X0,X1] :
( hBOOL(hAPP(X3,X2))
| hBOOL(X0)
| ~ hBOOL(hAPP(c_in(X1),X2)) )
| ~ spl0_190 ),
inference(forward_demodulation,[],[f6553,f906]) ).
fof(f6660,plain,
( spl0_43
| spl0_373
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f6625,f3270,f5326,f1835]) ).
fof(f7290,definition,
( spl0_435
<=> ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0)) ),
introduced(definition,[new_symbols(definition,[spl0_435])],[avatar_definition]) ).
fof(f7291,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| ~ spl0_435 ),
inference(avatar_component_clause,[],[f7290]) ).
fof(f7522,plain,
( ! [X0,X1] :
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| hBOOL(hAPP(c_in(X1),X0)) )
| ~ spl0_69 ),
inference(superposition,[],[f2157,f906]) ).
fof(f7554,plain,
( ! [X0] : hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X0))
| ~ spl0_69
| ~ spl0_373 ),
inference(forward_subsumption_resolution,[],[f7522,f5327]) ).
fof(f7562,plain,
( spl0_435
| ~ spl0_69
| ~ spl0_373 ),
inference(avatar_split_clause,[],[f7554,f5326,f2156,f7290]) ).
fof(f7563,plain,
( $false
| ~ spl0_435 ),
inference(resolution,[],[f7291,f901]) ).
fof(f7574,plain,
~ spl0_435,
inference(avatar_contradiction_clause,[],[f7563]) ).
fof(f7906,plain,
( ! [X0,X1] :
( X0 = X1
| ~ hBOOL(X1) )
| ~ spl0_83 ),
inference(resolution,[],[f2362,f1314]) ).
fof(f7931,plain,
( spl0_327
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f7906,f2361,f4159]) ).
fof(f8105,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(X1)
| ~ hBOOL(X0) )
| ~ spl0_327 ),
inference(superposition,[],[f1314,f4160]) ).
fof(f8295,plain,
( ! [X0,X1] :
( ~ hBOOL(X0)
| ~ hBOOL(X1) )
| ~ spl0_327 ),
inference(duplicate_literal_removal,[],[f8105]) ).
fof(f8448,plain,
( spl0_44
| spl0_44
| ~ spl0_327 ),
inference(avatar_split_clause,[],[f8295,f4159,f1839,f1839]) ).
fof(f8644,plain,
( ! [X0,X1] :
( X0 = X1
| hBOOL(hAPP(c_Not,X1)) )
| ~ spl0_348 ),
inference(superposition,[],[f1382,f4884]) ).
fof(f9018,plain,
( spl0_83
| ~ spl0_348 ),
inference(avatar_split_clause,[],[f8644,f4883,f2361]) ).
fof(f10380,definition,
( spl0_547
<=> ! [X0,X1] :
( hAPP(X0,hAPP(X0,X1)) = X1
| hBOOL(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_547])],[avatar_definition]) ).
fof(f10381,plain,
( ! [X0,X1] :
( hAPP(X0,hAPP(X0,X1)) = X1
| hBOOL(X0) )
| ~ spl0_547 ),
inference(avatar_component_clause,[],[f10380]) ).
fof(f10536,definition,
( spl0_585
<=> ! [X2,X0,X3] :
( hAPP(X0,X2) = X3
| hBOOL(X0)
| hBOOL(X3) ) ),
introduced(definition,[new_symbols(definition,[spl0_585])],[avatar_definition]) ).
fof(f10537,plain,
( ! [X2,X3,X0] :
( hAPP(X0,X2) = X3
| hBOOL(X0)
| hBOOL(X3) )
| ~ spl0_585 ),
inference(avatar_component_clause,[],[f10536]) ).
fof(f11054,plain,
( ! [X2,X3,X0] :
( hAPP(X0,X2) = X3
| hBOOL(X3)
| hBOOL(X0) )
| ~ spl0_187 ),
inference(superposition,[],[f1479,f3260]) ).
fof(f11059,plain,
( spl0_585
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f11054,f3259,f10536]) ).
fof(f11379,plain,
( ! [X2,X3,X0,X1,X4] :
( hAPP(X0,X1) = X2
| hBOOL(X2)
| hBOOL(X3)
| X1 = X3
| c_Not = X4
| hBOOL(X4) )
| ~ spl0_80
| ~ spl0_199
| ~ spl0_585 ),
inference(forward_subsumption_resolution,[],[f4513,f10537]) ).
fof(f11386,definition,
( spl0_676
<=> ! [X0,X3,X2,X1] :
( hAPP(X0,X1) = X2
| X1 = X3
| hBOOL(X3)
| hBOOL(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_676])],[avatar_definition]) ).
fof(f11387,plain,
( ! [X2,X3,X0,X1] :
( hAPP(X0,X1) = X2
| X1 = X3
| hBOOL(X3)
| hBOOL(X2) )
| ~ spl0_676 ),
inference(avatar_component_clause,[],[f11386]) ).
fof(f11388,plain,
( spl0_142
| spl0_676
| ~ spl0_80
| ~ spl0_199
| ~ spl0_585 ),
inference(avatar_split_clause,[],[f11379,f10536,f3310,f2271,f11386,f3076]) ).
fof(f11398,plain,
( ! [X0,X1] :
( hAPP(X0,hAPP(X0,X1)) = X1
| hBOOL(X0) )
| ~ spl0_142 ),
inference(superposition,[],[f1382,f3077]) ).
fof(f11411,plain,
( spl0_547
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f11398,f3076,f10380]) ).
fof(f11450,plain,
( ! [X2,X0,X1] :
( X0 = X2
| hBOOL(X1)
| hBOOL(X1)
| hBOOL(X0) )
| ~ spl0_547
| ~ spl0_585 ),
inference(superposition,[],[f10381,f10537]) ).
fof(f11536,plain,
( ! [X2,X0,X1] :
( X0 = X2
| hBOOL(X1)
| hBOOL(X0) )
| ~ spl0_547
| ~ spl0_585 ),
inference(duplicate_literal_removal,[],[f11450]) ).
fof(f11584,plain,
( spl0_43
| spl0_320
| ~ spl0_547
| ~ spl0_585 ),
inference(avatar_split_clause,[],[f11536,f10536,f10380,f4108,f1835]) ).
fof(f12186,plain,
( ! [X3,X0,X4,X5] :
( X0 = X4
| X3 = X5
| hBOOL(X5)
| hBOOL(X4) )
| ~ spl0_676 ),
inference(superposition,[],[f11387,f405]) ).
fof(f12399,plain,
( spl0_320
| spl0_320
| ~ spl0_676 ),
inference(avatar_split_clause,[],[f12186,f11386,f4108,f4108]) ).
cnf(s76,plain,
( spl0_35
| spl0_69 ),
inference(sat_conversion,[],[f2158]) ).
cnf(s121,plain,
spl0_80,
inference(sat_conversion,[],[f2274]) ).
cnf(s135,plain,
~ spl0_43,
inference(sat_conversion,[],[f2432]) ).
cnf(s216,plain,
( ~ spl0_80
| spl0_187
| spl0_190 ),
inference(sat_conversion,[],[f3272]) ).
cnf(s223,plain,
( spl0_44
| ~ spl0_80
| spl0_199 ),
inference(sat_conversion,[],[f3312]) ).
cnf(s421,plain,
~ spl0_44,
inference(sat_conversion,[],[f4282]) ).
cnf(s617,plain,
( ~ spl0_320
| spl0_348 ),
inference(sat_conversion,[],[f5782]) ).
cnf(s834,plain,
( ~ spl0_35
| spl0_43
| ~ spl0_190 ),
inference(sat_conversion,[],[f6622]) ).
cnf(s863,plain,
( spl0_43
| ~ spl0_190
| spl0_373 ),
inference(sat_conversion,[],[f6660]) ).
cnf(s1007,plain,
( ~ spl0_69
| ~ spl0_373
| spl0_435 ),
inference(sat_conversion,[],[f7562]) ).
cnf(s1008,plain,
~ spl0_435,
inference(sat_conversion,[],[f7574]) ).
cnf(s1141,plain,
( ~ spl0_83
| spl0_327 ),
inference(sat_conversion,[],[f7931]) ).
cnf(s1217,plain,
( spl0_44
| spl0_44
| ~ spl0_327 ),
inference(sat_conversion,[],[f8448]) ).
cnf(s1218,plain,
( spl0_44
| ~ spl0_327 ),
inference(rat,[],[s1217]) ).
cnf(s1389,plain,
( spl0_83
| ~ spl0_348 ),
inference(sat_conversion,[],[f9018]) ).
cnf(s1741,plain,
( ~ spl0_187
| spl0_585 ),
inference(sat_conversion,[],[f11059]) ).
cnf(s1820,plain,
( ~ spl0_80
| spl0_142
| ~ spl0_199
| ~ spl0_585
| spl0_676 ),
inference(sat_conversion,[],[f11388]) ).
cnf(s1828,plain,
( ~ spl0_142
| spl0_547 ),
inference(sat_conversion,[],[f11411]) ).
cnf(s1841,plain,
( spl0_43
| spl0_320
| ~ spl0_547
| ~ spl0_585 ),
inference(sat_conversion,[],[f11584]) ).
cnf(s1948,plain,
( spl0_320
| spl0_320
| ~ spl0_676 ),
inference(sat_conversion,[],[f12399]) ).
cnf(s1949,plain,
( spl0_320
| ~ spl0_676 ),
inference(rat,[],[s1948]) ).
cnf(s1969,plain,
( ~ spl0_69
| ~ spl0_373 ),
inference(rat,[],[s1007,s1008]) ).
cnf(s1972,plain,
~ spl0_327,
inference(rat,[],[s1218,s421]) ).
cnf(s1973,plain,
~ spl0_83,
inference(rat,[],[s1141,s1972]) ).
cnf(s1974,plain,
~ spl0_348,
inference(rat,[],[s1389,s1973]) ).
cnf(s1975,plain,
~ spl0_320,
inference(rat,[],[s617,s1974]) ).
cnf(s1976,plain,
~ spl0_676,
inference(rat,[],[s1949,s1975]) ).
cnf(s1992,plain,
( ~ spl0_80
| spl0_199 ),
inference(rat,[],[s223,s421]) ).
cnf(s2004,plain,
spl0_199,
inference(rat,[],[s1992,s121]) ).
cnf(s2013,plain,
~ spl0_190,
inference(rat,[],[s76,s1969,s834,s863,s135]) ).
cnf(s2014,plain,
spl0_187,
inference(rat,[],[s216,s121,s2013]) ).
cnf(s2016,plain,
spl0_585,
inference(rat,[],[s1741,s2014]) ).
cnf(s2033,plain,
~ spl0_547,
inference(rat,[],[s1841,s135,s1975,s2016]) ).
cnf(s2036,plain,
spl0_142,
inference(rat,[],[s1820,s1976,s2004,s121,s2016]) ).
cnf(s2042,plain,
$false,
inference(rat,[],[s1828,s2033,s2036]) ).
fof(f12421,plain,
$false,
inference(avatar_sat_refutation,[],[s2042]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT045-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.38 % Computer : n002.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 23:37:52 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.42 Running first-order theorem proving
% 0.09/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.11/2.35 % (4008907)Input is clausal, will run a generic CNF schedule.
% 10.11/2.35 % (4008913)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1531854213:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.11/2.35 % (4008916)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3677432658:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.11/2.35 % (4008917)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1006721911:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.11/2.35 % (4008912)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=3626102997:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.11/2.35 % (4008915)lrs+10_1_sil=8000:sp=occurrence:random_seed=206263206:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.11/2.35 % (4008914)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2783807260:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.11/2.35 % (4008918)dis-21_1_sil=8000:lcm=predicate:random_seed=228918722:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.11/2.35 % (4008918)Instruction limit reached!
% 10.11/2.35 % (4008918)------------------------------
% 10.11/2.35 % (4008918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.35 % (4008918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.35 % (4008918)CaDiCaL version: 2.1.3
% 10.11/2.35 % (4008918)Termination reason: Instruction limit
% 10.11/2.35 % (4008918)Termination phase: Saturation
% 10.11/2.35 % (4008918)Time elapsed: 0.064 s
% 10.11/2.35 % (4008918)Peak memory usage: 89 MB
% 10.11/2.35 % (4008918)Instructions burned: 118 (million)
% 10.11/2.35 % (4008915)Instruction limit reached!
% 10.11/2.35 % (4008915)------------------------------
% 10.11/2.35 % (4008915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.35 % (4008915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.35 % (4008915)CaDiCaL version: 2.1.3
% 10.11/2.35 % (4008915)Termination reason: Instruction limit
% 10.11/2.35 % (4008915)Termination phase: Saturation
% 10.11/2.35 % (4008915)Time elapsed: 0.071 s
% 10.11/2.35 % (4008915)Peak memory usage: 89 MB
% 10.11/2.35 % (4008915)Instructions burned: 108 (million)
% 10.11/2.35 % (4008916)Instruction limit reached!
% 10.11/2.35 % (4008916)------------------------------
% 10.11/2.35 % (4008916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.35 % (4008916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.35 % (4008916)CaDiCaL version: 2.1.3
% 10.11/2.35 % (4008916)Termination reason: Instruction limit
% 10.11/2.35 % (4008916)Termination phase: Saturation
% 10.11/2.35 % (4008916)Time elapsed: 0.072 s
% 10.11/2.35 % (4008916)Peak memory usage: 88 MB
% 10.11/2.35 % (4008916)Instructions burned: 115 (million)
% 10.11/2.35 % (4008917)Instruction limit reached!
% 10.11/2.35 % (4008917)------------------------------
% 10.11/2.35 % (4008917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.11/2.35 % (4008917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.11/2.35 % (4008917)CaDiCaL version: 2.1.3
% 10.11/2.35 % (4008917)Termination reason: Instruction limit
% 10.11/2.35 % (4008917)Termination phase: Saturation
% 10.11/2.35 % (4008917)Time elapsed: 0.118 s
% 10.11/2.35 % (4008917)Peak memory usage: 90 MB
% 10.11/2.35 % (4008917)Instructions burned: 180 (million)
% 10.11/2.35 % (4008926)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=2727183538:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.11/2.35 % (4008927)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1976941496: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)
% 10.11/2.35 % (4008928)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2716104243:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.11/2.35 % (4008929)lrs+10_64_to=lpo:sil=8000:random_seed=3837036960:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.11/2.35 % (4008926)Instruction limit reached!
% 17.55/3.70 % (4008926)------------------------------
% 17.55/3.70 % (4008926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008926)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008926)Termination reason: Instruction limit
% 17.55/3.70 % (4008926)Termination phase: Saturation
% 17.55/3.70 % (4008926)Time elapsed: 0.072 s
% 17.55/3.70 % (4008926)Peak memory usage: 88 MB
% 17.55/3.70 % (4008926)Instructions burned: 143 (million)
% 17.55/3.70 % (4008927)Instruction limit reached!
% 17.55/3.70 % (4008927)------------------------------
% 17.55/3.70 % (4008927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008927)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008927)Termination reason: Instruction limit
% 17.55/3.70 % (4008927)Termination phase: Saturation
% 17.55/3.70 % (4008927)Time elapsed: 0.094 s
% 17.55/3.70 % (4008927)Peak memory usage: 90 MB
% 17.55/3.70 % (4008927)Instructions burned: 190 (million)
% 17.55/3.70 % (4008928)Instruction limit reached!
% 17.55/3.70 % (4008928)------------------------------
% 17.55/3.70 % (4008928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008928)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008928)Termination reason: Instruction limit
% 17.55/3.70 % (4008928)Termination phase: Saturation
% 17.55/3.70 % (4008928)Time elapsed: 0.112 s
% 17.55/3.70 % (4008928)Peak memory usage: 90 MB
% 17.55/3.70 % (4008928)Instructions burned: 220 (million)
% 17.55/3.70 % (4008929)Instruction limit reached!
% 17.55/3.70 % (4008929)------------------------------
% 17.55/3.70 % (4008929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008929)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008929)Termination reason: Instruction limit
% 17.55/3.70 % (4008929)Termination phase: Saturation
% 17.55/3.70 % (4008929)Time elapsed: 0.077 s
% 17.55/3.70 % (4008929)Peak memory usage: 90 MB
% 17.55/3.70 % (4008929)Instructions burned: 126 (million)
% 17.55/3.70 % (4008934)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=227340718:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 17.55/3.70 % (4008935)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3706969654:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 17.55/3.70 % (4008934)Instruction limit reached!
% 17.55/3.70 % (4008934)------------------------------
% 17.55/3.70 % (4008934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008934)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008934)Termination reason: Instruction limit
% 17.55/3.70 % (4008934)Termination phase: Saturation
% 17.55/3.70 % (4008934)Time elapsed: 0.069 s
% 17.55/3.70 % (4008934)Peak memory usage: 90 MB
% 17.55/3.70 % (4008934)Instructions burned: 194 (million)
% 17.55/3.70 % (4008936)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3618959812:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 17.55/3.70 % (4008937)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=189891107:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 17.55/3.70 % (4008935)Instruction limit reached!
% 17.55/3.70 % (4008935)------------------------------
% 17.55/3.70 % (4008935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008935)CaDiCaL version: 2.1.3
% 17.55/3.70 % (4008935)Termination reason: Instruction limit
% 17.55/3.70 % (4008935)Termination phase: Saturation
% 17.55/3.70 % (4008935)Time elapsed: 0.098 s
% 17.55/3.70 % (4008935)Peak memory usage: 91 MB
% 17.55/3.70 % (4008935)Instructions burned: 157 (million)
% 17.55/3.70 % (4008937)Instruction limit reached!
% 17.55/3.70 % (4008937)------------------------------
% 17.55/3.70 % (4008937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.55/3.70 % (4008937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.55/3.70 % (4008937)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008937)Termination reason: Instruction limit
% 37.95/6.22 % (4008937)Termination phase: Saturation
% 37.95/6.22 % (4008937)Time elapsed: 0.056 s
% 37.95/6.22 % (4008937)Peak memory usage: 89 MB
% 37.95/6.22 % (4008937)Instructions burned: 106 (million)
% 37.95/6.22 % (4008941)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1853146264:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 37.95/6.22 % (4008941)Instruction limit reached!
% 37.95/6.22 % (4008941)------------------------------
% 37.95/6.22 % (4008941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.95/6.22 % (4008941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.95/6.22 % (4008941)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008941)Termination reason: Instruction limit
% 37.95/6.22 % (4008941)Termination phase: Saturation
% 37.95/6.22 % (4008941)Time elapsed: 0.031 s
% 37.95/6.22 % (4008941)Peak memory usage: 90 MB
% 37.95/6.22 % (4008941)Instructions burned: 109 (million)
% 37.95/6.22 % (4008944)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4124744155:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 37.95/6.22 % (4008943)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2471716943:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 37.95/6.22 % (4008946)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2195018494:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 37.95/6.22 % (4008946)Instruction limit reached!
% 37.95/6.22 % (4008946)------------------------------
% 37.95/6.22 % (4008946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.95/6.22 % (4008946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.95/6.22 % (4008946)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008946)Termination reason: Instruction limit
% 37.95/6.22 % (4008946)Termination phase: Saturation
% 37.95/6.22 % (4008946)Time elapsed: 0.046 s
% 37.95/6.22 % (4008946)Peak memory usage: 90 MB
% 37.95/6.22 % (4008946)Instructions burned: 137 (million)
% 37.95/6.22 % (4008943)Instruction limit reached!
% 37.95/6.22 % (4008943)------------------------------
% 37.95/6.22 % (4008943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.95/6.22 % (4008943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.95/6.22 % (4008943)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008943)Termination reason: Instruction limit
% 37.95/6.22 % (4008943)Termination phase: Saturation
% 37.95/6.22 % (4008943)Time elapsed: 0.143 s
% 37.95/6.22 % (4008943)Peak memory usage: 90 MB
% 37.95/6.22 % (4008943)Instructions burned: 242 (million)
% 37.95/6.22 % (4008950)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2678056615:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 37.95/6.22 % (4008951)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=11696696:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 37.95/6.22 % (4008950)Instruction limit reached!
% 37.95/6.22 % (4008950)------------------------------
% 37.95/6.22 % (4008950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.95/6.22 % (4008950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.95/6.22 % (4008950)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008950)Termination reason: Instruction limit
% 37.95/6.22 % (4008950)Termination phase: Saturation
% 37.95/6.22 % (4008950)Time elapsed: 0.156 s
% 37.95/6.22 % (4008950)Peak memory usage: 96 MB
% 37.95/6.22 % (4008950)Instructions burned: 500 (million)
% 37.95/6.22 % (4008951)Instruction limit reached!
% 37.95/6.22 % (4008951)------------------------------
% 37.95/6.22 % (4008951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.95/6.22 % (4008951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.95/6.22 % (4008951)CaDiCaL version: 2.1.3
% 37.95/6.22 % (4008951)Termination reason: Instruction limit
% 37.95/6.22 % (4008951)Termination phase: Saturation
% 37.95/6.22 % (4008951)Time elapsed: 0.125 s
% 37.95/6.22 % (4008951)Peak memory usage: 91 MB
% 37.95/6.22 % (4008951)Instructions burned: 191 (million)
% 37.95/6.22 % (4008954)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2771774418:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 37.95/6.22 % (4008954)Instruction limit reached!
% 37.95/6.22 % (4008954)------------------------------
% 39.37/6.50 % (4008954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008954)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008954)Termination reason: Instruction limit
% 39.37/6.50 % (4008954)Termination phase: Saturation
% 39.37/6.50 % (4008954)Time elapsed: 0.085 s
% 39.37/6.50 % (4008954)Peak memory usage: 91 MB
% 39.37/6.50 % (4008954)Instructions burned: 265 (million)
% 39.37/6.50 % (4008955)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1108750098:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 39.37/6.50 % (4008955)Instruction limit reached!
% 39.37/6.50 % (4008955)------------------------------
% 39.37/6.50 % (4008955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008955)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008955)Termination reason: Instruction limit
% 39.37/6.50 % (4008955)Termination phase: Saturation
% 39.37/6.50 % (4008955)Time elapsed: 0.102 s
% 39.37/6.50 % (4008955)Peak memory usage: 90 MB
% 39.37/6.50 % (4008955)Instructions burned: 156 (million)
% 39.37/6.50 % (4008957)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=1143049343:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 39.37/6.50 % (4008959)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1157783062:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 39.37/6.50 % (4008959)Instruction limit reached!
% 39.37/6.50 % (4008959)------------------------------
% 39.37/6.50 % (4008959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008959)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008959)Termination reason: Instruction limit
% 39.37/6.50 % (4008959)Termination phase: Saturation
% 39.37/6.50 % (4008959)Time elapsed: 0.295 s
% 39.37/6.50 % (4008959)Peak memory usage: 92 MB
% 39.37/6.50 % (4008959)Instructions burned: 539 (million)
% 39.37/6.50 % (4008962)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=465811385:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 39.37/6.50 % (4008962)Instruction limit reached!
% 39.37/6.50 % (4008962)------------------------------
% 39.37/6.50 % (4008962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008962)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008962)Termination reason: Instruction limit
% 39.37/6.50 % (4008962)Termination phase: Saturation
% 39.37/6.50 % (4008962)Time elapsed: 0.094 s
% 39.37/6.50 % (4008962)Peak memory usage: 90 MB
% 39.37/6.50 % (4008962)Instructions burned: 181 (million)
% 39.37/6.50 % (4008964)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=1053506148:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 39.37/6.50 % (4008936)Instruction limit reached!
% 39.37/6.50 % (4008936)------------------------------
% 39.37/6.50 % (4008936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008936)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008936)Termination reason: Instruction limit
% 39.37/6.50 % (4008936)Termination phase: Saturation
% 39.37/6.50 % (4008936)Time elapsed: 1.984 s
% 39.37/6.50 % (4008936)Peak memory usage: 152 MB
% 39.37/6.50 % (4008936)Instructions burned: 3396 (million)
% 39.37/6.50 % (4008944)Instruction limit reached!
% 39.37/6.50 % (4008944)------------------------------
% 39.37/6.50 % (4008944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008944)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008944)Termination reason: Instruction limit
% 39.37/6.50 % (4008944)Termination phase: Saturation
% 39.37/6.50 % (4008944)Time elapsed: 1.904 s
% 39.37/6.50 % (4008944)Peak memory usage: 162 MB
% 39.37/6.50 % (4008944)Instructions burned: 5210 (million)
% 39.37/6.50 % (4008966)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=1505711899:i=412:gtgl=4:gtg=exists_all_2973 on theBenchmark for (2973ds/412Mi)
% 39.37/6.50 % (4008968)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=3580903892:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 39.37/6.50 % (4008966)Instruction limit reached!
% 39.37/6.50 % (4008966)------------------------------
% 39.37/6.50 % (4008966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008966)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008966)Termination reason: Instruction limit
% 39.37/6.50 % (4008966)Termination phase: Saturation
% 39.37/6.50 % (4008966)Time elapsed: 0.195 s
% 39.37/6.50 % (4008966)Peak memory usage: 91 MB
% 39.37/6.50 % (4008966)Instructions burned: 413 (million)
% 39.37/6.50 % (4008970)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=2020753717:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 39.37/6.50 % (4008970)Instruction limit reached!
% 39.37/6.50 % (4008970)------------------------------
% 39.37/6.50 % (4008970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008970)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008970)Termination reason: Instruction limit
% 39.37/6.50 % (4008970)Termination phase: Saturation
% 39.37/6.50 % (4008970)Time elapsed: 0.160 s
% 39.37/6.50 % (4008970)Peak memory usage: 92 MB
% 39.37/6.50 % (4008970)Instructions burned: 303 (million)
% 39.37/6.50 % (4008972)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2392192364:st=4:i=720:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/720Mi)
% 39.37/6.50 % (4008957)Instruction limit reached!
% 39.37/6.50 % (4008957)------------------------------
% 39.37/6.50 % (4008957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008957)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008957)Termination reason: Instruction limit
% 39.37/6.50 % (4008957)Termination phase: Saturation
% 39.37/6.50 % (4008957)Time elapsed: 1.937 s
% 39.37/6.50 % (4008957)Peak memory usage: 148 MB
% 39.37/6.50 % (4008957)Instructions burned: 3258 (million)
% 39.37/6.50 % (4008974)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2939213773:i=598:bs=on:bd=preordered:av=off:ss=axioms_2963 on theBenchmark for (2963ds/598Mi)
% 39.37/6.50 % (4008972)Instruction limit reached!
% 39.37/6.50 % (4008972)------------------------------
% 39.37/6.50 % (4008972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008972)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008972)Termination reason: Instruction limit
% 39.37/6.50 % (4008972)Termination phase: Saturation
% 39.37/6.50 % (4008972)Time elapsed: 0.363 s
% 39.37/6.50 % (4008972)Peak memory usage: 93 MB
% 39.37/6.50 % (4008972)Instructions burned: 721 (million)
% 39.37/6.50 % (4008976)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1024905387:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 39.37/6.50 % (4008974)Instruction limit reached!
% 39.37/6.50 % (4008974)------------------------------
% 39.37/6.50 % (4008974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008974)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008974)Termination reason: Instruction limit
% 39.37/6.50 % (4008974)Termination phase: Saturation
% 39.37/6.50 % (4008974)Time elapsed: 0.391 s
% 39.37/6.50 % (4008974)Peak memory usage: 94 MB
% 39.37/6.50 % (4008974)Instructions burned: 599 (million)
% 39.37/6.50 % (4008978)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=722636405:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2958 on theBenchmark for (2958ds/1997Mi)
% 39.37/6.50 % (4008976)First to succeed.
% 39.37/6.50 % (4008976)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4008907"
% 39.37/6.50 % (4008978)Instruction limit reached!
% 39.37/6.50 % (4008978)------------------------------
% 39.37/6.50 % (4008978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.37/6.50 % (4008978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.37/6.50 % (4008978)CaDiCaL version: 2.1.3
% 39.37/6.50 % (4008978)Termination reason: Instruction limit
% 39.37/6.50 % (4008978)Termination phase: Saturation
% 39.37/6.50 % (4008978)Time elapsed: 1.191 s
% 39.37/6.50 % (4008978)Peak memory usage: 140 MB
% 39.37/6.50 % (4008978)Instructions burned: 1997 (million)
% 39.37/6.50 % (4008976)Refutation found. Thanks to Tanya!
% 39.37/6.50 % SZS status Unsatisfiable for theBenchmark
% 39.37/6.50 % SZS output start Proof for theBenchmark
% See solution above
% 40.16/6.70 % (4008976)------------------------------
% 40.16/6.70 % (4008976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/6.70 % (4008976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/6.70 % (4008976)CaDiCaL version: 2.1.3
% 40.16/6.70 % (4008976)Termination reason: Refutation
% 40.16/6.70 % (4008976)Time elapsed: 1.301 s
% 40.16/6.70 % (4008976)Peak memory usage: 141 MB
% 40.16/6.70 % (4008976)Instructions burned: 2126 (million)
% 40.16/6.70 % (4008976)------------------------------
% 40.16/6.70 % (4008976)------------------------------
% 40.16/6.70 % (4008907)Success in time 5.629 s
% 40.16/6.70 % Vampire exiting
%------------------------------------------------------------------------------