%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG398-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:20 AM UTC 2026
% Result : Unsatisfiable 91.67s 12.24s
% Output : CNFRefutation 93.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of formulae : 55 ( 31 unt; 2 def)
% Number of atoms : 81 ( 47 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 58 ( 32 ~; 24 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 65 ( 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [T_a,V_a] :
( V_a = c_HOL_Ozero__class_Ozero(T_a)
| c_HOL_Oinverse__class_Odivide(V_a,V_a,T_a) = c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f413,axiom,
! [T_a,V_a] :
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f766,axiom,
c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f785,axiom,
! [V_x,V_y] : c_HOL_Oinverse__class_Odivide(V_x,V_y,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(V_x,c_HOL_Oinverse__class_Oinverse(V_y,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f810,axiom,
c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f814,axiom,
! [T_a,V_lx,V_ly,V_rx] :
( c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,V_rx,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f830,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/sandbox/benchmark/theBenchmark.p') ).
fof(f832,axiom,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f835,negated_conjecture,
c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(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_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f879,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f880,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f900,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1023,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = X1
| c_HOL_Oinverse__class_Odivide(X1,X1,X0) = c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f1649,plain,
! [T_a] :
( ! [V_a] : c_HOL_Otimes__class_Otimes(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f413]) ).
fof(f1650,plain,
! [X0,X1] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X1)
| c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(X1),X1) = X0 ),
inference(cnf_transformation,[status(thm)],[f1649]) ).
fof(f2223,plain,
c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f766]) ).
fof(f2258,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Oinverse(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X0,X1,tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f785]) ).
fof(f2301,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f810]) ).
fof(f2308,plain,
! [T_a] :
( ! [V_lx,V_ly,V_rx] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,V_rx,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(miniscoping,[status(thm)],[f814]) ).
fof(f2309,plain,
! [X0,X1,X2,X3] :
( c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X1,X2,X0),X3,X0) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Otimes__class_Otimes(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(thm)],[f2308]) ).
fof(f2338,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)],[f830]) ).
fof(f2339,plain,
! [X0,X1,X2] :
( ~ class_Ring__and__Field_Ocomm__semiring__1(X2)
| c_HOL_Otimes__class_Otimes(X0,X1,X2) = c_HOL_Otimes__class_Otimes(X1,X0,X2) ),
inference(cnf_transformation,[status(thm)],[f2338]) ).
fof(f2342,plain,
! [T_a] :
( ! [V_a,V_p,V_x] : c_Polynomial_Opoly(c_Polynomial_Osmult(V_a,V_p,T_a),V_x,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_Polynomial_Opoly(V_p,V_x,T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(miniscoping,[status(thm)],[f832]) ).
fof(f2343,plain,
! [X0,X1,X2,X3] :
( ~ class_Ring__and__Field_Ocomm__semiring__0(X2)
| c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,X2),X3,X2) = c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Opoly(X1,X3,X2),X2) ),
inference(cnf_transformation,[status(thm)],[f2342]) ).
fof(f2347,plain,
c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(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_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_q____,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f835]) ).
fof(f2391,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f2392,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f880]) ).
fof(f2412,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(thm)],[f900]) ).
fof(f2480,plain,
c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f2223,f2301]) ).
fof(f2481,plain,
c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(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_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f2223,f2347]) ).
fof(f2482,plain,
c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(c_Polynomial_Osmult(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_q____,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2223,f2481]) ).
fof(f2486,plain,
! [X0] :
( X0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Oinverse__class_Odivide(X0,X0,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) ),
inference(resolution,[status(thm)],[f1023,f2412]) ).
fof(f2512,plain,
! [X0] : X0 = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f1650,f2391]) ).
fof(f2571,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)],[f2339,f2391]) ).
fof(f2791,plain,
! [X0,X1] : c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(X0,tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(X1,X0,tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f2571,f2258]) ).
fof(f7153,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2309,f2391]) ).
fof(f7376,plain,
! [X0,X1,X2] : c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X1,c_HOL_Oinverse__class_Oinverse(X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(paramodulation,[status(thm)],[f7153,f2258]) ).
fof(f7427,plain,
! [X0,X1,X2] : c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_HOL_Oinverse__class_Odivide(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2258,f7376]) ).
fof(f11801,plain,
! [X0,X1,X2] : c_Polynomial_Opoly(c_Polynomial_Osmult(X0,X1,tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X0,c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolution,[status(thm)],[f2343,f2392]) ).
fof(f11803,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),
inference(backward_demodulation,[status(thm)],[f11801,f2482]) ).
fof(f11805,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Oinverse__class_Oinverse(c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f7153,f11803]) ).
fof(f11806,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f2791,f11805]) ).
fof(f11807,plain,
c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(forward_demodulation,[status(thm)],[f7427,f11806]) ).
fof(f11809,plain,
( c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(paramodulation,[status(thm)],[f2486,f11807]) ).
fof(f11810,definition,
( sQ161_spl
<=> c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f11812,plain,
( sQ161_spl
| c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_HOL_Otimes__class_Otimes(c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f11810]) ).
fof(f11817,definition,
( sQ163_spl
<=> c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f11818,plain,
( ~ sQ163_spl
| c_Polynomial_Opoly(v_pa____,v_c____,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f11817]) ).
fof(f11820,plain,
( sQ163_spl
| ~ sQ161_spl ),
inference(split_clause,[status(thm)],[f11809,f11810,f11817]) ).
fof(f11821,plain,
( sQ161_spl
| c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) != c_Polynomial_Opoly(v_q____,v_x,tc_Complex_Ocomplex) ),
inference(forward_demodulation,[status(thm)],[f2512,f11812]) ).
fof(f11822,plain,
( sQ161_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11821]) ).
fof(f11823,plain,
sQ161_spl,
inference(contradiction_clause,[status(thm)],[f11822]) ).
fof(f11824,plain,
( ~ sQ163_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11818,f2480]) ).
fof(f11825,plain,
~ sQ163_spl,
inference(contradiction_clause,[status(thm)],[f11824]) ).
fof(f11826,plain,
$false,
inference(sat_refutation,[status(thm)],[f11820,f11823,f11825]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG398-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 13:21:15 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.44 % Drodi V4.1.1
% 91.67/12.24 % Refutation found
% 91.67/12.24 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 91.67/12.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 93.56/12.33 % Elapsed time: 11.946994 seconds
% 93.56/12.33 % CPU time: 94.121688 seconds
% 93.56/12.33 % Total memory used: 624.840 MB
% 93.56/12.33 % Net memory used: 603.747 MB
%------------------------------------------------------------------------------