%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW186+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 03:07:24 PM UTC 2026
% Result : Theorem 2.71s 0.90s
% Output : CNFRefutation 3.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of formulae : 86 ( 24 unt; 7 def)
% Number of atoms : 168 ( 92 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 141 ( 59 ~; 56 |; 8 &)
% ( 9 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 94 ( 94 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [V_h,V_p,V_a,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h) = 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))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [V_a,V_p,V_c,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p)) = 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/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [V_pa_2,V_a_2,T_b] :
( class_Groups_Ozero(T_b)
=> ( c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
& V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [V_q,T_a] :
( class_Groups_Ocomm__monoid__add(T_a)
=> c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_q) = V_q ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [V_a,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f997,axiom,
! [T] :
( class_Rings_Ocomm__semiring__0(T)
=> class_Groups_Ocomm__monoid__add(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1003,axiom,
! [T] :
( class_Rings_Ocomm__semiring__0(T)
=> class_Groups_Ozero(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1179,hypothesis,
( 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/sandbox/benchmark/theBenchmark.p') ).
fof(f1180,hypothesis,
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/sandbox/benchmark/theBenchmark.p') ).
fof(f1181,conjecture,
( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
& v_a = c_Groups_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1182,negated_conjecture,
~ ( v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
& v_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(negated_conjecture,[status(cth)],[f1181]) ).
fof(f1183,hypothesis,
class_Rings_Ocomm__semiring__0(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1193,plain,
! [V_h,V_p,V_a,T_a] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h) = 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)))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f1194,plain,
! [T_a] :
( ! [V_h,V_p,V_a] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(T_a,c_Polynomial_OpCons(T_a,V_a,V_p),V_h) = 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)))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1193]) ).
fof(f1195,plain,
! [X0,X1,X2,X3] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,c_Polynomial_OpCons(X0,X1,X2),X3) = c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Polynomial_Osmult(X0,X3,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X2,X3)),c_Polynomial_OpCons(X0,X1,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(X0,X2,X3)))
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1194]) ).
fof(f1196,plain,
! [V_a,V_p,V_c,T_a] :
( V_p = 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_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f1197,plain,
! [T_a] :
( ! [V_p] :
( V_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ! [V_a,V_c] : c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Polynomial_Osmult(T_a,V_c,V_p),c_Polynomial_OpCons(T_a,V_a,V_p)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) )
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1196]) ).
fof(f1198,plain,
! [X0,X1,X2,X3] :
( X2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Polynomial_Osmult(X0,X1,X2),c_Polynomial_OpCons(X0,X3,X2)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1197]) ).
fof(f1219,plain,
! [V_pa_2,V_a_2,T_b] :
( ( c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
& V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Groups_Ozero(T_b) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f1220,plain,
! [V_pa_2,V_a_2,T_b] :
( ( ( V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
| V_a_2 != c_Groups_Ozero__class_Ozero(T_b)
| c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) )
& ( ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
& V_a_2 = c_Groups_Ozero__class_Ozero(T_b) )
| c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) )
| ~ class_Groups_Ozero(T_b) ),
inference(NNF_transformation,[status(thm)],[f1219]) ).
fof(f1221,plain,
! [T_b] :
( ( ! [V_pa_2,V_a_2] :
( V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
| V_a_2 != c_Groups_Ozero__class_Ozero(T_b)
| c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) )
& ! [V_pa_2,V_a_2] :
( ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
& V_a_2 = c_Groups_Ozero__class_Ozero(T_b) )
| c_Polynomial_OpCons(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) )
| ~ class_Groups_Ozero(T_b) ),
inference(miniscoping,[status(thm)],[f1220]) ).
fof(f1222,plain,
! [X0,X1,X2] :
( X1 = c_Groups_Ozero__class_Ozero(X0)
| c_Polynomial_OpCons(X0,X1,X2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Groups_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
fof(f1228,plain,
! [V_q,T_a] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_q) = V_q
| ~ class_Groups_Ocomm__monoid__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f1229,plain,
! [T_a] :
( ! [V_q] : c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),V_q) = V_q
| ~ class_Groups_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f1228]) ).
fof(f1230,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X1) = X1
| ~ class_Groups_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1229]) ).
fof(f1234,plain,
! [V_a,T_a] :
( c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f1235,plain,
! [T_a] :
( ! [V_a] : c_Polynomial_Osmult(T_a,V_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1234]) ).
fof(f1236,plain,
! [X0,X1] :
( c_Polynomial_Osmult(X0,X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1235]) ).
fof(f4382,plain,
! [T] :
( class_Groups_Ocomm__monoid__add(T)
| ~ class_Rings_Ocomm__semiring__0(T) ),
inference(pre_NNF_transformation,[status(thm)],[f997]) ).
fof(f4383,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f4382]) ).
fof(f4394,plain,
! [T] :
( class_Groups_Ozero(T)
| ~ class_Rings_Ocomm__semiring__0(T) ),
inference(pre_NNF_transformation,[status(thm)],[f1003]) ).
fof(f4395,plain,
! [X0] :
( class_Groups_Ozero(X0)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f4394]) ).
fof(f4644,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(pre_NNF_transformation,[status(thm)],[f1179]) ).
fof(f4645,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,[status(thm)],[f4644]) ).
fof(f4646,plain,
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)),
inference(cnf_transformation,[status(thm)],[f1180]) ).
fof(f4647,plain,
( v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_a != c_Groups_Ozero__class_Ozero(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f1182]) ).
fof(f4648,plain,
( v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_a != c_Groups_Ozero__class_Ozero(t_a) ),
inference(cnf_transformation,[status(thm)],[f4647]) ).
fof(f4649,plain,
class_Rings_Ocomm__semiring__0(t_a),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f4672,definition,
( sQ0_spl
<=> 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,[sQ0_spl])],[split_symbol_definition]) ).
fof(f4675,definition,
( sQ1_spl
<=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f4678,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f4645,f4672,f4675]) ).
fof(f4679,definition,
( sQ2_spl
<=> v_a = c_Groups_Ozero__class_Ozero(t_a) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f4681,plain,
( sQ2_spl
| v_a != c_Groups_Ozero__class_Ozero(t_a) ),
inference(component_clause,[status(thm)],[f4679]) ).
fof(f4682,plain,
( ~ sQ1_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f4648,f4679,f4675]) ).
fof(f4824,plain,
! [X0,X1,X2] : 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))),
inference(resolution,[status(thm)],[f1195,f4649]) ).
fof(f4825,plain,
! [X0,X1,X2] :
( X1 = 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,X0,X1),c_Polynomial_OpCons(t_a,X2,X1)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(resolution,[status(thm)],[f1198,f4649]) ).
fof(f4827,plain,
c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(resolution,[status(thm)],[f4825,f4646]) ).
fof(f4828,plain,
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(paramodulation,[status(thm)],[f4646,f4825]) ).
fof(f4829,definition,
( sQ3_spl
<=> c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f4831,plain,
( sQ3_spl
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(component_clause,[status(thm)],[f4829]) ).
fof(f4832,plain,
( sQ0_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f4828,f4829,f4672]) ).
fof(f4833,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f4831]) ).
fof(f4834,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f4833]) ).
fof(f4835,plain,
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_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(backward_demodulation,[status(thm)],[f4827,f4646]) ).
fof(f4836,plain,
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)))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(forward_demodulation,[status(thm)],[f4827,f4835]) ).
fof(f4840,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) = 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,X0,c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,v_p,v_h))),
inference(paramodulation,[status(thm)],[f4827,f4824]) ).
fof(f4842,plain,
! [X0,X1,X2] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,X1,X2) = 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,X1),X2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(paramodulation,[status(thm)],[f4824,f4825]) ).
fof(f4843,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) = 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,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
inference(forward_demodulation,[status(thm)],[f4827,f4840]) ).
fof(f4845,plain,
c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(backward_demodulation,[status(thm)],[f4843,f4836]) ).
fof(f4847,definition,
! [X0] :
( sQ4_spl
<=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f4848,plain,
! [X0] :
( ~ sQ4_spl
| c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(component_clause,[status(thm)],[f4847]) ).
fof(f4853,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Polynomial_OpCons(t_a,v_a,v_p)),v_h) = 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_Polynomial_OpCons(t_a,v_a,v_p),v_h)),c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
inference(paramodulation,[status(thm)],[f4845,f4824]) ).
fof(f4856,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Polynomial_OpCons(t_a,v_a,v_p)),v_h) = 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,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
inference(forward_demodulation,[status(thm)],[f4845,f4853]) ).
fof(f4857,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,c_Polynomial_OpCons(t_a,v_a,v_p)),v_h) = c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h),
inference(forward_demodulation,[status(thm)],[f4843,f4856]) ).
fof(f4860,plain,
! [X0] :
( c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h) = 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,v_p),v_h) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(paramodulation,[status(thm)],[f4857,f4842]) ).
fof(f4863,definition,
( sQ5_spl
<=> c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f4864,plain,
( ~ sQ5_spl
| c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,v_a,v_p),v_h) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(component_clause,[status(thm)],[f4863]) ).
fof(f4866,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f4860,f4847,f4863]) ).
fof(f4871,plain,
( ~ sQ4_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4845,f4848]) ).
fof(f4872,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f4871]) ).
fof(f5517,plain,
! [X0] : c_Polynomial_Osmult(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(resolution,[status(thm)],[f1236,f4649]) ).
fof(f5520,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) = 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)))),
inference(backward_demodulation,[status(thm)],[f5517,f4843]) ).
fof(f8231,plain,
class_Groups_Ocomm__monoid__add(t_a),
inference(resolution,[status(thm)],[f4383,f4649]) ).
fof(f8238,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),X0) = X0,
inference(resolution,[status(thm)],[f8231,f1230]) ).
fof(f8389,plain,
! [X0] : c_Fundamental__Theorem__Algebra__Mirabelle_Ooffset__poly(t_a,c_Polynomial_OpCons(t_a,X0,v_p),v_h) = c_Polynomial_OpCons(t_a,X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),
inference(backward_demodulation,[status(thm)],[f8238,f5520]) ).
fof(f8600,plain,
( ~ sQ5_spl
| c_Polynomial_OpCons(t_a,v_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(backward_demodulation,[status(thm)],[f8389,f4864]) ).
fof(f8628,definition,
( sQ31_spl
<=> class_Rings_Ocomm__semiring__0(t_a) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f8630,plain,
( sQ31_spl
| ~ class_Rings_Ocomm__semiring__0(t_a) ),
inference(component_clause,[status(thm)],[f8628]) ).
fof(f8635,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8630,f4649]) ).
fof(f8636,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f8635]) ).
fof(f8697,plain,
class_Groups_Ozero(t_a),
inference(resolution,[status(thm)],[f4395,f4649]) ).
fof(f8701,plain,
! [X0,X1] :
( X0 = c_Groups_Ozero__class_Ozero(t_a)
| c_Polynomial_OpCons(t_a,X0,X1) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ),
inference(resolution,[status(thm)],[f8697,f1222]) ).
fof(f8784,plain,
( ~ sQ5_spl
| v_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(resolution,[status(thm)],[f8600,f8701]) ).
fof(f8801,plain,
( ~ sQ5_spl
| sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8784,f4681]) ).
fof(f8802,plain,
( ~ sQ5_spl
| sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f8801]) ).
fof(f8803,plain,
$false,
inference(sat_refutation,[status(thm)],[f4678,f4682,f4832,f4834,f4866,f4872,f8636,f8802]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW186+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:45:44 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.45 % Drodi V4.1.1
% 2.71/0.90 % Refutation found
% 2.71/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.71/0.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.17/0.95 % Elapsed time: 0.588764 seconds
% 3.17/0.95 % CPU time: 3.696872 seconds
% 3.17/0.95 % Total memory used: 265.715 MB
% 3.17/0.95 % Net memory used: 263.933 MB
%------------------------------------------------------------------------------