%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV628-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 : n006.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:08 PM UTC 2026
% Result : Unsatisfiable 15.32s 3.02s
% Output : Refutation 16.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of formulae : 117 ( 64 unt; 5 def)
% Number of atoms : 173 ( 109 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 105 ( 49 ~; 54 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 115 ( 0 sgn 115 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f114,axiom,
! [X0] :
( c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = X0
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__pred_0) ).
fof(f219,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X2,X1,X0),X1,X0) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide__eq__imp_0) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ofield(X0)
| c_HOL_Ozero__class_Ozero(X0) = X1
| c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X2,X1,X0),X1,X0) = X2 ),
inference(reorient_equations,[],[f219]) ).
fof(f227,axiom,
! [X0] : c_Nat_Osize__class_Osize(c_Suc(X0),tc_nat) = c_HOL_Oplus__class_Oplus(c_Nat_Osize__class_Osize(X0,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osize_I4_J_0) ).
fof(f249,axiom,
! [X0] : c_Nat_Osize__class_Osize(X0,tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__size_0) ).
fof(f258,axiom,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_Suc(X1),tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__Suc__right_0) ).
fof(f376,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_0) ).
fof(f668,axiom,
! [X2,X3,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(X1,X2,X0),X3,X0) = c_Power_Opower__class_Opower(X1,c_HOL_Otimes__class_Otimes(X2,X3,tc_nat),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Opwr__pwr_0) ).
fof(f923,axiom,
! [X2,X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ominus__class_Ominus(X1,X2,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(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_diff__mult__distrib2_0) ).
fof(f1182,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__add__inverse_0) ).
fof(f1183,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__add__inverse2_0) ).
fof(f1282,axiom,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X1,X2,X0),X1,X0) = c_Power_Opower__class_Opower(X1,c_Suc(X2),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I28_J_0) ).
fof(f1283,plain,
! [X2,X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(X1,c_Suc(X2),X0) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X1,X2,X0),X1,X0) ),
inference(reorient_equations,[],[f1282]) ).
fof(f1330,axiom,
! [X2,X0,X1] :
( c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)),c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X2,tc_Complex_Ocomplex)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__cancel_0) ).
fof(f1362,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I10_J_0) ).
fof(f1363,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) ),
inference(reorient_equations,[],[f1362]) ).
fof(f1618,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(X0),X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I11_J_0) ).
fof(f1638,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/sandbox/benchmark/theBenchmark.p',cls_gr0I_0) ).
fof(f1639,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,[],[f1638]) ).
fof(f1658,axiom,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f1708,axiom,
c_Orderings_Obot__class_Obot(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot__nat__def_0) ).
fof(f1709,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Orderings_Obot__class_Obot(tc_nat),
inference(reorient_equations,[],[f1708]) ).
fof(f1725,axiom,
! [X0] : c_FFT__Mirabelle_Oroot(X0) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__nonzero_0) ).
fof(f1726,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_FFT__Mirabelle_Oroot(X0),
inference(reorient_equations,[],[f1725]) ).
fof(f1754,axiom,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) = c_HOL_Oone__class_Oone(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Opwr__0_0) ).
fof(f1755,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X0)
| c_HOL_Oone__class_Oone(X0) = c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) ),
inference(reorient_equations,[],[f1754]) ).
fof(f1760,axiom,
! [X0] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__unity_0) ).
fof(f1761,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex),
inference(reorient_equations,[],[f1760]) ).
fof(f1763,axiom,
! [X0] :
( ~ class_Ring__and__Field_Ozero__neq__one(X0)
| c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f1764,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(reorient_equations,[],[f1763]) ).
fof(f1765,negated_conjecture,
c_FFT__Mirabelle_Oroot(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1766,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) != c_FFT__Mirabelle_Oroot(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(reorient_equations,[],[f1765]) ).
fof(f1873,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f1883,axiom,
class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ozero__neq__one) ).
fof(f1896,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
fof(f1907,definition,
sF0 = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1908,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1907]) ).
fof(f1909,definition,
sF1 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1910,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF1,
inference(reorient_equations,[],[f1909]) ).
fof(f1911,definition,
sF2 = c_FFT__Mirabelle_Oroot(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1912,plain,
c_FFT__Mirabelle_Oroot(sF1) = sF2,
inference(reorient_equations,[],[f1911]) ).
fof(f1913,plain,
sF0 != sF2,
inference(definition_folding,[],[f1766,f1912,f1910,f1908]) ).
fof(f1941,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_nat),tc_nat),
inference(forward_demodulation,[],[f1658,f1709]) ).
fof(f1955,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f1639,f1709]) ).
fof(f1973,plain,
! [X2,X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat)
| c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)),c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X2,tc_Complex_Ocomplex) ),
inference(forward_demodulation,[],[f1330,f1709]) ).
fof(f2059,plain,
! [X0] : c_Nat_Osize__class_Osize(c_Suc(X0),tc_nat) = c_HOL_Oplus__class_Oplus(c_Nat_Osize__class_Osize(X0,tc_nat),c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),tc_nat),
inference(forward_demodulation,[],[f227,f1709]) ).
fof(f2065,plain,
! [X0] :
( c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),tc_nat)) = X0
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(forward_demodulation,[],[f114,f1709]) ).
fof(f2071,plain,
c_Orderings_Obot__class_Obot(tc_nat) = sF1,
inference(forward_demodulation,[],[f1910,f1709]) ).
fof(f2078,plain,
! [X0] :
( c_Orderings_Obot__class_Obot(tc_nat) = X0
| c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat) ),
inference(forward_demodulation,[],[f1955,f1709]) ).
fof(f2110,plain,
! [X0] : c_Nat_Osize__class_Osize(c_Suc(X0),tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),tc_nat),
inference(forward_demodulation,[],[f2059,f249]) ).
fof(f2115,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),tc_nat)) = X0 ),
inference(forward_demodulation,[],[f2065,f1709]) ).
fof(f2122,plain,
! [X0] :
( sF1 = X0
| c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat) ),
inference(forward_demodulation,[],[f2078,f2071]) ).
fof(f2152,plain,
! [X0] : c_Nat_Osize__class_Osize(c_Suc(X0),tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_Suc(sF1),tc_nat),
inference(forward_demodulation,[],[f2110,f2071]) ).
fof(f2156,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF1,X0,tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(c_Orderings_Obot__class_Obot(tc_nat)),tc_nat)) = X0 ),
inference(forward_demodulation,[],[f2115,f2071]) ).
fof(f2163,plain,
! [X0] :
( c_HOL_Oord__class_Oless(sF1,X0,tc_nat)
| sF1 = X0 ),
inference(forward_demodulation,[],[f2122,f2071]) ).
fof(f2193,plain,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_Suc(sF1),tc_nat),
inference(forward_demodulation,[],[f2152,f249]) ).
fof(f2197,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(sF1,X0,tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(sF1),tc_nat)) = X0 ),
inference(forward_demodulation,[],[f2156,f2071]) ).
fof(f2230,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF2,sF1,tc_Complex_Ocomplex),
inference(superposition,[],[f1761,f1912]) ).
fof(f2231,plain,
sF0 = c_Power_Opower__class_Opower(sF2,sF1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2230,f1908]) ).
fof(f2232,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF2,
inference(superposition,[],[f1726,f1912]) ).
fof(f2239,plain,
! [X0] :
( c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(sF1),tc_nat)) = X0
| sF1 = X0 ),
inference(resolution,[],[f2197,f2163]) ).
fof(f2259,plain,
! [X0] : c_HOL_Otimes__class_Otimes(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0,
inference(resolution,[],[f1873,f1618]) ).
fof(f2260,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex) = X0,
inference(forward_demodulation,[],[f2259,f1908]) ).
fof(f2442,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_Complex_Ocomplex),
inference(resolution,[],[f1755,f1873]) ).
fof(f2443,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_Orderings_Obot__class_Obot(tc_nat),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2442,f1709]) ).
fof(f2444,plain,
! [X0] : c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,sF1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2443,f2071]) ).
fof(f2445,plain,
! [X0] : sF0 = c_Power_Opower__class_Opower(X0,sF1,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f2444,f1908]) ).
fof(f2666,plain,
! [X2,X0,X1] : c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_nat),tc_Complex_Ocomplex),
inference(resolution,[],[f668,f1873]) ).
fof(f2672,plain,
! [X0,X1] : sF0 = c_Power_Opower__class_Opower(X0,c_HOL_Otimes__class_Otimes(X1,sF1,tc_nat),tc_Complex_Ocomplex),
inference(superposition,[],[f2445,f2666]) ).
fof(f2799,definition,
( spl3_3
<=> c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF0 ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f2800,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF0
| spl3_3 ),
inference(avatar_component_clause,[],[f2799]) ).
fof(f2801,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF0
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f2799]) ).
fof(f3016,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != sF0
| ~ class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex) ),
inference(superposition,[],[f1764,f1908]) ).
fof(f3019,plain,
( ~ class_Ring__and__Field_Ozero__neq__one(tc_Complex_Ocomplex)
| ~ spl3_3 ),
inference(forward_subsumption_resolution,[],[f3016,f2801]) ).
fof(f3021,plain,
( $false
| ~ spl3_3 ),
inference(forward_subsumption_resolution,[],[f3019,f1883]) ).
fof(f3022,plain,
~ spl3_3,
inference(avatar_contradiction_clause,[],[f3021]) ).
fof(f3220,plain,
! [X0] : c_Suc(sF1) = c_HOL_Ominus__class_Ominus(c_Suc(X0),X0,tc_nat),
inference(superposition,[],[f1182,f2193]) ).
fof(f3707,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(X0,c_Suc(X1),tc_nat),c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),tc_nat) = X0,
inference(superposition,[],[f1183,f258]) ).
fof(f3728,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Ominus__class_Ominus(c_Suc(X1),X1,tc_nat),tc_nat) = X0,
inference(forward_demodulation,[],[f3707,f923]) ).
fof(f3733,plain,
! [X0] : c_HOL_Otimes__class_Otimes(X0,c_Suc(sF1),tc_nat) = X0,
inference(forward_demodulation,[],[f3728,f3220]) ).
fof(f3879,plain,
! [X0,X1] : c_Power_Opower__class_Opower(X0,c_Suc(X1),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),
inference(resolution,[],[f1283,f1873]) ).
fof(f3881,plain,
! [X0] : c_HOL_Otimes__class_Otimes(sF0,X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X0,c_Suc(sF1),tc_Complex_Ocomplex),
inference(superposition,[],[f3879,f2445]) ).
fof(f3895,plain,
c_Power_Opower__class_Opower(sF2,c_Suc(sF1),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(sF0,sF2,tc_Complex_Ocomplex),
inference(superposition,[],[f3879,f2231]) ).
fof(f3906,plain,
sF2 = c_Power_Opower__class_Opower(sF2,c_Suc(sF1),tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f3895,f2260]) ).
fof(f3920,plain,
! [X0] : c_Power_Opower__class_Opower(X0,c_Suc(sF1),tc_Complex_Ocomplex) = X0,
inference(forward_demodulation,[],[f3881,f2260]) ).
fof(f3954,plain,
! [X0] : c_Power_Opower__class_Opower(X0,c_Suc(c_Suc(sF1)),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,X0,tc_Complex_Ocomplex),
inference(superposition,[],[f3879,f3920]) ).
fof(f4153,definition,
( spl3_6
<=> ! [X1] : sF1 = c_HOL_Otimes__class_Otimes(X1,sF1,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f4154,plain,
( ! [X1] : sF1 = c_HOL_Otimes__class_Otimes(X1,sF1,tc_nat)
| ~ spl3_6 ),
inference(avatar_component_clause,[],[f4153]) ).
fof(f5068,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[],[f1363,f1873]) ).
fof(f5076,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_Suc(X0),tc_Complex_Ocomplex),
inference(superposition,[],[f3879,f5068]) ).
fof(f5974,plain,
! [X0,X1] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X1
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(resolution,[],[f220,f1896]) ).
fof(f5975,plain,
! [X0] :
( c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,c_Suc(c_Suc(sF1)),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = X0
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f5974,f3954]) ).
fof(f5981,plain,
! [X0,X1] :
( c_Power_Opower__class_Opower(X0,X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,c_Suc(X1),tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(superposition,[],[f5974,f3879]) ).
fof(f6067,plain,
( c_Power_Opower__class_Opower(sF2,sF1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF2,sF2,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2 ),
inference(superposition,[],[f5981,f3906]) ).
fof(f6076,plain,
c_Power_Opower__class_Opower(sF2,sF1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(sF2,sF2,tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f6067,f2232]) ).
fof(f6105,plain,
sF0 = c_HOL_Oinverse__class_Odivide(sF2,sF2,tc_Complex_Ocomplex),
inference(forward_demodulation,[],[f6076,f2231]) ).
fof(f8253,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex)
| sF1 = X0 ),
inference(superposition,[],[f5076,f2239]) ).
fof(f8285,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF0
| sF1 = c_HOL_Otimes__class_Otimes(X0,sF1,tc_nat) ),
inference(superposition,[],[f2672,f8253]) ).
fof(f14614,plain,
! [X2,X0,X1] :
( c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X2,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Otimes__class_Otimes(c_Suc(X0),X1,tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(X0),X2,tc_nat),tc_Complex_Ocomplex)
| c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_nat),tc_nat) ),
inference(resolution,[],[f1973,f376]) ).
fof(f14633,plain,
! [X2,X0,X1] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X2,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(c_HOL_Otimes__class_Otimes(c_Suc(X0),X1,tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(X0),X2,tc_nat),tc_Complex_Ocomplex),
inference(forward_subsumption_resolution,[],[f14614,f1941]) ).
fof(f16959,plain,
( ! [X0,X1] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(sF1),X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(sF1),c_HOL_Otimes__class_Otimes(c_Suc(X1),X0,tc_nat),tc_Complex_Ocomplex)
| ~ spl3_6 ),
inference(superposition,[],[f14633,f4154]) ).
fof(f17048,plain,
( ! [X0,X1] : c_Power_Opower__class_Opower(sF2,X0,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF2,c_HOL_Otimes__class_Otimes(c_Suc(X1),X0,tc_nat),tc_Complex_Ocomplex)
| ~ spl3_6 ),
inference(forward_demodulation,[],[f16959,f1912]) ).
fof(f17186,plain,
( ! [X0] : c_Power_Opower__class_Opower(sF2,c_Suc(sF1),tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(sF2,c_Suc(X0),tc_Complex_Ocomplex)
| ~ spl3_6 ),
inference(superposition,[],[f17048,f3733]) ).
fof(f17214,plain,
( ! [X0] : sF2 = c_Power_Opower__class_Opower(sF2,c_Suc(X0),tc_Complex_Ocomplex)
| ~ spl3_6 ),
inference(forward_demodulation,[],[f17186,f3906]) ).
fof(f17247,plain,
( sF2 = c_HOL_Oinverse__class_Odivide(sF2,sF2,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = sF2
| ~ spl3_6 ),
inference(superposition,[],[f5975,f17214]) ).
fof(f17255,plain,
( sF2 = c_HOL_Oinverse__class_Odivide(sF2,sF2,tc_Complex_Ocomplex)
| ~ spl3_6 ),
inference(forward_subsumption_resolution,[],[f17247,f2232]) ).
fof(f17259,plain,
( sF0 = sF2
| ~ spl3_6 ),
inference(forward_demodulation,[],[f17255,f6105]) ).
fof(f17263,plain,
( $false
| ~ spl3_6 ),
inference(forward_subsumption_resolution,[],[f17259,f1913]) ).
fof(f17264,plain,
~ spl3_6,
inference(avatar_contradiction_clause,[],[f17263]) ).
fof(f17318,plain,
( ! [X0] : sF1 = c_HOL_Otimes__class_Otimes(X0,sF1,tc_nat)
| spl3_3 ),
inference(forward_subsumption_resolution,[],[f8285,f2800]) ).
fof(f17475,plain,
( spl3_6
| spl3_3 ),
inference(avatar_split_clause,[],[f17318,f2799,f4153]) ).
cnf(s9,plain,
~ spl3_3,
inference(sat_conversion,[],[f3022]) ).
cnf(s85,plain,
~ spl3_6,
inference(sat_conversion,[],[f17264]) ).
cnf(s104,plain,
( spl3_3
| spl3_6 ),
inference(sat_conversion,[],[f17475]) ).
cnf(s136,plain,
spl3_3,
inference(rat,[],[s104,s85]) ).
cnf(s145,plain,
$false,
inference(rat,[],[s9,s136]) ).
fof(f17558,plain,
$false,
inference(avatar_sat_refutation,[],[s145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV628-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n006.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 12:04:40 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.24 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
% 10.45/2.18 % (3919569)Input is clausal, will run a generic CNF schedule.
% 10.45/2.18 % (3919578)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3890386640:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.45/2.18 % (3919579)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3992061399:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.45/2.18 % (3919574)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=2914117706:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.45/2.18 % (3919577)lrs+10_1_sil=8000:sp=occurrence:random_seed=4207995745:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.45/2.18 % (3919576)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2407146539:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.45/2.18 % (3919580)dis-21_1_sil=8000:lcm=predicate:random_seed=3584120182: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.45/2.18 % (3919575)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3709721265:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.45/2.18 % (3919578)Instruction limit reached!
% 10.45/2.18 % (3919578)------------------------------
% 10.45/2.18 % (3919578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.18 % (3919578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.18 % (3919578)CaDiCaL version: 2.1.3
% 10.45/2.18 % (3919578)Termination reason: Instruction limit
% 10.45/2.18 % (3919578)Termination phase: Saturation
% 10.45/2.18 % (3919578)Time elapsed: 0.042 s
% 10.45/2.18 % (3919578)Peak memory usage: 89 MB
% 10.45/2.18 % (3919578)Instructions burned: 115 (million)
% 10.45/2.18 % (3919580)Instruction limit reached!
% 10.45/2.18 % (3919580)------------------------------
% 10.45/2.18 % (3919580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.18 % (3919580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.18 % (3919580)CaDiCaL version: 2.1.3
% 10.45/2.18 % (3919580)Termination reason: Instruction limit
% 10.45/2.18 % (3919580)Termination phase: Saturation
% 10.45/2.18 % (3919580)Time elapsed: 0.066 s
% 10.45/2.18 % (3919580)Peak memory usage: 90 MB
% 10.45/2.18 % (3919580)Instructions burned: 118 (million)
% 10.45/2.18 % (3919577)Instruction limit reached!
% 10.45/2.18 % (3919577)------------------------------
% 10.45/2.18 % (3919577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.18 % (3919577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.18 % (3919577)CaDiCaL version: 2.1.3
% 10.45/2.18 % (3919577)Termination reason: Instruction limit
% 10.45/2.18 % (3919577)Termination phase: Saturation
% 10.45/2.18 % (3919577)Time elapsed: 0.071 s
% 10.45/2.18 % (3919577)Peak memory usage: 89 MB
% 10.45/2.18 % (3919577)Instructions burned: 107 (million)
% 10.45/2.18 % (3919588)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=103629046:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.45/2.18 % (3919579)Instruction limit reached!
% 10.45/2.18 % (3919579)------------------------------
% 10.45/2.18 % (3919579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.18 % (3919579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.18 % (3919579)CaDiCaL version: 2.1.3
% 10.45/2.18 % (3919579)Termination reason: Instruction limit
% 10.45/2.18 % (3919579)Termination phase: Saturation
% 10.45/2.18 % (3919579)Time elapsed: 0.115 s
% 10.45/2.18 % (3919579)Peak memory usage: 90 MB
% 10.45/2.18 % (3919579)Instructions burned: 180 (million)
% 10.45/2.18 % (3919588)Refutation not found, incomplete strategy
% 10.45/2.18 % (3919588)------------------------------
% 10.45/2.18 % (3919588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.45/2.18 % (3919588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.45/2.18 % (3919588)CaDiCaL version: 2.1.3
% 10.45/2.18 % (3919588)Termination reason: Refutation not found, incomplete strategy
% 10.45/2.18 % (3919588)Time elapsed: 0.006 s
% 10.45/2.18 % (3919588)Peak memory usage: 89 MB
% 10.45/2.18 % (3919588)Instructions burned: 17 (million)
% 10.45/2.18 % (3919589)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3722721342: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)
% 15.32/3.02 % (3919590)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1466488659:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 15.32/3.02 % (3919590)Refutation not found, incomplete strategy
% 15.32/3.02 % (3919590)------------------------------
% 15.32/3.02 % (3919590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919590)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919590)Termination reason: Refutation not found, incomplete strategy
% 15.32/3.02 % (3919590)Time elapsed: 0.029 s
% 15.32/3.02 % (3919590)Peak memory usage: 89 MB
% 15.32/3.02 % (3919590)Instructions burned: 48 (million)
% 15.32/3.02 % (3919592)lrs+10_64_to=lpo:sil=8000:random_seed=1729336564:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 15.32/3.02 % (3919588)------------------------------
% 15.32/3.02 % (3919588)------------------------------
% 15.32/3.02 % (3919589)Instruction limit reached!
% 15.32/3.02 % (3919589)------------------------------
% 15.32/3.02 % (3919589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919589)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919589)Termination reason: Instruction limit
% 15.32/3.02 % (3919589)Termination phase: Saturation
% 15.32/3.02 % (3919589)Time elapsed: 0.096 s
% 15.32/3.02 % (3919589)Peak memory usage: 90 MB
% 15.32/3.02 % (3919589)Instructions burned: 191 (million)
% 15.32/3.02 % (3919592)Instruction limit reached!
% 15.32/3.02 % (3919592)------------------------------
% 15.32/3.02 % (3919592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919592)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919592)Termination reason: Instruction limit
% 15.32/3.02 % (3919592)Termination phase: Saturation
% 15.32/3.02 % (3919592)Time elapsed: 0.081 s
% 15.32/3.02 % (3919592)Peak memory usage: 91 MB
% 15.32/3.02 % (3919592)Instructions burned: 127 (million)
% 15.32/3.02 % (3919596)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4221914768:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 15.32/3.02 % (3919597)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3932773992:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 15.32/3.02 % (3919596)Instruction limit reached!
% 15.32/3.02 % (3919596)------------------------------
% 15.32/3.02 % (3919596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919596)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919596)Termination reason: Instruction limit
% 15.32/3.02 % (3919596)Termination phase: Saturation
% 15.32/3.02 % (3919596)Time elapsed: 0.070 s
% 15.32/3.02 % (3919596)Peak memory usage: 91 MB
% 15.32/3.02 % (3919596)Instructions burned: 195 (million)
% 15.32/3.02 % (3919598)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3690040057:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 15.32/3.02 % (3919590)------------------------------
% 15.32/3.02 % (3919590)------------------------------
% 15.32/3.02 % (3919597)Instruction limit reached!
% 15.32/3.02 % (3919597)------------------------------
% 15.32/3.02 % (3919597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919597)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919597)Termination reason: Instruction limit
% 15.32/3.02 % (3919597)Termination phase: Saturation
% 15.32/3.02 % (3919597)Time elapsed: 0.096 s
% 15.32/3.02 % (3919597)Peak memory usage: 91 MB
% 15.32/3.02 % (3919597)Instructions burned: 158 (million)
% 15.32/3.02 % (3919601)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=3835826250:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 15.32/3.02 % (3919601)Instruction limit reached!
% 15.32/3.02 % (3919601)------------------------------
% 15.32/3.02 % (3919601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919601)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919601)Termination reason: Instruction limit
% 15.32/3.02 % (3919601)Termination phase: Saturation
% 15.32/3.02 % (3919601)Time elapsed: 0.031 s
% 15.32/3.02 % (3919601)Peak memory usage: 89 MB
% 15.32/3.02 % (3919601)Instructions burned: 109 (million)
% 15.32/3.02 % (3919603)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2583972421:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 15.32/3.02 % (3919604)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=362340012:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 15.32/3.02 % (3919603)Refutation not found, incomplete strategy
% 15.32/3.02 % (3919603)------------------------------
% 15.32/3.02 % (3919603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919603)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919603)Termination reason: Refutation not found, incomplete strategy
% 15.32/3.02 % (3919603)Time elapsed: 0.029 s
% 15.32/3.02 % (3919603)Peak memory usage: 90 MB
% 15.32/3.02 % (3919603)Instructions burned: 48 (million)
% 15.32/3.02 % (3919606)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1382686514:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 15.32/3.02 % (3919604)Instruction limit reached!
% 15.32/3.02 % (3919604)------------------------------
% 15.32/3.02 % (3919604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919604)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919604)Termination reason: Instruction limit
% 15.32/3.02 % (3919604)Termination phase: Saturation
% 15.32/3.02 % (3919604)Time elapsed: 0.146 s
% 15.32/3.02 % (3919604)Peak memory usage: 90 MB
% 15.32/3.02 % (3919604)Instructions burned: 242 (million)
% 15.32/3.02 % (3919603)------------------------------
% 15.32/3.02 % (3919603)------------------------------
% 15.32/3.02 % (3919610)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1062570338:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 15.32/3.02 % (3919610)Instruction limit reached!
% 15.32/3.02 % (3919610)------------------------------
% 15.32/3.02 % (3919610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919610)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919610)Termination reason: Instruction limit
% 15.32/3.02 % (3919610)Termination phase: Saturation
% 15.32/3.02 % (3919610)Time elapsed: 0.088 s
% 15.32/3.02 % (3919610)Peak memory usage: 90 MB
% 15.32/3.02 % (3919610)Instructions burned: 134 (million)
% 15.32/3.02 % (3919611)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=882054753:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 15.32/3.02 % (3919613)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2928640060:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 15.32/3.02 % (3919613)Instruction limit reached!
% 15.32/3.02 % (3919613)------------------------------
% 15.32/3.02 % (3919613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919613)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919613)Termination reason: Instruction limit
% 15.32/3.02 % (3919613)Termination phase: Saturation
% 15.32/3.02 % (3919613)Time elapsed: 0.127 s
% 15.32/3.02 % (3919613)Peak memory usage: 91 MB
% 15.32/3.02 % (3919613)Instructions burned: 192 (million)
% 15.32/3.02 % (3919611)Instruction limit reached!
% 15.32/3.02 % (3919611)------------------------------
% 15.32/3.02 % (3919611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919611)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919611)Termination reason: Instruction limit
% 15.32/3.02 % (3919611)Termination phase: Saturation
% 15.32/3.02 % (3919611)Time elapsed: 0.294 s
% 15.32/3.02 % (3919611)Peak memory usage: 93 MB
% 15.32/3.02 % (3919611)Instructions burned: 500 (million)
% 15.32/3.02 % (3919616)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3165426045:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 15.32/3.02 % (3919617)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2576403121:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 15.32/3.02 % (3919617)Instruction limit reached!
% 15.32/3.02 % (3919617)------------------------------
% 15.32/3.02 % (3919617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919617)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919617)Termination reason: Instruction limit
% 15.32/3.02 % (3919617)Termination phase: Saturation
% 15.32/3.02 % (3919617)Time elapsed: 0.092 s
% 15.32/3.02 % (3919617)Peak memory usage: 90 MB
% 15.32/3.02 % (3919617)Instructions burned: 156 (million)
% 15.32/3.02 % (3919616)Instruction limit reached!
% 15.32/3.02 % (3919616)------------------------------
% 15.32/3.02 % (3919616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919616)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919616)Termination reason: Instruction limit
% 15.32/3.02 % (3919616)Termination phase: Saturation
% 15.32/3.02 % (3919616)Time elapsed: 0.157 s
% 15.32/3.02 % (3919616)Peak memory usage: 93 MB
% 15.32/3.02 % (3919616)Instructions burned: 265 (million)
% 15.32/3.02 % (3919620)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=2308731197:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 15.32/3.02 % (3919621)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=473651281:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 15.32/3.02 % (3919598)Instruction limit reached!
% 15.32/3.02 % (3919598)------------------------------
% 15.32/3.02 % (3919598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919598)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919598)Termination reason: Instruction limit
% 15.32/3.02 % (3919598)Termination phase: Saturation
% 15.32/3.02 % (3919598)Time elapsed: 1.384 s
% 15.32/3.02 % (3919598)Peak memory usage: 151 MB
% 15.32/3.02 % (3919598)Instructions burned: 3396 (million)
% 15.32/3.02 % (3919574)First to succeed.
% 15.32/3.02 % (3919574)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3919569"
% 15.32/3.02 % (3919624)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3859493097:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 15.32/3.02 % (3919621)Instruction limit reached!
% 15.32/3.02 % (3919621)------------------------------
% 15.32/3.02 % (3919621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919621)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919621)Termination reason: Instruction limit
% 15.32/3.02 % (3919621)Termination phase: Saturation
% 15.32/3.02 % (3919621)Time elapsed: 0.302 s
% 15.32/3.02 % (3919621)Peak memory usage: 91 MB
% 15.32/3.02 % (3919621)Instructions burned: 537 (million)
% 15.32/3.02 % (3919624)Instruction limit reached!
% 15.32/3.02 % (3919624)------------------------------
% 15.32/3.02 % (3919624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.32/3.02 % (3919624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.32/3.02 % (3919624)CaDiCaL version: 2.1.3
% 15.32/3.02 % (3919624)Termination reason: Instruction limit
% 15.32/3.02 % (3919624)Termination phase: Saturation
% 15.32/3.02 % (3919624)Time elapsed: 0.060 s
% 15.32/3.02 % (3919624)Peak memory usage: 90 MB
% 15.32/3.02 % (3919624)Instructions burned: 183 (million)
% 15.32/3.02 % (3919626)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4254279719:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 15.32/3.02 % (3919627)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3854663581:i=412:gtgl=4:gtg=exists_all_2977 on theBenchmark for (2977ds/412Mi)
% 15.32/3.02 % (3919574)Refutation found. Thanks to Tanya!
% 15.32/3.02 % SZS status Unsatisfiable for theBenchmark
% 15.32/3.02 % SZS output start Proof for theBenchmark
% See solution above
% 16.93/3.21 % (3919574)------------------------------
% 16.93/3.21 % (3919574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.93/3.21 % (3919574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.93/3.21 % (3919574)CaDiCaL version: 2.1.3
% 16.93/3.21 % (3919574)Termination reason: Refutation
% 16.93/3.21 % (3919574)Time elapsed: 1.881 s
% 16.93/3.21 % (3919574)Peak memory usage: 148 MB
% 16.93/3.21 % (3919574)Instructions burned: 2909 (million)
% 16.93/3.21 % (3919574)------------------------------
% 16.93/3.21 % (3919574)------------------------------
% 16.93/3.21 % (3919569)Success in time 2.352 s
% 16.93/3.21 % Vampire exiting
%------------------------------------------------------------------------------