%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW285+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 : n019.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:34 PM UTC 2026
% Result : Theorem 1.76s 0.80s
% Output : CNFRefutation 1.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 27
% Syntax : Number of formulae : 95 ( 23 unt; 12 def)
% Number of atoms : 222 ( 62 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 217 ( 90 ~; 90 |; 13 &)
% ( 16 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 23 ( 21 usr; 13 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 54 ( 53 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [T_a] :
( class_Groups_Ozero(T_a)
=> c_Polynomial_Odegree(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,axiom,
~ ! [B_r] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) != hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),B_r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [V_n_2,V_a_2,T_a] :
( ( class_Rings_Ozero__neq__one(T_a)
& class_Rings_Ono__zero__divisors(T_a)
& class_Rings_Omult__zero(T_a)
& class_Power_Opower(T_a) )
=> ( hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,axiom,
! [V_b_2,V_a_2,T_a] :
( class_Rings_Oring__no__zero__divisors(T_a)
=> ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_b_2 = c_Groups_Ozero__class_Ozero(T_a)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1101,axiom,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1102,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1120,axiom,
class_Groups_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1137,axiom,
! [T_1] :
( class_Rings_Oidom(T_1)
=> class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1147,axiom,
! [T_1] :
( class_Rings_Oidom(T_1)
=> class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1156,axiom,
! [T_1] :
( class_Rings_Ocomm__semiring__1(T_1)
=> class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1164,axiom,
! [T_1] :
( class_Rings_Ocomm__semiring__0(T_1)
=> class_Rings_Omult__zero(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1170,axiom,
! [T_1] :
( class_Rings_Ocomm__semiring__1(T_1)
=> class_Power_Opower(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1185,plain,
v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f1309,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f1422,plain,
! [T_a] :
( c_Polynomial_Odegree(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Groups_Ozero(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f1423,plain,
! [X0] :
( c_Polynomial_Odegree(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Groups_Ozero(X0) ),
inference(cnf_transformation,[status(thm)],[f1422]) ).
fof(f1510,plain,
? [B_r] : hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),B_r),
inference(pre_NNF_transformation,[status(thm)],[f95]) ).
fof(f1511,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK6_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B_r,sK6_skl)],[f1510]) ).
fof(f1512,plain,
hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q),c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p)) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK6_skl),
inference(cnf_transformation,[status(thm)],[f1511]) ).
fof(f1523,plain,
! [V_n_2,V_a_2,T_a] :
( ( hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Ozero__neq__one(T_a)
| ~ class_Rings_Ono__zero__divisors(T_a)
| ~ class_Rings_Omult__zero(T_a)
| ~ class_Power_Opower(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f98]) ).
fof(f1524,plain,
! [V_n_2,V_a_2,T_a] :
( ( ( V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Ozero__neq__one(T_a)
| ~ class_Rings_Ono__zero__divisors(T_a)
| ~ class_Rings_Omult__zero(T_a)
| ~ class_Power_Opower(T_a) ),
inference(NNF_transformation,[status(thm)],[f1523]) ).
fof(f1525,plain,
! [T_a] :
( ( ! [V_n_2,V_a_2] :
( V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ! [V_n_2,V_a_2] :
( ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Ozero__neq__one(T_a)
| ~ class_Rings_Ono__zero__divisors(T_a)
| ~ class_Rings_Omult__zero(T_a)
| ~ class_Power_Opower(T_a) ),
inference(miniscoping,[status(thm)],[f1524]) ).
fof(f1527,plain,
! [X0,X1,X2] :
( X2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hAPP(hAPP(c_Power_Opower__class_Opower(X0),X1),X2) != c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Ozero__neq__one(X0)
| ~ class_Rings_Ono__zero__divisors(X0)
| ~ class_Rings_Omult__zero(X0)
| ~ class_Power_Opower(X0) ),
inference(cnf_transformation,[status(thm)],[f1525]) ).
fof(f1621,plain,
! [V_b_2,V_a_2,T_a] :
( ( hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_b_2 = c_Groups_Ozero__class_Ozero(T_a)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f126]) ).
fof(f1622,plain,
! [V_b_2,V_a_2,T_a] :
( ( ( ( V_b_2 != c_Groups_Ozero__class_Ozero(T_a)
& V_a_2 != c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( V_b_2 = c_Groups_Ozero__class_Ozero(T_a)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_a) ),
inference(NNF_transformation,[status(thm)],[f1621]) ).
fof(f1623,plain,
! [T_a] :
( ( ! [V_b_2,V_a_2] :
( ( V_b_2 != c_Groups_Ozero__class_Ozero(T_a)
& V_a_2 != c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ! [V_b_2,V_a_2] :
( V_b_2 = c_Groups_Ozero__class_Ozero(T_a)
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a_2),V_b_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Oring__no__zero__divisors(T_a) ),
inference(miniscoping,[status(thm)],[f1622]) ).
fof(f1625,plain,
! [X0,X1,X2] :
( X1 != 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)],[f1623]) ).
fof(f4516,plain,
class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1101]) ).
fof(f4517,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1102]) ).
fof(f4535,plain,
class_Groups_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1120]) ).
fof(f4537,plain,
class_Rings_Oidom(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1122]) ).
fof(f4564,plain,
! [T_1] :
( class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Oidom(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1137]) ).
fof(f4565,plain,
! [X0] :
( class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4564]) ).
fof(f4584,plain,
! [T_1] :
( class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Oidom(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1147]) ).
fof(f4585,plain,
! [X0] :
( class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f4584]) ).
fof(f4602,plain,
! [T_1] :
( class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Ocomm__semiring__1(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1156]) ).
fof(f4603,plain,
! [X0] :
( class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f4602]) ).
fof(f4618,plain,
! [T_1] :
( class_Rings_Omult__zero(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Ocomm__semiring__0(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1164]) ).
fof(f4619,plain,
! [X0] :
( class_Rings_Omult__zero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f4618]) ).
fof(f4630,plain,
! [T_1] :
( class_Power_Opower(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Ocomm__semiring__1(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1170]) ).
fof(f4631,plain,
! [X0] :
( class_Power_Opower(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f4630]) ).
fof(f4729,definition,
( sQ4_spl
<=> class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f4731,plain,
( sQ4_spl
| ~ class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4729]) ).
fof(f4749,definition,
( sQ8_spl
<=> class_Groups_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f4751,plain,
( sQ8_spl
| ~ class_Groups_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4749]) ).
fof(f4815,definition,
( sQ20_spl
<=> class_Rings_Oidom(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f4817,plain,
( sQ20_spl
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4815]) ).
fof(f4926,definition,
( sQ37_spl
<=> class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f4928,plain,
( sQ37_spl
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f4926]) ).
fof(f5004,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Groups_Ozero(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f1185,f1423]) ).
fof(f5005,definition,
( sQ50_spl
<=> c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f5008,plain,
( sQ50_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f5004,f4749,f5005]) ).
fof(f5099,plain,
hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____) = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),sK6_skl),
inference(forward_demodulation,[status(thm)],[f1309,f1512]) ).
fof(f5141,definition,
( sQ68_spl
<=> v_p = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f5143,plain,
( sQ68_spl
| v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5141]) ).
fof(f5210,definition,
( sQ83_spl
<=> class_Power_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f5212,plain,
( sQ83_spl
| ~ class_Power_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5210]) ).
fof(f5213,definition,
( sQ84_spl
<=> class_Rings_Omult__zero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f5215,plain,
( sQ84_spl
| ~ class_Rings_Omult__zero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5213]) ).
fof(f5216,definition,
( sQ85_spl
<=> class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f5218,plain,
( sQ85_spl
| ~ class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5216]) ).
fof(f5219,definition,
( sQ86_spl
<=> class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f5221,plain,
( sQ86_spl
| ~ class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5219]) ).
fof(f5222,definition,
( sQ87_spl
<=> hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f5228,plain,
( c_Polynomial_Odegree(tc_Complex_Ocomplex,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Rings_Ozero__neq__one(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Rings_Ono__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Rings_Omult__zero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Power_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(paramodulation,[status(thm)],[f1309,f1527]) ).
fof(f5229,plain,
( ~ sQ50_spl
| ~ sQ87_spl
| ~ sQ86_spl
| ~ sQ85_spl
| ~ sQ84_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f5228,f5210,f5213,f5216,f5219,f5222,f5005]) ).
fof(f5394,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4731,f4517]) ).
fof(f5395,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f5394]) ).
fof(f5402,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4751,f4535]) ).
fof(f5403,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f5402]) ).
fof(f5419,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4817,f4537]) ).
fof(f5420,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f5419]) ).
fof(f5424,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4928,f4516]) ).
fof(f5425,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f5424]) ).
fof(f5665,definition,
( sQ146_spl
<=> class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f5667,plain,
( sQ146_spl
| ~ class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f5665]) ).
fof(f5671,plain,
( v_p != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_p),v_r____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(paramodulation,[status(thm)],[f5099,f1625]) ).
fof(f5672,plain,
( ~ sQ68_spl
| sQ87_spl
| ~ sQ146_spl ),
inference(split_clause,[status(thm)],[f5671,f5665,f5222,f5141]) ).
fof(f7077,plain,
( sQ146_spl
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f4565,f5667]) ).
fof(f7078,plain,
( sQ146_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f7077,f4815,f5665]) ).
fof(f7467,plain,
( sQ85_spl
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f4585,f5218]) ).
fof(f7468,plain,
( sQ85_spl
| ~ sQ20_spl ),
inference(split_clause,[status(thm)],[f7467,f4815,f5216]) ).
fof(f7736,plain,
( sQ86_spl
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f4603,f5221]) ).
fof(f7737,plain,
( sQ86_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f7736,f4926,f5219]) ).
fof(f7853,plain,
( sQ84_spl
| ~ class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f4619,f5215]) ).
fof(f7854,plain,
( sQ84_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f7853,f4729,f5213]) ).
fof(f7940,plain,
( sQ83_spl
| ~ class_Rings_Ocomm__semiring__1(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f4631,f5212]) ).
fof(f7941,plain,
( sQ83_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f7940,f4926,f5210]) ).
fof(f8193,plain,
( sQ68_spl
| v_p != v_p ),
inference(forward_demodulation,[status(thm)],[f1185,f5143]) ).
fof(f8194,plain,
( sQ68_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f8193]) ).
fof(f8195,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f8194]) ).
fof(f8196,plain,
$false,
inference(sat_refutation,[status(thm)],[f5008,f5229,f5395,f5403,f5420,f5425,f5672,f7078,f7468,f7737,f7854,f7941,f8195]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW285+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n019.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 09:45:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.45 % Drodi V4.1.1
% 1.76/0.80 % Refutation found
% 1.76/0.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.76/0.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.84/0.84 % Elapsed time: 0.473813 seconds
% 1.84/0.84 % CPU time: 2.650164 seconds
% 1.84/0.84 % Total memory used: 242.154 MB
% 1.84/0.84 % Net memory used: 239.097 MB
%------------------------------------------------------------------------------