%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG413-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 09:19:58 AM UTC 2026
% Result : Unsatisfiable 11.56s 2.38s
% Output : Refutation 12.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of formulae : 55 ( 34 unt; 7 def)
% Number of atoms : 76 ( 45 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 45 ( 24 ~; 19 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 30 ( 0 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f581,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Oadd__c_0) ).
fof(f662,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Oab__group__add(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X1,X0),c_HOL_Oplus__class_Oplus(X2,X1,X0),X0) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__cancel__end_1) ).
fof(f726,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(X0),X1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I5_J_0) ).
fof(f988,axiom,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X0)
| c_RealVector_Onorm__class_Onorm(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) = c_RealVector_Onorm__class_Onorm(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_norm__minus__cancel_0) ).
fof(f989,plain,
! [X0,X1] :
( ~ class_RealVector_Oreal__normed__vector(X0)
| c_RealVector_Onorm__class_Onorm(X1,X0) = c_RealVector_Onorm__class_Onorm(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) ),
inference(reorient_equations,[],[f988]) ).
fof(f993,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X0)
| c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_poly__pCons_0) ).
fof(f1020,axiom,
! [X0] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pCons_Oprems_0) ).
fof(f1021,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(reorient_equations,[],[f1020]) ).
fof(f1024,axiom,
c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cx_I1_J_0) ).
fof(f1025,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),
inference(reorient_equations,[],[f1024]) ).
fof(f1045,negated_conjecture,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_ds____,c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1046,plain,
c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_ds____,c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(reorient_equations,[],[f1045]) ).
fof(f1161,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1162,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
fof(f1165,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1175,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add) ).
fof(f1249,definition,
sF0 = c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1250,plain,
c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1249]) ).
fof(f1251,definition,
sF1 = c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1252,plain,
c_RealVector_Oof__real(v_x____,tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1251]) ).
fof(f1253,definition,
sF2 = c_Polynomial_Opoly(v_ds____,sF1,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1254,plain,
c_Polynomial_Opoly(v_ds____,sF1,tc_Complex_Ocomplex) = sF2,
inference(reorient_equations,[],[f1253]) ).
fof(f1255,definition,
sF3 = c_HOL_Otimes__class_Otimes(sF1,sF2,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1256,plain,
c_HOL_Otimes__class_Otimes(sF1,sF2,tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1255]) ).
fof(f1257,definition,
sF4 = c_RealVector_Onorm__class_Onorm(sF3,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1258,plain,
c_RealVector_Onorm__class_Onorm(sF3,tc_Complex_Ocomplex) = sF4,
inference(reorient_equations,[],[f1257]) ).
fof(f1259,plain,
sF0 != sF4,
inference(definition_folding,[],[f1046,f1258,f1256,f1254,f1252,f1252,f1250]) ).
fof(f1312,plain,
! [X2,X0,X1] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f993,f1162]) ).
fof(f1313,plain,
! [X0] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_ds____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(sF1,sF2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(superposition,[],[f1312,f1254]) ).
fof(f1319,plain,
! [X0] : c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_ds____,tc_Complex_Ocomplex),sF1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X0,sF3,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1313,f1256]) ).
fof(f1321,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(v_d____,sF3,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
inference(superposition,[],[f1319,f1021]) ).
fof(f1327,definition,
( spl5_5
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
fof(f1331,definition,
( spl5_6
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(v_d____,sF3,tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).
fof(f1333,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(v_d____,sF3,tc_Complex_Ocomplex)
| ~ spl5_6 ),
inference(avatar_component_clause,[],[f1331]) ).
fof(f1336,plain,
( spl5_5
| spl5_6 ),
inference(avatar_split_clause,[],[f1321,f1331,f1327]) ).
fof(f1851,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF1,
inference(superposition,[],[f1025,f1252]) ).
fof(f1852,plain,
~ spl5_5,
inference(avatar_split_clause,[],[f1851,f1327]) ).
fof(f2056,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,X1,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[],[f581,f1161]) ).
fof(f2064,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(sF3,v_d____,tc_Complex_Ocomplex)
| ~ spl5_6 ),
inference(superposition,[],[f1333,f2056]) ).
fof(f2151,plain,
! [X0] : c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0,
inference(resolution,[],[f726,f1161]) ).
fof(f2294,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X0,
inference(superposition,[],[f2056,f2151]) ).
fof(f5550,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(X0,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f989,f1165]) ).
fof(f8181,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(X0,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(resolution,[],[f662,f1175]) ).
fof(f8193,plain,
( sF3 = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(v_d____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)
| ~ spl5_6 ),
inference(superposition,[],[f8181,f2064]) ).
fof(f8196,plain,
( sF3 = c_HOL_Ouminus__class_Ouminus(v_d____,tc_Complex_Ocomplex)
| ~ spl5_6 ),
inference(forward_demodulation,[],[f8193,f2294]) ).
fof(f8207,plain,
( c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex) = c_RealVector_Onorm__class_Onorm(sF3,tc_Complex_Ocomplex)
| ~ spl5_6 ),
inference(superposition,[],[f5550,f8196]) ).
fof(f8208,plain,
( c_RealVector_Onorm__class_Onorm(v_d____,tc_Complex_Ocomplex) = sF4
| ~ spl5_6 ),
inference(forward_demodulation,[],[f8207,f1258]) ).
fof(f8210,plain,
( sF0 = sF4
| ~ spl5_6 ),
inference(forward_demodulation,[],[f8208,f1250]) ).
fof(f8212,plain,
( $false
| ~ spl5_6 ),
inference(forward_subsumption_resolution,[],[f8210,f1259]) ).
fof(f8213,plain,
~ spl5_6,
inference(avatar_contradiction_clause,[],[f8212]) ).
cnf(s7,plain,
( spl5_5
| spl5_6 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s13,plain,
~ spl5_5,
inference(sat_conversion,[],[f1852]) ).
cnf(s48,plain,
~ spl5_6,
inference(sat_conversion,[],[f8213]) ).
cnf(s54,plain,
$false,
inference(rat,[],[s7,s48,s13]) ).
fof(f8214,plain,
$false,
inference(avatar_sat_refutation,[],[s54]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG413-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.19 % Computer : n002.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 20:22:22 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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.55/2.19 % (704069)Input is clausal, will run a generic CNF schedule.
% 10.55/2.19 % (704080)dis-21_1_sil=8000:lcm=predicate:random_seed=1941443315: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.55/2.19 % (704080)Instruction limit reached!
% 10.55/2.19 % (704080)------------------------------
% 10.55/2.19 % (704080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.19 % (704080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.19 % (704080)CaDiCaL version: 2.1.3
% 10.55/2.19 % (704080)Termination reason: Instruction limit
% 10.55/2.19 % (704080)Termination phase: Saturation
% 10.55/2.19 % (704080)Time elapsed: 0.034 s
% 10.55/2.19 % (704080)Peak memory usage: 89 MB
% 10.55/2.19 % (704080)Instructions burned: 117 (million)
% 10.55/2.19 % (704075)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3976711239:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.55/2.19 % (704074)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=1214831800:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.55/2.19 % (704077)lrs+10_1_sil=8000:sp=occurrence:random_seed=3043165443:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.55/2.19 % (704076)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3858705168:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.55/2.19 % (704079)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2198836664:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.55/2.19 % (704078)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3606295793:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.55/2.19 % (704078)Instruction limit reached!
% 10.55/2.19 % (704078)------------------------------
% 10.55/2.19 % (704078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.19 % (704078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.19 % (704078)CaDiCaL version: 2.1.3
% 10.55/2.19 % (704078)Termination reason: Instruction limit
% 10.55/2.19 % (704078)Termination phase: Saturation
% 10.55/2.19 % (704078)Time elapsed: 0.072 s
% 10.55/2.19 % (704078)Peak memory usage: 89 MB
% 10.55/2.19 % (704078)Instructions burned: 115 (million)
% 10.55/2.19 % (704077)Instruction limit reached!
% 10.55/2.19 % (704077)------------------------------
% 10.55/2.19 % (704077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.19 % (704077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.19 % (704077)CaDiCaL version: 2.1.3
% 10.55/2.19 % (704077)Termination reason: Instruction limit
% 10.55/2.19 % (704077)Termination phase: Saturation
% 10.55/2.19 % (704077)Time elapsed: 0.075 s
% 10.55/2.19 % (704077)Peak memory usage: 90 MB
% 10.55/2.19 % (704077)Instructions burned: 107 (million)
% 10.55/2.19 % (704082)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=1922916343:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 10.55/2.19 % (704082)Refutation not found, incomplete strategy
% 10.55/2.19 % (704082)------------------------------
% 10.55/2.19 % (704082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.19 % (704082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.19 % (704082)CaDiCaL version: 2.1.3
% 10.55/2.19 % (704082)Termination reason: Refutation not found, incomplete strategy
% 10.55/2.19 % (704082)Time elapsed: 0.005 s
% 10.55/2.19 % (704082)Peak memory usage: 88 MB
% 10.55/2.19 % (704082)Instructions burned: 15 (million)
% 10.55/2.19 % (704079)Instruction limit reached!
% 10.55/2.19 % (704079)------------------------------
% 10.55/2.19 % (704079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.55/2.19 % (704079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.55/2.19 % (704079)CaDiCaL version: 2.1.3
% 10.55/2.19 % (704079)Termination reason: Instruction limit
% 10.55/2.19 % (704079)Termination phase: Saturation
% 10.55/2.19 % (704079)Time elapsed: 0.129 s
% 10.55/2.19 % (704079)Peak memory usage: 91 MB
% 10.55/2.19 % (704079)Instructions burned: 185 (million)
% 10.55/2.19 % (704089)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3805897436:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 11.56/2.38 % (704090)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=248528512:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.56/2.38 % (704082)------------------------------
% 11.56/2.38 % (704082)------------------------------
% 11.56/2.38 % (704092)lrs+10_64_to=lpo:sil=8000:random_seed=2756471091:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 11.56/2.38 % (704089)Instruction limit reached!
% 11.56/2.38 % (704089)------------------------------
% 11.56/2.38 % (704089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704089)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704089)Termination reason: Instruction limit
% 11.56/2.38 % (704089)Termination phase: Saturation
% 11.56/2.38 % (704089)Time elapsed: 0.106 s
% 11.56/2.38 % (704089)Peak memory usage: 91 MB
% 11.56/2.38 % (704089)Instructions burned: 190 (million)
% 11.56/2.38 % (704090)Instruction limit reached!
% 11.56/2.38 % (704090)------------------------------
% 11.56/2.38 % (704090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704090)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704090)Termination reason: Instruction limit
% 11.56/2.38 % (704090)Termination phase: Saturation
% 11.56/2.38 % (704090)Time elapsed: 0.123 s
% 11.56/2.38 % (704090)Peak memory usage: 91 MB
% 11.56/2.38 % (704090)Instructions burned: 221 (million)
% 11.56/2.38 % (704092)Instruction limit reached!
% 11.56/2.38 % (704092)------------------------------
% 11.56/2.38 % (704092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704092)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704092)Termination reason: Instruction limit
% 11.56/2.38 % (704092)Termination phase: Saturation
% 11.56/2.38 % (704092)Time elapsed: 0.080 s
% 11.56/2.38 % (704092)Peak memory usage: 90 MB
% 11.56/2.38 % (704092)Instructions burned: 126 (million)
% 11.56/2.38 % (704095)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3220778667:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.56/2.38 % (704095)Instruction limit reached!
% 11.56/2.38 % (704095)------------------------------
% 11.56/2.38 % (704095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704095)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704095)Termination reason: Instruction limit
% 11.56/2.38 % (704095)Termination phase: Saturation
% 11.56/2.38 % (704095)Time elapsed: 0.073 s
% 11.56/2.38 % (704095)Peak memory usage: 91 MB
% 11.56/2.38 % (704095)Instructions burned: 197 (million)
% 11.56/2.38 % (704097)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2244650794:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 11.56/2.38 % (704098)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=955584072:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 11.56/2.38 % (704099)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=4066003544:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 11.56/2.38 % (704097)Instruction limit reached!
% 11.56/2.38 % (704097)------------------------------
% 11.56/2.38 % (704097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704097)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704097)Termination reason: Instruction limit
% 11.56/2.38 % (704097)Termination phase: Saturation
% 11.56/2.38 % (704097)Time elapsed: 0.094 s
% 11.56/2.38 % (704097)Peak memory usage: 91 MB
% 11.56/2.38 % (704097)Instructions burned: 157 (million)
% 11.56/2.38 % (704101)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4038023658:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 11.56/2.38 % (704099)Instruction limit reached!
% 11.56/2.38 % (704099)------------------------------
% 11.56/2.38 % (704099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704099)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704099)Termination reason: Instruction limit
% 11.56/2.38 % (704099)Termination phase: Saturation
% 11.56/2.38 % (704099)Time elapsed: 0.065 s
% 11.56/2.38 % (704099)Peak memory usage: 90 MB
% 11.56/2.38 % (704099)Instructions burned: 106 (million)
% 11.56/2.38 % (704101)Refutation not found, incomplete strategy
% 11.56/2.38 % (704101)------------------------------
% 11.56/2.38 % (704101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704101)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704101)Termination reason: Refutation not found, incomplete strategy
% 11.56/2.38 % (704101)Time elapsed: 0.011 s
% 11.56/2.38 % (704101)Peak memory usage: 89 MB
% 11.56/2.38 % (704101)Instructions burned: 35 (million)
% 11.56/2.38 % (704101)------------------------------
% 11.56/2.38 % (704101)------------------------------
% 11.56/2.38 % (704106)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=489030436:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 11.56/2.38 % (704107)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4233384913:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 11.56/2.38 % (704110)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=909973775:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 11.56/2.38 % (704106)Instruction limit reached!
% 11.56/2.38 % (704106)------------------------------
% 11.56/2.38 % (704106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704106)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704106)Termination reason: Instruction limit
% 11.56/2.38 % (704106)Termination phase: Saturation
% 11.56/2.38 % (704106)Time elapsed: 0.152 s
% 11.56/2.38 % (704106)Peak memory usage: 90 MB
% 11.56/2.38 % (704106)Instructions burned: 243 (million)
% 11.56/2.38 % (704110)Instruction limit reached!
% 11.56/2.38 % (704110)------------------------------
% 11.56/2.38 % (704110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704110)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704110)Termination reason: Instruction limit
% 11.56/2.38 % (704110)Termination phase: Saturation
% 11.56/2.38 % (704110)Time elapsed: 0.041 s
% 11.56/2.38 % (704110)Peak memory usage: 90 MB
% 11.56/2.38 % (704110)Instructions burned: 136 (million)
% 11.56/2.38 % (704113)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2360662535:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 11.56/2.38 % (704112)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=215707631:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 11.56/2.38 % (704113)Instruction limit reached!
% 11.56/2.38 % (704113)------------------------------
% 11.56/2.38 % (704113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704113)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704113)Termination reason: Instruction limit
% 11.56/2.38 % (704113)Termination phase: Saturation
% 11.56/2.38 % (704113)Time elapsed: 0.069 s
% 11.56/2.38 % (704113)Peak memory usage: 92 MB
% 11.56/2.38 % (704113)Instructions burned: 192 (million)
% 11.56/2.38 % (704116)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1527253130:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 11.56/2.38 % (704074)First to succeed.
% 11.56/2.38 % (704074)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-704069"
% 11.56/2.38 % (704116)Instruction limit reached!
% 11.56/2.38 % (704116)------------------------------
% 11.56/2.38 % (704116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704116)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704116)Termination reason: Instruction limit
% 11.56/2.38 % (704116)Termination phase: Saturation
% 11.56/2.38 % (704116)Time elapsed: 0.088 s
% 11.56/2.38 % (704116)Peak memory usage: 93 MB
% 11.56/2.38 % (704116)Instructions burned: 265 (million)
% 11.56/2.38 % (704112)Instruction limit reached!
% 11.56/2.38 % (704112)------------------------------
% 11.56/2.38 % (704112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704112)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704112)Termination reason: Instruction limit
% 11.56/2.38 % (704112)Termination phase: Saturation
% 11.56/2.38 % (704112)Time elapsed: 0.285 s
% 11.56/2.38 % (704112)Peak memory usage: 93 MB
% 11.56/2.38 % (704112)Instructions burned: 499 (million)
% 11.56/2.38 % (704118)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=768173876:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 11.56/2.38 % (704119)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=2802638575:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 11.56/2.38 % (704118)Instruction limit reached!
% 11.56/2.38 % (704118)------------------------------
% 11.56/2.38 % (704118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.56/2.38 % (704118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.56/2.38 % (704118)CaDiCaL version: 2.1.3
% 11.56/2.38 % (704118)Termination reason: Instruction limit
% 11.56/2.38 % (704118)Termination phase: Saturation
% 11.56/2.38 % (704118)Time elapsed: 0.053 s
% 11.56/2.38 % (704118)Peak memory usage: 91 MB
% 11.56/2.38 % (704118)Instructions burned: 157 (million)
% 11.56/2.38 % (704074)Refutation found. Thanks to Tanya!
% 11.56/2.38 % SZS status Unsatisfiable for theBenchmark
% 11.56/2.38 % SZS output start Proof for theBenchmark
% See solution above
% 12.40/2.48 % (704074)------------------------------
% 12.40/2.48 % (704074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.40/2.48 % (704074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.40/2.48 % (704074)CaDiCaL version: 2.1.3
% 12.40/2.48 % (704074)Termination reason: Refutation
% 12.40/2.48 % (704074)Time elapsed: 1.237 s
% 12.40/2.48 % (704074)Peak memory usage: 139 MB
% 12.40/2.48 % (704074)Instructions burned: 1926 (million)
% 12.40/2.48 % (704074)------------------------------
% 12.40/2.48 % (704074)------------------------------
% 12.40/2.48 % (704069)Success in time 1.715 s
% 12.40/2.48 % Vampire exiting
%------------------------------------------------------------------------------