%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL444-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 11:52:27 AM UTC 2026
% Result : Unsatisfiable 53.83s 17.23s
% Output : Refutation 115.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 8
% Syntax : Number of formulae : 27 ( 13 unt; 0 def)
% Number of atoms : 43 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 51 ( 35 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 34 ( 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [X2,X0,X1] :
( c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| ~ c_in(X0,X1,tc_PropLog_Opl(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_PropLog_Othms_OH_0) ).
fof(f238,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_insert(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OinsertCI_0) ).
fof(f239,axiom,
! [X2,X0,X1] : c_in(X0,c_insert(X0,X1,X2),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OinsertCI_1) ).
fof(f1446,axiom,
! [X2,X3,X0,X1] :
( c_in(c_PropLog_Opl_Oop_A_N_62(X1,X0,X3),c_PropLog_Othms(X2,X3),tc_PropLog_Opl(X3))
| ~ c_in(X0,c_PropLog_Othms(c_insert(X1,X2,tc_PropLog_Opl(X3)),X3),tc_PropLog_Opl(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_PropLog_Odeduction_0) ).
fof(f1447,axiom,
! [X2,X0,X1] : c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,X1),c_PropLog_Opl_Ofalse,X1),X0,X1),c_PropLog_Othms(X2,X1),tc_PropLog_Opl(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_PropLog_Othms_ODN_0) ).
fof(f1448,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,X3,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(X3,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_PropLog_Othms_OMP_0) ).
fof(f1449,axiom,
! [X2,X3,X0,X1] :
( c_in(X3,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,X3,X2),X1,tc_PropLog_Opl(X2))
| ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_PropLog_Othms__H__MP_0) ).
fof(f1450,negated_conjecture,
~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),v_q,t_a),t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1466,plain,
~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),v_q,t_a),c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(unit_resulting_resolution,[],[f1446,f1450]) ).
fof(f1482,plain,
~ c_in(v_q,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1466,f1446]) ).
fof(f1508,plain,
~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(unit_resulting_resolution,[],[f1448,f1447,f1482]) ).
fof(f1717,plain,
~ c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1508,f1446]) ).
fof(f1729,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1717,f1449]) ).
fof(f1732,plain,
~ c_in(v_q,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1729,f239]) ).
fof(f1740,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1732,f1449]) ).
fof(f1742,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1740,f238]) ).
fof(f1745,plain,
~ c_in(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1742,f239]) ).
fof(f1753,plain,
~ c_in(c_PropLog_Opl_Ofalse,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1745,f1446]) ).
fof(f1764,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,t_a),c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1753,f1449]) ).
fof(f1803,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1764,f238]) ).
fof(f1818,plain,
~ c_in(v_q,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1803,f239]) ).
fof(f1826,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1818,f1449]) ).
fof(f1828,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1826,f238]) ).
fof(f1830,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1828,f238]) ).
fof(f1834,plain,
! [X0] :
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a))
| ~ c_in(X0,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[],[f1830,f238]) ).
fof(f1855,plain,
~ c_in(v_p,c_PropLog_Othms(c_insert(v_p,c_insert(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),v_q,t_a),c_insert(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),v_H,tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[],[f1834,f239]) ).
fof(f1858,plain,
$false,
inference(unit_resulting_resolution,[],[f12,f239,f1855]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL444-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 15:43:16 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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.29/2.43 % (2198073)Input is clausal, will run a generic CNF schedule.
% 10.29/2.43 % (2198090)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2013662404:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.29/2.43 % (2198089)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3102505514:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.29/2.43 % (2198091)dis-21_1_sil=8000:lcm=predicate:random_seed=3544698144: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.29/2.43 % (2198086)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1102523837:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.29/2.43 % (2198085)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=4151308617:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.29/2.43 % (2198087)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=394908375:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.29/2.43 % (2198090)Instruction limit reached!
% 10.29/2.43 % (2198090)------------------------------
% 10.29/2.43 % (2198090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.43 % (2198090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.43 % (2198090)CaDiCaL version: 2.1.3
% 10.29/2.43 % (2198090)Termination reason: Instruction limit
% 10.29/2.43 % (2198090)Termination phase: Saturation
% 10.29/2.43 % (2198090)Time elapsed: 0.069 s
% 10.29/2.43 % (2198090)Peak memory usage: 90 MB
% 10.29/2.43 % (2198090)Instructions burned: 181 (million)
% 10.29/2.43 % (2198088)lrs+10_1_sil=8000:sp=occurrence:random_seed=3276699455:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.29/2.43 % (2198091)Instruction limit reached!
% 10.29/2.43 % (2198091)------------------------------
% 10.29/2.43 % (2198091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.43 % (2198091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.43 % (2198091)CaDiCaL version: 2.1.3
% 10.29/2.43 % (2198091)Termination reason: Instruction limit
% 10.29/2.43 % (2198091)Termination phase: Saturation
% 10.29/2.43 % (2198091)Time elapsed: 0.069 s
% 10.29/2.43 % (2198091)Peak memory usage: 89 MB
% 10.29/2.43 % (2198091)Instructions burned: 118 (million)
% 10.29/2.43 % (2198089)Instruction limit reached!
% 10.29/2.43 % (2198089)------------------------------
% 10.29/2.43 % (2198089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.43 % (2198089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.43 % (2198089)CaDiCaL version: 2.1.3
% 10.29/2.43 % (2198089)Termination reason: Instruction limit
% 10.29/2.43 % (2198089)Termination phase: Saturation
% 10.29/2.43 % (2198089)Time elapsed: 0.069 s
% 10.29/2.43 % (2198089)Peak memory usage: 89 MB
% 10.29/2.43 % (2198089)Instructions burned: 114 (million)
% 10.29/2.43 % (2198099)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=1499111513:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.29/2.43 % (2198099)Refutation not found, incomplete strategy
% 10.29/2.43 % (2198099)------------------------------
% 10.29/2.43 % (2198099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.43 % (2198099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.43 % (2198099)CaDiCaL version: 2.1.3
% 10.29/2.43 % (2198099)Termination reason: Refutation not found, incomplete strategy
% 10.29/2.43 % (2198099)Time elapsed: 0.002 s
% 10.29/2.43 % (2198099)Peak memory usage: 88 MB
% 10.29/2.43 % (2198099)Instructions burned: 4 (million)
% 10.29/2.43 % (2198088)Instruction limit reached!
% 10.29/2.43 % (2198088)------------------------------
% 10.29/2.43 % (2198088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.43 % (2198088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.43 % (2198088)CaDiCaL version: 2.1.3
% 10.29/2.43 % (2198088)Termination reason: Instruction limit
% 10.29/2.43 % (2198088)Termination phase: Saturation
% 10.29/2.43 % (2198088)Time elapsed: 0.071 s
% 10.29/2.43 % (2198088)Peak memory usage: 89 MB
% 10.29/2.43 % (2198088)Instructions burned: 108 (million)
% 10.29/2.43 % (2198102)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3935676422:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 16.51/3.30 % (2198101)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2078361160: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)
% 16.51/3.30 % (2198102)Refutation not found, incomplete strategy
% 16.51/3.30 % (2198102)------------------------------
% 16.51/3.30 % (2198102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.51/3.30 % (2198102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/3.30 % (2198102)CaDiCaL version: 2.1.3
% 16.51/3.30 % (2198102)Termination reason: Refutation not found, incomplete strategy
% 16.51/3.30 % (2198102)Time elapsed: 0.005 s
% 16.51/3.30 % (2198102)Peak memory usage: 88 MB
% 16.51/3.30 % (2198102)Instructions burned: 6 (million)
% 16.51/3.30 % (2198099)------------------------------
% 16.51/3.30 % (2198099)------------------------------
% 16.51/3.30 % (2198119)lrs+10_64_to=lpo:sil=8000:random_seed=1837218397:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 16.51/3.30 % (2198101)Instruction limit reached!
% 16.51/3.30 % (2198101)------------------------------
% 16.51/3.30 % (2198101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.51/3.30 % (2198101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/3.30 % (2198101)CaDiCaL version: 2.1.3
% 16.51/3.30 % (2198101)Termination reason: Instruction limit
% 16.51/3.30 % (2198101)Termination phase: Saturation
% 16.51/3.30 % (2198101)Time elapsed: 0.116 s
% 16.51/3.30 % (2198101)Peak memory usage: 91 MB
% 16.51/3.30 % (2198101)Instructions burned: 190 (million)
% 16.51/3.30 % (2198119)Instruction limit reached!
% 16.51/3.30 % (2198119)------------------------------
% 16.51/3.30 % (2198119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.51/3.30 % (2198119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/3.30 % (2198119)CaDiCaL version: 2.1.3
% 16.51/3.30 % (2198119)Termination reason: Instruction limit
% 16.51/3.30 % (2198119)Termination phase: Saturation
% 16.51/3.30 % (2198119)Time elapsed: 0.081 s
% 16.51/3.30 % (2198119)Peak memory usage: 89 MB
% 16.51/3.30 % (2198119)Instructions burned: 127 (million)
% 16.51/3.30 % (2198175)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2523603385:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 16.51/3.30 % (2198175)Instruction limit reached!
% 16.51/3.30 % (2198175)------------------------------
% 16.51/3.30 % (2198175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.51/3.30 % (2198175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/3.30 % (2198175)CaDiCaL version: 2.1.3
% 16.51/3.30 % (2198175)Termination reason: Instruction limit
% 16.51/3.30 % (2198175)Termination phase: Saturation
% 16.51/3.30 % (2198175)Time elapsed: 0.068 s
% 16.51/3.30 % (2198175)Peak memory usage: 90 MB
% 16.51/3.30 % (2198175)Instructions burned: 197 (million)
% 16.51/3.30 % (2198102)------------------------------
% 16.51/3.30 % (2198102)------------------------------
% 16.51/3.30 % (2198185)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1364827113:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 16.51/3.30 % (2198196)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3293924743:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 16.51/3.30 % (2198203)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=3701869483:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 16.51/3.30 % (2198185)Instruction limit reached!
% 16.51/3.30 % (2198185)------------------------------
% 16.51/3.30 % (2198185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.51/3.30 % (2198185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.51/3.30 % (2198185)CaDiCaL version: 2.1.3
% 16.51/3.30 % (2198185)Termination reason: Instruction limit
% 16.51/3.30 % (2198185)Termination phase: Saturation
% 16.51/3.30 % (2198185)Time elapsed: 0.094 s
% 16.51/3.30 % (2198185)Peak memory usage: 91 MB
% 16.51/3.30 % (2198185)Instructions burned: 158 (million)
% 16.51/3.30 % (2198203)Instruction limit reached!
% 16.51/3.30 % (2198203)------------------------------
% 16.51/3.30 % (2198203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198203)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198203)Termination reason: Instruction limit
% 31.51/5.47 % (2198203)Termination phase: Saturation
% 31.51/5.47 % (2198203)Time elapsed: 0.033 s
% 31.51/5.47 % (2198203)Peak memory usage: 89 MB
% 31.51/5.47 % (2198203)Instructions burned: 111 (million)
% 31.51/5.47 % (2198204)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3691836124:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 31.51/5.47 % (2198204)Refutation not found, incomplete strategy
% 31.51/5.47 % (2198204)------------------------------
% 31.51/5.47 % (2198204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198204)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198204)Termination reason: Refutation not found, incomplete strategy
% 31.51/5.47 % (2198204)Time elapsed: 0.009 s
% 31.51/5.47 % (2198204)Peak memory usage: 88 MB
% 31.51/5.47 % (2198204)Instructions burned: 12 (million)
% 31.51/5.47 % (2198209)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=667634571:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 31.51/5.47 % (2198208)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3551527333:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 31.51/5.47 % (2198208)Instruction limit reached!
% 31.51/5.47 % (2198208)------------------------------
% 31.51/5.47 % (2198208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198208)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198208)Termination reason: Instruction limit
% 31.51/5.47 % (2198208)Termination phase: Saturation
% 31.51/5.47 % (2198208)Time elapsed: 0.126 s
% 31.51/5.47 % (2198208)Peak memory usage: 89 MB
% 31.51/5.47 % (2198208)Instructions burned: 243 (million)
% 31.51/5.47 % (2198204)------------------------------
% 31.51/5.47 % (2198204)------------------------------
% 31.51/5.47 % (2198246)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2306022600:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 31.51/5.47 % (2198254)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3133839442:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 31.51/5.47 % (2198246)Instruction limit reached!
% 31.51/5.47 % (2198246)------------------------------
% 31.51/5.47 % (2198246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198246)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198246)Termination reason: Instruction limit
% 31.51/5.47 % (2198246)Termination phase: Saturation
% 31.51/5.47 % (2198246)Time elapsed: 0.084 s
% 31.51/5.47 % (2198246)Peak memory usage: 90 MB
% 31.51/5.47 % (2198246)Instructions burned: 135 (million)
% 31.51/5.47 % (2198278)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3021167348:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 31.51/5.47 % (2198254)Instruction limit reached!
% 31.51/5.47 % (2198254)------------------------------
% 31.51/5.47 % (2198254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198254)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198254)Termination reason: Instruction limit
% 31.51/5.47 % (2198254)Termination phase: Saturation
% 31.51/5.47 % (2198254)Time elapsed: 0.254 s
% 31.51/5.47 % (2198254)Peak memory usage: 98 MB
% 31.51/5.47 % (2198254)Instructions burned: 499 (million)
% 31.51/5.47 % (2198278)Instruction limit reached!
% 31.51/5.47 % (2198278)------------------------------
% 31.51/5.47 % (2198278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.51/5.47 % (2198278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/5.47 % (2198278)CaDiCaL version: 2.1.3
% 31.51/5.47 % (2198278)Termination reason: Instruction limit
% 31.51/5.47 % (2198278)Termination phase: Saturation
% 31.51/5.47 % (2198278)Time elapsed: 0.135 s
% 31.51/5.47 % (2198278)Peak memory usage: 92 MB
% 31.51/5.47 % (2198278)Instructions burned: 191 (million)
% 45.87/7.53 % (2198280)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1670210710:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 45.87/7.53 % (2198281)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=807592938:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 45.87/7.53 % (2198280)Instruction limit reached!
% 45.87/7.53 % (2198280)------------------------------
% 45.87/7.53 % (2198280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.87/7.53 % (2198280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/7.53 % (2198280)CaDiCaL version: 2.1.3
% 45.87/7.53 % (2198280)Termination reason: Instruction limit
% 45.87/7.53 % (2198280)Termination phase: Saturation
% 45.87/7.53 % (2198280)Time elapsed: 0.147 s
% 45.87/7.53 % (2198280)Peak memory usage: 92 MB
% 45.87/7.53 % (2198280)Instructions burned: 266 (million)
% 45.87/7.53 % (2198281)Instruction limit reached!
% 45.87/7.53 % (2198281)------------------------------
% 45.87/7.53 % (2198281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.87/7.53 % (2198281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/7.53 % (2198281)CaDiCaL version: 2.1.3
% 45.87/7.53 % (2198281)Termination reason: Instruction limit
% 45.87/7.53 % (2198281)Termination phase: Saturation
% 45.87/7.53 % (2198281)Time elapsed: 0.093 s
% 45.87/7.53 % (2198281)Peak memory usage: 90 MB
% 45.87/7.53 % (2198281)Instructions burned: 156 (million)
% 45.87/7.53 % (2198284)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=1950085488:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 45.87/7.53 % (2198285)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2821910803:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 45.87/7.53 % (2198196)Instruction limit reached!
% 45.87/7.53 % (2198196)------------------------------
% 45.87/7.53 % (2198196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.87/7.53 % (2198196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/7.53 % (2198196)CaDiCaL version: 2.1.3
% 45.87/7.53 % (2198196)Termination reason: Instruction limit
% 45.87/7.53 % (2198196)Termination phase: Saturation
% 45.87/7.53 % (2198196)Time elapsed: 1.322 s
% 45.87/7.53 % (2198196)Peak memory usage: 150 MB
% 45.87/7.53 % (2198196)Instructions burned: 3396 (million)
% 45.87/7.53 % (2198285)Instruction limit reached!
% 45.87/7.53 % (2198285)------------------------------
% 45.87/7.53 % (2198285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.87/7.53 % (2198285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/7.53 % (2198285)CaDiCaL version: 2.1.3
% 45.87/7.53 % (2198285)Termination reason: Instruction limit
% 45.87/7.53 % (2198285)Termination phase: Saturation
% 45.87/7.53 % (2198285)Time elapsed: 0.246 s
% 45.87/7.53 % (2198285)Peak memory usage: 90 MB
% 45.87/7.53 % (2198285)Instructions burned: 537 (million)
% 45.87/7.53 % (2198288)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4030832091:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 45.87/7.53 % (2198288)Instruction limit reached!
% 45.87/7.53 % (2198288)------------------------------
% 45.87/7.53 % (2198288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.87/7.53 % (2198288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.87/7.53 % (2198288)CaDiCaL version: 2.1.3
% 45.87/7.53 % (2198288)Termination reason: Instruction limit
% 45.87/7.53 % (2198288)Termination phase: Saturation
% 45.87/7.53 % (2198288)Time elapsed: 0.056 s
% 45.87/7.53 % (2198288)Peak memory usage: 95 MB
% 45.87/7.53 % (2198288)Instructions burned: 185 (million)
% 45.87/7.53 % (2198289)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=1188241227:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 45.87/7.53 % (2198291)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=1943171040:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 45.87/7.53 % (2198291)Instruction limit reached!
% 45.87/7.53 % (2198291)------------------------------
% 45.87/7.53 % (2198291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198291)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198291)Termination reason: Instruction limit
% 62.29/9.96 % (2198291)Termination phase: Saturation
% 62.29/9.96 % (2198291)Time elapsed: 0.117 s
% 62.29/9.96 % (2198291)Peak memory usage: 96 MB
% 62.29/9.96 % (2198291)Instructions burned: 412 (million)
% 62.29/9.96 % (2198294)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=2729268514:s2pl=no:i=8478:s2at=4:nm=6_2976 on theBenchmark for (2976ds/8478Mi)
% 62.29/9.96 % (2198284)Instruction limit reached!
% 62.29/9.96 % (2198284)------------------------------
% 62.29/9.96 % (2198284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198284)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198284)Termination reason: Instruction limit
% 62.29/9.96 % (2198284)Termination phase: Saturation
% 62.29/9.96 % (2198284)Time elapsed: 1.828 s
% 62.29/9.96 % (2198284)Peak memory usage: 148 MB
% 62.29/9.96 % (2198284)Instructions burned: 3256 (million)
% 62.29/9.96 % (2198209)Instruction limit reached!
% 62.29/9.96 % (2198209)------------------------------
% 62.29/9.96 % (2198209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198209)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198209)Termination reason: Instruction limit
% 62.29/9.96 % (2198209)Termination phase: Saturation
% 62.29/9.96 % (2198209)Time elapsed: 2.796 s
% 62.29/9.96 % (2198209)Peak memory usage: 166 MB
% 62.29/9.96 % (2198209)Instructions burned: 5209 (million)
% 62.29/9.96 % (2198297)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=527807398:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2963 on theBenchmark for (2963ds/303Mi)
% 62.29/9.96 % (2198298)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1507170063:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi)
% 62.29/9.96 % (2198297)Instruction limit reached!
% 62.29/9.96 % (2198297)------------------------------
% 62.29/9.96 % (2198297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198297)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198297)Termination reason: Instruction limit
% 62.29/9.96 % (2198297)Termination phase: Saturation
% 62.29/9.96 % (2198297)Time elapsed: 0.152 s
% 62.29/9.96 % (2198297)Peak memory usage: 92 MB
% 62.29/9.96 % (2198297)Instructions burned: 305 (million)
% 62.29/9.96 % (2198301)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3752716483:i=598:bs=on:bd=preordered:av=off:ss=axioms_2961 on theBenchmark for (2961ds/598Mi)
% 62.29/9.96 % (2198298)Instruction limit reached!
% 62.29/9.96 % (2198298)------------------------------
% 62.29/9.96 % (2198298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198298)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198298)Termination reason: Instruction limit
% 62.29/9.96 % (2198298)Termination phase: Saturation
% 62.29/9.96 % (2198298)Time elapsed: 0.401 s
% 62.29/9.96 % (2198298)Peak memory usage: 93 MB
% 62.29/9.96 % (2198298)Instructions burned: 721 (million)
% 62.29/9.96 % (2198303)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2986443282:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi)
% 62.29/9.96 % (2198301)Instruction limit reached!
% 62.29/9.96 % (2198301)------------------------------
% 62.29/9.96 % (2198301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.29/9.96 % (2198301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.29/9.96 % (2198301)CaDiCaL version: 2.1.3
% 62.29/9.96 % (2198301)Termination reason: Instruction limit
% 62.29/9.96 % (2198301)Termination phase: Saturation
% 62.29/9.96 % (2198301)Time elapsed: 0.364 s
% 62.29/9.96 % (2198301)Peak memory usage: 94 MB
% 62.29/9.96 % (2198301)Instructions burned: 599 (million)
% 62.29/9.96 % (2198305)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=1009277851:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi)
% 93.04/14.11 % (2198294)Instruction limit reached!
% 93.04/14.11 % (2198294)------------------------------
% 93.04/14.11 % (2198294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.04/14.11 % (2198294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.04/14.11 % (2198294)CaDiCaL version: 2.1.3
% 93.04/14.11 % (2198294)Termination reason: Instruction limit
% 93.04/14.11 % (2198294)Termination phase: Saturation
% 93.04/14.11 % (2198294)Time elapsed: 2.626 s
% 93.04/14.11 % (2198294)Peak memory usage: 193 MB
% 93.04/14.11 % (2198294)Instructions burned: 8480 (million)
% 93.04/14.11 % (2198307)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=4131603341:i=2088:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2088Mi)
% 93.04/14.11 % (2198305)Instruction limit reached!
% 93.04/14.11 % (2198305)------------------------------
% 93.04/14.11 % (2198305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.04/14.11 % (2198305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.04/14.11 % (2198305)CaDiCaL version: 2.1.3
% 93.04/14.11 % (2198305)Termination reason: Instruction limit
% 93.04/14.11 % (2198305)Termination phase: Saturation
% 93.04/14.11 % (2198305)Time elapsed: 1.297 s
% 93.04/14.11 % (2198305)Peak memory usage: 137 MB
% 93.04/14.11 % (2198305)Instructions burned: 1997 (million)
% 93.04/14.11 % (2198307)Instruction limit reached!
% 93.04/14.11 % (2198307)------------------------------
% 93.04/14.11 % (2198307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.04/14.11 % (2198307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.04/14.11 % (2198307)CaDiCaL version: 2.1.3
% 93.04/14.11 % (2198307)Termination reason: Instruction limit
% 93.04/14.11 % (2198307)Termination phase: Saturation
% 93.04/14.11 % (2198307)Time elapsed: 0.740 s
% 93.04/14.11 % (2198307)Peak memory usage: 138 MB
% 93.04/14.11 % (2198307)Instructions burned: 2091 (million)
% 93.04/14.11 % (2198309)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=761125901:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 93.04/14.11 % (2198310)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=406403112:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi)
% 93.04/14.11 % (2198310)Refutation not found, incomplete strategy
% 93.04/14.11 % (2198310)------------------------------
% 93.04/14.11 % (2198310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.04/14.11 % (2198310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.04/14.11 % (2198310)CaDiCaL version: 2.1.3
% 93.04/14.11 % (2198310)Termination reason: Refutation not found, incomplete strategy
% 93.04/14.11 % (2198310)Time elapsed: 0.011 s
% 93.04/14.11 % (2198310)Peak memory usage: 89 MB
% 93.04/14.11 % (2198310)Instructions burned: 35 (million)
% 93.04/14.11 % (2198303)Instruction limit reached!
% 93.04/14.11 % (2198303)------------------------------
% 93.04/14.11 % (2198303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.04/14.11 % (2198303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.04/14.11 % (2198303)CaDiCaL version: 2.1.3
% 93.04/14.11 % (2198303)Termination reason: Instruction limit
% 93.04/14.11 % (2198303)Termination phase: Saturation
% 93.04/14.11 % (2198303)Time elapsed: 1.782 s
% 93.04/14.11 % (2198303)Peak memory usage: 144 MB
% 93.04/14.11 % (2198303)Instructions burned: 2990 (million)
% 93.04/14.11 % (2198310)------------------------------
% 93.04/14.11 % (2198310)------------------------------
% 93.04/14.11 % (2198313)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1834526338:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2939 on theBenchmark for (2939ds/2942Mi)
% 93.04/14.11 % (2198314)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1028998269:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2938 on theBenchmark for (2938ds/6922Mi)
% 93.04/14.11 % (2198309)Instruction limit reached!
% 93.04/14.11 % (2198309)------------------------------
% 93.04/14.11 % (2198309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198309)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198309)Termination reason: Instruction limit
% 53.83/17.23 % (2198309)Termination phase: Saturation
% 53.83/17.23 % (2198309)Time elapsed: 0.616 s
% 53.83/17.23 % (2198309)Peak memory usage: 107 MB
% 53.83/17.23 % (2198309)Instructions burned: 1099 (million)
% 53.83/17.23 % (2198317)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3032163816:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2934 on theBenchmark for (2934ds/596Mi)
% 53.83/17.23 % (2198317)Instruction limit reached!
% 53.83/17.23 % (2198317)------------------------------
% 53.83/17.23 % (2198317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198317)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198317)Termination reason: Instruction limit
% 53.83/17.23 % (2198317)Termination phase: Saturation
% 53.83/17.23 % (2198317)Time elapsed: 0.176 s
% 53.83/17.23 % (2198317)Peak memory usage: 97 MB
% 53.83/17.23 % (2198317)Instructions burned: 600 (million)
% 53.83/17.23 % (2198319)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2175692255:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2931 on theBenchmark for (2931ds/4123Mi)
% 53.83/17.23 % (2198313)Instruction limit reached!
% 53.83/17.23 % (2198313)------------------------------
% 53.83/17.23 % (2198313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198313)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198313)Termination reason: Instruction limit
% 53.83/17.23 % (2198313)Termination phase: Saturation
% 53.83/17.23 % (2198313)Time elapsed: 1.903 s
% 53.83/17.23 % (2198313)Peak memory usage: 147 MB
% 53.83/17.23 % (2198313)Instructions burned: 2943 (million)
% 53.83/17.23 % (2198321)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=692777916:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2919 on theBenchmark for (2919ds/16411Mi)
% 53.83/17.23 % (2198319)Instruction limit reached!
% 53.83/17.23 % (2198319)------------------------------
% 53.83/17.23 % (2198319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198319)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198319)Termination reason: Instruction limit
% 53.83/17.23 % (2198319)Termination phase: Saturation
% 53.83/17.23 % (2198319)Time elapsed: 1.318 s
% 53.83/17.23 % (2198319)Peak memory usage: 161 MB
% 53.83/17.23 % (2198319)Instructions burned: 4128 (million)
% 53.83/17.23 % (2198289)Instruction limit reached!
% 53.83/17.23 % (2198289)------------------------------
% 53.83/17.23 % (2198289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198289)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198289)Termination reason: Instruction limit
% 53.83/17.23 % (2198289)Termination phase: Saturation
% 53.83/17.23 % (2198289)Time elapsed: 6.146 s
% 53.83/17.23 % (2198289)Peak memory usage: 203 MB
% 53.83/17.23 % (2198289)Instructions burned: 10310 (million)
% 53.83/17.23 % (2198323)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=196589798:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2917 on theBenchmark for (2917ds/1670Mi)
% 53.83/17.23 % (2198325)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3584959036:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2916 on theBenchmark for (2916ds/1722Mi)
% 53.83/17.23 % (2198323)Instruction limit reached!
% 53.83/17.23 % (2198323)------------------------------
% 53.83/17.23 % (2198323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198323)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198323)Termination reason: Instruction limit
% 53.83/17.23 % (2198323)Termination phase: Saturation
% 53.83/17.23 % (2198323)Time elapsed: 0.565 s
% 53.83/17.23 % (2198323)Peak memory usage: 138 MB
% 53.83/17.23 % (2198323)Instructions burned: 1670 (million)
% 53.83/17.23 % (2198327)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=654123230:cts=off:cond=on:i=9530:bs=on:fsd=on_2910 on theBenchmark for (2910ds/9530Mi)
% 53.83/17.23 % (2198325)Instruction limit reached!
% 53.83/17.23 % (2198325)------------------------------
% 53.83/17.23 % (2198325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198325)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198325)Termination reason: Instruction limit
% 53.83/17.23 % (2198325)Termination phase: Saturation
% 53.83/17.23 % (2198325)Time elapsed: 1.133 s
% 53.83/17.23 % (2198325)Peak memory usage: 136 MB
% 53.83/17.23 % (2198325)Instructions burned: 1722 (million)
% 53.83/17.23 % (2198329)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3575579258:st=2:i=4495:sd=10:ss=included_2903 on theBenchmark for (2903ds/4495Mi)
% 53.83/17.23 % (2198314)Instruction limit reached!
% 53.83/17.23 % (2198314)------------------------------
% 53.83/17.23 % (2198314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198314)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198314)Termination reason: Instruction limit
% 53.83/17.23 % (2198314)Termination phase: Saturation
% 53.83/17.23 % (2198314)Time elapsed: 3.671 s
% 53.83/17.23 % (2198314)Peak memory usage: 175 MB
% 53.83/17.23 % (2198314)Instructions burned: 6922 (million)
% 53.83/17.23 % (2198331)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3926322954:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2900 on theBenchmark for (2900ds/4920Mi)
% 53.83/17.23 % (2198327)Instruction limit reached!
% 53.83/17.23 % (2198327)------------------------------
% 53.83/17.23 % (2198327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198327)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198327)Termination reason: Instruction limit
% 53.83/17.23 % (2198327)Termination phase: Saturation
% 53.83/17.23 % (2198327)Time elapsed: 3.126 s
% 53.83/17.23 % (2198327)Peak memory usage: 169 MB
% 53.83/17.23 % (2198327)Instructions burned: 9530 (million)
% 53.83/17.23 % (2198335)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2078105829:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2878 on theBenchmark for (2878ds/2083Mi)
% 53.83/17.23 % (2198329)Instruction limit reached!
% 53.83/17.23 % (2198329)------------------------------
% 53.83/17.23 % (2198329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198329)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198329)Termination reason: Instruction limit
% 53.83/17.23 % (2198329)Termination phase: Saturation
% 53.83/17.23 % (2198329)Time elapsed: 2.675 s
% 53.83/17.23 % (2198329)Peak memory usage: 157 MB
% 53.83/17.23 % (2198329)Instructions burned: 4496 (million)
% 53.83/17.23 % (2198337)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3615522242:i=4629:av=off:gsp=on_2875 on theBenchmark for (2875ds/4629Mi)
% 53.83/17.23 % (2198335)Instruction limit reached!
% 53.83/17.23 % (2198335)------------------------------
% 53.83/17.23 % (2198335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198335)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198335)Termination reason: Instruction limit
% 53.83/17.23 % (2198335)Termination phase: Saturation
% 53.83/17.23 % (2198335)Time elapsed: 0.800 s
% 53.83/17.23 % (2198335)Peak memory usage: 138 MB
% 53.83/17.23 % (2198335)Instructions burned: 2083 (million)
% 53.83/17.23 % (2198430)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1889900239:i=1258:av=off_2869 on theBenchmark for (2869ds/1258Mi)
% 53.83/17.23 % (2198331)Instruction limit reached!
% 53.83/17.23 % (2198331)------------------------------
% 53.83/17.23 % (2198331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198331)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198331)Termination reason: Instruction limit
% 53.83/17.23 % (2198331)Termination phase: Saturation
% 53.83/17.23 % (2198331)Time elapsed: 3.067 s
% 53.83/17.23 % (2198331)Peak memory usage: 159 MB
% 53.83/17.23 % (2198331)Instructions burned: 4921 (million)
% 53.83/17.23 % (2198473)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2664909624:i=7343:av=off:ss=included_2868 on theBenchmark for (2868ds/7343Mi)
% 53.83/17.23 % (2198430)Instruction limit reached!
% 53.83/17.23 % (2198430)------------------------------
% 53.83/17.23 % (2198430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198430)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198430)Termination reason: Instruction limit
% 53.83/17.23 % (2198430)Termination phase: Saturation
% 53.83/17.23 % (2198430)Time elapsed: 0.386 s
% 53.83/17.23 % (2198430)Peak memory usage: 101 MB
% 53.83/17.23 % (2198430)Instructions burned: 1261 (million)
% 53.83/17.23 % (2198475)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=240325141:i=1325:sd=2:ss=axioms:sgt=16_2864 on theBenchmark for (2864ds/1325Mi)
% 53.83/17.23 % (2198475)Refutation not found, incomplete strategy
% 53.83/17.23 % (2198475)------------------------------
% 53.83/17.23 % (2198475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198475)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198475)Termination reason: Refutation not found, incomplete strategy
% 53.83/17.23 % (2198475)Time elapsed: 0.003 s
% 53.83/17.23 % (2198475)Peak memory usage: 88 MB
% 53.83/17.23 % (2198475)Instructions burned: 4 (million)
% 53.83/17.23 % (2198475)------------------------------
% 53.83/17.23 % (2198475)------------------------------
% 53.83/17.23 % (2198578)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1177862748:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2861 on theBenchmark for (2861ds/2646Mi)
% 53.83/17.23 % (2198578)Instruction limit reached!
% 53.83/17.23 % (2198578)------------------------------
% 53.83/17.23 % (2198578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198578)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198578)Termination reason: Instruction limit
% 53.83/17.23 % (2198578)Termination phase: Saturation
% 53.83/17.23 % (2198578)Time elapsed: 1.305 s
% 53.83/17.23 % (2198578)Peak memory usage: 143 MB
% 53.83/17.23 % (2198578)Instructions burned: 2646 (million)
% 53.83/17.23 % (2198337)Instruction limit reached!
% 53.83/17.23 % (2198337)------------------------------
% 53.83/17.23 % (2198337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.83/17.23 % (2198337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/17.23 % (2198337)CaDiCaL version: 2.1.3
% 53.83/17.23 % (2198337)Termination reason: Instruction limit
% 53.83/17.23 % (2198337)Termination phase: Saturation
% 53.83/17.23 % (2198337)Time elapsed: 2.768 s
% 53.83/17.23 % (2198337)Peak memory usage: 150 MB
% 53.83/17.23 % (2198337)Instructions burned: 4630 (million)
% 53.83/17.23 % (2198609)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=5577035:i=1489:sd=2:ep=R:ss=axioms_2847 on theBenchmark for (2847ds/1489Mi)
% 53.83/17.23 % (2198610)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3996061225:i=1503_2846 on theBenchmark for (2846ds/1503Mi)
% 53.83/17.23 % (2198609)First to succeed.
% 53.83/17.23 % (2198609)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2198073"
% 53.83/17.23 % (2198609)Refutation found. Thanks to Tanya!
% 53.83/17.23 % SZS status Unsatisfiable for theBenchmark
% 53.83/17.23 % SZS output start Proof for theBenchmark
% See solution above
% 115.35/17.63 % (2198609)------------------------------
% 115.35/17.63 % (2198609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.35/17.63 % (2198609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.35/17.63 % (2198609)CaDiCaL version: 2.1.3
% 115.35/17.63 % (2198609)Termination reason: Refutation
% 115.35/17.63 % (2198609)Time elapsed: 0.439 s
% 115.35/17.63 % (2198609)Peak memory usage: 130 MB
% 115.35/17.63 % (2198609)Instructions burned: 1029 (million)
% 115.35/17.63 % (2198609)------------------------------
% 115.35/17.63 % (2198609)------------------------------
% 115.35/17.63 % (2198073)Success in time 16.476 s
% 115.35/17.63 % Vampire exiting
%------------------------------------------------------------------------------