%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW247+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 : n009.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 116.25s 15.39s
% Output : CNFRefutation 105.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 96 ( 28 unt; 0 def)
% Number of atoms : 213 ( 137 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 198 ( 81 ~; 83 |; 13 &)
% ( 6 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 167 ( 163 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( class_Rings_Oidom(t_a)
=> ! [B_z] :
( B_z != c_Groups_Ozero__class_Ozero(t_a)
=> hAPP(c_Polynomial_Opoly(t_a,v_cs____),B_z) = c_Groups_Ozero__class_Ozero(t_a) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V_p,T_a] :
( class_Groups_Ozero(T_a)
=> ~ ! [B_a,B_q] : V_p != hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [V_x,V_p,V_a,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [V_p,T_a] :
( class_Groups_Ocomm__monoid__add(T_a)
=> hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = V_p ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [V_pa_2,V_a_2,T_b] :
( class_Rings_Oidom(T_b)
=> ( hAPP(hAPP(c_Polynomial_Osmult(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(f47,axiom,
! [V_r,V_q,V_c,V_p,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> ( hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),V_q)) = hAPP(hAPP(c_Polynomial_OpCons(T_a),V_r),V_q)
=> ( V_q = c_Polynomial_Osynthetic__div(T_a,V_p,V_c)
& V_r = hAPP(c_Polynomial_Opoly(T_a,V_p),V_c) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [V_b_2,V_a_2,T_b] :
( class_Rings_Oring__no__zero__divisors(T_b)
=> ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_b)
<=> ( V_b_2 = c_Groups_Ozero__class_Ozero(T_b)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [V_a_2,V_b_2,T_b] :
( class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_b)
=> ( V_b_2 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2)
<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f996,axiom,
! [T] :
( class_Rings_Oidom(T)
=> class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f999,axiom,
! [T] :
( class_Rings_Oidom(T)
=> class_Rings_Oring__no__zero__divisors(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1005,axiom,
! [T] :
( class_Rings_Oidom(T)
=> class_Groups_Ocomm__monoid__add(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1007,axiom,
! [T] :
( class_Rings_Oidom(T)
=> class_Rings_Ocomm__semiring__0(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1024,axiom,
! [T] :
( class_Rings_Oidom(T)
=> class_Groups_Ozero(T) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1213,conjecture,
hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) = hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1214,negated_conjecture,
hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____),
inference(negated_conjecture,[status(cth)],[f1213]) ).
fof(f1215,hypothesis,
class_Rings_Oidom(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1221,plain,
( ! [B_z] :
( hAPP(c_Polynomial_Opoly(t_a,v_cs____),B_z) = c_Groups_Ozero__class_Ozero(t_a)
| B_z = c_Groups_Ozero__class_Ozero(t_a) )
| ~ class_Rings_Oidom(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f1222,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(t_a,v_cs____),X0) = c_Groups_Ozero__class_Ozero(t_a)
| X0 = c_Groups_Ozero__class_Ozero(t_a)
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
fof(f1247,plain,
! [V_p,T_a] :
( ? [B_a,B_q] : V_p = hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q)
| ~ class_Groups_Ozero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f1248,plain,
! [T_a] :
( ! [V_p] :
? [B_a,B_q] : V_p = hAPP(hAPP(c_Polynomial_OpCons(T_a),B_a),B_q)
| ~ class_Groups_Ozero(T_a) ),
inference(miniscoping,[status(thm)],[f1247]) ).
fof(f1249,plain,
! [T_a] :
( ! [V_p] : V_p = hAPP(hAPP(c_Polynomial_OpCons(T_a),sK3_skl(V_p,T_a)),sK4_skl(V_p,T_a))
| ~ class_Groups_Ozero(T_a) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(B_a,sK3_skl(V_p,T_a)),skolemize(B_q,sK4_skl(V_p,T_a))],[f1248]) ).
fof(f1250,plain,
! [X0,X1] :
( X1 = hAPP(hAPP(c_Polynomial_OpCons(X0),sK3_skl(X1,X0)),sK4_skl(X1,X0))
| ~ class_Groups_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f1249]) ).
fof(f1254,plain,
! [V_x,V_p,V_a,T_a] :
( hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f1255,plain,
! [T_a] :
( ! [V_x,V_p,V_a] : hAPP(c_Polynomial_Opoly(T_a,hAPP(hAPP(c_Polynomial_OpCons(T_a),V_a),V_p)),V_x) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),hAPP(c_Polynomial_Opoly(T_a,V_p),V_x)))
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1254]) ).
fof(f1256,plain,
! [X0,X1,X2,X3] :
( hAPP(c_Polynomial_Opoly(X0,hAPP(hAPP(c_Polynomial_OpCons(X0),X1),X2)),X3) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X3),hAPP(c_Polynomial_Opoly(X0,X2),X3)))
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1255]) ).
fof(f1297,plain,
! [V_p,T_a] :
( hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = V_p
| ~ class_Groups_Ocomm__monoid__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f1298,plain,
! [T_a] :
( ! [V_p] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = V_p
| ~ class_Groups_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f1297]) ).
fof(f1299,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0)),X1),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = X1
| ~ class_Groups_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1298]) ).
fof(f1326,plain,
! [V_pa_2,V_a_2,T_b] :
( ( hAPP(hAPP(c_Polynomial_Osmult(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_Rings_Oidom(T_b) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f1327,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) )
| hAPP(hAPP(c_Polynomial_Osmult(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)
| hAPP(hAPP(c_Polynomial_Osmult(T_b),V_a_2),V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) )
| ~ class_Rings_Oidom(T_b) ),
inference(NNF_transformation,[status(thm)],[f1326]) ).
fof(f1328,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) )
| hAPP(hAPP(c_Polynomial_Osmult(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)
| hAPP(hAPP(c_Polynomial_Osmult(T_b),V_a_2),V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) )
| ~ class_Rings_Oidom(T_b) ),
inference(miniscoping,[status(thm)],[f1327]) ).
fof(f1330,plain,
! [X0,X1,X2] :
( X1 != c_Groups_Ozero__class_Ozero(X0)
| hAPP(hAPP(c_Polynomial_Osmult(X0),X1),X2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1328]) ).
fof(f1368,plain,
! [V_r,V_q,V_c,V_p,T_a] :
( ( V_q = c_Polynomial_Osynthetic__div(T_a,V_p,V_c)
& V_r = hAPP(c_Polynomial_Opoly(T_a,V_p),V_c) )
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),V_q)) != hAPP(hAPP(c_Polynomial_OpCons(T_a),V_r),V_q)
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f1369,plain,
! [T_a] :
( ! [V_r,V_q,V_c,V_p] :
( ( V_q = c_Polynomial_Osynthetic__div(T_a,V_p,V_c)
& V_r = hAPP(c_Polynomial_Opoly(T_a,V_p),V_c) )
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a)),V_p),hAPP(hAPP(c_Polynomial_Osmult(T_a),V_c),V_q)) != hAPP(hAPP(c_Polynomial_OpCons(T_a),V_r),V_q) )
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1368]) ).
fof(f1370,plain,
! [X0,X1,X2,X3,X4] :
( X4 = hAPP(c_Polynomial_Opoly(X0,X1),X2)
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X0)),X1),hAPP(hAPP(c_Polynomial_Osmult(X0),X2),X3)) != hAPP(hAPP(c_Polynomial_OpCons(X0),X4),X3)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1369]) ).
fof(f1474,plain,
! [V_b_2,V_a_2,T_b] :
( ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_b)
<=> ( V_b_2 = c_Groups_Ozero__class_Ozero(T_b)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_b) ),
inference(pre_NNF_transformation,[status(thm)],[f79]) ).
fof(f1475,plain,
! [V_b_2,V_a_2,T_b] :
( ( ( ( V_b_2 != c_Groups_Ozero__class_Ozero(T_b)
& V_a_2 != c_Groups_Ozero__class_Ozero(T_b) )
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_b) )
& ( V_b_2 = c_Groups_Ozero__class_Ozero(T_b)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_b)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) != c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_b) ),
inference(NNF_transformation,[status(thm)],[f1474]) ).
fof(f1476,plain,
! [T_b] :
( ( ! [V_b_2,V_a_2] :
( ( V_b_2 != c_Groups_Ozero__class_Ozero(T_b)
& V_a_2 != c_Groups_Ozero__class_Ozero(T_b) )
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_b) )
& ! [V_b_2,V_a_2] :
( V_b_2 = c_Groups_Ozero__class_Ozero(T_b)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_b)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_b),V_a_2),V_b_2) != c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_b) ),
inference(miniscoping,[status(thm)],[f1475]) ).
fof(f1479,plain,
! [X0,X1,X2] :
( X2 != c_Groups_Ozero__class_Ozero(X0)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Oring__no__zero__divisors(X0) ),
inference(cnf_transformation,[status(thm)],[f1476]) ).
fof(f1504,plain,
! [V_a_2,V_b_2,T_b] :
( ( V_b_2 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2)
<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_b) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_b) ),
inference(pre_NNF_transformation,[status(thm)],[f88]) ).
fof(f1505,plain,
! [V_a_2,V_b_2,T_b] :
( ( ( V_a_2 != c_Groups_Ozero__class_Ozero(T_b)
| V_b_2 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2) )
& ( V_a_2 = c_Groups_Ozero__class_Ozero(T_b)
| V_b_2 != hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2) ) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_b) ),
inference(NNF_transformation,[status(thm)],[f1504]) ).
fof(f1506,plain,
! [T_b] :
( ( ! [V_a_2] :
( V_a_2 != c_Groups_Ozero__class_Ozero(T_b)
| ! [V_b_2] : V_b_2 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2) )
& ! [V_a_2] :
( V_a_2 = c_Groups_Ozero__class_Ozero(T_b)
| ! [V_b_2] : V_b_2 != hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_b),V_b_2),V_a_2) ) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_b) ),
inference(miniscoping,[status(thm)],[f1505]) ).
fof(f1508,plain,
! [X0,X1,X2] :
( X2 != c_Groups_Ozero__class_Ozero(X0)
| X1 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),X2)
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X0) ),
inference(cnf_transformation,[status(thm)],[f1506]) ).
fof(f4439,plain,
! [T] :
( class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T)
| ~ class_Rings_Oidom(T) ),
inference(pre_NNF_transformation,[status(thm)],[f996]) ).
fof(f4440,plain,
! [X0] :
( class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4439]) ).
fof(f4445,plain,
! [T] :
( class_Rings_Oring__no__zero__divisors(T)
| ~ class_Rings_Oidom(T) ),
inference(pre_NNF_transformation,[status(thm)],[f999]) ).
fof(f4446,plain,
! [X0] :
( class_Rings_Oring__no__zero__divisors(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4445]) ).
fof(f4457,plain,
! [T] :
( class_Groups_Ocomm__monoid__add(T)
| ~ class_Rings_Oidom(T) ),
inference(pre_NNF_transformation,[status(thm)],[f1005]) ).
fof(f4458,plain,
! [X0] :
( class_Groups_Ocomm__monoid__add(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4457]) ).
fof(f4461,plain,
! [T] :
( class_Rings_Ocomm__semiring__0(T)
| ~ class_Rings_Oidom(T) ),
inference(pre_NNF_transformation,[status(thm)],[f1007]) ).
fof(f4462,plain,
! [X0] :
( class_Rings_Ocomm__semiring__0(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4461]) ).
fof(f4495,plain,
! [T] :
( class_Groups_Ozero(T)
| ~ class_Rings_Oidom(T) ),
inference(pre_NNF_transformation,[status(thm)],[f1024]) ).
fof(f4496,plain,
! [X0] :
( class_Groups_Ozero(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4495]) ).
fof(f4762,plain,
hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____),
inference(cnf_transformation,[status(thm)],[f1214]) ).
fof(f4763,plain,
class_Rings_Oidom(t_a),
inference(cnf_transformation,[status(thm)],[f1215]) ).
fof(f4781,plain,
! [X0,X1] :
( hAPP(hAPP(c_Polynomial_Osmult(X0),c_Groups_Ozero__class_Ozero(X0)),X1) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Oidom(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1330]) ).
fof(f4788,plain,
! [X0,X1] :
( hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),c_Groups_Ozero__class_Ozero(X0)) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Oring__no__zero__divisors(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1479]) ).
fof(f4789,plain,
! [X0,X1] :
( X1 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(X0),X1),c_Groups_Ozero__class_Ozero(X0))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1508]) ).
fof(f5005,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(t_a,v_cs____),X0) = c_Groups_Ozero__class_Ozero(t_a)
| X0 = c_Groups_Ozero__class_Ozero(t_a) ),
inference(backward_subsumption_resolution,[status(thm)],[f1222,f4763]) ).
fof(f6464,plain,
! [X0] : hAPP(hAPP(c_Polynomial_Osmult(t_a),c_Groups_Ozero__class_Ozero(t_a)),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)),
inference(resolution,[status(thm)],[f4781,f4763]) ).
fof(f7052,plain,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(t_a),
inference(resolution,[status(thm)],[f4440,f4763]) ).
fof(f7135,plain,
class_Rings_Oring__no__zero__divisors(t_a),
inference(resolution,[status(thm)],[f4446,f4763]) ).
fof(f7660,plain,
class_Groups_Ocomm__monoid__add(t_a),
inference(resolution,[status(thm)],[f4458,f4763]) ).
fof(f7662,plain,
! [X0] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = X0,
inference(resolution,[status(thm)],[f7660,f1299]) ).
fof(f7672,plain,
class_Rings_Ocomm__semiring__0(t_a),
inference(resolution,[status(thm)],[f4462,f4763]) ).
fof(f7677,plain,
! [X0,X1,X2,X3] :
( X3 = hAPP(c_Polynomial_Opoly(t_a,X0),X1)
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),hAPP(hAPP(c_Polynomial_Osmult(t_a),X1),X2)) != hAPP(hAPP(c_Polynomial_OpCons(t_a),X3),X2) ),
inference(resolution,[status(thm)],[f7672,f1370]) ).
fof(f7705,plain,
! [X0,X1,X2] : hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)),X2) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X2),hAPP(c_Polynomial_Opoly(t_a,X1),X2))),
inference(resolution,[status(thm)],[f7672,f1256]) ).
fof(f8441,plain,
! [X0,X1,X2] :
( X1 = hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a))
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(t_a)),X0),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) != hAPP(hAPP(c_Polynomial_OpCons(t_a),X1),X2) ),
inference(paramodulation,[status(thm)],[f6464,f7677]) ).
fof(f8444,plain,
! [X0,X1,X2] :
( X1 = hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a))
| X0 != hAPP(hAPP(c_Polynomial_OpCons(t_a),X1),X2) ),
inference(forward_demodulation,[status(thm)],[f7662,f8441]) ).
fof(f8445,plain,
! [X0,X1] : X0 = hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1)),c_Groups_Ozero__class_Ozero(t_a)),
inference(destructive_equality_resolution,[status(thm)],[f8444]) ).
fof(f8664,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)) = c_Groups_Ozero__class_Ozero(t_a),
inference(resolution,[status(thm)],[f4788,f7135]) ).
fof(f9200,plain,
class_Groups_Ozero(t_a),
inference(resolution,[status(thm)],[f4496,f4763]) ).
fof(f9207,plain,
! [X0] : X0 = hAPP(hAPP(c_Polynomial_OpCons(t_a),sK3_skl(X0,t_a)),sK4_skl(X0,t_a)),
inference(resolution,[status(thm)],[f9200,f1250]) ).
fof(f9224,plain,
! [X0] : sK3_skl(X0,t_a) = hAPP(c_Polynomial_Opoly(t_a,X0),c_Groups_Ozero__class_Ozero(t_a)),
inference(paramodulation,[status(thm)],[f9207,f8445]) ).
fof(f9246,plain,
! [X0,X1] : X0 = sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),X1),t_a),
inference(backward_demodulation,[status(thm)],[f9224,f8445]) ).
fof(f9883,plain,
! [X0] : X0 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)),
inference(resolution,[status(thm)],[f4789,f7052]) ).
fof(f10372,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_Groups_Otimes__class_Otimes(t_a),X1),c_Groups_Ozero__class_Ozero(t_a))) ),
inference(paramodulation,[status(thm)],[f5005,f7705]) ).
fof(f10416,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(t_a),X0),c_Groups_Ozero__class_Ozero(t_a)) ),
inference(forward_demodulation,[status(thm)],[f8664,f10372]) ).
fof(f10417,plain,
! [X0,X1] :
( X1 = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),X0),v_cs____)),X1) = X0 ),
inference(forward_demodulation,[status(thm)],[f9883,f10416]) ).
fof(f13766,plain,
( v_y____ = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != v_c____ ),
inference(paramodulation,[status(thm)],[f10417,f4762]) ).
fof(f14023,plain,
( v_x____ = c_Groups_Ozero__class_Ozero(t_a)
| v_y____ = c_Groups_Ozero__class_Ozero(t_a) ),
inference(resolution,[status(thm)],[f13766,f10417]) ).
fof(f14037,plain,
! [X0] :
( v_x____ = c_Groups_Ozero__class_Ozero(t_a)
| sK3_skl(X0,t_a) = hAPP(c_Polynomial_Opoly(t_a,X0),v_y____) ),
inference(paramodulation,[status(thm)],[f14023,f9224]) ).
fof(f14881,plain,
( v_x____ = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a) ),
inference(paramodulation,[status(thm)],[f14037,f4762]) ).
fof(f14905,plain,
( v_x____ = c_Groups_Ozero__class_Ozero(t_a)
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != v_c____ ),
inference(forward_demodulation,[status(thm)],[f9246,f14881]) ).
fof(f14921,plain,
( v_y____ = v_x____
| hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____) != v_c____ ),
inference(backward_demodulation,[status(thm)],[f15199,f13766]) ).
fof(f14941,plain,
! [X0] : sK3_skl(X0,t_a) = hAPP(c_Polynomial_Opoly(t_a,X0),v_x____),
inference(backward_demodulation,[status(thm)],[f15199,f9224]) ).
fof(f15199,plain,
v_x____ = c_Groups_Ozero__class_Ozero(t_a),
inference(forward_subsumption_resolution,[status(thm)],[f14905,f10417]) ).
fof(f15211,plain,
sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a) != hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____),
inference(backward_demodulation,[status(thm)],[f14941,f4762]) ).
fof(f15212,plain,
( v_y____ = v_x____
| sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a) != v_c____ ),
inference(backward_demodulation,[status(thm)],[f14941,f14921]) ).
fof(f15323,plain,
v_c____ != hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_y____),
inference(forward_demodulation,[status(thm)],[f9246,f15211]) ).
fof(f15324,plain,
( v_y____ = v_x____
| v_c____ != v_c____ ),
inference(forward_demodulation,[status(thm)],[f9246,f15212]) ).
fof(f15326,plain,
v_c____ != hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____)),v_x____),
inference(backward_demodulation,[status(thm)],[f15328,f15323]) ).
fof(f15328,plain,
v_y____ = v_x____,
inference(trivial_equality_resolution,[status(thm)],[f15324]) ).
fof(f15332,plain,
v_c____ != sK3_skl(hAPP(hAPP(c_Polynomial_OpCons(t_a),v_c____),v_cs____),t_a),
inference(forward_demodulation,[status(thm)],[f14941,f15326]) ).
fof(f15333,plain,
v_c____ != v_c____,
inference(forward_demodulation,[status(thm)],[f9246,f15332]) ).
fof(f15334,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f15333]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW247+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n009.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 09:43:57 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.37/0.62 % Drodi V4.1.1
% 116.25/15.39 % Refutation found
% 116.25/15.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 116.25/15.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 84.08/16.70 % Elapsed time: 16.034936 seconds
% 84.08/16.70 % CPU time: 114.433838 seconds
% 84.08/16.70 % Total memory used: 790.450 MB
% 84.08/16.70 % Net memory used: 746.205 MB
%------------------------------------------------------------------------------