%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW245+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 : n026.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:30 PM UTC 2026
% Result : Theorem 0.36s 0.69s
% Output : CNFRefutation 0.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 6
% Syntax : Number of formulae : 50 ( 6 unt; 1 def)
% Number of atoms : 200 ( 147 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 252 ( 102 ~; 97 |; 40 &)
% ( 1 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 10 con; 0-4 aty)
% Number of variables : 71 ( 44 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
( class_Rings_Oidom(t_a)
=> ( v_c____ != c_Groups_Ozero__class_Ozero(t_a)
=> ? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( class_Rings_Oidom(t_a)
=> ( v_c____ = c_Groups_Ozero__class_Ozero(t_a)
=> ? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,axiom,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1160,conjecture,
? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1161,negated_conjecture,
~ ? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____))) )
& ( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
=> c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) ),
inference(negated_conjecture,[status(cth)],[f1160]) ).
fof(f1162,hypothesis,
class_Rings_Oidom(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1174,plain,
( ? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f1175,plain,
( ? [B_a] :
( ? [B_k,B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(miniscoping,[status(thm)],[f1174]) ).
fof(f1176,plain,
( ( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),sK4_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK3_skl,sK5_skl)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& sK3_skl != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(B_a,sK3_skl),skolemize(B_k,sK4_skl),skolemize(B_q,sK5_skl)],[f1175]) ).
fof(f1177,plain,
( sK3_skl != c_Groups_Ozero__class_Ozero(t_a)
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1176]) ).
fof(f1178,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1176]) ).
fof(f1179,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1176]) ).
fof(f1180,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK4_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK3_skl,sK5_skl)),X0))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1176]) ).
fof(f1181,plain,
( ? [B_k,B_a] :
( ? [B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f1182,plain,
( ? [B_a] :
( ? [B_k,B_q] :
( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )
& B_a != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(miniscoping,[status(thm)],[f1181]) ).
fof(f1183,plain,
( ( ! [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),B_z))
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
& sK6_skl != c_Groups_Ozero__class_Ozero(t_a) )
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl]),skolemize(B_a,sK6_skl),skolemize(B_k,sK7_skl),skolemize(B_q,sK8_skl)],[f1182]) ).
fof(f1184,plain,
( sK6_skl != c_Groups_Ozero__class_Ozero(t_a)
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f1185,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f1186,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f1187,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0))
| v_c____ != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1183]) ).
fof(f1471,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f4612,plain,
! [B_k,B_a] :
( ! [B_q] :
( ? [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
| ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) )
| B_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f1161]) ).
fof(f4613,definition,
! [B_k,B_q] :
( sP6_prd(B_q,B_k)
<=> ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f4614,plain,
! [B_k,B_a] :
( ! [B_q] :
( ? [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
| ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| sP6_prd(B_q,B_k) )
| B_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(formula_renaming,[status(thm)],[f4612,f4613]) ).
fof(f4615,plain,
! [B_a] :
( ! [B_k,B_q] :
( ? [B_z] : hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),B_z) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),B_z),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),B_z))
| ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| sP6_prd(B_q,B_k) )
| B_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(miniscoping,[status(thm)],[f4614]) ).
fof(f4616,plain,
! [B_a] :
( ! [B_k,B_q] :
( hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(B_q,B_k,B_a)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(B_q,B_k,B_a)),B_k)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,B_a,B_q)),sK31_skl(B_q,B_k,B_a)))
| ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| sP6_prd(B_q,B_k) )
| B_a = c_Groups_Ozero__class_Ozero(t_a) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl]),skolemize(B_z,sK31_skl(B_q,B_k,B_a))],[f4615]) ).
fof(f4618,plain,
! [X0,X1,X2] :
( hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),sK31_skl(X1,X2,X0)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),sK31_skl(X1,X2,X0)),X2)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,X0,X1)),sK31_skl(X1,X2,X0)))
| c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,X1))),X2)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| sP6_prd(X1,X2)
| X0 = c_Groups_Ozero__class_Ozero(t_a) ),
inference(cnf_transformation,[status(thm)],[f4616]) ).
fof(f4619,plain,
class_Rings_Oidom(t_a),
inference(cnf_transformation,[status(thm)],[f1162]) ).
fof(f4658,plain,
! [B_k,B_q] :
( ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| sP6_prd(B_q,B_k) )
& ( ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| ~ sP6_prd(B_q,B_k) ) ),
inference(NNF_transformation,[status(thm)],[f4613]) ).
fof(f4659,plain,
( ! [B_k,B_q] :
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| sP6_prd(B_q,B_k) )
& ! [B_k,B_q] :
( ( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(B_q,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,B_q))),B_k)) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) )
| ~ sP6_prd(B_q,B_k) ) ),
inference(miniscoping,[status(thm)],[f4658]) ).
fof(f4660,plain,
! [X0,X1] :
( c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ sP6_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4659]) ).
fof(f4864,plain,
( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1178,f1471]) ).
fof(f4865,plain,
! [X0,X1] :
( ~ sP6_prd(X0,X1)
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(resolution,[status(thm)],[f4864,f4660]) ).
fof(f4866,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1179,f4864]) ).
fof(f4869,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| sP6_prd(sK5_skl,sK4_skl)
| sK3_skl = c_Groups_Ozero__class_Ozero(t_a)
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(resolution,[status(thm)],[f1180,f4618]) ).
fof(f4870,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| sP6_prd(sK5_skl,sK4_skl)
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f4869,f1177]) ).
fof(f4871,plain,
( v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(backward_subsumption_resolution,[status(thm)],[f4866,f4872]) ).
fof(f4872,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK5_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK5_skl))),sK4_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| v_c____ = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f4870,f4865]) ).
fof(f4895,plain,
( sK6_skl != c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1184,f4871]) ).
fof(f4896,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1185,f4871]) ).
fof(f4897,plain,
( c_Polynomial_OpCons(t_a,v_c____,v_cs____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ class_Rings_Oidom(t_a) ),
inference(resolution,[status(thm)],[f4896,f1471]) ).
fof(f4898,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| c_Polynomial_OpCons(t_a,v_c____,v_cs____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1186,f4871]) ).
fof(f4901,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) = c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| ~ class_Rings_Oidom(t_a) ),
inference(backward_subsumption_resolution,[status(thm)],[f4898,f4897]) ).
fof(f4902,plain,
! [X0,X1] :
( ~ sP6_prd(X0,X1)
| ~ class_Rings_Oidom(t_a) ),
inference(resolution,[status(thm)],[f4897,f4660]) ).
fof(f4964,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)),X0) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),hAPP(hAPP(c_Power_Opower__class_Opower(t_a),X0),sK7_skl)),hAPP(c_Polynomial_Opoly(t_a,c_Polynomial_OpCons(t_a,sK6_skl,sK8_skl)),X0))
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f1187,f4871]) ).
fof(f4965,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| sP6_prd(sK8_skl,sK7_skl)
| sK6_skl = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(resolution,[status(thm)],[f4964,f4618]) ).
fof(f4966,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| sP6_prd(sK8_skl,sK7_skl)
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f4965,f4895]) ).
fof(f5016,plain,
~ class_Rings_Oidom(t_a),
inference(backward_subsumption_resolution,[status(thm)],[f4901,f5017]) ).
fof(f5017,plain,
( c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_If(tc_Nat_Onat,c_fequal(sK8_skl,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Nat_OSuc(c_Polynomial_Odegree(t_a,sK8_skl))),sK7_skl)) != c_Nat_OSuc(c_Polynomial_Odegree(t_a,c_Polynomial_OpCons(t_a,v_c____,v_cs____)))
| ~ class_Rings_Oidom(t_a) ),
inference(forward_subsumption_resolution,[status(thm)],[f4966,f4902]) ).
fof(f5145,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4619,f5016]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW245+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.46 % Computer : n026.cluster.edu
% 0.16/0.46 % Model : x86_64 x86_64
% 0.16/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.46 % Memory : 8046.5625MB
% 0.16/0.46 % OS : Linux 6.8.0-71-generic
% 0.16/0.46 % CPULimit : 300
% 0.16/0.46 % WCLimit : 300
% 0.16/0.46 % DateTime : Mon Sep 21 09:45:52 UTC 2026
% 0.16/0.46 % CPUTime :
% 0.33/0.64 % Drodi V4.1.1
% 0.36/0.69 % Refutation found
% 0.36/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.36/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.37/0.77 % Elapsed time: 0.286299 seconds
% 0.37/0.77 % CPU time: 0.612984 seconds
% 0.37/0.77 % Total memory used: 122.171 MB
% 0.37/0.77 % Net memory used: 121.384 MB
%------------------------------------------------------------------------------