%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV585-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 01:19:02 PM UTC 2026
% Result : Unsatisfiable 18.58s 3.35s
% Output : Refutation 19.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 74 ( 44 unt; 7 def)
% Number of atoms : 106 ( 57 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 66 ( 34 ~; 31 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 8 con; 0-3 aty)
% Number of variables : 47 ( 0 sgn 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f189,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__mult__distrib2_0) ).
fof(f262,axiom,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat)
| c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_even__nat__div__two__times__two_0) ).
fof(f441,axiom,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__iff__Suc__add_1) ).
fof(f538,axiom,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(X0,tc_nat)
| c_Suc(c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_odd__nat__div__two__times__two__plus__one_0) ).
fof(f613,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__diff__inverse_0) ).
fof(f638,axiom,
c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comp__arith_I115_J_0) ).
fof(f643,axiom,
! [X0] : c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat) = c_HOL_Oplus__class_Oplus(X0,X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__mult__2_0) ).
fof(f644,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_nat) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat),
inference(reorient_equations,[],[f643]) ).
fof(f679,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f695,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__SucI_0) ).
fof(f702,axiom,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X2,X0,tc_nat),c_HOL_Otimes__class_Otimes(X2,X1,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__less__cancel1_1) ).
fof(f739,negated_conjecture,
c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),v_n,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f740,negated_conjecture,
! [X0] :
( v_x != c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat))
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f741,plain,
! [X0] :
( c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat)) != v_x
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(reorient_equations,[],[f740]) ).
fof(f742,negated_conjecture,
! [X0] :
( v_x != c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f743,plain,
! [X0] :
( c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat) != v_x
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(reorient_equations,[],[f742]) ).
fof(f814,definition,
sF0 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f815,plain,
c_Int_OBit1(c_Int_OPls) = sF0,
inference(reorient_equations,[],[f814]) ).
fof(f816,definition,
sF1 = c_Int_OBit0(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f817,plain,
c_Int_OBit0(sF0) = sF1,
inference(reorient_equations,[],[f816]) ).
fof(f818,definition,
sF2 = c_Int_Onumber__class_Onumber__of(sF1,tc_nat),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f819,plain,
c_Int_Onumber__class_Onumber__of(sF1,tc_nat) = sF2,
inference(reorient_equations,[],[f818]) ).
fof(f820,definition,
sF3 = c_HOL_Otimes__class_Otimes(sF2,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f821,plain,
c_HOL_Otimes__class_Otimes(sF2,v_n,tc_nat) = sF3,
inference(reorient_equations,[],[f820]) ).
fof(f822,plain,
c_HOL_Oord__class_Oless(v_x,sF3,tc_nat),
inference(definition_folding,[],[f739,f821,f819,f817,f815]) ).
fof(f823,definition,
! [X0] : sF4(X0) = c_HOL_Otimes__class_Otimes(sF2,X0,tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f824,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,X0,tc_nat) = sF4(X0),
inference(reorient_equations,[],[f823]) ).
fof(f825,definition,
! [X0] : sF5(X0) = c_Suc(sF4(X0)),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f826,plain,
! [X0] : c_Suc(sF4(X0)) = sF5(X0),
inference(reorient_equations,[],[f825]) ).
fof(f827,plain,
! [X0] :
( v_x != sF5(X0)
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(definition_folding,[],[f741,f826,f824,f819,f817,f815]) ).
fof(f828,plain,
! [X0] :
( v_x != sF4(X0)
| ~ c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(definition_folding,[],[f743,f824,f819,f817,f815]) ).
fof(f920,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(sF2,X0,tc_nat),sF3,tc_nat)
| c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(superposition,[],[f702,f821]) ).
fof(f924,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF4(X0),sF3,tc_nat)
| c_HOL_Oord__class_Oless(X0,v_n,tc_nat) ),
inference(forward_demodulation,[],[f920,f824]) ).
fof(f935,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_nat) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_nat),X0,tc_nat),
inference(superposition,[],[f644,f815]) ).
fof(f956,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_nat) = c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(sF1,tc_nat),X0,tc_nat),
inference(forward_demodulation,[],[f935,f817]) ).
fof(f957,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_nat) = c_HOL_Otimes__class_Otimes(sF2,X0,tc_nat),
inference(forward_demodulation,[],[f956,f819]) ).
fof(f958,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,X0,tc_nat) = sF4(X0),
inference(forward_demodulation,[],[f957,f824]) ).
fof(f962,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat) = sF4(X0),
inference(superposition,[],[f644,f958]) ).
fof(f963,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat) = sF4(X0),
inference(forward_demodulation,[],[f962,f638]) ).
fof(f1341,plain,
! [X0] :
( c_Suc(c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat)) = X0
| c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat) = X0 ),
inference(resolution,[],[f538,f262]) ).
fof(f1342,plain,
! [X0] :
( c_Suc(sF4(c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat))) = X0
| c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat) = X0 ),
inference(forward_demodulation,[],[f1341,f963]) ).
fof(f1343,plain,
! [X0] :
( sF5(c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)) = X0
| c_HOL_Otimes__class_Otimes(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat),tc_nat) = X0 ),
inference(forward_demodulation,[],[f1342,f826]) ).
fof(f1344,plain,
! [X0] :
( sF5(c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)) = X0
| sF4(c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)) = X0 ),
inference(forward_demodulation,[],[f1343,f963]) ).
fof(f1346,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(resolution,[],[f695,f679]) ).
fof(f1928,plain,
~ c_HOL_Oord__class_Oless(sF3,v_x,tc_nat),
inference(resolution,[],[f1346,f822]) ).
fof(f6871,plain,
c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF0),tc_nat),
inference(superposition,[],[f638,f815]) ).
fof(f6876,plain,
c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Int_Onumber__class_Onumber__of(sF1,tc_nat),
inference(forward_demodulation,[],[f6871,f817]) ).
fof(f6877,plain,
c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = sF2,
inference(forward_demodulation,[],[f6876,f819]) ).
fof(f6883,plain,
! [X0] :
( sF5(c_Divides_Odiv__class_Odiv(X0,sF2,tc_nat)) = X0
| sF4(c_Divides_Odiv__class_Odiv(X0,sF2,tc_nat)) = X0 ),
inference(superposition,[],[f1344,f6877]) ).
fof(f6961,plain,
! [X0] :
( v_x != X0
| ~ c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Odiv(X0,sF2,tc_nat),v_n,tc_nat)
| sF4(c_Divides_Odiv__class_Odiv(X0,sF2,tc_nat)) = X0 ),
inference(superposition,[],[f827,f6883]) ).
fof(f7094,plain,
( ~ c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat)
| v_x = sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)) ),
inference(equality_resolution,[],[f6961]) ).
fof(f7095,plain,
~ c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat),
inference(forward_subsumption_resolution,[],[f7094,f828]) ).
fof(f7097,plain,
c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat) = c_HOL_Oplus__class_Oplus(v_n,c_HOL_Ominus__class_Ominus(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat),tc_nat),
inference(resolution,[],[f7095,f613]) ).
fof(f18042,definition,
( spl6_291
<=> v_x = sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)) ),
introduced(definition,[new_symbols(definition,[spl6_291])],[avatar_definition]) ).
fof(f18043,plain,
( v_x != sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat))
| spl6_291 ),
inference(avatar_component_clause,[],[f18042]) ).
fof(f18044,plain,
( v_x = sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat))
| ~ spl6_291 ),
inference(avatar_component_clause,[],[f18042]) ).
fof(f18275,plain,
( ~ c_HOL_Oord__class_Oless(v_x,sF3,tc_nat)
| c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat)
| ~ spl6_291 ),
inference(superposition,[],[f924,f18044]) ).
fof(f18389,plain,
( c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat)
| ~ spl6_291 ),
inference(forward_subsumption_resolution,[],[f18275,f822]) ).
fof(f18398,plain,
( $false
| ~ spl6_291 ),
inference(forward_subsumption_resolution,[],[f18389,f7095]) ).
fof(f18399,plain,
~ spl6_291,
inference(avatar_contradiction_clause,[],[f18398]) ).
fof(f20068,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(v_n,X0,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(sF3,c_HOL_Otimes__class_Otimes(sF2,X0,tc_nat),tc_nat),
inference(superposition,[],[f189,f821]) ).
fof(f20153,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF2,c_HOL_Oplus__class_Oplus(v_n,X0,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(sF3,sF4(X0),tc_nat),
inference(forward_demodulation,[],[f20068,f824]) ).
fof(f20182,plain,
! [X0] : c_HOL_Oplus__class_Oplus(sF3,sF4(X0),tc_nat) = sF4(c_HOL_Oplus__class_Oplus(v_n,X0,tc_nat)),
inference(forward_demodulation,[],[f20153,f824]) ).
fof(f20788,plain,
sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)) = c_HOL_Oplus__class_Oplus(sF3,sF4(c_HOL_Ominus__class_Ominus(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat),v_n,tc_nat)),tc_nat),
inference(superposition,[],[f20182,f7097]) ).
fof(f20967,plain,
c_HOL_Oord__class_Oless(sF3,c_Suc(sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat))),tc_nat),
inference(superposition,[],[f441,f20788]) ).
fof(f21012,plain,
c_HOL_Oord__class_Oless(sF3,sF5(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)),tc_nat),
inference(forward_demodulation,[],[f20967,f826]) ).
fof(f21028,plain,
( c_HOL_Oord__class_Oless(sF3,v_x,tc_nat)
| v_x = sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)) ),
inference(superposition,[],[f21012,f6883]) ).
fof(f21029,plain,
v_x = sF4(c_Divides_Odiv__class_Odiv(v_x,sF2,tc_nat)),
inference(forward_subsumption_resolution,[],[f21028,f1928]) ).
fof(f21030,plain,
( $false
| spl6_291 ),
inference(forward_subsumption_resolution,[],[f21029,f18043]) ).
fof(f21031,plain,
spl6_291,
inference(avatar_contradiction_clause,[],[f21030]) ).
cnf(s400,plain,
~ spl6_291,
inference(sat_conversion,[],[f18399]) ).
cnf(s444,plain,
spl6_291,
inference(sat_conversion,[],[f21031]) ).
cnf(s445,plain,
$false,
inference(rat,[],[s400,s444]) ).
fof(f21032,plain,
$false,
inference(avatar_sat_refutation,[],[s445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV585-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 % Computer : n008.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Mon Sep 28 11:57:24 UTC 2026
% 0.08/0.24 % CPUTime :
% 0.08/0.24 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.29 Running first-order theorem proving
% 0.24/0.29 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.58/3.35 % (2200115)Input is clausal, will run a generic CNF schedule.
% 18.58/3.35 % (2200122)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=3363759427:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.58/3.35 % (2200128)dis-21_1_sil=8000:lcm=predicate:random_seed=163920050: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)
% 18.58/3.35 % (2200125)lrs+10_1_sil=8000:sp=occurrence:random_seed=2053001303:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.58/3.35 % (2200124)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3971121007:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.58/3.35 % (2200126)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1584978298:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.58/3.35 % (2200123)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4188859788:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.58/3.35 % (2200128)Instruction limit reached!
% 18.58/3.35 % (2200128)------------------------------
% 18.58/3.35 % (2200128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200128)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200128)Termination reason: Instruction limit
% 18.58/3.35 % (2200128)Termination phase: Saturation
% 18.58/3.35 % (2200128)Time elapsed: 0.090 s
% 18.58/3.35 % (2200128)Peak memory usage: 89 MB
% 18.58/3.35 % (2200128)Instructions burned: 117 (million)
% 18.58/3.35 % (2200127)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1718272775:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.58/3.35 % (2200125)Instruction limit reached!
% 18.58/3.35 % (2200125)------------------------------
% 18.58/3.35 % (2200125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200125)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200125)Termination reason: Instruction limit
% 18.58/3.35 % (2200125)Termination phase: Saturation
% 18.58/3.35 % (2200125)Time elapsed: 0.113 s
% 18.58/3.35 % (2200125)Peak memory usage: 89 MB
% 18.58/3.35 % (2200125)Instructions burned: 108 (million)
% 18.58/3.35 % (2200126)Instruction limit reached!
% 18.58/3.35 % (2200126)------------------------------
% 18.58/3.35 % (2200126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200126)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200126)Termination reason: Instruction limit
% 18.58/3.35 % (2200126)Termination phase: Saturation
% 18.58/3.35 % (2200126)Time elapsed: 0.117 s
% 18.58/3.35 % (2200126)Peak memory usage: 89 MB
% 18.58/3.35 % (2200126)Instructions burned: 114 (million)
% 18.58/3.35 % (2200127)Instruction limit reached!
% 18.58/3.35 % (2200127)------------------------------
% 18.58/3.35 % (2200127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200127)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200127)Termination reason: Instruction limit
% 18.58/3.35 % (2200127)Termination phase: Saturation
% 18.58/3.35 % (2200127)Time elapsed: 0.189 s
% 18.58/3.35 % (2200127)Peak memory usage: 90 MB
% 18.58/3.35 % (2200127)Instructions burned: 180 (million)
% 18.58/3.35 % (2200136)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=803390865:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.58/3.35 % (2200138)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3281964476:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 18.58/3.35 % (2200137)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3701003883:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 18.58/3.35 % (2200136)Instruction limit reached!
% 18.58/3.35 % (2200136)------------------------------
% 18.58/3.35 % (2200136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200136)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200136)Termination reason: Instruction limit
% 18.58/3.35 % (2200136)Termination phase: Saturation
% 18.58/3.35 % (2200136)Time elapsed: 0.132 s
% 18.58/3.35 % (2200136)Peak memory usage: 89 MB
% 18.58/3.35 % (2200136)Instructions burned: 143 (million)
% 18.58/3.35 % (2200139)lrs+10_64_to=lpo:sil=8000:random_seed=2173738785:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 18.58/3.35 % (2200137)Instruction limit reached!
% 18.58/3.35 % (2200137)------------------------------
% 18.58/3.35 % (2200137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200137)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200137)Termination reason: Instruction limit
% 18.58/3.35 % (2200137)Termination phase: Saturation
% 18.58/3.35 % (2200137)Time elapsed: 0.162 s
% 18.58/3.35 % (2200137)Peak memory usage: 90 MB
% 18.58/3.35 % (2200137)Instructions burned: 190 (million)
% 18.58/3.35 % (2200138)Instruction limit reached!
% 18.58/3.35 % (2200138)------------------------------
% 18.58/3.35 % (2200138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200138)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200138)Termination reason: Instruction limit
% 18.58/3.35 % (2200138)Termination phase: Saturation
% 18.58/3.35 % (2200138)Time elapsed: 0.202 s
% 18.58/3.35 % (2200138)Peak memory usage: 90 MB
% 18.58/3.35 % (2200138)Instructions burned: 220 (million)
% 18.58/3.35 % (2200139)Instruction limit reached!
% 18.58/3.35 % (2200139)------------------------------
% 18.58/3.35 % (2200139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200139)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200139)Termination reason: Instruction limit
% 18.58/3.35 % (2200139)Termination phase: Saturation
% 18.58/3.35 % (2200139)Time elapsed: 0.112 s
% 18.58/3.35 % (2200139)Peak memory usage: 89 MB
% 18.58/3.35 % (2200139)Instructions burned: 126 (million)
% 18.58/3.35 % (2200143)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1675703404:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 18.58/3.35 % (2200145)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=819052806:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 18.58/3.35 % (2200146)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2086330180:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 18.58/3.35 % (2200147)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=4196436309:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 18.58/3.35 % (2200143)Instruction limit reached!
% 18.58/3.35 % (2200143)------------------------------
% 18.58/3.35 % (2200143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200143)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200143)Termination reason: Instruction limit
% 18.58/3.35 % (2200143)Termination phase: Saturation
% 18.58/3.35 % (2200143)Time elapsed: 0.196 s
% 18.58/3.35 % (2200143)Peak memory usage: 90 MB
% 18.58/3.35 % (2200143)Instructions burned: 194 (million)
% 18.58/3.35 % (2200147)Instruction limit reached!
% 18.58/3.35 % (2200147)------------------------------
% 18.58/3.35 % (2200147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200147)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200147)Termination reason: Instruction limit
% 18.58/3.35 % (2200147)Termination phase: Saturation
% 18.58/3.35 % (2200147)Time elapsed: 0.098 s
% 18.58/3.35 % (2200147)Peak memory usage: 89 MB
% 18.58/3.35 % (2200147)Instructions burned: 106 (million)
% 18.58/3.35 % (2200145)Instruction limit reached!
% 18.58/3.35 % (2200145)------------------------------
% 18.58/3.35 % (2200145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200145)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200145)Termination reason: Instruction limit
% 18.58/3.35 % (2200145)Termination phase: Saturation
% 18.58/3.35 % (2200145)Time elapsed: 0.162 s
% 18.58/3.35 % (2200145)Peak memory usage: 90 MB
% 18.58/3.35 % (2200145)Instructions burned: 157 (million)
% 18.58/3.35 % (2200152)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3062385899:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 18.58/3.35 % (2200153)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=746887235:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 18.58/3.35 % (2200154)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1168917610:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 18.58/3.35 % (2200152)Instruction limit reached!
% 18.58/3.35 % (2200152)------------------------------
% 18.58/3.35 % (2200152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200152)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200152)Termination reason: Instruction limit
% 18.58/3.35 % (2200152)Termination phase: Saturation
% 18.58/3.35 % (2200152)Time elapsed: 0.108 s
% 18.58/3.35 % (2200152)Peak memory usage: 90 MB
% 18.58/3.35 % (2200152)Instructions burned: 108 (million)
% 18.58/3.35 % (2200153)Instruction limit reached!
% 18.58/3.35 % (2200153)------------------------------
% 18.58/3.35 % (2200153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200153)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200153)Termination reason: Instruction limit
% 18.58/3.35 % (2200153)Termination phase: Saturation
% 18.58/3.35 % (2200153)Time elapsed: 0.237 s
% 18.58/3.35 % (2200153)Peak memory usage: 89 MB
% 18.58/3.35 % (2200153)Instructions burned: 242 (million)
% 18.58/3.35 % (2200158)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=388615432:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 18.58/3.35 % (2200158)Instruction limit reached!
% 18.58/3.35 % (2200158)------------------------------
% 18.58/3.35 % (2200158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200158)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200158)Termination reason: Instruction limit
% 18.58/3.35 % (2200158)Termination phase: Saturation
% 18.58/3.35 % (2200158)Time elapsed: 0.138 s
% 18.58/3.35 % (2200158)Peak memory usage: 90 MB
% 18.58/3.35 % (2200158)Instructions burned: 135 (million)
% 18.58/3.35 % (2200159)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3818405548:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 18.58/3.35 % (2200161)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4201296602:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 18.58/3.35 % (2200122)First to succeed.
% 18.58/3.35 % (2200122)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2200115"
% 18.58/3.35 % (2200161)Instruction limit reached!
% 18.58/3.35 % (2200161)------------------------------
% 18.58/3.35 % (2200161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200161)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200161)Termination reason: Instruction limit
% 18.58/3.35 % (2200161)Termination phase: Saturation
% 18.58/3.35 % (2200161)Time elapsed: 0.203 s
% 18.58/3.35 % (2200161)Peak memory usage: 90 MB
% 18.58/3.35 % (2200161)Instructions burned: 191 (million)
% 18.58/3.35 % (2200159)Instruction limit reached!
% 18.58/3.35 % (2200159)------------------------------
% 18.58/3.35 % (2200159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.58/3.35 % (2200159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.58/3.35 % (2200159)CaDiCaL version: 2.1.3
% 18.58/3.35 % (2200159)Termination reason: Instruction limit
% 18.58/3.35 % (2200159)Termination phase: Saturation
% 18.58/3.35 % (2200159)Time elapsed: 0.484 s
% 18.58/3.35 % (2200159)Peak memory usage: 93 MB
% 18.58/3.35 % (2200159)Instructions burned: 499 (million)
% 18.58/3.35 % (2200122)Refutation found. Thanks to Tanya!
% 18.58/3.35 % SZS status Unsatisfiable for theBenchmark
% 18.58/3.35 % SZS output start Proof for theBenchmark
% See solution above
% 19.25/3.57 % (2200122)------------------------------
% 19.25/3.57 % (2200122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.25/3.57 % (2200122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.25/3.57 % (2200122)CaDiCaL version: 2.1.3
% 19.25/3.57 % (2200122)Termination reason: Refutation
% 19.25/3.57 % (2200122)Time elapsed: 2.177 s
% 19.25/3.57 % (2200122)Peak memory usage: 156 MB
% 19.25/3.57 % (2200122)Instructions burned: 3799 (million)
% 19.25/3.57 % (2200122)------------------------------
% 19.25/3.57 % (2200122)------------------------------
% 19.25/3.57 % (2200115)Success in time 2.651 s
% 19.25/3.57 % Vampire exiting
%------------------------------------------------------------------------------