%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV617-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 : n010.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 03:13:48 PM UTC 2026
% Result : Unsatisfiable 79.34s 25.69s
% Output : Proof 79.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 41
% Syntax : Number of formulae : 207 ( 99 unt; 0 def)
% Number of atoms : 379 ( 109 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 463 ( 291 ~; 172 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-4 aty)
% Number of variables : 330 ( 27 sgn 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f651,axiom,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__unity_0) ).
fof(f651_nnf,plain,
! [V_n] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f651]) ).
fof(f651_sk,plain,
! [V_n] : c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(V_n),V_n,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f651_nnf]) ).
cnf(c651,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X0),X0,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(t44,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X1,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(equality_encoding,[status(esa)],[c651]) ).
cnf(t3246,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X1,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t44]) ).
cnf(f650,axiom,
( c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),V_n,T_a) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(V_a,V_n,T_a),c_Power_Opower__class_Opower(V_b,V_n,T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__divide_0) ).
fof(f650_nnf,plain,
! [T_a,V_a,V_b,V_n] :
( c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),V_n,T_a) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(V_a,V_n,T_a),c_Power_Opower__class_Opower(V_b,V_n,T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(nnf_transformation,[status(thm)],[f650]) ).
fof(f650_sk,plain,
! [T_a,V_a,V_b,V_n] :
( c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(V_a,V_b,T_a),V_n,T_a) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(V_a,V_n,T_a),c_Power_Opower__class_Opower(V_b,V_n,T_a),T_a)
| ~ class_Ring__and__Field_Odivision__by__zero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(skolemisation,[status(esa)],[f650_nnf]) ).
cnf(c650,plain,
( c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,X2,X0),X3,X0) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X3,X0),c_Power_Opower__class_Opower(X2,X3,X0),X0)
| ~ class_Ring__and__Field_Odivision__by__zero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(esa)],[f650_sk]) ).
cnf(t243,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,ifeq(class_Ring__and__Field_Odivision__by__zero(X1),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X2,X3,X1),X4,X1),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1)) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1),
inference(equality_encoding,[status(esa)],[c650]) ).
cnf(t2001,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,ifeq(class_Ring__and__Field_Odivision__by__zero(X1),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X2,X3,X1),X4,X1),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1)) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X2,X4,X1),c_Power_Opower__class_Opower(X3,X4,X1),X1),
inference(orient,[status(thm)],[t243]) ).
cnf(t3249,plain,
c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X2),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),true,ifeq(class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X2),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t2001,t3246]) ).
cnf(t4735,plain,
c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),true,ifeq(class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X2),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t3249,t3246]) ).
cnf(f646,axiom,
( c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide__1_0) ).
fof(f646_nnf,plain,
! [T_a,V_a] :
( c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(nnf_transformation,[status(thm)],[f646]) ).
fof(f646_sk,plain,
! [T_a,V_a] :
( c_HOL_Oinverse__class_Odivide(V_a,c_HOL_Oone__class_Oone(T_a),T_a) = V_a
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(skolemisation,[status(esa)],[f646_nnf]) ).
cnf(c646,plain,
( c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(X0),X0) = X1
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(esa)],[f646_sk]) ).
cnf(hi619,axiom,
ifeq(class_Ring__and__Field_Ofield(X0),true,c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(X0),X0),X1) = X1,
inference(equality_encoding,[status(esa)],[c646]) ).
cnf(f757,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ofield) ).
fof(f757_nnf,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f757]) ).
cnf(c757,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f757_nnf]) ).
cnf(hi728,axiom,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c757]) ).
cnf(t21,plain,
c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(hyper_resolution,[status(thm)],[hi619,hi728]) ).
cnf(t261,plain,
c_HOL_Oinverse__class_Odivide(X1,c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t4736,plain,
c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),true,ifeq(class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X2),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t4735,t261]) ).
cnf(t3,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c757]) ).
cnf(t1848,plain,
class_Ring__and__Field_Ofield(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t4737,plain,
c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex) = ifeq(true,true,ifeq(class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X2),X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t4736,t1848]) ).
cnf(t41,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t41]) ).
cnf(t4738,plain,
c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex) = ifeq(class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t4737,t256]) ).
cnf(f742,axiom,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__F_h41c08bf998eef835) ).
fof(f742_nnf,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f742]) ).
cnf(c742,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f742_nnf]) ).
cnf(t2,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c742]) ).
cnf(t1715,plain,
class_Ring__and__Field_Odivision__by__zero(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t4739,plain,
c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex) = ifeq(true,true,c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t4738,t1715]) ).
cnf(t4740,plain,
c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t4739,t256]) ).
cnf(t4635,plain,
c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(X1,c_FFT__Mirabelle_Oroot(X2),tc_Complex_Ocomplex),X2,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(X1,X2,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t4740]) ).
cnf(t63,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t257,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t63]) ).
cnf(f662,axiom,
( 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',cls_divide__self_0) ).
fof(f662_nnf,plain,
! [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) ),
inference(nnf_transformation,[status(thm)],[f662]) ).
fof(f662_sk,plain,
! [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) ),
inference(skolemisation,[status(esa)],[f662_nnf]) ).
cnf(c662,plain,
( X1 = c_HOL_Ozero__class_Ozero(X0)
| c_HOL_Oinverse__class_Odivide(X1,X1,X0) = c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(esa)],[f662_sk]) ).
cnf(t112,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,or(eq(c_HOL_Oinverse__class_Odivide(X2,X2,X1),c_HOL_Oone__class_Oone(X1)),eq(X2,c_HOL_Ozero__class_Ozero(X1))),true) = true,
inference(equality_encoding,[status(esa)],[c662]) ).
cnf(t728,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,or(eq(c_HOL_Oinverse__class_Odivide(X2,X2,X1),c_HOL_Oone__class_Oone(X1)),eq(X2,c_HOL_Ozero__class_Ozero(X1))),true) = true,
inference(orient,[status(thm)],[t112]) ).
cnf(f640,axiom,
c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_root__nonzero_0) ).
fof(f640_nnf,plain,
! [V_n] : c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f640]) ).
fof(f640_sk,plain,
! [V_n] : c_FFT__Mirabelle_Oroot(V_n) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f640_nnf]) ).
cnf(c640,plain,
c_FFT__Mirabelle_Oroot(X0) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f640_sk]) ).
cnf(t40,plain,
eq(c_FFT__Mirabelle_Oroot(X1),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) = false,
inference(equality_encoding,[status(esa)],[c640]) ).
cnf(t3317,plain,
eq(c_FFT__Mirabelle_Oroot(X1),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) = false,
inference(orient,[status(thm)],[t40]) ).
cnf(t3320,plain,
true = ifeq(class_Ring__and__Field_Ofield(tc_Complex_Ocomplex),true,or(eq(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),false),true),
inference(cp,[status(thm)],[t728,t3317]) ).
cnf(t4721,plain,
true = ifeq(true,true,or(eq(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),false),true),
inference(step,[status(thm)],[t3320,t1848]) ).
cnf(t4722,plain,
true = or(eq(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),false),
inference(step,[status(thm)],[t4721,t256]) ).
cnf(t6,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t267,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t4723,plain,
true = eq(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
inference(step,[status(thm)],[t4722,t267]) ).
cnf(t4429,plain,
eq(c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)) = true,
inference(orient,[status(thm)],[t4723]) ).
cnf(t4430,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = ifeq(true,true,c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t257,t4429]) ).
cnf(t4724,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t4430,t256]) ).
cnf(t4432,plain,
c_HOL_Oinverse__class_Odivide(c_FFT__Mirabelle_Oroot(X1),c_FFT__Mirabelle_Oroot(X1),tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t4724]) ).
cnf(t4636,plain,
c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(X1),X1,tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t4635,t4432]) ).
cnf(t4741,plain,
c_HOL_Oone__class_Oone(tc_Complex_Ocomplex) = c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t4636,t3246]) ).
cnf(t4653,plain,
c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t4741]) ).
cnf(f655,axiom,
( c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_eq__iff__diff__eq__0_0) ).
fof(f655_nnf,plain,
! [T_a,V_x] :
( c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [T_a,V_x] :
( c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
( c_HOL_Ominus__class_Ominus(X1,X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_OrderedGroup_Oab__group__add(X0) ),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(hi627,axiom,
ifeq(class_OrderedGroup_Oab__group__add(X0),true,c_HOL_Ominus__class_Ominus(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0)) = c_HOL_Ozero__class_Ozero(X0),
inference(equality_encoding,[status(esa)],[c655]) ).
cnf(f752,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Oab__group__add) ).
fof(f752_nnf,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f752]) ).
cnf(c752,plain,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f752_nnf]) ).
cnf(hi723,axiom,
class_OrderedGroup_Oab__group__add(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c752]) ).
cnf(t22,plain,
c_HOL_Ominus__class_Ominus(X1,X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(hyper_resolution,[status(thm)],[hi627,hi723]) ).
cnf(t2237,plain,
c_HOL_Ominus__class_Ominus(X1,X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t22]) ).
cnf(f669,axiom,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_divide__zero__left_0) ).
fof(f669_nnf,plain,
! [T_a,V_a] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
! [T_a,V_a] :
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ofield(T_a) ),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c669,plain,
( c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X0),X1,X0) = c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ofield(X0) ),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
cnf(t92,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X1),X2,X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(equality_encoding,[status(esa)],[c669]) ).
cnf(t2005,plain,
ifeq(class_Ring__and__Field_Ofield(X1),true,c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(X1),X2,X1),c_HOL_Ozero__class_Ozero(X1)) = c_HOL_Ozero__class_Ozero(X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t2006,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = ifeq(true,true,c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(cp,[status(thm)],[t2005,t1848]) ).
cnf(t4672,plain,
c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex),
inference(step,[status(thm)],[t2006,t256]) ).
cnf(t3446,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),X1,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t4672]) ).
cnf(f28,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f28_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(f30,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f30_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f32,axiom,
( ~ c_lessequals(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_linorder__not__less_1) ).
fof(f32_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(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)],[f32]) ).
fof(f32_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(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)],[f32_nnf]) ).
cnf(c32,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(f35,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f35_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f224,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(f224_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)],[f224]) ).
fof(f224_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)],[f224_nnf]) ).
cnf(c224,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)],[f224_sk]) ).
cnf(f235,axiom,
( ~ c_lessequals(c_Power_Opower__class_Opower(V_x,c_HOL_Ozero__class_Ozero(tc_nat),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_power__le__zero__eq_0) ).
fof(f235_nnf,plain,
! [T_a,V_x] :
( ~ c_lessequals(c_Power_Opower__class_Opower(V_x,c_HOL_Ozero__class_Ozero(tc_nat),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
! [T_a,V_x] :
( ~ c_lessequals(c_Power_Opower__class_Opower(V_x,c_HOL_Ozero__class_Ozero(tc_nat),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c235,plain,
( ~ c_lessequals(c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
cnf(f325,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(f325_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)],[f325]) ).
fof(f325_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)],[f325_nnf]) ).
cnf(c325,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)],[f325_sk]) ).
cnf(f352,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f352_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f352_nnf]) ).
cnf(c352,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(f353,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f353_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f353]) ).
fof(f353_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f353_nnf]) ).
cnf(c353,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f353_sk]) ).
cnf(f443,axiom,
( ~ c_lessequals(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__le__zero_0) ).
fof(f443_nnf,plain,
! [T_a] :
( ~ c_lessequals(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)],[f443]) ).
fof(f443_sk,plain,
! [T_a] :
( ~ c_lessequals(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)],[f443_nnf]) ).
cnf(c443,plain,
( ~ c_lessequals(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)],[f443_sk]) ).
cnf(f445,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(f445_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)],[f445]) ).
fof(f445_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)],[f445_nnf]) ).
cnf(c445,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)],[f445_sk]) ).
cnf(f458,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(f458_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)],[f458]) ).
fof(f458_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)],[f458_nnf]) ).
cnf(c458,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)],[f458_sk]) ).
cnf(f508,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(f508_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)],[f508]) ).
fof(f508_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)],[f508_nnf]) ).
cnf(c508,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f508_sk]) ).
cnf(f509,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f509_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f509]) ).
fof(f509_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f509_nnf]) ).
cnf(c509,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f509_sk]) ).
cnf(f510,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f510_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f510]) ).
fof(f510_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f510_nnf]) ).
cnf(c510,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f510_sk]) ).
cnf(f511,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(f511_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)],[f511]) ).
fof(f511_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)],[f511_nnf]) ).
cnf(c511,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f511_sk]) ).
cnf(f512,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(f512_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)],[f512]) ).
fof(f512_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)],[f512_nnf]) ).
cnf(c512,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f512_sk]) ).
cnf(f520,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(f520_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)],[f520]) ).
fof(f520_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)],[f520_nnf]) ).
cnf(c520,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)],[f520_sk]) ).
cnf(f523,axiom,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).
fof(f523_nnf,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f523]) ).
fof(f523_sk,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f523_nnf]) ).
cnf(c523,plain,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X1,X0),X0)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(X1,X0),c_Int_Onumber__class_Onumber__of(X2,X0),X0)
| ~ class_Int_Onumber(X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f523_sk]) ).
cnf(f527,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f527_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f527]) ).
fof(f527_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f527_nnf]) ).
cnf(c527,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f527_sk]) ).
cnf(f542,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(f542_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)],[f542]) ).
fof(f542_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)],[f542_nnf]) ).
cnf(c542,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)],[f542_sk]) ).
cnf(f568,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(f568_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)],[f568]) ).
fof(f568_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)],[f568_nnf]) ).
cnf(c568,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)],[f568_sk]) ).
cnf(f570,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(f570_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)],[f570]) ).
fof(f570_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)],[f570_nnf]) ).
cnf(c570,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)],[f570_sk]) ).
cnf(f571,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(f571_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)],[f571]) ).
fof(f571_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)],[f571_nnf]) ).
cnf(c571,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)],[f571_sk]) ).
cnf(f572,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(f572_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)],[f572]) ).
fof(f572_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)],[f572_nnf]) ).
cnf(c572,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)],[f572_sk]) ).
cnf(f644,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(f644_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)],[f644]) ).
fof(f644_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)],[f644_nnf]) ).
cnf(c644,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)],[f644_sk]) ).
cnf(f652,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(f652_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)],[f652]) ).
fof(f652_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)],[f652_nnf]) ).
cnf(c652,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)],[f652_sk]) ).
cnf(f673,negated_conjecture,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f673_nnf,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f673]) ).
fof(f673_sk,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f673_nnf]) ).
cnf(c673,plain,
c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f673_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c28,c30,c32,c35,c224,c235,c325,c352,c353,c443,c445,c458,c508,c509,c510,c511,c512,c520,c523,c527,c542,c568,c570,c571,c572,c640,c644,c652,c673]) ).
cnf(g0_0,plain,
true != ifeq(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_n,tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),false,true),
inference(rw,[status(thm)],[g0_0,t3246]) ).
cnf(g0_2,plain,
true != ifeq(c_HOL_Oinverse__class_Odivide(c_HOL_Ominus__class_Ominus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),false,true),
inference(rw,[status(thm)],[g0_1,t4653]) ).
cnf(g0_3,plain,
true != ifeq(c_HOL_Oinverse__class_Odivide(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ominus__class_Ominus(c_Power_Opower__class_Opower(c_FFT__Mirabelle_Oroot(v_n),v_k,tc_Complex_Ocomplex),c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),false,true),
inference(rw,[status(thm)],[g0_2,t2237]) ).
cnf(g0_4,plain,
true != ifeq(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),false,true),
inference(rw,[status(thm)],[g0_3,t3446]) ).
cnf(g0_5,plain,
true != false,
inference(rw,[status(thm)],[g0_4,t256]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV617-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/15.40 % Computer : n010.cluster.edu
% 0.03/15.40 % Model : x86_64 x86_64
% 0.03/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/15.40 % Memory : 8046.5625MB
% 0.03/15.40 % OS : Linux 6.8.0-71-generic
% 0.03/15.40 % CPULimit : 300
% 0.03/15.40 % WCLimit : 300
% 0.03/15.40 % DateTime : Thu Sep 24 20:44:00 UTC 2026
% 0.03/15.40 % CPUTime :
% 0.03/15.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 79.34/25.69 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 79.34/25.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------