%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW182+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:29:47 PM UTC 2026
% Result : Theorem 5.03s 1.46s
% Output : Refutation 5.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 12
% Syntax : Number of formulae : 58 ( 16 unt; 5 def)
% Number of atoms : 111 ( 29 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 100 ( 47 ~; 43 |; 0 &)
% ( 5 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 57 ( 0 sgn 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__0(X1)
=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_offset__poly__0) ).
fof(f38,axiom,
! [X0,X1] :
( class_Rings_Ocomm__semiring__0(X1)
=> c_Polynomial_Osmult(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_smult__0__right) ).
fof(f71,axiom,
! [X0,X1] :
( class_Groups_Ocomm__monoid__add(X1)
=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_add__poly__code_I1_J) ).
fof(f77,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,c_Polynomial_OpCons(X3,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0)),c_Polynomial_OpCons(X3,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_offset__poly__pCons) ).
fof(f998,axiom,
! [X0] :
( class_Rings_Ocomm__semiring__0(X0)
=> class_Groups_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clrel_Rings_Ocomm__semiring__0__Groups_Ocomm__monoid__add) ).
fof(f1180,conjecture,
c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1181,negated_conjecture,
c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h) != c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
inference(negated_conjecture,[status(cth)],[f1180]) ).
fof(f1182,axiom,
class_Rings_Ocomm__semiring__0(t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0) ).
fof(f1186,plain,
c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) != c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h),
inference(flattening,[],[f1181]) ).
fof(f1294,plain,
! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f1340,plain,
! [X0,X1] :
( c_Polynomial_Osmult(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(ennf_transformation,[],[f38]) ).
fof(f1370,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0) = X0
| ~ class_Groups_Ocomm__monoid__add(X1) ),
inference(ennf_transformation,[],[f71]) ).
fof(f1373,plain,
! [X0,X1,X2,X3] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,c_Polynomial_OpCons(X3,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0)),c_Polynomial_OpCons(X3,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0)))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f77]) ).
fof(f2317,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(ennf_transformation,[],[f998]) ).
fof(f2703,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0)
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(cnf_transformation,[],[f1294]) ).
fof(f2761,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)) = c_Polynomial_Osmult(X1,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)))
| ~ class_Rings_Ocomm__semiring__0(X1) ),
inference(cnf_transformation,[],[f1340]) ).
fof(f2801,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)),X0) = X0
| ~ class_Groups_Ocomm__monoid__add(X1) ),
inference(cnf_transformation,[],[f1370]) ).
fof(f2808,plain,
! [X2,X3,X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,c_Polynomial_OpCons(X3,X2,X1),X0) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0)),c_Polynomial_OpCons(X3,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X3,X1,X0)))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(cnf_transformation,[],[f1373]) ).
fof(f3956,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[],[f2317]) ).
fof(f4136,plain,
c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) != c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h),
inference(cnf_transformation,[],[f1186]) ).
fof(f4137,plain,
class_Rings_Ocomm__semiring__0(t_a),
inference(cnf_transformation,[],[f1182]) ).
fof(f4487,definition,
( spl30_1
<=> c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f4489,plain,
( c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) != c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),v_h)
| spl30_1 ),
inference(avatar_component_clause,[],[f4487]) ).
fof(f4490,plain,
~ spl30_1,
inference(avatar_split_clause,[],[f4136,f4487]) ).
fof(f4545,definition,
( spl30_2
<=> class_Rings_Ocomm__semiring__0(t_a) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f4547,plain,
( class_Rings_Ocomm__semiring__0(t_a)
| ~ spl30_2 ),
inference(avatar_component_clause,[],[f4545]) ).
fof(f4548,plain,
spl30_2,
inference(avatar_split_clause,[],[f4137,f4545]) ).
fof(f4557,plain,
( ! [X0] : c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Polynomial_Osmult(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))
| ~ spl30_2 ),
inference(resolution,[],[f4547,f2761]) ).
fof(f4564,plain,
( ! [X2,X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)),c_Polynomial_OpCons(t_a,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)))
| ~ spl30_2 ),
inference(resolution,[],[f4547,f2808]) ).
fof(f4589,plain,
( class_Groups_Ocomm__monoid__add(t_a)
| ~ spl30_2 ),
inference(resolution,[],[f4547,f3956]) ).
fof(f4617,definition,
( spl30_4
<=> ! [X2,X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)),c_Polynomial_OpCons(t_a,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2))) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
fof(f4618,plain,
( ! [X2,X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,X1),X2) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X2,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)),c_Polynomial_OpCons(t_a,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2)))
| ~ spl30_4 ),
inference(avatar_component_clause,[],[f4617]) ).
fof(f4619,plain,
( spl30_4
| ~ spl30_2 ),
inference(avatar_split_clause,[],[f4564,f4545,f4617]) ).
fof(f4624,plain,
( ! [X0,X1] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ class_Rings_Ocomm__semiring__0(t_a) )
| ~ spl30_4 ),
inference(superposition,[],[f4618,f2703]) ).
fof(f4734,plain,
( ! [X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ spl30_2
| ~ spl30_4 ),
inference(forward_subsumption_resolution,[],[f4624,f4547]) ).
fof(f4737,plain,
( ! [X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ spl30_2
| ~ spl30_4 ),
inference(forward_demodulation,[],[f4734,f4557]) ).
fof(f4930,definition,
( spl30_9
<=> class_Groups_Ocomm__monoid__add(t_a) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
fof(f4932,plain,
( class_Groups_Ocomm__monoid__add(t_a)
| ~ spl30_9 ),
inference(avatar_component_clause,[],[f4930]) ).
fof(f4933,plain,
( spl30_9
| ~ spl30_2 ),
inference(avatar_split_clause,[],[f4589,f4545,f4930]) ).
fof(f4935,definition,
( spl30_10
<=> ! [X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))) ),
introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition]) ).
fof(f4936,plain,
( ! [X0,X1] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ spl30_10 ),
inference(avatar_component_clause,[],[f4935]) ).
fof(f4937,plain,
( spl30_10
| ~ spl30_2
| ~ spl30_4 ),
inference(avatar_split_clause,[],[f4737,f4617,f4545,f4935]) ).
fof(f5005,plain,
( ! [X0,X1] :
( c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)
| ~ class_Groups_Ocomm__monoid__add(t_a) )
| ~ spl30_10 ),
inference(superposition,[],[f2801,f4936]) ).
fof(f5116,plain,
( ! [X0,X1] : c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X1)
| ~ spl30_9
| ~ spl30_10 ),
inference(forward_subsumption_resolution,[],[f5005,f4932]) ).
fof(f5130,plain,
( $false
| spl30_1
| ~ spl30_9
| ~ spl30_10 ),
inference(backward_subsumption_resolution,[],[f4489,f5116]) ).
fof(f5131,plain,
( spl30_1
| ~ spl30_9
| ~ spl30_10 ),
inference(avatar_contradiction_clause,[],[f5130]) ).
cnf(s1,plain,
~ spl30_1,
inference(sat_conversion,[],[f4490]) ).
cnf(s2,plain,
spl30_2,
inference(sat_conversion,[],[f4548]) ).
cnf(s4,plain,
( ~ spl30_2
| spl30_4 ),
inference(sat_conversion,[],[f4619]) ).
cnf(s9,plain,
( ~ spl30_2
| spl30_9 ),
inference(sat_conversion,[],[f4933]) ).
cnf(s10,plain,
( ~ spl30_2
| ~ spl30_4
| spl30_10 ),
inference(sat_conversion,[],[f4937]) ).
cnf(s12,plain,
( spl30_1
| ~ spl30_9
| ~ spl30_10 ),
inference(sat_conversion,[],[f5131]) ).
cnf(s14,plain,
spl30_9,
inference(rat,[],[s9,s2]) ).
cnf(s15,plain,
spl30_4,
inference(rat,[],[s4,s2]) ).
cnf(s17,plain,
spl30_10,
inference(rat,[],[s10,s2,s15]) ).
cnf(s18,plain,
spl30_1,
inference(rat,[],[s12,s14,s17]) ).
cnf(s19,plain,
$false,
inference(rat,[],[s1,s18]) ).
fof(f5134,plain,
$false,
inference(avatar_sat_refutation,[],[s19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW182+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n007.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 13:10:41 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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
% 5.03/1.46 % (2386585)Detected formulas, will run a generic FOF schedule.
% 5.03/1.46 % (2386592)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3826567484:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.03/1.46 % (2386590)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=3871149284:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.03/1.46 % (2386596)dis-21_1_sil=8000:lcm=predicate:random_seed=414998219:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.03/1.46 % (2386595)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3514414043:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.03/1.46 % (2386594)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=111203605:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.03/1.46 % (2386593)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1558336695:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.03/1.46 % (2386591)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4113704863:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.03/1.46 % (2386593)Refutation not found, incomplete strategy
% 5.03/1.46 % (2386593)------------------------------
% 5.03/1.46 % (2386593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386593)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386593)Termination reason: Refutation not found, incomplete strategy
% 5.03/1.46 % (2386593)Time elapsed: 0.004 s
% 5.03/1.46 % (2386593)Peak memory usage: 89 MB
% 5.03/1.46 % (2386593)Instructions burned: 5 (million)
% 5.03/1.46 % (2386596)Instruction limit reached!
% 5.03/1.46 % (2386596)------------------------------
% 5.03/1.46 % (2386596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386596)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386596)Termination reason: Instruction limit
% 5.03/1.46 % (2386596)Termination phase: Saturation
% 5.03/1.46 % (2386596)Time elapsed: 0.069 s
% 5.03/1.46 % (2386596)Peak memory usage: 91 MB
% 5.03/1.46 % (2386596)Instructions burned: 130 (million)
% 5.03/1.46 % (2386594)Instruction limit reached!
% 5.03/1.46 % (2386594)------------------------------
% 5.03/1.46 % (2386594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386594)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386594)Termination reason: Instruction limit
% 5.03/1.46 % (2386594)Termination phase: Saturation
% 5.03/1.46 % (2386594)Time elapsed: 0.074 s
% 5.03/1.46 % (2386594)Peak memory usage: 89 MB
% 5.03/1.46 % (2386594)Instructions burned: 124 (million)
% 5.03/1.46 % (2386595)Instruction limit reached!
% 5.03/1.46 % (2386595)------------------------------
% 5.03/1.46 % (2386595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386595)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386595)Termination reason: Instruction limit
% 5.03/1.46 % (2386595)Termination phase: Saturation
% 5.03/1.46 % (2386595)Time elapsed: 0.091 s
% 5.03/1.46 % (2386595)Peak memory usage: 91 MB
% 5.03/1.46 % (2386595)Instructions burned: 139 (million)
% 5.03/1.46 % (2386604)lrs+10_1_sil=8000:sp=occurrence:random_seed=2181463207:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.03/1.46 % (2386605)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4097033537:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.03/1.46 % (2386605)Refutation not found, incomplete strategy
% 5.03/1.46 % (2386605)------------------------------
% 5.03/1.46 % (2386605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386605)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386605)Termination reason: Refutation not found, incomplete strategy
% 5.03/1.46 % (2386605)Time elapsed: 0.009 s
% 5.03/1.46 % (2386605)Peak memory usage: 89 MB
% 5.03/1.46 % (2386605)Instructions burned: 17 (million)
% 5.03/1.46 % (2386606)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2672793186:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.03/1.46 % (2386593)------------------------------
% 5.03/1.46 % (2386593)------------------------------
% 5.03/1.46 % (2386604)Instruction limit reached!
% 5.03/1.46 % (2386604)------------------------------
% 5.03/1.46 % (2386604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386604)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386604)Termination reason: Instruction limit
% 5.03/1.46 % (2386604)Termination phase: Saturation
% 5.03/1.46 % (2386604)Time elapsed: 0.185 s
% 5.03/1.46 % (2386604)Peak memory usage: 92 MB
% 5.03/1.46 % (2386604)Instructions burned: 285 (million)
% 5.03/1.46 % (2386610)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=304144681:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.03/1.46 % (2386606)Instruction limit reached!
% 5.03/1.46 % (2386606)------------------------------
% 5.03/1.46 % (2386606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386606)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386606)Termination reason: Instruction limit
% 5.03/1.46 % (2386606)Termination phase: Saturation
% 5.03/1.46 % (2386606)Time elapsed: 0.185 s
% 5.03/1.46 % (2386606)Peak memory usage: 92 MB
% 5.03/1.46 % (2386606)Instructions burned: 326 (million)
% 5.03/1.46 % (2386592)First to succeed.
% 5.03/1.46 % (2386592)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2386585"
% 5.03/1.46 % (2386605)------------------------------
% 5.03/1.46 % (2386605)------------------------------
% 5.03/1.46 % (2386611)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1829153507:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.03/1.46 % (2386610)Instruction limit reached!
% 5.03/1.46 % (2386610)------------------------------
% 5.03/1.46 % (2386610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.03/1.46 % (2386610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.03/1.46 % (2386610)CaDiCaL version: 2.1.3
% 5.03/1.46 % (2386610)Termination reason: Instruction limit
% 5.03/1.46 % (2386610)Termination phase: Saturation
% 5.03/1.46 % (2386610)Time elapsed: 0.130 s
% 5.03/1.46 % (2386610)Peak memory usage: 92 MB
% 5.03/1.46 % (2386610)Instructions burned: 248 (million)
% 5.03/1.46 % (2386611)Also succeeded, but the first one will report.
% 5.03/1.46 % (2386613)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2977851999:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.03/1.46 % (2386614)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=963998195:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.03/1.46 % (2386592)Refutation found. Thanks to Tanya!
% 5.03/1.46 % SZS status Theorem for theBenchmark
% 5.03/1.46 % SZS output start Proof for theBenchmark
% See solution above
% 5.98/1.65 % (2386592)------------------------------
% 5.98/1.65 % (2386592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.98/1.65 % (2386592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.98/1.65 % (2386592)CaDiCaL version: 2.1.3
% 5.98/1.65 % (2386592)Termination reason: Refutation
% 5.98/1.65 % (2386592)Time elapsed: 0.482 s
% 5.98/1.65 % (2386592)Peak memory usage: 147 MB
% 5.98/1.65 % (2386592)Instructions burned: 1337 (million)
% 5.98/1.65 % (2386592)------------------------------
% 5.98/1.65 % (2386592)------------------------------
% 5.98/1.65 % (2386585)Success in time 0.797 s
% 5.98/1.65 % Vampire exiting
%------------------------------------------------------------------------------