%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV602-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 : n008.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:47 PM UTC 2026
% Result : Unsatisfiable 34.04s 4.98s
% Output : Proof 34.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 46
% Syntax : Number of formulae : 192 ( 96 unt; 0 def)
% Number of atoms : 344 ( 103 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 482 ( 330 ~; 152 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 7 con; 0-3 aty)
% Number of variables : 242 ( 20 sgn 120 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f678,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(f678_nnf,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f678]) ).
fof(f678_sk,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f678_nnf]) ).
cnf(c678,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f678_sk]) ).
cnf(t26,plain,
eq(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = false,
inference(equality_encoding,[status(esa)],[c678]) ).
cnf(f902,axiom,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__pi_0) ).
fof(f902_nnf,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f902]) ).
cnf(c902,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f902_nnf]) ).
cnf(t9,plain,
c_Transcendental_Osin(c_Transcendental_Opi) = c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(equality_encoding,[status(esa)],[c902]) ).
cnf(t264,plain,
c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Transcendental_Osin(c_Transcendental_Opi),
inference(orient,[status(thm)],[t9]) ).
cnf(t1530,plain,
eq(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = false,
inference(step,[status(thm)],[t26,t264]) ).
cnf(t286,plain,
eq(c_Transcendental_Osin(c_Transcendental_Opi),c_HOL_Oone__class_Oone(tc_RealDef_Oreal)) = false,
inference(orient,[status(thm)],[t1530]) ).
cnf(t1387,plain,
eq(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Osin(c_Transcendental_Opi)) = false,
inference(rw,[status(thm)],[t286]) ).
cnf(t10,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t265,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t1706,plain,
true = false,
inference(step,[status(thm)],[t1387,t265]) ).
cnf(t1467,plain,
false = true,
inference(orient,[status(thm)],[t1706]) ).
cnf(f12,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(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,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)],[f12_sk]) ).
cnf(f16,axiom,
~ c_Parity_Oeven__odd__class_Oeven(c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),V_x,tc_nat)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_odd__Suc__mult__two__ex_1) ).
fof(f16_nnf,plain,
! [V_x] : ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),V_x,tc_nat)),tc_nat),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [V_x] : ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),V_x,tc_nat)),tc_nat),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
~ c_Parity_Oeven__odd__class_Oeven(c_Suc(c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),X0,tc_nat)),tc_nat),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f17,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(f17_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)],[f17]) ).
fof(f17_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)],[f17_nnf]) ).
cnf(c17,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)],[f17_sk]) ).
cnf(f20,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(f20_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)],[f20]) ).
fof(f20_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)],[f20_nnf]) ).
cnf(c20,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f21,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(f21_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f22,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(f22_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)],[f22]) ).
fof(f22_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)],[f22_nnf]) ).
cnf(c22,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(f23,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(f23_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)],[f23]) ).
fof(f23_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)],[f23_nnf]) ).
cnf(c23,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f32,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(f32_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)],[f32]) ).
fof(f32_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)],[f32_nnf]) ).
cnf(c32,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)],[f32_sk]) ).
cnf(f145,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(f145_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)],[f145]) ).
fof(f145_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)],[f145_nnf]) ).
cnf(c145,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)],[f145_sk]) ).
cnf(f146,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(f146_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)],[f146]) ).
fof(f146_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)],[f146_nnf]) ).
cnf(c146,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)],[f146_sk]) ).
cnf(f149,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(f149_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)],[f149]) ).
fof(f149_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)],[f149_nnf]) ).
cnf(c149,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)],[f149_sk]) ).
cnf(f150,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(f150_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)],[f150]) ).
fof(f150_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)],[f150_nnf]) ).
cnf(c150,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)],[f150_sk]) ).
cnf(f222,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f222_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c222,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f223,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f223_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f258,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(f258_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)],[f258]) ).
fof(f258_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)],[f258_nnf]) ).
cnf(c258,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)],[f258_sk]) ).
cnf(f301,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(f301_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)],[f301]) ).
fof(f301_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)],[f301_nnf]) ).
cnf(c301,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
cnf(f303,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(f303_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)],[f303]) ).
fof(f303_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)],[f303_nnf]) ).
cnf(c303,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
cnf(f305,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(f305_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)],[f305]) ).
fof(f305_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)],[f305_nnf]) ).
cnf(c305,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f305_sk]) ).
cnf(f308,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(f308_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)],[f308]) ).
fof(f308_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)],[f308_nnf]) ).
cnf(c308,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(f334,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(f334_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)],[f334]) ).
fof(f334_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)],[f334_nnf]) ).
cnf(c334,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)],[f334_sk]) ).
cnf(f426,axiom,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__lemma__1__1(V_x),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__zero__lemma_0) ).
fof(f426_nnf,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__lemma__1__1(V_x),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f426]) ).
fof(f426_sk,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__lemma__1__1(V_x),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f426_nnf]) ).
cnf(c426,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__lemma__1__1(X0),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| c_Transcendental_Ocos(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
cnf(f430,axiom,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(V_x,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_even__Suc_0) ).
fof(f430_nnf,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(V_x,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(V_x,tc_nat) ),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c430,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Suc(X0),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
cnf(f434,axiom,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__1(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__2(V_x),tc_nat)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_cos__zero__iff_0) ).
fof(f434_nnf,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__1(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__2(V_x),tc_nat)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f434]) ).
fof(f434_sk,plain,
! [V_x] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__1(V_x),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__2(V_x),tc_nat)
| c_Transcendental_Ocos(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f434_nnf]) ).
cnf(c434,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__1(X0),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Transcendental_Osko__Transcendental__Xcos__zero__iff__1__2(X0),tc_nat)
| c_Transcendental_Ocos(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f434_sk]) ).
cnf(f460,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(f460_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)],[f460]) ).
fof(f460_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)],[f460_nnf]) ).
cnf(c460,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)],[f460_sk]) ).
cnf(f463,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(f463_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)],[f463]) ).
fof(f463_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)],[f463_nnf]) ).
cnf(c463,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)],[f463_sk]) ).
cnf(f488,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(f488_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)],[f488]) ).
fof(f488_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)],[f488_nnf]) ).
cnf(c488,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)],[f488_sk]) ).
cnf(f491,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(f491_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)],[f491]) ).
fof(f491_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)],[f491_nnf]) ).
cnf(c491,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)],[f491_sk]) ).
cnf(f532,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(f532_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)],[f532]) ).
fof(f532_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)],[f532_nnf]) ).
cnf(c532,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)],[f532_sk]) ).
cnf(f547,axiom,
~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__real__of__nat__less__zero_0) ).
fof(f547_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f547]) ).
fof(f547_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(V_n,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f547_nnf]) ).
cnf(c547,plain,
~ c_HOL_Oord__class_Oless(c_RealDef_Oreal(X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f547_sk]) ).
cnf(f548,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(f548_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)],[f548]) ).
fof(f548_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)],[f548_nnf]) ).
cnf(c548,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)],[f548_sk]) ).
cnf(f671,axiom,
c_Int_OPls != c_Int_OMin,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I37_J_0) ).
fof(f671_nnf,plain,
c_Int_OPls != c_Int_OMin,
inference(nnf_transformation,[status(thm)],[f671]) ).
fof(f671_sk,plain,
c_Int_OPls != c_Int_OMin,
inference(skolemisation,[status(esa)],[f671_nnf]) ).
cnf(c671,plain,
c_Int_OPls != c_Int_OMin,
inference(cnf_transformation,[status(esa)],[f671_sk]) ).
cnf(f672,axiom,
c_Int_OMin != c_Int_OPls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I40_J_0) ).
fof(f672_nnf,plain,
c_Int_OMin != c_Int_OPls,
inference(nnf_transformation,[status(thm)],[f672]) ).
fof(f672_sk,plain,
c_Int_OMin != c_Int_OPls,
inference(skolemisation,[status(esa)],[f672_nnf]) ).
cnf(c672,plain,
c_Int_OMin != c_Int_OPls,
inference(cnf_transformation,[status(esa)],[f672_sk]) ).
cnf(f674,axiom,
c_Int_OMin != c_Int_OBit0(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I42_J_0) ).
fof(f674_nnf,plain,
! [V_l] : c_Int_OMin != c_Int_OBit0(V_l),
inference(nnf_transformation,[status(thm)],[f674]) ).
fof(f674_sk,plain,
! [V_l] : c_Int_OMin != c_Int_OBit0(V_l),
inference(skolemisation,[status(esa)],[f674_nnf]) ).
cnf(c674,plain,
c_Int_OMin != c_Int_OBit0(X0),
inference(cnf_transformation,[status(esa)],[f674_sk]) ).
cnf(f675,axiom,
c_Int_OBit0(V_k) != c_Int_OMin,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I45_J_0) ).
fof(f675_nnf,plain,
! [V_k] : c_Int_OBit0(V_k) != c_Int_OMin,
inference(nnf_transformation,[status(thm)],[f675]) ).
fof(f675_sk,plain,
! [V_k] : c_Int_OBit0(V_k) != c_Int_OMin,
inference(skolemisation,[status(esa)],[f675_nnf]) ).
cnf(c675,plain,
c_Int_OBit0(X0) != c_Int_OMin,
inference(cnf_transformation,[status(esa)],[f675_sk]) ).
cnf(f773,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sin__cos__between__zero__two__pi_0) ).
fof(f773_nnf,plain,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f773]) ).
fof(f773_sk,plain,
! [V_x] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),V_x,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Transcendental_Osin(V_x) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Transcendental_Ocos(V_x) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f773_nnf]) ).
cnf(c773,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),X0,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(X0,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| c_Transcendental_Osin(X0) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Transcendental_Ocos(X0) != c_HOL_Oone__class_Oone(tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f773_sk]) ).
cnf(f842,axiom,
c_Int_OPls != c_Int_OBit1(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I39_J_0) ).
fof(f842_nnf,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f842]) ).
fof(f842_sk,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f842_nnf]) ).
cnf(c842,plain,
c_Int_OPls != c_Int_OBit1(X0),
inference(cnf_transformation,[status(esa)],[f842_sk]) ).
cnf(f844,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(f844_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)],[f844]) ).
fof(f844_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)],[f844_nnf]) ).
cnf(c844,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)],[f844_sk]) ).
cnf(f845,axiom,
c_Int_OBit1(V_k) != c_Int_OPls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rel__simps_I46_J_0) ).
fof(f845_nnf,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(nnf_transformation,[status(thm)],[f845]) ).
fof(f845_sk,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(skolemisation,[status(esa)],[f845_nnf]) ).
cnf(c845,plain,
c_Int_OBit1(X0) != c_Int_OPls,
inference(cnf_transformation,[status(esa)],[f845_sk]) ).
cnf(f850,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(f850_nnf,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f850]) ).
fof(f850_sk,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f850_nnf]) ).
cnf(c850,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f850_sk]) ).
cnf(f853,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(f853_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)],[f853]) ).
fof(f853_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)],[f853_nnf]) ).
cnf(c853,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)],[f853_sk]) ).
cnf(f857,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(f857_nnf,plain,
! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(nnf_transformation,[status(thm)],[f857]) ).
fof(f857_sk,plain,
! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(skolemisation,[status(esa)],[f857_nnf]) ).
cnf(c857,plain,
c_Int_OBit1(X0) != c_Int_OBit0(X1),
inference(cnf_transformation,[status(esa)],[f857_sk]) ).
cnf(f897,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(f897_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)],[f897]) ).
fof(f897_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)],[f897_nnf]) ).
cnf(c897,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)],[f897_sk]) ).
cnf(f910,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(f910_nnf,plain,
! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f910]) ).
fof(f910_sk,plain,
! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f910_nnf]) ).
cnf(c910,plain,
c_Int_OBit0(X0) != c_Int_OBit1(X1),
inference(cnf_transformation,[status(esa)],[f910_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c12,c16,c17,c20,c21,c22,c23,c32,c145,c146,c149,c150,c222,c223,c258,c301,c303,c305,c308,c334,c426,c430,c434,c460,c463,c488,c491,c532,c547,c548,c671,c672,c674,c675,c678,c773,c842,c844,c845,c850,c853,c857,c897,c910]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1467]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV602-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.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 20:41:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.04/4.98 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.04/4.98 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------