%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG350-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 : n020.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:21 PM UTC 2026
% Result : Unsatisfiable 7.08s 1.38s
% Output : Proof 7.08s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t154,axiom,
sF2 = hBOOL(hAPP(v_P,v_xa)),
introduced(definition) ).
cnf(t153,axiom,
sF1 = hAPP(v_P,v_xa),
introduced(definition) ).
cnf(t166,plain,
hAPP(v_P,v_xa) = sF1,
inference(orient,[status(thm)],[t153]) ).
cnf(t290,plain,
sF2 = hBOOL(sF1),
inference(step,[status(thm)],[t154,t166]) ).
cnf(f351,negated_conjecture,
hBOOL(hAPP(v_P,v_xa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f351_nnf,plain,
hBOOL(hAPP(v_P,v_xa)),
inference(nnf_transformation,[status(thm)],[f351]) ).
cnf(c351,plain,
hBOOL(hAPP(v_P,v_xa)),
inference(cnf_transformation,[status(esa)],[f351_nnf]) ).
cnf(t14,plain,
hBOOL(hAPP(v_P,v_xa)) = true,
inference(equality_encoding,[status(esa)],[c351]) ).
cnf(t279,plain,
hBOOL(sF1) = true,
inference(step,[status(thm)],[t14,t166]) ).
cnf(t170,plain,
hBOOL(sF1) = true,
inference(orient,[status(thm)],[t279]) ).
cnf(t291,plain,
sF2 = true,
inference(step,[status(thm)],[t290,t170]) ).
cnf(t184,plain,
true = sF2,
inference(orient,[status(thm)],[t291]) ).
cnf(f324,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_real__less__def_0) ).
fof(f324_nnf,plain,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f324]) ).
fof(f324_sk,plain,
! [V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal)
| c_lessequals(V_x,V_y,tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f324_nnf]) ).
cnf(c324,plain,
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_RealDef_Oreal)
| c_lessequals(X0,X1,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
cnf(t28,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),true,c_lessequals(X1,X2,tc_RealDef_Oreal),true) = true,
inference(equality_encoding,[status(esa)],[c324]) ).
cnf(t338,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),sF2,c_lessequals(X1,X2,tc_RealDef_Oreal),true) = true,
inference(step,[status(thm)],[t28,t184]) ).
cnf(t339,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),sF2,c_lessequals(X1,X2,tc_RealDef_Oreal),sF2) = true,
inference(step,[status(thm)],[t338,t184]) ).
cnf(t340,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),sF2,c_lessequals(X1,X2,tc_RealDef_Oreal),sF2) = sF2,
inference(step,[status(thm)],[t339,t184]) ).
cnf(t226,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X2,tc_RealDef_Oreal),sF2,c_lessequals(X1,X2,tc_RealDef_Oreal),sF2) = sF2,
inference(orient,[status(thm)],[t340]) ).
cnf(f337,axiom,
( ~ hBOOL(hAPP(v_P,V_x))
| c_HOL_Oord__class_Oless(V_x,v_Y____,tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Y_0) ).
fof(f337_nnf,plain,
! [V_x] :
( ~ hBOOL(hAPP(v_P,V_x))
| c_HOL_Oord__class_Oless(V_x,v_Y____,tc_RealDef_Oreal) ),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [V_x] :
( ~ hBOOL(hAPP(v_P,V_x))
| c_HOL_Oord__class_Oless(V_x,v_Y____,tc_RealDef_Oreal) ),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
( ~ hBOOL(hAPP(v_P,X0))
| c_HOL_Oord__class_Oless(X0,v_Y____,tc_RealDef_Oreal) ),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(t29,plain,
ifeq(hBOOL(hAPP(v_P,X1)),true,c_HOL_Oord__class_Oless(X1,v_Y____,tc_RealDef_Oreal),true) = true,
inference(equality_encoding,[status(esa)],[c337]) ).
cnf(t341,plain,
ifeq(hBOOL(hAPP(v_P,X1)),sF2,c_HOL_Oord__class_Oless(X1,v_Y____,tc_RealDef_Oreal),true) = true,
inference(step,[status(thm)],[t29,t184]) ).
cnf(t342,plain,
ifeq(hBOOL(hAPP(v_P,X1)),sF2,c_HOL_Oord__class_Oless(X1,v_Y____,tc_RealDef_Oreal),sF2) = true,
inference(step,[status(thm)],[t341,t184]) ).
cnf(t343,plain,
ifeq(hBOOL(hAPP(v_P,X1)),sF2,c_HOL_Oord__class_Oless(X1,v_Y____,tc_RealDef_Oreal),sF2) = sF2,
inference(step,[status(thm)],[t342,t184]) ).
cnf(t230,plain,
ifeq(hBOOL(hAPP(v_P,X1)),sF2,c_HOL_Oord__class_Oless(X1,v_Y____,tc_RealDef_Oreal),sF2) = sF2,
inference(orient,[status(thm)],[t343]) ).
cnf(t231,plain,
sF2 = ifeq(hBOOL(sF1),sF2,c_HOL_Oord__class_Oless(v_xa,v_Y____,tc_RealDef_Oreal),sF2),
inference(cp,[status(thm)],[t230,t166]) ).
cnf(t303,plain,
hBOOL(sF1) = sF2,
inference(step,[status(thm)],[t170,t184]) ).
cnf(t198,plain,
hBOOL(sF1) = sF2,
inference(orient,[status(thm)],[t303]) ).
cnf(t344,plain,
sF2 = ifeq(sF2,sF2,c_HOL_Oord__class_Oless(v_xa,v_Y____,tc_RealDef_Oreal),sF2),
inference(step,[status(thm)],[t231,t198]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t202,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t345,plain,
sF2 = c_HOL_Oord__class_Oless(v_xa,v_Y____,tc_RealDef_Oreal),
inference(step,[status(thm)],[t344,t202]) ).
cnf(t233,plain,
c_HOL_Oord__class_Oless(v_xa,v_Y____,tc_RealDef_Oreal) = sF2,
inference(orient,[status(thm)],[t345]) ).
cnf(t234,plain,
sF2 = ifeq(sF2,sF2,c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),sF2),
inference(cp,[status(thm)],[t226,t233]) ).
cnf(t346,plain,
sF2 = c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
inference(step,[status(thm)],[t234,t202]) ).
cnf(f352,negated_conjecture,
~ c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f352_nnf,plain,
~ c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
~ c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f352_nnf]) ).
cnf(c352,plain,
~ c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(t13,plain,
c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal) = false,
inference(equality_encoding,[status(esa)],[c352]) ).
cnf(t169,plain,
c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal) = false,
inference(orient,[status(thm)],[t13]) ).
cnf(t152,axiom,
sF0 = c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal),
introduced(definition) ).
cnf(t280,plain,
sF0 = false,
inference(step,[status(thm)],[t152,t169]) ).
cnf(t171,plain,
false = sF0,
inference(orient,[status(thm)],[t280]) ).
cnf(t288,plain,
c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal) = sF0,
inference(step,[status(thm)],[t169,t171]) ).
cnf(t179,plain,
c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal) = sF0,
inference(orient,[status(thm)],[t288]) ).
cnf(t347,plain,
sF2 = sF0,
inference(step,[status(thm)],[t346,t179]) ).
cnf(t235,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t347]) ).
cnf(t362,plain,
true = sF0,
inference(step,[status(thm)],[t184,t235]) ).
cnf(t250,plain,
true = sF0,
inference(orient,[status(thm)],[t362]) ).
cnf(f221,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(f221_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)],[f221]) ).
fof(f221_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)],[f221_nnf]) ).
cnf(c221,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f222,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(f222_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)],[f222]) ).
fof(f222_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)],[f222_nnf]) ).
cnf(c222,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f223,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(f223_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f224,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(f224_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)],[f224]) ).
fof(f224_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)],[f224_nnf]) ).
cnf(c224,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(f246,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(f246_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)],[f246]) ).
fof(f246_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)],[f246_nnf]) ).
cnf(c246,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)],[f246_sk]) ).
cnf(f247,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(f247_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)],[f247]) ).
fof(f247_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)],[f247_nnf]) ).
cnf(c247,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)],[f247_sk]) ).
cnf(f248,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(f248_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)],[f248]) ).
fof(f248_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)],[f248_nnf]) ).
cnf(c248,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)],[f248_sk]) ).
cnf(f249,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(f249_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)],[f249]) ).
fof(f249_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)],[f249_nnf]) ).
cnf(c249,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)],[f249_sk]) ).
cnf(f309,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(f309_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)],[f309]) ).
fof(f309_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)],[f309_nnf]) ).
cnf(c309,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
cnf(f311,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(f311_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)],[f311]) ).
fof(f311_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)],[f311_nnf]) ).
cnf(c311,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
cnf(f313,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(f313_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)],[f313]) ).
fof(f313_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)],[f313_nnf]) ).
cnf(c313,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
cnf(f316,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(f316_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)],[f316]) ).
fof(f316_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)],[f316_nnf]) ).
cnf(c316,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c221,c222,c223,c224,c246,c247,c248,c249,c309,c311,c313,c316,c352]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t250]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t171]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG350-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 05:27:18 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.08/1.38 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.08/1.38 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------