%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG432-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.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 : Fri Sep 25 12:52:31 PM UTC 2026
% Result : Unsatisfiable 50.20s 6.88s
% Output : Proof 50.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 38
% Syntax : Number of formulae : 194 ( 98 unt; 0 def)
% Number of atoms : 322 ( 127 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 370 ( 242 ~; 128 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 7 con; 0-4 aty)
% Number of variables : 291 ( 31 sgn 112 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f736,negated_conjecture,
c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f736_nnf,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f736]) ).
fof(f736_sk,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f736_nnf]) ).
cnf(c736,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f736_sk]) ).
cnf(t29,plain,
eq(c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) = false,
inference(equality_encoding,[status(esa)],[c736]) ).
cnf(t599,plain,
eq(c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) = false,
inference(orient,[status(thm)],[t29]) ).
cnf(f714,axiom,
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__pCons_0) ).
fof(f714_nnf,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f714]) ).
fof(f714_sk,plain,
! [T_a,V_a,V_p,V_x] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(V_a,V_p,T_a),V_x,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Otimes__class_Otimes(V_x,c_Polynomial_Opoly(V_p,V_x,T_a),T_a),T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__0(T_a) ),
inference(skolemisation,[status(esa)],[f714_nnf]) ).
cnf(c714,plain,
( c_Polynomial_Opoly(c_Polynomial_OpCons(X1,X2,X0),X3,X0) = c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(X3,c_Polynomial_Opoly(X2,X3,X0),X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f714_sk]) ).
cnf(t142,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X2,X3,X1),X4,X1),c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X4,c_Polynomial_Opoly(X3,X4,X1),X1),X1)) = c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X4,c_Polynomial_Opoly(X3,X4,X1),X1),X1),
inference(equality_encoding,[status(esa)],[c714]) ).
cnf(t567,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X2,X3,X1),X4,X1),c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X4,c_Polynomial_Opoly(X3,X4,X1),X1),X1)) = c_HOL_Oplus__class_Oplus(X2,c_HOL_Otimes__class_Otimes(X4,c_Polynomial_Opoly(X3,X4,X1),X1),X1),
inference(orient,[status(thm)],[t142]) ).
cnf(f473,axiom,
( 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',cls_poly__smult_0) ).
fof(f473_nnf,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(nnf_transformation,[status(thm)],[f473]) ).
fof(f473_sk,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(skolemisation,[status(esa)],[f473_nnf]) ).
cnf(c473,plain,
( c_Polynomial_Opoly(c_Polynomial_Osmult(X1,X2,X0),X3,X0) = c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(X0) ),
inference(cnf_transformation,[status(esa)],[f473_sk]) ).
cnf(t81,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,X3,X1),X4,X1),c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X3,X4,X1),X1)) = c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X3,X4,X1),X1),
inference(equality_encoding,[status(esa)],[c473]) ).
cnf(t563,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__0(X1),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,X3,X1),X4,X1),c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X3,X4,X1),X1)) = c_HOL_Otimes__class_Otimes(X2,c_Polynomial_Opoly(X3,X4,X1),X1),
inference(orient,[status(thm)],[t81]) ).
cnf(f735,negated_conjecture,
c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f735_nnf,plain,
c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f735]) ).
cnf(c735,plain,
c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f735_nnf]) ).
cnf(t9,plain,
c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(equality_encoding,[status(esa)],[c735]) ).
cnf(t592,plain,
c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t9]) ).
cnf(t593,plain,
c_HOL_Otimes__class_Otimes(X1,c_Polynomial_Opoly(v_p,v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t563,t592]) ).
cnf(t5612,plain,
c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t593,t592]) ).
cnf(f650,axiom,
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I10_J_0) ).
fof(f650_nnf,plain,
! [T_a,V_a] :
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f650]) ).
fof(f650_sk,plain,
! [T_a,V_a] :
( c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f650_nnf]) ).
cnf(c650,plain,
( c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(X0),X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f650_sk]) ).
cnf(t33,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(X1),X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(equality_encoding,[status(esa)],[c650]) ).
cnf(t453,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_HOL_Otimes__class_Otimes(X2,c_HOL_Ozero__class_Ozero(X1),X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(orient,[status(thm)],[t33]) ).
cnf(f853,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1) ).
fof(f853_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f853]) ).
cnf(c853,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f853_nnf]) ).
cnf(t1,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c853]) ).
cnf(t382,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t454,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(true,true,c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t453,t382]) ).
cnf(t10,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t216,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t5552,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t454,t216]) ).
cnf(t1315,plain,
c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t5552]) ).
cnf(t5613,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t5612,t1315]) ).
cnf(f854,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
fof(f854_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f854]) ).
cnf(c854,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f854_nnf]) ).
cnf(t0,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c854]) ).
cnf(t447,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t5614,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(true,true,c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t5613,t447]) ).
cnf(t5615,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t5614,t216]) ).
cnf(t2953,plain,
c_Polynomial_Opoly(c_Polynomial_Osmult(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t5615]) ).
cnf(t2955,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_Polynomial_Opoly(c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t567,t2953]) ).
cnf(t5702,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t2955,t2953]) ).
cnf(t5703,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t5702,t1315]) ).
cnf(f703,axiom,
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Osemiring__rules_I6_J_0) ).
fof(f703_nnf,plain,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f703]) ).
fof(f703_sk,plain,
! [T_a,V_a] :
( c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f703_nnf]) ).
cnf(c703,plain,
( c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(X0),X0) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f703_sk]) ).
cnf(t19,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_HOL_Oplus__class_Oplus(X2,c_HOL_Ozero__class_Ozero(X1),X1),X2) = X2,
inference(equality_encoding,[status(esa)],[c703]) ).
cnf(t219,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_HOL_Oplus__class_Oplus(X2,c_HOL_Ozero__class_Ozero(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t392,plain,
X1 = ifeq(true,true,c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),X1),
inference(cp,[status(thm)],[t219,t382]) ).
cnf(t5546,plain,
X1 = c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t392,t216]) ).
cnf(t1016,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t5546]) ).
cnf(t5704,plain,
X1 = ifeq(class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t5703,t1016]) ).
cnf(t5705,plain,
X1 = ifeq(true,true,c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(X1,c_HOL_Otimes__class_Otimes(v_x,c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t5704,t447]) ).
cnf(t5706,plain,
X1 = c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t5705,t216]) ).
cnf(t5484,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,c_Polynomial_Osmult(X2,v_p,tc_Complex_Ocomplex),tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t5706]) ).
cnf(f184,axiom,
( c_Polynomial_Osmult(c_HOL_Oone__class_Oone(T_a),V_p,T_a) = V_p
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_smult__1__left_0) ).
fof(f184_nnf,plain,
! [T_a,V_p] :
( c_Polynomial_Osmult(c_HOL_Oone__class_Oone(T_a),V_p,T_a) = V_p
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [T_a,V_p] :
( c_Polynomial_Osmult(c_HOL_Oone__class_Oone(T_a),V_p,T_a) = V_p
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( c_Polynomial_Osmult(c_HOL_Oone__class_Oone(X0),X1,X0) = X1
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(t25,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_Polynomial_Osmult(c_HOL_Oone__class_Oone(X1),X2,X1),X2) = X2,
inference(equality_encoding,[status(esa)],[c184]) ).
cnf(t221,plain,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X1),true,c_Polynomial_Osmult(c_HOL_Oone__class_Oone(X1),X2,X1),X2) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t390,plain,
X1 = ifeq(true,true,c_Polynomial_Osmult(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),X1),
inference(cp,[status(thm)],[t221,t382]) ).
cnf(t5544,plain,
X1 = c_Polynomial_Osmult(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t390,t216]) ).
cnf(t967,plain,
c_Polynomial_Osmult(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t5544]) ).
cnf(t5486,plain,
X1 = c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t5484,t967]) ).
cnf(t5495,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(X1,v_p,tc_Complex_Ocomplex),v_x,tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t5486]) ).
cnf(t5707,plain,
eq(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t599,t5495]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t401,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t5708,plain,
true = false,
inference(step,[status(thm)],[t5707,t401]) ).
cnf(t5503,plain,
true = false,
inference(rw,[status(thm)],[t5708]) ).
cnf(t5526,plain,
false = true,
inference(orient,[status(thm)],[t5503]) ).
cnf(f51,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f51_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(f52,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f52_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(f126,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f126_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f126_nnf]) ).
cnf(c126,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(f132,axiom,
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__pos__poly__0_0) ).
fof(f132_nnf,plain,
! [T_a] :
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [T_a] :
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(T_a)),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c132,plain,
( ~ c_Polynomial_Opos__poly(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(f140,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f140_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f140]) ).
fof(f140_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f140_nnf]) ).
cnf(c140,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
cnf(f221,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f221_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c221,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f265,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f265_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c265,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f266,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f266_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f266]) ).
fof(f266_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f266_nnf]) ).
cnf(c266,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f266_sk]) ).
cnf(f320,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f320_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f320]) ).
fof(f320_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f320_nnf]) ).
cnf(c320,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f320_sk]) ).
cnf(f378,axiom,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_complex__i__not__one_0) ).
fof(f378_nnf,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f378]) ).
fof(f378_sk,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f378_nnf]) ).
cnf(c378,plain,
c_Complex_Oii != c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f412,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f412_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f412]) ).
fof(f412_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f412_nnf]) ).
cnf(c412,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f434,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f434_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f434]) ).
fof(f434_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c434,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f535,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f535_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f535]) ).
fof(f535_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f535_nnf]) ).
cnf(c535,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f535_sk]) ).
cnf(f536,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f536_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f536]) ).
fof(f536_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f536_nnf]) ).
cnf(c536,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f536_sk]) ).
cnf(f550,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f550_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f550]) ).
fof(f550_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f550_nnf]) ).
cnf(c550,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f550_sk]) ).
cnf(f551,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f551_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f551]) ).
fof(f551_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f551_nnf]) ).
cnf(c551,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f551_sk]) ).
cnf(f557,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f557_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f557]) ).
fof(f557_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f557_nnf]) ).
cnf(c557,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f557_sk]) ).
cnf(f589,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f589_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(nnf_transformation,[status(thm)],[f589]) ).
fof(f589_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
inference(skolemisation,[status(esa)],[f589_nnf]) ).
cnf(c589,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(X0),X0),X0)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(X0) ),
inference(cnf_transformation,[status(esa)],[f589_sk]) ).
cnf(f612,axiom,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__iszero__1_0) ).
fof(f612_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f612]) ).
fof(f612_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f612_nnf]) ).
cnf(c612,plain,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Osemiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f612_sk]) ).
cnf(f631,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f631_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f631]) ).
fof(f631_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f631_nnf]) ).
cnf(c631,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f631_sk]) ).
cnf(f632,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f632_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f632]) ).
fof(f632_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f632_nnf]) ).
cnf(c632,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f632_sk]) ).
cnf(f633,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f633_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f633]) ).
fof(f633_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f633_nnf]) ).
cnf(c633,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f633_sk]) ).
cnf(f634,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f634_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f634]) ).
fof(f634_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f634_nnf]) ).
cnf(c634,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f634_sk]) ).
cnf(f655,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f655_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(f667,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f667_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f667]) ).
fof(f667_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f667_nnf]) ).
cnf(c667,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f667_sk]) ).
cnf(f696,axiom,
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp__not__eq__zero_0) ).
fof(f696_nnf,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(nnf_transformation,[status(thm)],[f696]) ).
fof(f696_sk,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(skolemisation,[status(esa)],[f696_nnf]) ).
cnf(c696,plain,
( c_Transcendental_Oexp(X1,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| ~ class_SEQ_Obanach(X0) ),
inference(cnf_transformation,[status(esa)],[f696_sk]) ).
cnf(f718,axiom,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_complex__i__not__zero_0) ).
fof(f718_nnf,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f718]) ).
fof(f718_sk,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f718_nnf]) ).
cnf(c718,plain,
c_Complex_Oii != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f718_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c51,c52,c126,c132,c140,c221,c265,c266,c320,c378,c412,c434,c535,c536,c550,c551,c557,c589,c612,c631,c632,c633,c634,c655,c667,c696,c718,c736]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5526]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG432-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.44 % Computer : n001.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 05:43:54 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 50.20/6.88 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.20/6.88 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------