%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG401-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 11:49:21 AM UTC 2026
% Result : Unsatisfiable 53.09s 12.38s
% Output : CNFRefutation 47.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 19
% Syntax : Number of formulae : 73 ( 24 unt; 4 def)
% Number of atoms : 146 ( 43 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 145 ( 72 ~; 69 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 5 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 109 ( 109 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f247,axiom,
! [T_a,V_p] :
( c_HOL_Oplus__class_Oplus(V_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f659,axiom,
! [T_a,V_p,V_q] :
( V_q = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f660,axiom,
! [T_a,V_p] :
( c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f666,axiom,
! [T_a,V_p,V_c,V_q,V_r] :
( V_r = c_Polynomial_Opoly(V_p,V_c,T_a)
| c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a)) != c_Polynomial_OpCons(V_r,V_q,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f673,axiom,
! [T_a,V_p,V_q,V_a] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(V_a,V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))
| c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f674,axiom,
! [T_a,V_p,V_a,V_q] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a))
| c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f758,axiom,
! [V_z] : c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),V_z,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(V_z,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),V_z,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f852,axiom,
! [T_a,V_x,V_y] :
( c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f866,axiom,
c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f878,axiom,
v_s____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f880,negated_conjecture,
c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f988,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f989,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f998,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1011,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1460,plain,
! [T_a] :
( ! [V_p] : c_HOL_Oplus__class_Oplus(V_p,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a)) = V_p
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(miniscoping,[status(thm)],[f247]) ).
fof(f1461,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0)) = X1
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1460]) ).
fof(f2146,plain,
! [T_a,V_q] :
( V_q = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a))
| ! [V_p] : ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f659]) ).
fof(f2147,plain,
! [X0,X1,X2] :
( X2 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0),X2,tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f2146]) ).
fof(f2148,plain,
! [T_a] :
( ! [V_p] : c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(T_a),V_p,T_a),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(miniscoping,[status(thm)],[f660]) ).
fof(f2149,plain,
! [X0,X1] :
( c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(X0),X1,X0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f2148]) ).
fof(f2160,plain,
! [T_a,V_p,V_c,V_r] :
( V_r = c_Polynomial_Opoly(V_p,V_c,T_a)
| ! [V_q] : c_HOL_Oplus__class_Oplus(V_p,c_Polynomial_Osmult(V_c,V_q,T_a),tc_Polynomial_Opoly(T_a)) != c_Polynomial_OpCons(V_r,V_q,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f666]) ).
fof(f2161,plain,
! [X0,X1,X2,X3,X4] :
( X4 = c_Polynomial_Opoly(X1,X2,X0)
| c_HOL_Oplus__class_Oplus(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0)) != c_Polynomial_OpCons(X4,X3,X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(thm)],[f2160]) ).
fof(f2174,plain,
! [T_a,V_p,V_q] :
( ! [V_a] : ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(V_a,V_p,T_a),V_q,tc_Polynomial_Opoly(T_a))
| c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f673]) ).
fof(f2175,plain,
! [X0,X1,X2,X3] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(X3,X1,X0),X2,tc_Polynomial_Opoly(X0))
| c_Ring__and__Field_Odvd__class_Odvd(X1,X2,tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f2174]) ).
fof(f2176,plain,
! [T_a,V_p,V_q] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(V_p,V_q,tc_Polynomial_Opoly(T_a))
| ! [V_a] : c_Ring__and__Field_Odvd__class_Odvd(V_p,c_Polynomial_Osmult(V_a,V_q,T_a),tc_Polynomial_Opoly(T_a))
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f674]) ).
fof(f2177,plain,
! [X0,X1,X2,X3] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(X1,X3,tc_Polynomial_Opoly(X0))
| c_Ring__and__Field_Odvd__class_Odvd(X1,c_Polynomial_Osmult(X2,X3,X0),tc_Polynomial_Opoly(X0))
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f2176]) ).
fof(f2316,plain,
! [X0] : c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f758]) ).
fof(f2485,plain,
! [T_a] :
( ! [V_x,V_y] : c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f852]) ).
fof(f2486,plain,
! [X0,X1,X2] :
( c_HOL_Otimes__class_Otimes(X1,X2,X0) = c_HOL_Otimes__class_Otimes(X2,X1,X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f2485]) ).
fof(f2511,plain,
c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f866]) ).
fof(f2533,plain,
v_s____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(cnf_transformation,[status(thm)],[f878]) ).
fof(f2535,plain,
c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),v_w____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f880]) ).
fof(f2643,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f988]) ).
fof(f2644,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f989]) ).
fof(f2653,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f998]) ).
fof(f2666,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f1011]) ).
fof(f2846,plain,
! [X0] : c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),c_Polynomial_Opoly(c_Polynomial_OpCons(v_a____,v_s____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2511,f2316]) ).
fof(f3393,definition,
( sQ79_spl
<=> class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f3394,plain,
( ~ sQ79_spl
| class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f3393]) ).
fof(f3395,plain,
( sQ79_spl
| ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f3393]) ).
fof(f3411,plain,
! [X0,X1,X2] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(X0,X2,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(X0,c_Polynomial_Osmult(X1,X2,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolution,[status(thm)],[f2643,f2177]) ).
fof(f3412,plain,
! [X0,X1,X2] :
( ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(X2,X0,tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(X0,X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolution,[status(thm)],[f2643,f2175]) ).
fof(f3421,definition,
( sQ83_spl
<=> class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f3423,plain,
( sQ83_spl
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f3421]) ).
fof(f3445,plain,
( sQ83_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2644,f3423]) ).
fof(f3446,plain,
sQ83_spl,
inference(contradiction_clause,[status(thm)],[f3445]) ).
fof(f3546,plain,
( sQ79_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2666,f3395]) ).
fof(f3547,plain,
sQ79_spl,
inference(contradiction_clause,[status(thm)],[f3546]) ).
fof(f3586,plain,
! [X0,X1] :
( ~ sQ79_spl
| X1 = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolution,[status(thm)],[f3394,f2147]) ).
fof(f3738,plain,
! [X0] :
( ~ class_Ring__and__Field_Ofield(tc_Complex_Ocomplex)
| c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolution,[status(thm)],[f3412,f2149]) ).
fof(f3742,definition,
! [X0] :
( sQ102_spl
<=> c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f3743,plain,
! [X0] :
( ~ sQ102_spl
| c_Ring__and__Field_Odvd__class_Odvd(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(component_clause,[status(thm)],[f3742]) ).
fof(f3745,plain,
( ~ sQ79_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f3738,f3742,f3393]) ).
fof(f3747,plain,
! [X0] :
( ~ sQ102_spl
| c_Ring__and__Field_Odvd__class_Odvd(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(forward_demodulation,[status(thm)],[f2533,f3743]) ).
fof(f3828,plain,
! [X0,X1] :
( ~ sQ79_spl
| X1 = v_s____
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(forward_demodulation,[status(thm)],[f2533,f3586]) ).
fof(f3832,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ c_Ring__and__Field_Odvd__class_Odvd(c_Polynomial_Osmult(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),X1,tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex) = v_s____ ),
inference(resolution,[status(thm)],[f3828,f3411]) ).
fof(f3843,plain,
! [X0] :
( ~ sQ102_spl
| ~ sQ79_spl
| c_Polynomial_Osmult(X0,v_s____,tc_Complex_Ocomplex) = v_s____ ),
inference(resolution,[status(thm)],[f3832,f3747]) ).
fof(f7356,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0,
inference(resolution,[status(thm)],[f1461,f2653]) ).
fof(f7359,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = X0,
inference(forward_demodulation,[status(thm)],[f2533,f7356]) ).
fof(f12620,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,X0,tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2486,f2643]) ).
fof(f20918,plain,
! [X0,X1,X2] :
( ~ sQ102_spl
| ~ sQ79_spl
| X1 = c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex)
| c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex)
| ~ class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f3843,f2161]) ).
fof(f20951,definition,
! [X0,X1,X2] :
( sQ1158_spl
<=> ( X1 = c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex)
| c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex) ) ),
introduced(definition,[new_symbols(definition,[sQ1158_spl])],[split_symbol_definition]) ).
fof(f20952,plain,
! [X0,X1,X2] :
( ~ sQ1158_spl
| X1 = c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex)
| c_HOL_Oplus__class_Oplus(X0,v_s____,tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f20951]) ).
fof(f20954,plain,
( ~ sQ102_spl
| ~ sQ79_spl
| sQ1158_spl
| ~ sQ83_spl ),
inference(split_clause,[status(thm)],[f20918,f3421,f20951,f3393,f3742]) ).
fof(f20957,plain,
! [X0,X1,X2] :
( ~ sQ1158_spl
| X1 = c_Polynomial_Opoly(X0,X2,tc_Complex_Ocomplex)
| X0 != c_Polynomial_OpCons(X1,v_s____,tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f7359,f20952]) ).
fof(f20958,plain,
! [X0,X1] :
( ~ sQ1158_spl
| X0 = c_Polynomial_Opoly(c_Polynomial_OpCons(X0,v_s____,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) ),
inference(destructive_equality_resolution,[status(thm)],[f20957]) ).
fof(f21227,plain,
! [X0] :
( ~ sQ1158_spl
| c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),X0,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(X0,v_k____,tc_Complex_Ocomplex),v_a____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(backward_demodulation,[status(thm)],[f20958,f2846]) ).
fof(f21229,plain,
( ~ sQ1158_spl
| c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),v_a____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(backward_demodulation,[status(thm)],[f21227,f2535]) ).
fof(f21312,plain,
( ~ sQ1158_spl
| c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(v_a____,c_Power_Opower__class_Opower(v_w____,v_k____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f12620,f21229]) ).
fof(f21314,plain,
( ~ sQ1158_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f21312]) ).
fof(f21315,plain,
~ sQ1158_spl,
inference(contradiction_clause,[status(thm)],[f21314]) ).
fof(f21316,plain,
$false,
inference(sat_refutation,[status(thm)],[f3446,f3547,f3745,f20954,f21315]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG401-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n014.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Mon Sep 21 13:19:25 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.23/5.57 % Drodi V4.1.1
% 53.09/12.38 % Refutation found
% 53.09/12.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 53.09/12.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.29/12.85 % Elapsed time: 7.374945 seconds
% 4.29/12.85 % CPU time: 54.912704 seconds
% 4.29/12.85 % Total memory used: 484.217 MB
% 4.29/12.85 % Net memory used: 467.252 MB
%------------------------------------------------------------------------------