%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW186+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 : n012.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 4.78s 1.05s
% Output : Refutation 5.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of formulae : 87 ( 15 unt; 6 def)
% Number of atoms : 203 ( 72 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 208 ( 92 ~; 92 |; 8 &)
% ( 8 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 7 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 49 ( 0 sgn 49 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2,X3] :
( class_Rings_Ocomm__semiring__0(X3)
=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X1),c_Polynomial_OpCons(X3,X0,X1)) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
=> X1 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_offset__poly__eq__0__lemma) ).
fof(f12,axiom,
! [X0,X1,X2] :
( class_Groups_Ozero(X2)
=> ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_pCons__eq__0__iff) ).
fof(f14,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(f16,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(f997,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(f1003,axiom,
! [X0] :
( class_Rings_Ocomm__semiring__0(X0)
=> class_Groups_Ozero(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clrel_Rings_Ocomm__semiring__0__Groups_Ozero) ).
fof(f1179,axiom,
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1180,axiom,
c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,v_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)),c_Polynomial_OpCons(t_a,v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f1181,conjecture,
( v_a = c_Groups_Ozero__class_Ozero(t_a)
& v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_2) ).
fof(f1182,negated_conjecture,
~ ( v_a = c_Groups_Ozero__class_Ozero(t_a)
& v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(negated_conjecture,[status(cth)],[f1181]) ).
fof(f1183,axiom,
class_Rings_Ocomm__semiring__0(t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0) ).
fof(f1294,plain,
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(ennf_transformation,[],[f1179]) ).
fof(f1295,plain,
( v_a != c_Groups_Ozero__class_Ozero(t_a)
| v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(ennf_transformation,[],[f1182]) ).
fof(f1398,plain,
! [X0,X1,X2] :
( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
<=> ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) ) )
| ~ class_Groups_Ozero(X2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f1403,plain,
! [X0,X1,X2,X3] :
( X1 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X1),c_Polynomial_OpCons(X3,X0,X1)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(ennf_transformation,[],[f5]) ).
fof(f1404,plain,
! [X0,X1,X2,X3] :
( X1 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X1),c_Polynomial_OpCons(X3,X0,X1)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(flattening,[],[f1403]) ).
fof(f1421,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,[],[f16]) ).
fof(f1478,plain,
! [X0] :
( class_Groups_Ozero(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(ennf_transformation,[],[f1003]) ).
fof(f1479,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(ennf_transformation,[],[f997]) ).
fof(f1847,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,[],[f14]) ).
fof(f1905,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Groups_Ozero__class_Ozero(X2) != X1
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0 )
& ( ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_OpCons(X2,X1,X0) ) )
| ~ class_Groups_Ozero(X2) ),
inference(nnf_transformation,[],[f1398]) ).
fof(f1906,plain,
! [X0,X1,X2] :
( ( ( c_Polynomial_OpCons(X2,X1,X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2))
| c_Groups_Ozero__class_Ozero(X2) != X1
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != X0 )
& ( ( X1 = c_Groups_Ozero__class_Ozero(X2)
& X0 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_OpCons(X2,X1,X0) ) )
| ~ class_Groups_Ozero(X2) ),
inference(flattening,[],[f1905]) ).
fof(f2026,plain,
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(cnf_transformation,[],[f1294]) ).
fof(f2027,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,v_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h)),c_Polynomial_OpCons(t_a,v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h))),
inference(cnf_transformation,[],[f1180]) ).
fof(f2028,plain,
( v_a != c_Groups_Ozero__class_Ozero(t_a)
| v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(cnf_transformation,[],[f1295]) ).
fof(f2029,plain,
class_Rings_Ocomm__semiring__0(t_a),
inference(cnf_transformation,[],[f1183]) ).
fof(f2205,plain,
! [X2,X0,X1] :
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X2)) != c_Polynomial_OpCons(X2,X1,X0)
| c_Groups_Ozero__class_Ozero(X2) = X1
| ~ class_Groups_Ozero(X2) ),
inference(cnf_transformation,[],[f1906]) ).
fof(f2210,plain,
! [X2,X3,X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X3),c_Polynomial_Osmult(X3,X2,X1),c_Polynomial_OpCons(X3,X0,X1)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3)) = X1
| ~ class_Rings_Ocomm__semiring__0(X3) ),
inference(cnf_transformation,[],[f1404]) ).
fof(f2226,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,[],[f1421]) ).
fof(f2349,plain,
! [X0] :
( class_Groups_Ozero(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[],[f1478]) ).
fof(f2350,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f2818,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,[],[f1847]) ).
fof(f3079,definition,
( spl11_1
<=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f3080,plain,
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ spl11_1 ),
inference(avatar_component_clause,[],[f3079]) ).
fof(f3083,definition,
( spl11_2
<=> v_a = c_Groups_Ozero__class_Ozero(t_a) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
fof(f3085,plain,
( v_a != c_Groups_Ozero__class_Ozero(t_a)
| spl11_2 ),
inference(avatar_component_clause,[],[f3083]) ).
fof(f3086,plain,
( ~ spl11_1
| ~ spl11_2 ),
inference(avatar_split_clause,[],[f2028,f3083,f3079]) ).
fof(f3088,definition,
( spl11_3
<=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
fof(f3089,plain,
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ spl11_3 ),
inference(avatar_component_clause,[],[f3088]) ).
fof(f3090,plain,
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| spl11_3 ),
inference(avatar_component_clause,[],[f3088]) ).
fof(f3091,plain,
( ~ spl11_3
| spl11_1 ),
inference(avatar_split_clause,[],[f2026,f3079,f3088]) ).
fof(f3092,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ class_Rings_Ocomm__semiring__0(t_a) ),
inference(superposition,[],[f2210,f2027]) ).
fof(f3126,plain,
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ class_Rings_Ocomm__semiring__0(t_a) ),
inference(trivial_inequality_removal,[],[f3092]) ).
fof(f3220,definition,
( spl11_24
<=> class_Groups_Ocomm__monoid__add(t_a) ),
introduced(definition,[new_symbols(definition,[spl11_24])],[avatar_definition]) ).
fof(f3221,plain,
( class_Groups_Ocomm__monoid__add(t_a)
| ~ spl11_24 ),
inference(avatar_component_clause,[],[f3220]) ).
fof(f3222,plain,
( ~ class_Groups_Ocomm__monoid__add(t_a)
| spl11_24 ),
inference(avatar_component_clause,[],[f3220]) ).
fof(f3259,plain,
( ~ class_Rings_Ocomm__semiring__0(t_a)
| spl11_3 ),
inference(forward_subsumption_resolution,[],[f3126,f3090]) ).
fof(f3260,plain,
( $false
| spl11_3 ),
inference(forward_subsumption_resolution,[],[f3259,f2029]) ).
fof(f3261,plain,
spl11_3,
inference(avatar_contradiction_clause,[],[f3260]) ).
fof(f3262,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),v_h)
| ~ spl11_1
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3089,f3080]) ).
fof(f3285,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,v_h,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),v_h)),c_Polynomial_OpCons(t_a,v_a,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),v_h)))
| ~ spl11_1 ),
inference(superposition,[],[f2027,f3080]) ).
fof(f3286,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Polynomial_Osmult(t_a,v_h,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ spl11_1
| ~ spl11_3 ),
inference(forward_demodulation,[],[f3285,f3262]) ).
fof(f3334,definition,
( spl11_35
<=> class_Groups_Ozero(t_a) ),
introduced(definition,[new_symbols(definition,[spl11_35])],[avatar_definition]) ).
fof(f3335,plain,
( class_Groups_Ozero(t_a)
| ~ spl11_35 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3336,plain,
( ~ class_Groups_Ozero(t_a)
| spl11_35 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3364,plain,
( ~ class_Rings_Ocomm__semiring__0(t_a)
| spl11_35 ),
inference(resolution,[],[f3336,f2349]) ).
fof(f3365,plain,
( $false
| spl11_35 ),
inference(forward_subsumption_resolution,[],[f3364,f2029]) ).
fof(f3366,plain,
spl11_35,
inference(avatar_contradiction_clause,[],[f3365]) ).
fof(f3395,definition,
( spl11_41
<=> c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
introduced(definition,[new_symbols(definition,[spl11_41])],[avatar_definition]) ).
fof(f3396,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))
| spl11_41 ),
inference(avatar_component_clause,[],[f3395]) ).
fof(f3397,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))
| ~ spl11_41 ),
inference(avatar_component_clause,[],[f3395]) ).
fof(f3578,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = 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,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ class_Rings_Ocomm__semiring__0(t_a)
| ~ spl11_1
| ~ spl11_3 ),
inference(superposition,[],[f3286,f2226]) ).
fof(f3614,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = 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,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))
| ~ spl11_1
| ~ spl11_3 ),
inference(forward_subsumption_resolution,[],[f3578,f2029]) ).
fof(f3615,plain,
( ~ class_Rings_Ocomm__semiring__0(t_a)
| spl11_24 ),
inference(resolution,[],[f3222,f2350]) ).
fof(f3616,plain,
( $false
| spl11_24 ),
inference(forward_subsumption_resolution,[],[f3615,f2029]) ).
fof(f3617,plain,
spl11_24,
inference(avatar_contradiction_clause,[],[f3616]) ).
fof(f4274,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))
| ~ class_Groups_Ocomm__monoid__add(t_a)
| ~ spl11_1
| ~ spl11_3 ),
inference(superposition,[],[f3614,f2818]) ).
fof(f4318,plain,
( ~ class_Groups_Ocomm__monoid__add(t_a)
| ~ spl11_1
| ~ spl11_3
| spl11_41 ),
inference(forward_subsumption_resolution,[],[f4274,f3396]) ).
fof(f4325,plain,
( $false
| ~ spl11_1
| ~ spl11_3
| ~ spl11_24
| spl11_41 ),
inference(forward_subsumption_resolution,[],[f4318,f3221]) ).
fof(f4326,plain,
( ~ spl11_1
| ~ spl11_3
| ~ spl11_24
| spl11_41 ),
inference(avatar_contradiction_clause,[],[f4325]) ).
fof(f4347,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_a = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Groups_Ozero(t_a)
| ~ spl11_41 ),
inference(superposition,[],[f2205,f3397]) ).
fof(f4353,plain,
( v_a = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Groups_Ozero(t_a)
| ~ spl11_41 ),
inference(trivial_inequality_removal,[],[f4347]) ).
fof(f4358,plain,
( ~ class_Groups_Ozero(t_a)
| spl11_2
| ~ spl11_41 ),
inference(forward_subsumption_resolution,[],[f4353,f3085]) ).
fof(f4373,plain,
( $false
| spl11_2
| ~ spl11_35
| ~ spl11_41 ),
inference(forward_subsumption_resolution,[],[f4358,f3335]) ).
fof(f4374,plain,
( spl11_2
| ~ spl11_35
| ~ spl11_41 ),
inference(avatar_contradiction_clause,[],[f4373]) ).
cnf(s1,plain,
( ~ spl11_1
| ~ spl11_2 ),
inference(sat_conversion,[],[f3086]) ).
cnf(s2,plain,
( spl11_1
| ~ spl11_3 ),
inference(sat_conversion,[],[f3091]) ).
cnf(s30,plain,
spl11_3,
inference(sat_conversion,[],[f3261]) ).
cnf(s39,plain,
spl11_35,
inference(sat_conversion,[],[f3366]) ).
cnf(s50,plain,
spl11_24,
inference(sat_conversion,[],[f3617]) ).
cnf(s72,plain,
( ~ spl11_1
| ~ spl11_3
| ~ spl11_24
| spl11_41 ),
inference(sat_conversion,[],[f4326]) ).
cnf(s73,plain,
( spl11_2
| ~ spl11_35
| ~ spl11_41 ),
inference(sat_conversion,[],[f4374]) ).
cnf(s86,plain,
spl11_1,
inference(rat,[],[s2,s30]) ).
cnf(s87,plain,
spl11_41,
inference(rat,[],[s72,s30,s50,s86]) ).
cnf(s90,plain,
spl11_2,
inference(rat,[],[s73,s39,s87]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s1,s90,s86]) ).
fof(f4376,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWW186+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.12 % Computer : n012.cluster.edu
% 0.05/0.12 % Model : x86_64 x86_64
% 0.05/0.12 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.12 % Memory : 8046.5625MB
% 0.05/0.12 % OS : Linux 6.8.0-71-generic
% 0.05/0.12 % CPULimit : 300
% 0.05/0.12 % WCLimit : 300
% 0.05/0.12 % DateTime : Mon Sep 28 13:12:34 UTC 2026
% 0.05/0.12 % CPUTime :
% 0.05/0.12 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.14 Running first-order theorem proving
% 0.05/0.14 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
% 4.78/1.04 % (3370443)Detected formulas, will run a generic FOF schedule.
% 4.78/1.04 % (3370451)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=128868931:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.78/1.04 % (3370454)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2388584944:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.78/1.04 % (3370450)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=391933275:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.78/1.04 % (3370453)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1425289837:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.78/1.04 % (3370452)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2126557120:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.78/1.04 % (3370455)dis-21_1_sil=8000:lcm=predicate:random_seed=3107928976: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)
% 4.78/1.04 % (3370449)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=1825932685:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.78/1.04 % (3370455)Instruction limit reached!
% 4.78/1.04 % (3370455)------------------------------
% 4.78/1.04 % (3370455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370455)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370455)Termination reason: Instruction limit
% 4.78/1.04 % (3370455)Termination phase: Saturation
% 4.78/1.04 % (3370455)Time elapsed: 0.038 s
% 4.78/1.04 % (3370455)Peak memory usage: 90 MB
% 4.78/1.04 % (3370455)Instructions burned: 137 (million)
% 4.78/1.04 % (3370452)Instruction limit reached!
% 4.78/1.04 % (3370452)------------------------------
% 4.78/1.04 % (3370452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370452)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370452)Termination reason: Instruction limit
% 4.78/1.04 % (3370452)Termination phase: Saturation
% 4.78/1.04 % (3370452)Time elapsed: 0.038 s
% 4.78/1.04 % (3370452)Peak memory usage: 91 MB
% 4.78/1.04 % (3370452)Instructions burned: 120 (million)
% 4.78/1.04 % (3370453)Instruction limit reached!
% 4.78/1.04 % (3370453)------------------------------
% 4.78/1.04 % (3370453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370453)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370453)Termination reason: Instruction limit
% 4.78/1.04 % (3370453)Termination phase: Saturation
% 4.78/1.04 % (3370453)Time elapsed: 0.038 s
% 4.78/1.04 % (3370453)Peak memory usage: 89 MB
% 4.78/1.04 % (3370453)Instructions burned: 123 (million)
% 4.78/1.04 % (3370454)Instruction limit reached!
% 4.78/1.04 % (3370454)------------------------------
% 4.78/1.04 % (3370454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370454)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370454)Termination reason: Instruction limit
% 4.78/1.04 % (3370454)Termination phase: Saturation
% 4.78/1.04 % (3370454)Time elapsed: 0.043 s
% 4.78/1.04 % (3370454)Peak memory usage: 91 MB
% 4.78/1.04 % (3370454)Instructions burned: 141 (million)
% 4.78/1.04 % (3370463)lrs+10_1_sil=8000:sp=occurrence:random_seed=3857506688:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.78/1.04 % (3370465)lrs+1011_1_sil=32000:sp=occurrence:random_seed=680074431:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 4.78/1.04 % (3370464)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2518517492:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 4.78/1.04 % (3370464)Refutation not found, incomplete strategy
% 4.78/1.04 % (3370464)------------------------------
% 4.78/1.04 % (3370464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370464)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370464)Termination reason: Refutation not found, incomplete strategy
% 4.78/1.04 % (3370464)Time elapsed: 0.004 s
% 4.78/1.04 % (3370464)Peak memory usage: 89 MB
% 4.78/1.04 % (3370464)Instructions burned: 16 (million)
% 4.78/1.04 % (3370466)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=4016098816:s2a=on:i=248:s2at=1.23:gtg=position_2998 on theBenchmark for (2998ds/248Mi)
% 4.78/1.04 % (3370466)Instruction limit reached!
% 4.78/1.04 % (3370466)------------------------------
% 4.78/1.04 % (3370466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.04 % (3370466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.04 % (3370466)CaDiCaL version: 2.1.3
% 4.78/1.04 % (3370466)Termination reason: Instruction limit
% 4.78/1.04 % (3370466)Termination phase: Saturation
% 4.78/1.04 % (3370466)Time elapsed: 0.072 s
% 4.78/1.04 % (3370466)Peak memory usage: 92 MB
% 4.78/1.04 % (3370466)Instructions burned: 249 (million)
% 4.78/1.04 % (3370463)Instruction limit reached!
% 4.78/1.05 % (3370463)------------------------------
% 4.78/1.05 % (3370463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.05 % (3370463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.05 % (3370463)CaDiCaL version: 2.1.3
% 4.78/1.05 % (3370463)Termination reason: Instruction limit
% 4.78/1.05 % (3370463)Termination phase: Saturation
% 4.78/1.05 % (3370463)Time elapsed: 0.100 s
% 4.78/1.05 % (3370463)Peak memory usage: 92 MB
% 4.78/1.05 % (3370463)Instructions burned: 287 (million)
% 4.78/1.05 % (3370465)Instruction limit reached!
% 4.78/1.05 % (3370465)------------------------------
% 4.78/1.05 % (3370465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.05 % (3370465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.05 % (3370465)CaDiCaL version: 2.1.3
% 4.78/1.05 % (3370465)Termination reason: Instruction limit
% 4.78/1.05 % (3370465)Termination phase: Saturation
% 4.78/1.05 % (3370465)Time elapsed: 0.107 s
% 4.78/1.05 % (3370465)Peak memory usage: 92 MB
% 4.78/1.05 % (3370465)Instructions burned: 325 (million)
% 4.78/1.05 % (3370464)------------------------------
% 4.78/1.05 % (3370464)------------------------------
% 4.78/1.05 % (3370471)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2368249802:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 4.78/1.05 % (3370472)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1374673692:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 4.78/1.05 % (3370473)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1142183888:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 4.78/1.05 % (3370471)First to succeed.
% 4.78/1.05 % (3370471)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3370443"
% 4.78/1.05 % (3370473)Instruction limit reached!
% 4.78/1.05 % (3370473)------------------------------
% 4.78/1.05 % (3370473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.05 % (3370473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.05 % (3370473)CaDiCaL version: 2.1.3
% 4.78/1.05 % (3370473)Termination reason: Instruction limit
% 4.78/1.05 % (3370473)Termination phase: Saturation
% 4.78/1.05 % (3370473)Time elapsed: 0.032 s
% 4.78/1.05 % (3370473)Peak memory usage: 91 MB
% 4.78/1.05 % (3370473)Instructions burned: 113 (million)
% 4.78/1.05 % (3370474)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2218166967:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 4.78/1.05 % (3370474)Instruction limit reached!
% 4.78/1.05 % (3370474)------------------------------
% 4.78/1.05 % (3370474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.78/1.05 % (3370474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.78/1.05 % (3370474)CaDiCaL version: 2.1.3
% 4.78/1.05 % (3370474)Termination reason: Instruction limit
% 4.78/1.05 % (3370474)Termination phase: Saturation
% 4.78/1.05 % (3370474)Time elapsed: 0.035 s
% 4.78/1.05 % (3370474)Peak memory usage: 90 MB
% 4.78/1.05 % (3370474)Instructions burned: 131 (million)
% 4.78/1.05 % (3370449)Also succeeded, but the first one will report.
% 4.78/1.05 % (3370450)Also succeeded, but the first one will report.
% 4.78/1.05 % (3370451)Also succeeded, but the first one will report.
% 4.78/1.05 % (3370478)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1926196240:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 4.78/1.05 % (3370471)Refutation found. Thanks to Tanya!
% 4.78/1.05 % SZS status Theorem for theBenchmark
% 4.78/1.05 % SZS output start Proof for theBenchmark
% See solution above
% 5.11/1.14 % (3370471)------------------------------
% 5.11/1.14 % (3370471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.14 % (3370471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.14 % (3370471)CaDiCaL version: 2.1.3
% 5.11/1.14 % (3370471)Termination reason: Refutation
% 5.11/1.14 % (3370471)Time elapsed: 0.038 s
% 5.11/1.14 % (3370471)Peak memory usage: 92 MB
% 5.11/1.14 % (3370471)Instructions burned: 119 (million)
% 5.11/1.14 % (3370471)------------------------------
% 5.11/1.14 % (3370471)------------------------------
% 5.11/1.14 % (3370443)Success in time 0.712 s
% 5.11/1.14 % Vampire exiting
%------------------------------------------------------------------------------