%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV592-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n013.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:45 PM UTC 2026
% Result : Unsatisfiable 20.04s 3.32s
% Output : Proof 20.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 32
% Syntax : Number of formulae : 152 ( 68 unt; 0 def)
% Number of atoms : 268 ( 61 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 334 ( 218 ~; 116 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-4 aty)
% Number of variables : 237 ( 6 sgn 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f861,negated_conjecture,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) != c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f861_nnf,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) != c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f861]) ).
fof(f861_sk,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) != c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f861_nnf]) ).
cnf(c861,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)) != c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f861_sk]) ).
cnf(t88,plain,
eq(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)),c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal)) = false,
inference(equality_encoding,[status(esa)],[c861]) ).
cnf(t3280,plain,
eq(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)),c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal)) = false,
inference(orient,[status(thm)],[t88]) ).
cnf(f859,axiom,
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__minus_0) ).
fof(f859_nnf,plain,
! [T_a,V_a] :
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(nnf_transformation,[status(thm)],[f859]) ).
fof(f859_sk,plain,
! [T_a,V_a] :
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = V_a
| ~ class_OrderedGroup_Ogroup__add(T_a) ),
inference(skolemisation,[status(esa)],[f859_nnf]) ).
cnf(c859,plain,
( c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0) = X1
| ~ class_OrderedGroup_Ogroup__add(X0) ),
inference(cnf_transformation,[status(esa)],[f859_sk]) ).
cnf(hi833,axiom,
ifeq(class_OrderedGroup_Ogroup__add(X0),true,c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,X0),X0),X1) = X1,
inference(equality_encoding,[status(esa)],[c859]) ).
cnf(f911,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add) ).
fof(f911_nnf,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f911]) ).
cnf(c911,plain,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f911_nnf]) ).
cnf(hi884,axiom,
class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c911]) ).
cnf(t21,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(hyper_resolution,[status(thm)],[hi833,hi884]) ).
cnf(t287,plain,
c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(f847,axiom,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sin__periodic__pi2_0) ).
fof(f847_nnf,plain,
! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f847]) ).
fof(f847_sk,plain,
! [V_x] : c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,V_x,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(V_x),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f847_nnf]) ).
cnf(c847,plain,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X0,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X0),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f847_sk]) ).
cnf(t58,plain,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
inference(equality_encoding,[status(esa)],[c847]) ).
cnf(t3266,plain,
c_Transcendental_Osin(c_HOL_Oplus__class_Oplus(c_Transcendental_Opi,X1,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
inference(orient,[status(thm)],[t58]) ).
cnf(f822,axiom,
V_y = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_y,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_eq__diff__eq_H_0) ).
fof(f822_nnf,plain,
! [V_y,V_z] : V_y = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_y,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f822]) ).
fof(f822_sk,plain,
! [V_y,V_z] : V_y = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_y,V_z,tc_RealDef_Oreal),V_z,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f822_nnf]) ).
cnf(c822,plain,
X0 = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_RealDef_Oreal),X1,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f822_sk]) ).
cnf(t42,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = X1,
inference(equality_encoding,[status(esa)],[c822]) ).
cnf(t282,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = X1,
inference(orient,[status(thm)],[t42]) ).
cnf(t2686,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X1,X2,tc_RealDef_Oreal),X2,tc_RealDef_Oreal) = X1,
inference(rw,[status(thm)],[t282]) ).
cnf(f481,axiom,
( c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_class__semiring_Oadd__c_0) ).
fof(f481_nnf,plain,
! [T_a,V_x,V_y] :
( c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f481]) ).
fof(f481_sk,plain,
! [T_a,V_x,V_y] :
( c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f481_nnf]) ).
cnf(c481,plain,
( c_HOL_Oplus__class_Oplus(X1,X2,X0) = c_HOL_Oplus__class_Oplus(X2,X1,X0)
| ~ class_Ring__and__Field_Ocomm__semiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f481_sk]) ).
cnf(hi468,axiom,
ifeq(class_Ring__and__Field_Ocomm__semiring__1(X0),true,c_HOL_Oplus__class_Oplus(X1,X2,X0),c_HOL_Oplus__class_Oplus(X2,X1,X0)) = c_HOL_Oplus__class_Oplus(X2,X1,X0),
inference(equality_encoding,[status(esa)],[c481]) ).
cnf(f886,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1) ).
fof(f886_nnf,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f886]) ).
cnf(c886,plain,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f886_nnf]) ).
cnf(hi859,axiom,
class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c886]) ).
cnf(t40,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X2,X1,tc_RealDef_Oreal),
inference(hyper_resolution,[status(thm)],[hi468,hi859]) ).
cnf(t2669,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_RealDef_Oreal) = c_HOL_Oplus__class_Oplus(X2,X1,tc_RealDef_Oreal),
inference(orient,[status(thm)],[t40]) ).
cnf(t3921,plain,
c_HOL_Oplus__class_Oplus(X2,c_HOL_Ominus__class_Ominus(X1,X2,tc_RealDef_Oreal),tc_RealDef_Oreal) = X1,
inference(step,[status(thm)],[t2686,t2669]) ).
cnf(t3622,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(X2,X1,tc_RealDef_Oreal),tc_RealDef_Oreal) = X2,
inference(orient,[status(thm)],[t3921]) ).
cnf(t3627,plain,
c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_Transcendental_Osin(X1),
inference(cp,[status(thm)],[t3266,t3622]) ).
cnf(t3743,plain,
c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)),tc_RealDef_Oreal) = c_Transcendental_Osin(X1),
inference(orient,[status(thm)],[t3627]) ).
cnf(t3753,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
inference(cp,[status(thm)],[t287,t3743]) ).
cnf(t3762,plain,
c_Transcendental_Osin(c_HOL_Ominus__class_Ominus(X1,c_Transcendental_Opi,tc_RealDef_Oreal)) = c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(X1),tc_RealDef_Oreal),
inference(orient,[status(thm)],[t3753]) ).
cnf(t3940,plain,
eq(c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal),c_HOL_Ouminus__class_Ouminus(c_Transcendental_Osin(v_x),tc_RealDef_Oreal)) = false,
inference(step,[status(thm)],[t3280,t3762]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1593,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t3941,plain,
true = false,
inference(step,[status(thm)],[t3940,t1593]) ).
cnf(t3764,plain,
true = false,
inference(rw,[status(thm)],[t3941]) ).
cnf(t3766,plain,
false = true,
inference(orient,[status(thm)],[t3764]) ).
cnf(f133,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f133_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)],[f133]) ).
fof(f133_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)],[f133_nnf]) ).
cnf(c133,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)],[f133_sk]) ).
cnf(f176,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/sandbox/benchmark/theBenchmark.p',cls_real__sqrt__not__eq__zero_0) ).
fof(f176_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)],[f176]) ).
fof(f176_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)],[f176_nnf]) ).
cnf(c176,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)],[f176_sk]) ).
cnf(f185,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/sandbox/benchmark/theBenchmark.p',cls_zero__less__norm__iff_0) ).
fof(f185_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)],[f185]) ).
fof(f185_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)],[f185_nnf]) ).
cnf(c185,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)],[f185_sk]) ).
cnf(f197,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f197_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)],[f197]) ).
fof(f197_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)],[f197_nnf]) ).
cnf(c197,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)],[f197_sk]) ).
cnf(f262,axiom,
c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_cos__arctan__not__zero_0) ).
fof(f262_nnf,plain,
! [V_x] : c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [V_x] : c_Transcendental_Ocos(c_Transcendental_Oarctan(V_x)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c262,plain,
c_Transcendental_Ocos(c_Transcendental_Oarctan(X0)) != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f291,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f291_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)],[f291]) ).
fof(f291_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)],[f291_nnf]) ).
cnf(c291,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)],[f291_sk]) ).
cnf(f365,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/sandbox/benchmark/theBenchmark.p',cls_norm__not__less__zero_0) ).
fof(f365_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)],[f365]) ).
fof(f365_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)],[f365_nnf]) ).
cnf(c365,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)],[f365_sk]) ).
cnf(f403,axiom,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pi__not__less__zero_0) ).
fof(f403_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)],[f403]) ).
fof(f403_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)],[f403_nnf]) ).
cnf(c403,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)],[f403_sk]) ).
cnf(f404,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f404_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)],[f404]) ).
fof(f404_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)],[f404_nnf]) ).
cnf(c404,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
cnf(f406,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f406_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)],[f406]) ).
fof(f406_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)],[f406_nnf]) ).
cnf(c406,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f406_sk]) ).
cnf(f408,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f408_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)],[f408]) ).
fof(f408_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)],[f408_nnf]) ).
cnf(c408,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f408_sk]) ).
cnf(f411,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f411_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)],[f411]) ).
fof(f411_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)],[f411_nnf]) ).
cnf(c411,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f411_sk]) ).
cnf(f477,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/sandbox/benchmark/theBenchmark.p',cls_not__real__square__gt__zero_1) ).
fof(f477_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)],[f477]) ).
fof(f477_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)],[f477_nnf]) ).
cnf(c477,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)],[f477_sk]) ).
cnf(f541,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f541_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)],[f541]) ).
fof(f541_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)],[f541_nnf]) ).
cnf(c541,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f541_sk]) ).
cnf(f542,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f542_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)],[f542]) ).
fof(f542_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)],[f542_nnf]) ).
cnf(c542,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f542_sk]) ).
cnf(f543,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_real__less__def_1) ).
fof(f543_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f543]) ).
fof(f543_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f543_nnf]) ).
cnf(c543,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f543_sk]) ).
cnf(f544,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f544_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)],[f544]) ).
fof(f544_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)],[f544_nnf]) ).
cnf(c544,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f544_sk]) ).
cnf(f667,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs__not__less__zero_0) ).
fof(f667_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)],[f667]) ).
fof(f667_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)],[f667_nnf]) ).
cnf(c667,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)],[f667_sk]) ).
cnf(f699,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ozero__class_Ozero(T_a),T_a),T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__less__abs__iff_0) ).
fof(f699_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)],[f699]) ).
fof(f699_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)],[f699_nnf]) ).
cnf(c699,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)],[f699_sk]) ).
cnf(f755,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f755_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)],[f755]) ).
fof(f755_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)],[f755_nnf]) ).
cnf(c755,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)],[f755_sk]) ).
cnf(f756,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f756_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)],[f756]) ).
fof(f756_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)],[f756_nnf]) ).
cnf(c756,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)],[f756_sk]) ).
cnf(f759,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f759_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)],[f759]) ).
fof(f759_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)],[f759_nnf]) ).
cnf(c759,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)],[f759_sk]) ).
cnf(f760,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f760_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)],[f760]) ).
fof(f760_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)],[f760_nnf]) ).
cnf(c760,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)],[f760_sk]) ).
cnf(f814,axiom,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_pi__neq__zero_0) ).
fof(f814_nnf,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f814]) ).
fof(f814_sk,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f814_nnf]) ).
cnf(c814,plain,
c_Transcendental_Opi != c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f814_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c133,c176,c185,c197,c262,c291,c365,c403,c404,c406,c408,c411,c477,c541,c542,c543,c544,c667,c699,c755,c756,c759,c760,c814,c861]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3766]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV592-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n013.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:39:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 20.04/3.32 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.04/3.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------