%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW269+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:33 PM UTC 2026
% Result : Theorem 183.77s 23.89s
% Output : CNFRefutation 183.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 22
% Syntax : Number of formulae : 94 ( 24 unt; 8 def)
% Number of atoms : 213 ( 109 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 198 ( 79 ~; 88 |; 10 &)
% ( 12 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 110 ( 109 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [V_g_2,V_f_2] :
( ! [B_x] : hAPP(V_f_2,B_x) = hAPP(V_g_2,B_x)
=> V_f_2 = V_g_2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
v_d____ = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [B_w] :
( B_w != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),B_w) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [V_q_2,V_pa_2,T_a] :
( ( class_Rings_Oidom(T_a)
& class_Int_Oring__char__0(T_a) )
=> ( c_Polynomial_Opoly(T_a,V_pa_2) = c_Polynomial_Opoly(T_a,V_q_2)
<=> V_pa_2 = V_q_2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [V_x,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Ozero__class_Ozero(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [V_a,T_a] :
( class_Groups_Omonoid__add(T_a)
=> c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [V_r,V_q,V_c,V_p,T_a] :
( class_Rings_Ocomm__semiring__0(T_a)
=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q)) = 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [V_pa_2,V_a_2,T_a] :
( class_Rings_Oidom(T_a)
=> ( c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1069,axiom,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1071,axiom,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1084,axiom,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1092,axiom,
class_Rings_Oidom(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1135,axiom,
! [T_1] :
( class_Groups_Ocomm__monoid__add(T_1)
=> class_Groups_Omonoid__add(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1159,conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1160,negated_conjecture,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(negated_conjecture,[status(cth)],[f1159]) ).
fof(f1161,plain,
! [V_g_2,V_f_2] :
( V_f_2 = V_g_2
| ? [B_x] : hAPP(V_f_2,B_x) != hAPP(V_g_2,B_x) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f1162,plain,
! [V_g_2,V_f_2] :
( V_f_2 = V_g_2
| hAPP(V_f_2,sK0_skl(V_f_2,V_g_2)) != hAPP(V_g_2,sK0_skl(V_f_2,V_g_2)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B_x,sK0_skl(V_f_2,V_g_2))],[f1161]) ).
fof(f1163,plain,
! [X0,X1] :
( hAPP(X0,sK0_skl(X1,X0)) != hAPP(X1,sK0_skl(X1,X0))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f1162]) ).
fof(f1164,plain,
c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = v_d____,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f1165,plain,
! [B_w] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),B_w) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex)
| B_w = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f1166,plain,
! [X0] :
( c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(cnf_transformation,[status(thm)],[f1165]) ).
fof(f1205,plain,
! [V_q_2,V_pa_2,T_a] :
( ( c_Polynomial_Opoly(T_a,V_pa_2) = c_Polynomial_Opoly(T_a,V_q_2)
<=> V_pa_2 = V_q_2 )
| ~ class_Rings_Oidom(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f1206,plain,
! [V_q_2,V_pa_2,T_a] :
( ( ( V_pa_2 != V_q_2
| c_Polynomial_Opoly(T_a,V_pa_2) = c_Polynomial_Opoly(T_a,V_q_2) )
& ( V_pa_2 = V_q_2
| c_Polynomial_Opoly(T_a,V_pa_2) != c_Polynomial_Opoly(T_a,V_q_2) ) )
| ~ class_Rings_Oidom(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
inference(NNF_transformation,[status(thm)],[f1205]) ).
fof(f1207,plain,
! [T_a] :
( ( ! [V_q_2,V_pa_2] :
( V_pa_2 != V_q_2
| c_Polynomial_Opoly(T_a,V_pa_2) = c_Polynomial_Opoly(T_a,V_q_2) )
& ! [V_q_2,V_pa_2] :
( V_pa_2 = V_q_2
| c_Polynomial_Opoly(T_a,V_pa_2) != c_Polynomial_Opoly(T_a,V_q_2) ) )
| ~ class_Rings_Oidom(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
inference(miniscoping,[status(thm)],[f1206]) ).
fof(f1208,plain,
! [X0,X1,X2] :
( X1 = X2
| c_Polynomial_Opoly(X0,X1) != c_Polynomial_Opoly(X0,X2)
| ~ class_Int_Oring__char__0(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1215,plain,
! [V_x,T_a] :
( hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f1216,plain,
! [T_a] :
( ! [V_x] : hAPP(c_Polynomial_Opoly(T_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))),V_x) = c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1215]) ).
fof(f1217,plain,
! [X0,X1] :
( c_Groups_Ozero__class_Ozero(X0) = hAPP(c_Polynomial_Opoly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1)
| ~ class_Rings_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f1216]) ).
fof(f1407,plain,
! [V_a,T_a] :
( c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a
| ~ class_Groups_Omonoid__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f1408,plain,
! [T_a] :
( ! [V_a] : c_Groups_Oplus__class_Oplus(T_a,V_a,c_Groups_Ozero__class_Ozero(T_a)) = V_a
| ~ class_Groups_Omonoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f1407]) ).
fof(f1409,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(X0,X1,c_Groups_Ozero__class_Ozero(X0)) = X1
| ~ class_Groups_Omonoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1408]) ).
fof(f1447,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) )
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q)) != c_Polynomial_OpCons(T_a,V_r,V_q)
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f1448,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) )
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(T_a),V_p,c_Polynomial_Osmult(T_a,V_c,V_q)) != c_Polynomial_OpCons(T_a,V_r,V_q) )
| ~ class_Rings_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f1447]) ).
fof(f1449,plain,
! [X0,X1,X2,X3,X4] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(X1),X2,c_Polynomial_Osmult(X1,X3,X4)) != c_Polynomial_OpCons(X1,X0,X4)
| ~ class_Rings_Ocomm__semiring__0(X1)
| X0 = hAPP(c_Polynomial_Opoly(X1,X2),X3) ),
inference(cnf_transformation,[status(thm)],[f1448]) ).
fof(f1458,plain,
! [V_pa_2,V_a_2,T_a] :
( ( c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Oidom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f1459,plain,
! [V_pa_2,V_a_2,T_a] :
( ( ( ( V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
& V_a_2 != c_Groups_Ozero__class_Ozero(T_a) )
| c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) )
& ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )
| ~ class_Rings_Oidom(T_a) ),
inference(NNF_transformation,[status(thm)],[f1458]) ).
fof(f1460,plain,
! [T_a] :
( ( ! [V_pa_2,V_a_2] :
( ( V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
& V_a_2 != c_Groups_Ozero__class_Ozero(T_a) )
| c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) )
& ! [V_pa_2,V_a_2] :
( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Polynomial_Osmult(T_a,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)) ) )
| ~ class_Rings_Oidom(T_a) ),
inference(miniscoping,[status(thm)],[f1459]) ).
fof(f1462,plain,
! [X0,X1,X2] :
( X1 != c_Groups_Ozero__class_Ozero(X0)
| c_Polynomial_Osmult(X0,X1,X2) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1460]) ).
fof(f4636,plain,
class_Groups_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1069]) ).
fof(f4638,plain,
class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1071]) ).
fof(f4651,plain,
class_Int_Oring__char__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1084]) ).
fof(f4659,plain,
class_Rings_Oidom(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1092]) ).
fof(f4741,plain,
! [T_1] :
( class_Groups_Omonoid__add(tc_Polynomial_Opoly(T_1))
| ~ class_Groups_Ocomm__monoid__add(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1135]) ).
fof(f4742,plain,
! [X0] :
( class_Groups_Omonoid__add(tc_Polynomial_Opoly(X0))
| ~ class_Groups_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f4741]) ).
fof(f4785,plain,
c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(thm)],[f1160]) ).
fof(f4863,plain,
! [X0,X1] :
( 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)],[f1462]) ).
fof(f4896,plain,
! [X0] :
( v_d____ = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = X0 ),
inference(backward_demodulation,[status(thm)],[f1164,f1166]) ).
fof(f4907,plain,
! [X0] :
( hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0) = v_d____
| v_d____ = X0 ),
inference(forward_demodulation,[status(thm)],[f1164,f4896]) ).
fof(f5122,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0),
inference(resolution,[status(thm)],[f1217,f4638]) ).
fof(f5123,plain,
! [X0] : v_d____ = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),X0),
inference(forward_demodulation,[status(thm)],[f1164,f5122]) ).
fof(f5158,plain,
! [X0] :
( X0 = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____))
| hAPP(X0,sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0)) != v_d____
| sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),X0) = v_d____ ),
inference(paramodulation,[status(thm)],[f4907,f1163]) ).
fof(f5191,definition,
( sQ16_spl
<=> c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f5192,plain,
( ~ sQ16_spl
| c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) ),
inference(component_clause,[status(thm)],[f5191]) ).
fof(f5362,plain,
class_Groups_Omonoid__add(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(resolution,[status(thm)],[f4636,f4742]) ).
fof(f6340,plain,
( c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))
| v_d____ = sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) ),
inference(resolution,[status(thm)],[f5158,f5123]) ).
fof(f6346,definition,
( sQ61_spl
<=> v_d____ = sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f6347,plain,
( ~ sQ61_spl
| v_d____ = sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))) ),
inference(component_clause,[status(thm)],[f6346]) ).
fof(f6349,plain,
( sQ16_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f6340,f6346,f5191]) ).
fof(f6441,plain,
! [X0] : c_Polynomial_Osmult(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex),X0) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(resolution,[status(thm)],[f4863,f4659]) ).
fof(f6442,plain,
! [X0] : c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_Osmult(tc_Complex_Ocomplex,v_d____,X0),
inference(forward_demodulation,[status(thm)],[f1164,f6441]) ).
fof(f6449,definition,
( sQ68_spl
<=> class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f6451,plain,
( sQ68_spl
| ~ class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f6449]) ).
fof(f6456,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X2)
| ~ class_Rings_Ocomm__semiring__0(tc_Complex_Ocomplex)
| X0 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),v_d____) ),
inference(paramodulation,[status(thm)],[f6442,f1449]) ).
fof(f6457,definition,
! [X0,X1,X2] :
( sQ69_spl
<=> ( c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X2)
| X0 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),v_d____) ) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f6458,plain,
! [X0,X1,X2] :
( ~ sQ69_spl
| c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X1,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X2)
| X0 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),v_d____) ),
inference(component_clause,[status(thm)],[f6457]) ).
fof(f6460,plain,
( ~ sQ68_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f6456,f6457,f6449]) ).
fof(f6461,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6451,f4638]) ).
fof(f6462,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f6461]) ).
fof(f6586,plain,
! [X0] : c_Groups_Oplus__class_Oplus(tc_Polynomial_Opoly(tc_Complex_Ocomplex),X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = X0,
inference(resolution,[status(thm)],[f1409,f5362]) ).
fof(f6591,plain,
! [X0,X1,X2] :
( ~ sQ69_spl
| X1 != c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X2)
| X0 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,X1),v_d____) ),
inference(backward_demodulation,[status(thm)],[f6586,f6458]) ).
fof(f6592,plain,
! [X0,X1] :
( ~ sQ69_spl
| X0 = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,X0,X1)),v_d____) ),
inference(destructive_equality_resolution,[status(thm)],[f6591]) ).
fof(f6694,plain,
( ~ sQ61_spl
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____)
| c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))) = c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)) ),
inference(paramodulation,[status(thm)],[f6347,f1163]) ).
fof(f6695,definition,
( sQ86_spl
<=> hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))) = hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f6697,plain,
( sQ86_spl
| hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),sK0_skl(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))) != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____) ),
inference(component_clause,[status(thm)],[f6695]) ).
fof(f6698,plain,
( ~ sQ61_spl
| ~ sQ86_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f6694,f5191,f6695,f6346]) ).
fof(f6760,plain,
( sQ86_spl
| v_d____ != hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)),v_d____) ),
inference(forward_demodulation,[status(thm)],[f5123,f6697]) ).
fof(f6761,plain,
( sQ86_spl
| ~ sQ69_spl
| v_d____ != v_d____ ),
inference(forward_demodulation,[status(thm)],[f6592,f6760]) ).
fof(f6762,plain,
( sQ86_spl
| ~ sQ69_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f6761]) ).
fof(f6763,plain,
( sQ86_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f6762]) ).
fof(f6953,definition,
( sQ96_spl
<=> class_Rings_Oidom(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f6955,plain,
( sQ96_spl
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f6953]) ).
fof(f7102,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6955,f4659]) ).
fof(f7103,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f7102]) ).
fof(f7496,definition,
( sQ122_spl
<=> class_Int_Oring__char__0(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f7498,plain,
( sQ122_spl
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f7496]) ).
fof(f7510,plain,
( sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7498,f4651]) ).
fof(f7511,plain,
sQ122_spl,
inference(contradiction_clause,[status(thm)],[f7510]) ).
fof(f8347,plain,
( ~ sQ16_spl
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____)
| ~ class_Int_Oring__char__0(tc_Complex_Ocomplex)
| ~ class_Rings_Oidom(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f5192,f1208]) ).
fof(f8358,definition,
( sQ151_spl
<=> c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f8359,plain,
( ~ sQ151_spl
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = c_Polynomial_OpCons(tc_Complex_Ocomplex,v_d____,v_ds____) ),
inference(component_clause,[status(thm)],[f8358]) ).
fof(f8361,plain,
( ~ sQ16_spl
| sQ151_spl
| ~ sQ122_spl
| ~ sQ96_spl ),
inference(split_clause,[status(thm)],[f8347,f6953,f7496,f8358,f5191]) ).
fof(f8365,plain,
( ~ sQ151_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8359,f4785]) ).
fof(f8366,plain,
~ sQ151_spl,
inference(contradiction_clause,[status(thm)],[f8365]) ).
fof(f8367,plain,
$false,
inference(sat_refutation,[status(thm)],[f6349,f6460,f6462,f6698,f6763,f7103,f7511,f8361,f8366]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW269+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n003.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % 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:46:15 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.34/0.59 % Drodi V4.1.1
% 183.77/23.89 % Refutation found
% 183.77/23.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 183.77/23.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 59.73/25.22 % Elapsed time: 24.551781 seconds
% 59.73/25.22 % CPU time: 179.909171 seconds
% 59.73/25.22 % Total memory used: 775.398 MB
% 59.73/25.22 % Net memory used: 728.566 MB
%------------------------------------------------------------------------------