%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG419-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 : n004.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:59 AM UTC 2026
% Result : Unsatisfiable 11.03s 2.26s
% Output : Refutation 11.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 30
% Syntax : Number of formulae : 106 ( 57 unt; 14 def)
% Number of atoms : 181 ( 102 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 118 ( 43 ~; 73 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 17 con; 0-3 aty)
% Number of variables : 55 ( 0 sgn 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f82,axiom,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,X1,tc_nat) = c_HOL_Oplus__class_Oplus(X1,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__add__commute_0) ).
fof(f681,axiom,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__add__left__cancel__less_1) ).
fof(f684,axiom,
! [X0,X1] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f685,axiom,
! [X0,X1] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f756,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(X0)),X0) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X1,X0),c_Polynomial_Odegree(X2,X0),tc_nat)
| X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_degree__mult__eq_0) ).
fof(f757,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Oidom(X0)
| c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X1,X0),c_Polynomial_Odegree(X2,X0),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X1,X2,tc_Polynomial_Opoly(X0)),X0)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = X2
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)) = X1 ),
inference(reorient_equations,[],[f756]) ).
fof(f804,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X1,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0),X0),X2,tc_Polynomial_Opoly(X0)),X0) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_degree__linear__power_0) ).
fof(f859,axiom,
c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_oa_0) ).
fof(f860,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),
inference(reorient_equations,[],[f859]) ).
fof(f862,axiom,
v_s____ != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sne_0) ).
fof(f863,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_s____,
inference(reorient_equations,[],[f862]) ).
fof(f865,axiom,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr0I_0) ).
fof(f866,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(reorient_equations,[],[f865]) ).
fof(f942,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Olinorder(X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| c_HOL_Oord__class_Oless(X2,X1,X0)
| X2 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neqE_0) ).
fof(f943,plain,
! [X2,X0,X1] :
( c_HOL_Oord__class_Oless(X2,X1,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0)
| X1 = X2 ),
inference(reorient_equations,[],[f942]) ).
fof(f995,axiom,
! [X0] :
( ~ class_HOL_Ozero(X0)
| c_Polynomial_Odegree(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_degree__0_0) ).
fof(f996,plain,
! [X0] :
( ~ class_HOL_Ozero(X0)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0) ),
inference(reorient_equations,[],[f995]) ).
fof(f1024,negated_conjecture,
~ c_HOL_Oord__class_Oless(c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(c_Polynomial_OpCons(c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1065,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Orderings_Olinorder) ).
fof(f1133,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(f1155,axiom,
class_Ring__and__Field_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Oidom) ).
fof(f1162,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__HOL_Ozero) ).
fof(f1218,definition,
sF0 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1219,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF0,
inference(reorient_equations,[],[f1218]) ).
fof(f1220,definition,
sF1 = c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1221,plain,
c_Polynomial_Odegree(v_s____,tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1220]) ).
fof(f1223,definition,
sF2 = c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1224,plain,
c_Polynomial_Oorder(v_a____,v_pa____,tc_Complex_Ocomplex) = sF2,
inference(reorient_equations,[],[f1223]) ).
fof(f1226,definition,
sF3 = c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1227,plain,
c_HOL_Ouminus__class_Ouminus(v_a____,tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1226]) ).
fof(f1228,definition,
sF4 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1229,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF4,
inference(reorient_equations,[],[f1228]) ).
fof(f1230,definition,
sF5 = tc_Polynomial_Opoly(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1231,plain,
tc_Polynomial_Opoly(tc_Complex_Ocomplex) = sF5,
inference(reorient_equations,[],[f1230]) ).
fof(f1232,definition,
sF6 = c_HOL_Ozero__class_Ozero(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1233,plain,
c_HOL_Ozero__class_Ozero(sF5) = sF6,
inference(reorient_equations,[],[f1232]) ).
fof(f1234,definition,
sF7 = c_Polynomial_OpCons(sF4,sF6,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1235,plain,
c_Polynomial_OpCons(sF4,sF6,tc_Complex_Ocomplex) = sF7,
inference(reorient_equations,[],[f1234]) ).
fof(f1236,definition,
sF8 = c_Polynomial_OpCons(sF3,sF7,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1237,plain,
c_Polynomial_OpCons(sF3,sF7,tc_Complex_Ocomplex) = sF8,
inference(reorient_equations,[],[f1236]) ).
fof(f1238,definition,
sF9 = c_Power_Opower__class_Opower(sF8,sF2,sF5),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1239,plain,
c_Power_Opower__class_Opower(sF8,sF2,sF5) = sF9,
inference(reorient_equations,[],[f1238]) ).
fof(f1240,definition,
sF10 = c_HOL_Otimes__class_Otimes(sF9,v_s____,sF5),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1241,plain,
c_HOL_Otimes__class_Otimes(sF9,v_s____,sF5) = sF10,
inference(reorient_equations,[],[f1240]) ).
fof(f1242,definition,
sF11 = c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1243,plain,
c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex) = sF11,
inference(reorient_equations,[],[f1242]) ).
fof(f1244,plain,
~ c_HOL_Oord__class_Oless(sF1,sF11,tc_nat),
inference(definition_folding,[],[f1024,f1243,f1241,f1231,f1239,f1231,f1224,f1237,f1235,f1233,f1231,f1229,f1227,f1221]) ).
fof(f1445,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != sF2,
inference(superposition,[],[f860,f1224]) ).
fof(f1446,plain,
sF0 != sF2,
inference(forward_demodulation,[],[f1445,f1219]) ).
fof(f1665,plain,
v_s____ != c_HOL_Ozero__class_Ozero(sF5),
inference(superposition,[],[f863,f1231]) ).
fof(f1666,plain,
v_s____ != sF6,
inference(forward_demodulation,[],[f1665,f1233]) ).
fof(f1673,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),
inference(resolution,[],[f1162,f996]) ).
fof(f1674,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(c_HOL_Ozero__class_Ozero(sF5),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1673,f1231]) ).
fof(f1678,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Polynomial_Odegree(sF6,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1674,f1233]) ).
fof(f1682,plain,
sF0 = c_Polynomial_Odegree(sF6,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f1678,f1219]) ).
fof(f1779,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0 ),
inference(resolution,[],[f1155,f757]) ).
fof(f1780,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,sF5),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X1
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0 ),
inference(forward_demodulation,[],[f1779,f1231]) ).
fof(f1781,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(sF5) = X1
| c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,sF5),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0 ),
inference(forward_demodulation,[],[f1780,f1231]) ).
fof(f1782,plain,
! [X0,X1] :
( sF6 = X1
| c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,sF5),tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0 ),
inference(forward_demodulation,[],[f1781,f1233]) ).
fof(f1783,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(sF5) = X0
| sF6 = X1
| c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,sF5),tc_Complex_Ocomplex) ),
inference(forward_demodulation,[],[f1782,f1231]) ).
fof(f1784,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),c_Polynomial_Odegree(X1,tc_Complex_Ocomplex),tc_nat) = c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,X1,sF5),tc_Complex_Ocomplex)
| sF6 = X1
| sF6 = X0 ),
inference(forward_demodulation,[],[f1783,f1233]) ).
fof(f1795,plain,
! [X0] :
( c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,v_s____,sF5),tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),sF1,tc_nat)
| v_s____ = sF6
| sF6 = X0 ),
inference(superposition,[],[f1784,f1221]) ).
fof(f1821,plain,
! [X0] :
( c_Polynomial_Odegree(c_HOL_Otimes__class_Otimes(X0,v_s____,sF5),tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(X0,tc_Complex_Ocomplex),sF1,tc_nat)
| sF6 = X0 ),
inference(forward_subsumption_resolution,[],[f1795,f1666]) ).
fof(f2117,plain,
! [X0,X1] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = X1,
inference(resolution,[],[f804,f1133]) ).
fof(f2118,plain,
! [X0,X1] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(sF5),tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,sF5),tc_Complex_Ocomplex) = X1,
inference(forward_demodulation,[],[f2117,f1231]) ).
fof(f2119,plain,
! [X0,X1] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,sF5),tc_Complex_Ocomplex) = X1,
inference(forward_demodulation,[],[f2118,f1233]) ).
fof(f2120,plain,
! [X0,X1] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X0,c_Polynomial_OpCons(sF4,sF6,tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1,sF5),tc_Complex_Ocomplex) = X1,
inference(forward_demodulation,[],[f2119,f1229]) ).
fof(f2121,plain,
! [X0,X1] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(c_Polynomial_OpCons(X0,sF7,tc_Complex_Ocomplex),X1,sF5),tc_Complex_Ocomplex) = X1,
inference(forward_demodulation,[],[f2120,f1235]) ).
fof(f2140,definition,
( spl12_36
<=> sF6 = sF9 ),
introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition]) ).
fof(f2141,plain,
( sF6 != sF9
| spl12_36 ),
inference(avatar_component_clause,[],[f2140]) ).
fof(f2142,plain,
( sF6 = sF9
| ~ spl12_36 ),
inference(avatar_component_clause,[],[f2140]) ).
fof(f2277,plain,
( c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(sF9,tc_Complex_Ocomplex),sF1,tc_nat)
| sF6 = sF9 ),
inference(superposition,[],[f1821,f1241]) ).
fof(f2291,plain,
( c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(sF9,tc_Complex_Ocomplex),sF1,tc_nat)
| spl12_36 ),
inference(forward_subsumption_resolution,[],[f2277,f2141]) ).
fof(f3766,plain,
( sF11 = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(sF9,tc_Complex_Ocomplex),sF1,tc_nat)
| spl12_36 ),
inference(forward_demodulation,[],[f2291,f1243]) ).
fof(f3791,plain,
! [X0] : c_Polynomial_Odegree(c_Power_Opower__class_Opower(sF8,X0,sF5),tc_Complex_Ocomplex) = X0,
inference(superposition,[],[f2121,f1237]) ).
fof(f3796,plain,
sF2 = c_Polynomial_Odegree(sF9,tc_Complex_Ocomplex),
inference(superposition,[],[f3791,f1239]) ).
fof(f3819,plain,
( ~ c_HOL_Oord__class_Oless(sF11,sF1,tc_nat)
| spl12_36 ),
inference(superposition,[],[f685,f3766]) ).
fof(f3846,plain,
( c_HOL_Oord__class_Oless(sF1,sF11,tc_nat)
| ~ class_Orderings_Olinorder(tc_nat)
| sF1 = sF11
| spl12_36 ),
inference(resolution,[],[f3819,f943]) ).
fof(f3849,plain,
( ~ class_Orderings_Olinorder(tc_nat)
| sF1 = sF11
| spl12_36 ),
inference(forward_subsumption_resolution,[],[f3846,f1244]) ).
fof(f3851,plain,
( sF1 = sF11
| spl12_36 ),
inference(forward_subsumption_resolution,[],[f3849,f1065]) ).
fof(f6472,definition,
( spl12_94
<=> sF1 = sF11 ),
introduced(definition,[new_symbols(definition,[spl12_94])],[avatar_definition]) ).
fof(f6473,plain,
( sF1 != sF11
| spl12_94 ),
inference(avatar_component_clause,[],[f6472]) ).
fof(f6474,plain,
( sF1 = sF11
| ~ spl12_94 ),
inference(avatar_component_clause,[],[f6472]) ).
fof(f6598,plain,
( sF2 = c_Polynomial_Odegree(sF6,tc_Complex_Ocomplex)
| ~ spl12_36 ),
inference(forward_demodulation,[],[f3796,f2142]) ).
fof(f6613,plain,
( sF0 = sF2
| ~ spl12_36 ),
inference(forward_demodulation,[],[f6598,f1682]) ).
fof(f6627,plain,
( $false
| ~ spl12_36 ),
inference(forward_subsumption_resolution,[],[f6613,f1446]) ).
fof(f6628,plain,
~ spl12_36,
inference(avatar_contradiction_clause,[],[f6627]) ).
fof(f6681,plain,
( c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Odegree(sF9,tc_Complex_Ocomplex),sF1,tc_nat)
| spl12_36 ),
inference(forward_subsumption_resolution,[],[f2277,f2141]) ).
fof(f6694,plain,
( c_Polynomial_Odegree(sF10,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(sF2,sF1,tc_nat)
| spl12_36 ),
inference(forward_demodulation,[],[f6681,f3796]) ).
fof(f6702,plain,
( sF11 = c_HOL_Oplus__class_Oplus(sF2,sF1,tc_nat)
| spl12_36 ),
inference(forward_demodulation,[],[f6694,f1243]) ).
fof(f6844,plain,
( $false
| spl12_36
| spl12_94 ),
inference(forward_subsumption_resolution,[],[f3851,f6473]) ).
fof(f6845,plain,
( spl12_36
| spl12_94 ),
inference(avatar_contradiction_clause,[],[f6844]) ).
fof(f6874,plain,
( sF11 = c_HOL_Oplus__class_Oplus(sF1,sF2,tc_nat)
| spl12_36 ),
inference(superposition,[],[f82,f6702]) ).
fof(f6894,plain,
( sF1 = c_HOL_Oplus__class_Oplus(sF1,sF2,tc_nat)
| spl12_36
| ~ spl12_94 ),
inference(forward_demodulation,[],[f6874,f6474]) ).
fof(f7011,plain,
( ! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(sF1,X0,tc_nat),sF1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,sF2,tc_nat) )
| spl12_36
| ~ spl12_94 ),
inference(superposition,[],[f681,f6894]) ).
fof(f7017,plain,
( ! [X0] : ~ c_HOL_Oord__class_Oless(X0,sF2,tc_nat)
| spl12_36
| ~ spl12_94 ),
inference(forward_subsumption_resolution,[],[f7011,f684]) ).
fof(f7022,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = sF2
| spl12_36
| ~ spl12_94 ),
inference(resolution,[],[f7017,f866]) ).
fof(f7035,plain,
( sF0 = sF2
| spl12_36
| ~ spl12_94 ),
inference(forward_demodulation,[],[f7022,f1219]) ).
fof(f7036,plain,
( $false
| spl12_36
| ~ spl12_94 ),
inference(forward_subsumption_resolution,[],[f7035,f1446]) ).
fof(f7037,plain,
( spl12_36
| ~ spl12_94 ),
inference(avatar_contradiction_clause,[],[f7036]) ).
cnf(s134,plain,
~ spl12_36,
inference(sat_conversion,[],[f6628]) ).
cnf(s137,plain,
( spl12_36
| spl12_94 ),
inference(sat_conversion,[],[f6845]) ).
cnf(s141,plain,
( spl12_36
| ~ spl12_94 ),
inference(sat_conversion,[],[f7037]) ).
cnf(s142,plain,
~ spl12_94,
inference(rat,[],[s141,s134]) ).
cnf(s144,plain,
$false,
inference(rat,[],[s137,s142,s134]) ).
fof(f7038,plain,
$false,
inference(avatar_sat_refutation,[],[s144]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG419-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.08/0.19 % Computer : n004.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 20:20:07 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 11.03/2.21 % (717228)Input is clausal, will run a generic CNF schedule.
% 11.03/2.21 % (717235)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4291535233:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.03/2.21 % (717233)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=1161852176:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.03/2.21 % (717238)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2068380019:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.03/2.21 % (717234)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3251588848:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.03/2.21 % (717237)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2120992620:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.03/2.21 % (717236)lrs+10_1_sil=8000:sp=occurrence:random_seed=3456630415:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.03/2.21 % (717239)dis-21_1_sil=8000:lcm=predicate:random_seed=1049196004:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.03/2.21 % (717236)Instruction limit reached!
% 11.03/2.21 % (717236)------------------------------
% 11.03/2.21 % (717236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.21 % (717236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.21 % (717236)CaDiCaL version: 2.1.3
% 11.03/2.21 % (717236)Termination reason: Instruction limit
% 11.03/2.21 % (717236)Termination phase: Saturation
% 11.03/2.21 % (717236)Time elapsed: 0.070 s
% 11.03/2.21 % (717236)Peak memory usage: 90 MB
% 11.03/2.21 % (717236)Instructions burned: 107 (million)
% 11.03/2.21 % (717239)Instruction limit reached!
% 11.03/2.21 % (717239)------------------------------
% 11.03/2.21 % (717239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.21 % (717239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.21 % (717239)CaDiCaL version: 2.1.3
% 11.03/2.21 % (717239)Termination reason: Instruction limit
% 11.03/2.21 % (717239)Termination phase: Saturation
% 11.03/2.21 % (717239)Time elapsed: 0.069 s
% 11.03/2.21 % (717239)Peak memory usage: 89 MB
% 11.03/2.21 % (717239)Instructions burned: 118 (million)
% 11.03/2.21 % (717237)Instruction limit reached!
% 11.03/2.21 % (717237)------------------------------
% 11.03/2.21 % (717237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.21 % (717237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.21 % (717237)CaDiCaL version: 2.1.3
% 11.03/2.21 % (717237)Termination reason: Instruction limit
% 11.03/2.21 % (717237)Termination phase: Saturation
% 11.03/2.21 % (717237)Time elapsed: 0.075 s
% 11.03/2.21 % (717237)Peak memory usage: 89 MB
% 11.03/2.21 % (717237)Instructions burned: 115 (million)
% 11.03/2.21 % (717238)Instruction limit reached!
% 11.03/2.21 % (717238)------------------------------
% 11.03/2.21 % (717238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.21 % (717238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.21 % (717238)CaDiCaL version: 2.1.3
% 11.03/2.21 % (717238)Termination reason: Instruction limit
% 11.03/2.21 % (717238)Termination phase: Saturation
% 11.03/2.21 % (717238)Time elapsed: 0.118 s
% 11.03/2.21 % (717238)Peak memory usage: 90 MB
% 11.03/2.21 % (717238)Instructions burned: 181 (million)
% 11.03/2.21 % (717249)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=399948921:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 11.03/2.21 % (717247)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=2929151594:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.03/2.21 % (717248)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=215896885: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.03/2.21 % (717250)lrs+10_64_to=lpo:sil=8000:random_seed=2995035564:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 11.03/2.21 % (717247)Instruction limit reached!
% 11.03/2.21 % (717247)------------------------------
% 11.03/2.21 % (717247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717247)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717247)Termination reason: Instruction limit
% 11.03/2.26 % (717247)Termination phase: Saturation
% 11.03/2.26 % (717247)Time elapsed: 0.087 s
% 11.03/2.26 % (717247)Peak memory usage: 90 MB
% 11.03/2.26 % (717247)Instructions burned: 144 (million)
% 11.03/2.26 % (717248)Instruction limit reached!
% 11.03/2.26 % (717248)------------------------------
% 11.03/2.26 % (717248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717248)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717248)Termination reason: Instruction limit
% 11.03/2.26 % (717248)Termination phase: Saturation
% 11.03/2.26 % (717248)Time elapsed: 0.098 s
% 11.03/2.26 % (717248)Peak memory usage: 91 MB
% 11.03/2.26 % (717248)Instructions burned: 189 (million)
% 11.03/2.26 % (717250)Instruction limit reached!
% 11.03/2.26 % (717250)------------------------------
% 11.03/2.26 % (717250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717250)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717250)Termination reason: Instruction limit
% 11.03/2.26 % (717250)Termination phase: Saturation
% 11.03/2.26 % (717250)Time elapsed: 0.070 s
% 11.03/2.26 % (717250)Peak memory usage: 89 MB
% 11.03/2.26 % (717250)Instructions burned: 128 (million)
% 11.03/2.26 % (717249)Instruction limit reached!
% 11.03/2.26 % (717249)------------------------------
% 11.03/2.26 % (717249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717249)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717249)Termination reason: Instruction limit
% 11.03/2.26 % (717249)Termination phase: Saturation
% 11.03/2.26 % (717249)Time elapsed: 0.130 s
% 11.03/2.26 % (717249)Peak memory usage: 91 MB
% 11.03/2.26 % (717249)Instructions burned: 219 (million)
% 11.03/2.26 % (717255)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1462492436:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 11.03/2.26 % (717256)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=970579475:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 11.03/2.26 % (717257)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=632204913:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 11.03/2.26 % (717258)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=3264260767:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 11.03/2.26 % (717258)Instruction limit reached!
% 11.03/2.26 % (717258)------------------------------
% 11.03/2.26 % (717258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717258)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717258)Termination reason: Instruction limit
% 11.03/2.26 % (717258)Termination phase: Saturation
% 11.03/2.26 % (717258)Time elapsed: 0.059 s
% 11.03/2.26 % (717258)Peak memory usage: 89 MB
% 11.03/2.26 % (717258)Instructions burned: 107 (million)
% 11.03/2.26 % (717256)Instruction limit reached!
% 11.03/2.26 % (717256)------------------------------
% 11.03/2.26 % (717256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717256)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717256)Termination reason: Instruction limit
% 11.03/2.26 % (717256)Termination phase: Saturation
% 11.03/2.26 % (717256)Time elapsed: 0.097 s
% 11.03/2.26 % (717256)Peak memory usage: 91 MB
% 11.03/2.26 % (717256)Instructions burned: 158 (million)
% 11.03/2.26 % (717255)Instruction limit reached!
% 11.03/2.26 % (717255)------------------------------
% 11.03/2.26 % (717255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717255)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717255)Termination reason: Instruction limit
% 11.03/2.26 % (717255)Termination phase: Saturation
% 11.03/2.26 % (717255)Time elapsed: 0.113 s
% 11.03/2.26 % (717255)Peak memory usage: 90 MB
% 11.03/2.26 % (717255)Instructions burned: 194 (million)
% 11.03/2.26 % (717263)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1500918710:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 11.03/2.26 % (717264)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2682489920:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 11.03/2.26 % (717265)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2122001315:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 11.03/2.26 % (717263)Instruction limit reached!
% 11.03/2.26 % (717263)------------------------------
% 11.03/2.26 % (717263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717263)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717263)Termination reason: Instruction limit
% 11.03/2.26 % (717263)Termination phase: Saturation
% 11.03/2.26 % (717263)Time elapsed: 0.067 s
% 11.03/2.26 % (717263)Peak memory usage: 90 MB
% 11.03/2.26 % (717263)Instructions burned: 108 (million)
% 11.03/2.26 % (717264)Instruction limit reached!
% 11.03/2.26 % (717264)------------------------------
% 11.03/2.26 % (717264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717264)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717264)Termination reason: Instruction limit
% 11.03/2.26 % (717264)Termination phase: Saturation
% 11.03/2.26 % (717264)Time elapsed: 0.146 s
% 11.03/2.26 % (717264)Peak memory usage: 90 MB
% 11.03/2.26 % (717264)Instructions burned: 243 (million)
% 11.03/2.26 % (717269)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1328341041:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 11.03/2.26 % (717269)Instruction limit reached!
% 11.03/2.26 % (717269)------------------------------
% 11.03/2.26 % (717269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717269)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717269)Termination reason: Instruction limit
% 11.03/2.26 % (717269)Termination phase: Saturation
% 11.03/2.26 % (717269)Time elapsed: 0.061 s
% 11.03/2.26 % (717269)Peak memory usage: 89 MB
% 11.03/2.26 % (717269)Instructions burned: 135 (million)
% 11.03/2.26 % (717270)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3679890657:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 11.03/2.26 % (717272)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3157378298:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 11.03/2.26 % (717272)Instruction limit reached!
% 11.03/2.26 % (717272)------------------------------
% 11.03/2.26 % (717272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717272)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717272)Termination reason: Instruction limit
% 11.03/2.26 % (717272)Termination phase: Saturation
% 11.03/2.26 % (717272)Time elapsed: 0.123 s
% 11.03/2.26 % (717272)Peak memory usage: 92 MB
% 11.03/2.26 % (717272)Instructions burned: 192 (million)
% 11.03/2.26 % (717233)First to succeed.
% 11.03/2.26 % (717233)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-717228"
% 11.03/2.26 % (717270)Instruction limit reached!
% 11.03/2.26 % (717270)------------------------------
% 11.03/2.26 % (717270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.26 % (717270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.26 % (717270)CaDiCaL version: 2.1.3
% 11.03/2.26 % (717270)Termination reason: Instruction limit
% 11.03/2.26 % (717270)Termination phase: Saturation
% 11.03/2.26 % (717270)Time elapsed: 0.301 s
% 11.03/2.26 % (717270)Peak memory usage: 94 MB
% 11.03/2.26 % (717270)Instructions burned: 501 (million)
% 11.03/2.26 % (717275)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1257957972:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 11.03/2.26 % (717276)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3035725283:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 11.03/2.26 % (717233)Refutation found. Thanks to Tanya!
% 11.03/2.26 % SZS status Unsatisfiable for theBenchmark
% 11.03/2.26 % SZS output start Proof for theBenchmark
% See solution above
% 11.72/2.45 % (717233)------------------------------
% 11.72/2.45 % (717233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.45 % (717233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.45 % (717233)CaDiCaL version: 2.1.3
% 11.72/2.45 % (717233)Termination reason: Refutation
% 11.72/2.45 % (717233)Time elapsed: 1.169 s
% 11.72/2.45 % (717233)Peak memory usage: 139 MB
% 11.72/2.45 % (717233)Instructions burned: 1792 (million)
% 11.72/2.45 % (717233)------------------------------
% 11.72/2.45 % (717233)------------------------------
% 11.72/2.45 % (717228)Success in time 1.597 s
% 11.72/2.45 % Vampire exiting
%------------------------------------------------------------------------------