%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG380-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:52:25 PM UTC 2026
% Result : Unsatisfiable 120.86s 16.21s
% Output : Proof 120.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 65
% Syntax : Number of formulae : 297 ( 169 unt; 0 def)
% Number of atoms : 469 ( 149 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 538 ( 366 ~; 172 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 10 con; 0-4 aty)
% Number of variables : 423 ( 53 sgn 176 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1031,negated_conjecture,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1031_nnf,plain,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(nnf_transformation,[status(thm)],[f1031]) ).
fof(f1031_sk,plain,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(skolemisation,[status(esa)],[f1031_nnf]) ).
cnf(c1031,plain,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex) != c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a),
inference(cnf_transformation,[status(esa)],[f1031_sk]) ).
cnf(u6,axiom,
eq(c_HOL_Otimes__class_Otimes(c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),c_Complex_Orcis(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Orcis(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),v_a)) = false,
inference(equality_encoding,[status(esa)],[c1031]) ).
cnf(f620,axiom,
c_Complex_Orcis(V_r,V_a) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),c_Complex_Ocis(V_a),tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rcis__def_0) ).
fof(f620_nnf,plain,
! [V_r,V_a] : c_Complex_Orcis(V_r,V_a) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),c_Complex_Ocis(V_a),tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f620]) ).
fof(f620_sk,plain,
! [V_r,V_a] : c_Complex_Orcis(V_r,V_a) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),c_Complex_Ocis(V_a),tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f620_nnf]) ).
cnf(c620,plain,
c_Complex_Orcis(X0,X1) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),c_Complex_Ocis(X1),tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f620_sk]) ).
cnf(d0,axiom,
c_Complex_Orcis(X0,X1) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),c_Complex_Ocis(X1),tc_Complex_Ocomplex),
inference(equality_encoding,[status(esa)],[c620]) ).
cnf(t250,plain,
eq(c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(definition_unfolding,[status(thm)],[u6,d0]) ).
cnf(f619,axiom,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(V_r1,V_a),c_Complex_Orcis(V_r2,V_b),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(V_r1,V_r2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rcis__mult_0) ).
fof(f619_nnf,plain,
! [V_r1,V_a,V_r2,V_b] : c_HOL_Otimes__class_Otimes(c_Complex_Orcis(V_r1,V_a),c_Complex_Orcis(V_r2,V_b),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(V_r1,V_r2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal)),
inference(nnf_transformation,[status(thm)],[f619]) ).
fof(f619_sk,plain,
! [V_r1,V_a,V_r2,V_b] : c_HOL_Otimes__class_Otimes(c_Complex_Orcis(V_r1,V_a),c_Complex_Orcis(V_r2,V_b),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(V_r1,V_r2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_a,V_b,tc_RealDef_Oreal)),
inference(skolemisation,[status(esa)],[f619_nnf]) ).
cnf(c619,plain,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(X0,X1),c_Complex_Orcis(X2,X3),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)),
inference(cnf_transformation,[status(esa)],[f619_sk]) ).
cnf(u1,axiom,
c_HOL_Otimes__class_Otimes(c_Complex_Orcis(X0,X1),c_Complex_Orcis(X2,X3),tc_Complex_Ocomplex) = c_Complex_Orcis(c_HOL_Otimes__class_Otimes(X0,X2,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(X1,X3,tc_RealDef_Oreal)),
inference(equality_encoding,[status(esa)],[c619]) ).
cnf(t207,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(X2),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X3,tc_Complex_Ocomplex),c_Complex_Ocis(X4),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oplus__class_Oplus(X2,X4,tc_RealDef_Oreal)),tc_Complex_Ocomplex),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t2140,plain,
c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(X2),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X3,tc_Complex_Ocomplex),c_Complex_Ocis(X4),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Otimes__class_Otimes(X1,X3,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oplus__class_Oplus(X2,X4,tc_RealDef_Oreal)),tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t207]) ).
cnf(t4680,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),c_NthRoot_Osqrt(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal)),tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t250,t2140]) ).
cnf(f614,axiom,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__mult_0) ).
fof(f614_nnf,plain,
! [V_x,V_y] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f614]) ).
fof(f614_sk,plain,
! [V_x,V_y] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f614_nnf]) ).
cnf(c614,plain,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X1,tc_RealDef_Oreal)) = c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X0),c_NthRoot_Osqrt(X1),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f614_sk]) ).
cnf(t84,plain,
c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X2),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal)),
inference(equality_encoding,[status(esa)],[c614]) ).
cnf(t2161,plain,
c_HOL_Otimes__class_Otimes(c_NthRoot_Osqrt(X1),c_NthRoot_Osqrt(X2),tc_RealDef_Oreal) = c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X1,X2,tc_RealDef_Oreal)),
inference(orient,[status(thm)],[t84]) ).
cnf(t4681,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t4680,t2161]) ).
cnf(f945,axiom,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__abs2_0) ).
fof(f945_nnf,plain,
! [V_x] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f945]) ).
fof(f945_sk,plain,
! [V_x] : c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(V_x,V_x,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f945_nnf]) ).
cnf(c945,plain,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X0,X0,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f945_sk]) ).
cnf(t56,plain,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(equality_encoding,[status(esa)],[c945]) ).
cnf(t2523,plain,
c_NthRoot_Osqrt(c_HOL_Otimes__class_Otimes(X1,X1,tc_RealDef_Oreal)) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(orient,[status(thm)],[t56]) ).
cnf(t4682,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(v_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t4681,t2523]) ).
cnf(f994,axiom,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sum__of__halves_0) ).
fof(f994_nnf,plain,
! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
inference(nnf_transformation,[status(thm)],[f994]) ).
fof(f994_sk,plain,
! [V_x] : c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = V_x,
inference(skolemisation,[status(esa)],[f994_nnf]) ).
cnf(c994,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X0,
inference(cnf_transformation,[status(esa)],[f994_sk]) ).
cnf(t157,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(equality_encoding,[status(esa)],[c994]) ).
cnf(t269,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(orient,[status(thm)],[t157]) ).
cnf(t4683,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t4682,t269]) ).
cnf(t2776,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(orient,[status(thm)],[t4683]) ).
cnf(t63,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t264,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t63]) ).
cnf(f866,axiom,
( c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__abs__def_1) ).
fof(f866_nnf,plain,
! [V_r] :
( c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r ),
inference(nnf_transformation,[status(thm)],[f866]) ).
fof(f866_sk,plain,
! [V_r] :
( c_HOL_Oord__class_Oless(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal) = V_r ),
inference(skolemisation,[status(esa)],[f866_nnf]) ).
cnf(c866,plain,
( c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal) = X0 ),
inference(cnf_transformation,[status(esa)],[f866_sk]) ).
cnf(t95,plain,
or(eq(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),X1),c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)) = true,
inference(equality_encoding,[status(esa)],[c866]) ).
cnf(t1474,plain,
or(eq(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),X1),c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)) = true,
inference(orient,[status(thm)],[t95]) ).
cnf(t49,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1610,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t49]) ).
cnf(f47,axiom,
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_norm__not__less__zero_0) ).
fof(f47_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
( ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X1,X0),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(t100,plain,
or(not(class_RealVector_Oreal__normed__vector(X1)),not(c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X2,X1),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(t1441,plain,
or(not(class_RealVector_Oreal__normed__vector(X1)),not(c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(X2,X1),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))) = true,
inference(orient,[status(thm)],[t100]) ).
cnf(f946,axiom,
c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(V_r,V_a),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_complex__mod__rcis_0) ).
fof(f946_nnf,plain,
! [V_r,V_a] : c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(V_r,V_a),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f946]) ).
fof(f946_sk,plain,
! [V_r,V_a] : c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(V_r,V_a),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(V_r,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f946_nnf]) ).
cnf(c946,plain,
c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(X0,X1),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f946_sk]) ).
cnf(u3,axiom,
c_RealVector_Onorm__class_Onorm(c_Complex_Orcis(X0,X1),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),
inference(equality_encoding,[status(esa)],[c946]) ).
cnf(t92,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(X2),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(definition_unfolding,[status(thm)],[u3,d0]) ).
cnf(t2736,plain,
c_RealVector_Onorm__class_Onorm(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(X2),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(orient,[status(thm)],[t92]) ).
cnf(f125,axiom,
c_Complex_Orcis(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rcis__zero__arg_0) ).
fof(f125_nnf,plain,
! [V_r] : c_Complex_Orcis(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [V_r] : c_Complex_Orcis(V_r,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(V_r,tc_Complex_Ocomplex),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
c_Complex_Orcis(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(u0,axiom,
c_Complex_Orcis(X0,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_RealVector_Oof__real(X0,tc_Complex_Ocomplex),
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(t85,plain,
c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),tc_Complex_Ocomplex) = c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t2380,plain,
c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),c_Complex_Ocis(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)),tc_Complex_Ocomplex) = c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),
inference(orient,[status(thm)],[t85]) ).
cnf(t2737,plain,
c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(cp,[status(thm)],[t2736,t2380]) ).
cnf(t2909,plain,
c_RealVector_Onorm__class_Onorm(c_RealVector_Oof__real(X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(orient,[status(thm)],[t2737]) ).
cnf(t2911,plain,
true = or(not(class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex)),not(c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
inference(cp,[status(thm)],[t1441,t2909]) ).
cnf(f1191,axiom,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_Complex__Ocomplex__RealVector_Oreal__normed__vector) ).
fof(f1191_nnf,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(nnf_transformation,[status(thm)],[f1191]) ).
cnf(c1191,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex),
inference(cnf_transformation,[status(esa)],[f1191_nnf]) ).
cnf(t4,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) = true,
inference(equality_encoding,[status(esa)],[c1191]) ).
cnf(t1568,plain,
class_RealVector_Oreal__normed__vector(tc_Complex_Ocomplex) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t4718,plain,
true = or(not(true),not(c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
inference(step,[status(thm)],[t2911,t1568]) ).
cnf(t11,plain,
not(true) = false,
introduced(definition) ).
cnf(t2749,plain,
not(true) = false,
inference(orient,[status(thm)],[t11]) ).
cnf(t4719,plain,
true = or(false,not(c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal))),
inference(step,[status(thm)],[t4718,t2749]) ).
cnf(t15,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t271,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t15]) ).
cnf(t4720,plain,
true = not(c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)),
inference(step,[status(thm)],[t4719,t271]) ).
cnf(t3454,plain,
not(c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal)) = true,
inference(orient,[status(thm)],[t4720]) ).
cnf(t3458,plain,
false = ifeq(true,true,c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),false),
inference(cp,[status(thm)],[t1610,t3454]) ).
cnf(t40,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t40]) ).
cnf(t4722,plain,
false = c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(step,[status(thm)],[t3458,t256]) ).
cnf(t3491,plain,
c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) = false,
inference(orient,[status(thm)],[t4722]) ).
cnf(t3495,plain,
true = or(eq(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal)),false),
inference(cp,[status(thm)],[t1474,t3491]) ).
cnf(t13,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t270,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t4772,plain,
true = eq(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal)),
inference(step,[status(thm)],[t3495,t270]) ).
cnf(t4563,plain,
eq(c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal)) = true,
inference(orient,[status(thm)],[t4772]) ).
cnf(t4568,plain,
c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal) = ifeq(true,true,c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal)),
inference(cp,[status(thm)],[t264,t4563]) ).
cnf(t4773,plain,
c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(step,[status(thm)],[t4568,t256]) ).
cnf(t4572,plain,
c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_HOL_Oabs__class_Oabs(X1,tc_RealDef_Oreal),
inference(orient,[status(thm)],[t4773]) ).
cnf(t4774,plain,
eq(c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(c_RealVector_Oof__real(c_HOL_Oabs__class_Oabs(v_r,tc_RealDef_Oreal),tc_Complex_Ocomplex),c_Complex_Ocis(v_a),tc_Complex_Ocomplex)) = false,
inference(step,[status(thm)],[t2776,t4572]) ).
cnf(t12,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1564,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t4775,plain,
true = false,
inference(step,[status(thm)],[t4774,t1564]) ).
cnf(t4586,plain,
true = false,
inference(rw,[status(thm)],[t4775]) ).
cnf(t4587,plain,
false = true,
inference(orient,[status(thm)],[t4586]) ).
cnf(f9,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sum__power2__gt__zero__iff_0) ).
fof(f9_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f12,axiom,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__not__less__zero_0) ).
fof(f12_nnf,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f14,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/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f14_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)],[f14]) ).
fof(f14_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)],[f14_nnf]) ).
cnf(c14,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f16,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f16_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)],[f16]) ).
fof(f16_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)],[f16_nnf]) ).
cnf(c16,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f18,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f18_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)],[f18]) ).
fof(f18_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)],[f18_nnf]) ).
cnf(c18,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(f21,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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f21_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)],[f21]) ).
fof(f21_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)],[f21_nnf]) ).
cnf(c21,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f110,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/sandbox2/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f110_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)],[f110]) ).
fof(f110_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)],[f110_nnf]) ).
cnf(c110,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)],[f110_sk]) ).
cnf(f111,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/sandbox2/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f111_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)],[f111]) ).
fof(f111_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)],[f111_nnf]) ).
cnf(c111,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)],[f111_sk]) ).
cnf(f120,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__norm__iff_0) ).
fof(f120_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(T_a),T_a),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c120,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(c_HOL_Ozero__class_Ozero(X0),X0),tc_RealDef_Oreal)
| ~ class_RealVector_Oreal__normed__vector(X0) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(f129,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__sqrt__not__eq__zero_0) ).
fof(f129_nnf,plain,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f129_nnf]) ).
cnf(c129,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_NthRoot_Osqrt(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(f228,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(V_y,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__sum__power2__lt__zero_0) ).
fof(f228_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(V_y,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(V_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_Power_Opower__class_Opower(V_y,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c228,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_Power_Opower__class_Opower(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),c_Power_Opower__class_Opower(X2,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(f442,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/sandbox2/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f442_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)],[f442]) ).
fof(f442_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)],[f442_nnf]) ).
cnf(c442,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)],[f442_sk]) ).
cnf(f492,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/sandbox2/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f492_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)],[f492]) ).
fof(f492_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)],[f492_nnf]) ).
cnf(c492,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)],[f492_sk]) ).
cnf(f508,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__less__power2_0) ).
fof(f508_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f508]) ).
fof(f508_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(T_a),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f508_nnf]) ).
cnf(c508,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_Power_Opower__class_Opower(c_HOL_Ozero__class_Ozero(X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f508_sk]) ).
cnf(f517,axiom,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__zero__not__eq__one_0) ).
fof(f517_nnf,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f517]) ).
fof(f517_sk,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f517_nnf]) ).
cnf(c517,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f517_sk]) ).
cnf(f518,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/sandbox2/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f518_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)],[f518]) ).
fof(f518_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)],[f518_nnf]) ).
cnf(c518,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)],[f518_sk]) ).
cnf(f526,axiom,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__neq__zero_0) ).
fof(f526_nnf,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f526]) ).
fof(f526_sk,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f526_nnf]) ).
cnf(c526,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f526_sk]) ).
cnf(f662,axiom,
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(V_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power2__less__0_0) ).
fof(f662_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(V_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),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)],[f662]) ).
fof(f662_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(V_a,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),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)],[f662_nnf]) ).
cnf(c662,plain,
( ~ c_HOL_Oord__class_Oless(c_Power_Opower__class_Opower(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__idom(X0) ),
inference(cnf_transformation,[status(esa)],[f662_sk]) ).
cnf(f665,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__real__square__gt__zero_1) ).
fof(f665_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f665]) ).
fof(f665_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f665_nnf]) ).
cnf(c665,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f665_sk]) ).
cnf(f692,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/sandbox2/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f692_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)],[f692]) ).
fof(f692_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)],[f692_nnf]) ).
cnf(c692,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)],[f692_sk]) ).
cnf(f705,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_abs__add__one__not__less__self_0) ).
fof(f705_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f705]) ).
fof(f705_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f705_nnf]) ).
cnf(c705,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(X0,tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f705_sk]) ).
cnf(f708,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f708_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)],[f708]) ).
fof(f708_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)],[f708_nnf]) ).
cnf(c708,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f708_sk]) ).
cnf(f709,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f709_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)],[f709]) ).
fof(f709_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)],[f709_nnf]) ).
cnf(c709,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f709_sk]) ).
cnf(f710,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_1) ).
fof(f710_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f710]) ).
fof(f710_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f710_nnf]) ).
cnf(c710,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f710_sk]) ).
cnf(f711,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f711_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)],[f711]) ).
fof(f711_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)],[f711_nnf]) ).
cnf(c711,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f711_sk]) ).
cnf(f716,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/sandbox2/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f716_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)],[f716]) ).
fof(f716_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)],[f716_nnf]) ).
cnf(c716,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)],[f716_sk]) ).
cnf(f790,axiom,
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(V_w),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_iszero__number__of__Bit1_0) ).
fof(f790_nnf,plain,
! [T_a,V_w] :
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(V_w),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
inference(nnf_transformation,[status(thm)],[f790]) ).
fof(f790_sk,plain,
! [T_a,V_w] :
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(V_w),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a)
| ~ class_Int_Oring__char__0(T_a) ),
inference(skolemisation,[status(esa)],[f790_nnf]) ).
cnf(c790,plain,
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(X1),X0),X0)
| ~ class_Int_Onumber__ring(X0)
| ~ class_Int_Oring__char__0(X0) ),
inference(cnf_transformation,[status(esa)],[f790_sk]) ).
cnf(f821,axiom,
~ c_HOL_Oeq__class_Oeq(c_Int_OPls,c_Int_OBit1(V_k2),tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__int__code_I4_J_0) ).
fof(f821_nnf,plain,
! [V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OPls,c_Int_OBit1(V_k2),tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f821]) ).
fof(f821_sk,plain,
! [V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OPls,c_Int_OBit1(V_k2),tc_Int_Oint),
inference(skolemisation,[status(esa)],[f821_nnf]) ).
cnf(c821,plain,
~ c_HOL_Oeq__class_Oeq(c_Int_OPls,c_Int_OBit1(X0),tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f821_sk]) ).
cnf(f822,axiom,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OPls,tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__int__code_I10_J_0) ).
fof(f822_nnf,plain,
! [V_k1] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OPls,tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f822]) ).
fof(f822_sk,plain,
! [V_k1] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OPls,tc_Int_Oint),
inference(skolemisation,[status(esa)],[f822_nnf]) ).
cnf(c822,plain,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(X0),c_Int_OPls,tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f822_sk]) ).
cnf(f827,axiom,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OBit0(V_k2),tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__int__code_I15_J_0) ).
fof(f827_nnf,plain,
! [V_k1,V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OBit0(V_k2),tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f827]) ).
fof(f827_sk,plain,
! [V_k1,V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(V_k1),c_Int_OBit0(V_k2),tc_Int_Oint),
inference(skolemisation,[status(esa)],[f827_nnf]) ).
cnf(c827,plain,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit1(X0),c_Int_OBit0(X1),tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f827_sk]) ).
cnf(f828,axiom,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit0(V_k1),c_Int_OBit1(V_k2),tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_eq__int__code_I14_J_0) ).
fof(f828_nnf,plain,
! [V_k1,V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit0(V_k1),c_Int_OBit1(V_k2),tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f828]) ).
fof(f828_sk,plain,
! [V_k1,V_k2] : ~ c_HOL_Oeq__class_Oeq(c_Int_OBit0(V_k1),c_Int_OBit1(V_k2),tc_Int_Oint),
inference(skolemisation,[status(esa)],[f828_nnf]) ).
cnf(c828,plain,
~ c_HOL_Oeq__class_Oeq(c_Int_OBit0(X0),c_Int_OBit1(X1),tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f828_sk]) ).
cnf(f844,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/sandbox2/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f844_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)],[f844]) ).
fof(f844_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)],[f844_nnf]) ).
cnf(c844,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)],[f844_sk]) ).
cnf(f856,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/sandbox2/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).
fof(f856_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)],[f856]) ).
fof(f856_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)],[f856_nnf]) ).
cnf(c856,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)],[f856_sk]) ).
cnf(f879,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/sandbox2/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f879_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)],[f879]) ).
fof(f879_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)],[f879_nnf]) ).
cnf(c879,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)],[f879_sk]) ).
cnf(f914,axiom,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(T_a),T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__iszero__1_0) ).
fof(f914_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)],[f914]) ).
fof(f914_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)],[f914_nnf]) ).
cnf(c914,plain,
( ~ c_Int_Oiszero(c_HOL_Oone__class_Oone(X0),X0)
| ~ class_Ring__and__Field_Osemiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f914_sk]) ).
cnf(f925,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f925_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)],[f925]) ).
fof(f925_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)],[f925_nnf]) ).
cnf(c925,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)],[f925_sk]) ).
cnf(f926,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f926_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)],[f926]) ).
fof(f926_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)],[f926_nnf]) ).
cnf(c926,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)],[f926_sk]) ).
cnf(f929,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f929_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)],[f929]) ).
fof(f929_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)],[f929_nnf]) ).
cnf(c929,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)],[f929_sk]) ).
cnf(f930,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/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f930_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)],[f930]) ).
fof(f930_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)],[f930_nnf]) ).
cnf(c930,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)],[f930_sk]) ).
cnf(f938,axiom,
c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__two__neq__zero_0) ).
fof(f938_nnf,plain,
c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f938]) ).
fof(f938_sk,plain,
c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f938_nnf]) ).
cnf(c938,plain,
c_Transcendental_Ocos(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f938_sk]) ).
cnf(f951,axiom,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__half__neq__zero_0) ).
fof(f951_nnf,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f951]) ).
fof(f951_sk,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f951_nnf]) ).
cnf(c951,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f951_sk]) ).
cnf(f980,axiom,
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__iszero__Numeral1_0) ).
fof(f980_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f980]) ).
fof(f980_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),T_a),T_a)
| ~ class_Int_Onumber__ring(T_a) ),
inference(skolemisation,[status(esa)],[f980_nnf]) ).
cnf(c980,plain,
( ~ c_Int_Oiszero(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),X0),X0)
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[status(esa)],[f980_sk]) ).
cnf(f993,axiom,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pi__half__neq__two_0) ).
fof(f993_nnf,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f993]) ).
fof(f993_sk,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f993_nnf]) ).
cnf(c993,plain,
c_HOL_Oinverse__class_Odivide(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal) != c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f993_sk]) ).
cnf(f997,axiom,
c_Int_OPls != c_Int_OBit1(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I39_J_0) ).
fof(f997_nnf,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f997]) ).
fof(f997_sk,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f997_nnf]) ).
cnf(c997,plain,
c_Int_OPls != c_Int_OBit1(X0),
inference(cnf_transformation,[status(esa)],[f997_sk]) ).
cnf(f999,axiom,
c_Int_OBit1(V_k) != c_Int_OPls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I46_J_0) ).
fof(f999_nnf,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(nnf_transformation,[status(thm)],[f999]) ).
fof(f999_sk,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(skolemisation,[status(esa)],[f999_nnf]) ).
cnf(c999,plain,
c_Int_OBit1(X0) != c_Int_OPls,
inference(cnf_transformation,[status(esa)],[f999_sk]) ).
cnf(f1005,axiom,
c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I50_J_0) ).
fof(f1005_nnf,plain,
! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(nnf_transformation,[status(thm)],[f1005]) ).
fof(f1005_sk,plain,
! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(skolemisation,[status(esa)],[f1005_nnf]) ).
cnf(c1005,plain,
c_Int_OBit1(X0) != c_Int_OBit0(X1),
inference(cnf_transformation,[status(esa)],[f1005_sk]) ).
cnf(f1029,axiom,
c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I49_J_0) ).
fof(f1029_nnf,plain,
! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f1029]) ).
fof(f1029_sk,plain,
! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f1029_nnf]) ).
cnf(c1029,plain,
c_Int_OBit0(X0) != c_Int_OBit1(X1),
inference(cnf_transformation,[status(esa)],[f1029_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c12,c14,c16,c18,c21,c47,c110,c111,c120,c129,c228,c442,c492,c508,c517,c518,c526,c662,c665,c692,c705,c708,c709,c710,c711,c716,c790,c821,c822,c827,c828,c844,c856,c879,c914,c925,c926,c929,c930,c938,c951,c980,c993,c997,c999,c1005,c1029,c1031]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4587]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG380-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 05:33:05 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 120.86/16.21 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.86/16.21 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------