%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG395-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 : n014.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:27 PM UTC 2026
% Result : Unsatisfiable 19.79s 2.96s
% Output : Proof 19.79s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t82,axiom,
sF0 = ifeq(v_thesis____,true,false,true),
introduced(definition) ).
cnf(f749,negated_conjecture,
~ v_thesis____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f749_nnf,plain,
~ v_thesis____,
inference(nnf_transformation,[status(thm)],[f749]) ).
fof(f749_sk,plain,
~ v_thesis____,
inference(skolemisation,[status(esa)],[f749_nnf]) ).
cnf(c749,plain,
~ v_thesis____,
inference(cnf_transformation,[status(esa)],[f749_sk]) ).
cnf(t0,plain,
v_thesis____ = false,
inference(equality_encoding,[status(esa)],[c749]) ).
cnf(t90,plain,
false = v_thesis____,
inference(orient,[status(thm)],[t0]) ).
cnf(t764,plain,
sF0 = ifeq(v_thesis____,true,v_thesis____,true),
inference(step,[status(thm)],[t82,t90]) ).
cnf(t16,plain,
ifeq(v_thesis____,true,false,true) = true,
inference(equality_encoding,[status(esa)],[c749]) ).
cnf(t763,plain,
ifeq(v_thesis____,true,v_thesis____,true) = true,
inference(step,[status(thm)],[t16,t90]) ).
cnf(t107,plain,
ifeq(v_thesis____,true,v_thesis____,true) = true,
inference(orient,[status(thm)],[t763]) ).
cnf(t765,plain,
sF0 = true,
inference(step,[status(thm)],[t764,t107]) ).
cnf(t108,plain,
true = sF0,
inference(orient,[status(thm)],[t765]) ).
cnf(f750,negated_conjecture,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,V_xa,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f750_nnf,plain,
! [V_xa] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,V_xa,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
inference(nnf_transformation,[status(thm)],[f750]) ).
fof(f750_sk,plain,
! [V_xa] :
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,V_xa,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,V_xa),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
inference(skolemisation,[status(esa)],[f750_nnf]) ).
cnf(c750,plain,
( ~ c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X0,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal)
| v_thesis____ ),
inference(cnf_transformation,[status(esa)],[f750_sk]) ).
cnf(t61,plain,
ifeq(c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(equality_encoding,[status(esa)],[c750]) ).
cnf(t83,axiom,
sF1(X1) = c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t105,plain,
c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex) = sF1(X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t1014,plain,
ifeq(c_lessequals(c_RealVector_Onorm__class_Onorm(sF1(X1),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t61,t105]) ).
cnf(t84,axiom,
sF2(X1) = c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t787,plain,
sF2(X1) = c_RealVector_Onorm__class_Onorm(sF1(X1),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t84,t105]) ).
cnf(t134,plain,
c_RealVector_Onorm__class_Onorm(sF1(X1),tc_Complex_Ocomplex) = sF2(X1),
inference(orient,[status(thm)],[t787]) ).
cnf(t1015,plain,
ifeq(c_lessequals(sF2(X1),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1014,t134]) ).
cnf(t1016,plain,
ifeq(c_lessequals(sF2(X1),c_RealVector_Onorm__class_Onorm(sF1(hAPP(v_x,X1)),tc_Complex_Ocomplex),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1015,t105]) ).
cnf(t1017,plain,
ifeq(c_lessequals(sF2(X1),sF2(hAPP(v_x,X1)),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1016,t134]) ).
cnf(t85,axiom,
sF3(X1) = hAPP(v_x,X1),
introduced(definition) ).
cnf(t102,plain,
hAPP(v_x,X1) = sF3(X1),
inference(orient,[status(thm)],[t85]) ).
cnf(t1018,plain,
ifeq(c_lessequals(sF2(X1),sF2(sF3(X1)),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1017,t102]) ).
cnf(t87,axiom,
sF5(X1) = c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
introduced(definition) ).
cnf(t832,plain,
sF5(X1) = c_RealVector_Onorm__class_Onorm(sF1(hAPP(v_x,X1)),tc_Complex_Ocomplex),
inference(step,[status(thm)],[t87,t105]) ).
cnf(t833,plain,
sF5(X1) = sF2(hAPP(v_x,X1)),
inference(step,[status(thm)],[t832,t134]) ).
cnf(t834,plain,
sF5(X1) = sF2(sF3(X1)),
inference(step,[status(thm)],[t833,t102]) ).
cnf(t184,plain,
sF2(sF3(X1)) = sF5(X1),
inference(orient,[status(thm)],[t834]) ).
cnf(t1019,plain,
ifeq(c_lessequals(sF2(X1),sF5(X1),tc_RealDef_Oreal),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1018,t184]) ).
cnf(t88,axiom,
sF6(X1) = c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
introduced(definition) ).
cnf(t970,plain,
sF6(X1) = c_lessequals(c_RealVector_Onorm__class_Onorm(sF1(X1),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(step,[status(thm)],[t88,t105]) ).
cnf(t971,plain,
sF6(X1) = c_lessequals(sF2(X1),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,hAPP(v_x,X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(step,[status(thm)],[t970,t134]) ).
cnf(t972,plain,
sF6(X1) = c_lessequals(sF2(X1),c_RealVector_Onorm__class_Onorm(sF1(hAPP(v_x,X1)),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(step,[status(thm)],[t971,t105]) ).
cnf(t973,plain,
sF6(X1) = c_lessequals(sF2(X1),sF2(hAPP(v_x,X1)),tc_RealDef_Oreal),
inference(step,[status(thm)],[t972,t134]) ).
cnf(t974,plain,
sF6(X1) = c_lessequals(sF2(X1),sF2(sF3(X1)),tc_RealDef_Oreal),
inference(step,[status(thm)],[t973,t102]) ).
cnf(t975,plain,
sF6(X1) = c_lessequals(sF2(X1),sF5(X1),tc_RealDef_Oreal),
inference(step,[status(thm)],[t974,t184]) ).
cnf(t439,plain,
c_lessequals(sF2(X1),sF5(X1),tc_RealDef_Oreal) = sF6(X1),
inference(orient,[status(thm)],[t975]) ).
cnf(t1020,plain,
ifeq(sF6(X1),true,v_thesis____,true) = true,
inference(step,[status(thm)],[t1019,t439]) ).
cnf(t1021,plain,
ifeq(sF6(X1),sF0,v_thesis____,true) = true,
inference(step,[status(thm)],[t1020,t108]) ).
cnf(t1022,plain,
ifeq(sF6(X1),sF0,v_thesis____,sF0) = true,
inference(step,[status(thm)],[t1021,t108]) ).
cnf(t1023,plain,
ifeq(sF6(X1),sF0,v_thesis____,sF0) = sF0,
inference(step,[status(thm)],[t1022,t108]) ).
cnf(t726,plain,
ifeq(sF6(X1),sF0,v_thesis____,sF0) = sF0,
inference(orient,[status(thm)],[t1023]) ).
cnf(f734,axiom,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(V_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,V_w,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_poly__minimum__modulus_0) ).
fof(f734_nnf,plain,
! [V_p,V_w] : c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(V_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,V_w,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f734]) ).
fof(f734_sk,plain,
! [V_p,V_w] : c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(V_p),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(V_p,V_w,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f734_nnf]) ).
cnf(c734,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X0,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(X0),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X0,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f734_sk]) ).
cnf(t43,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = true,
inference(equality_encoding,[status(esa)],[c734]) ).
cnf(t908,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = sF0,
inference(step,[status(thm)],[t43,t108]) ).
cnf(t330,plain,
c_lessequals(c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(X1),tc_Complex_Ocomplex),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(X1,X2,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal) = sF0,
inference(orient,[status(thm)],[t908]) ).
cnf(t331,plain,
sF0 = c_lessequals(c_RealVector_Onorm__class_Onorm(sF1(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),tc_Complex_Ocomplex),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(cp,[status(thm)],[t330,t105]) ).
cnf(t909,plain,
sF0 = c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),c_RealVector_Onorm__class_Onorm(c_Polynomial_Opoly(v_pa____,X1,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(step,[status(thm)],[t331,t134]) ).
cnf(t910,plain,
sF0 = c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),c_RealVector_Onorm__class_Onorm(sF1(X1),tc_Complex_Ocomplex),tc_RealDef_Oreal),
inference(step,[status(thm)],[t909,t105]) ).
cnf(t911,plain,
sF0 = c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),sF2(X1),tc_RealDef_Oreal),
inference(step,[status(thm)],[t910,t134]) ).
cnf(t333,plain,
c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),sF2(X1),tc_RealDef_Oreal) = sF0,
inference(orient,[status(thm)],[t911]) ).
cnf(t334,plain,
sF0 = c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),sF5(X1),tc_RealDef_Oreal),
inference(cp,[status(thm)],[t333,t184]) ).
cnf(t336,plain,
c_lessequals(sF2(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)),sF5(X1),tc_RealDef_Oreal) = sF0,
inference(orient,[status(thm)],[t334]) ).
cnf(t441,plain,
sF6(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)) = sF0,
inference(cp,[status(thm)],[t439,t336]) ).
cnf(t449,plain,
sF6(v_sko__Fundamental__Theorem__Algebra__Mi_h5c979da0438526d5(v_pa____)) = sF0,
inference(orient,[status(thm)],[t441]) ).
cnf(t727,plain,
sF0 = ifeq(sF0,sF0,v_thesis____,sF0),
inference(cp,[status(thm)],[t726,t449]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t106,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t1024,plain,
sF0 = v_thesis____,
inference(step,[status(thm)],[t727,t106]) ).
cnf(t728,plain,
v_thesis____ = sF0,
inference(orient,[status(thm)],[t1024]) ).
cnf(t1025,plain,
false = sF0,
inference(step,[status(thm)],[t90,t728]) ).
cnf(t729,plain,
false = sF0,
inference(orient,[status(thm)],[t1025]) ).
cnf(f4,axiom,
~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__exp__less__zero_0) ).
fof(f4_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f7,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(f7_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)],[f7]) ).
fof(f7_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)],[f7_nnf]) ).
cnf(c7,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)],[f7_sk]) ).
cnf(f50,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(f50_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)],[f50]) ).
fof(f50_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)],[f50_nnf]) ).
cnf(c50,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)],[f50_sk]) ).
cnf(f63,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(f63_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)],[f63]) ).
fof(f63_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)],[f63_nnf]) ).
cnf(c63,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)],[f63_sk]) ).
cnf(f121,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(f121_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)],[f121]) ).
fof(f121_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)],[f121_nnf]) ).
cnf(c121,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)],[f121_sk]) ).
cnf(f218,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(f218_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)],[f218]) ).
fof(f218_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)],[f218_nnf]) ).
cnf(c218,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)],[f218_sk]) ).
cnf(f252,axiom,
~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__exp__le__zero_0) ).
fof(f252_nnf,plain,
! [V_x] : ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f252]) ).
fof(f252_sk,plain,
! [V_x] : ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f252_nnf]) ).
cnf(c252,plain,
~ c_lessequals(c_Transcendental_Oexp(X0,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f252_sk]) ).
cnf(f345,axiom,
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_exp__not__eq__zero_0) ).
fof(f345_nnf,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(nnf_transformation,[status(thm)],[f345]) ).
fof(f345_sk,plain,
! [T_a,V_x] :
( c_Transcendental_Oexp(V_x,T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_RealVector_Oreal__normed__field(T_a)
| ~ class_SEQ_Obanach(T_a) ),
inference(skolemisation,[status(esa)],[f345_nnf]) ).
cnf(c345,plain,
( c_Transcendental_Oexp(X1,X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_RealVector_Oreal__normed__field(X0)
| ~ class_SEQ_Obanach(X0) ),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
cnf(f363,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(f363_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)],[f363]) ).
fof(f363_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)],[f363_nnf]) ).
cnf(c363,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)],[f363_sk]) ).
cnf(f432,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(f432_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)],[f432]) ).
fof(f432_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)],[f432_nnf]) ).
cnf(c432,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)],[f432_sk]) ).
cnf(f575,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(f575_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)],[f575]) ).
fof(f575_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)],[f575_nnf]) ).
cnf(c575,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f575_sk]) ).
cnf(f576,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(f576_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)],[f576]) ).
fof(f576_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)],[f576_nnf]) ).
cnf(c576,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f576_sk]) ).
cnf(f577,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(f577_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f577]) ).
fof(f577_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f577_nnf]) ).
cnf(c577,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f577_sk]) ).
cnf(f578,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(f578_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)],[f578]) ).
fof(f578_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)],[f578_nnf]) ).
cnf(c578,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f578_sk]) ).
cnf(f591,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(f591_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)],[f591]) ).
fof(f591_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)],[f591_nnf]) ).
cnf(c591,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)],[f591_sk]) ).
cnf(f614,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(f614_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)],[f614]) ).
fof(f614_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)],[f614_nnf]) ).
cnf(c614,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)],[f614_sk]) ).
cnf(f644,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(f644_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)],[f644]) ).
fof(f644_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)],[f644_nnf]) ).
cnf(c644,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)],[f644_sk]) ).
cnf(f645,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(f645_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)],[f645]) ).
fof(f645_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)],[f645_nnf]) ).
cnf(c645,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)],[f645_sk]) ).
cnf(f646,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(f646_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)],[f646]) ).
fof(f646_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)],[f646_nnf]) ).
cnf(c646,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)],[f646_sk]) ).
cnf(f647,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(f647_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)],[f647]) ).
fof(f647_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)],[f647_nnf]) ).
cnf(c647,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)],[f647_sk]) ).
cnf(f686,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(f686_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)],[f686]) ).
fof(f686_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)],[f686_nnf]) ).
cnf(c686,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f686_sk]) ).
cnf(f688,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(f688_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)],[f688]) ).
fof(f688_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)],[f688_nnf]) ).
cnf(c688,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f688_sk]) ).
cnf(f690,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(f690_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)],[f690]) ).
fof(f690_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)],[f690_nnf]) ).
cnf(c690,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f690_sk]) ).
cnf(f693,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(f693_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)],[f693]) ).
fof(f693_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)],[f693_nnf]) ).
cnf(c693,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f693_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c4,c7,c50,c63,c121,c218,c252,c345,c363,c432,c575,c576,c577,c578,c591,c614,c644,c645,c646,c647,c686,c688,c690,c693,c749]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t108]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t729]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG395-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.38 % Computer : n014.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 05:33:04 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.79/2.96 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.79/2.96 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------