%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL855-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 : n007.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 02:03:13 PM UTC 2026
% Result : Unsatisfiable 17.94s 12.80s
% Output : Proof 17.94s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t224,axiom,
sF2 = ifeq(c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),true,false,true),
introduced(definition) ).
cnf(t222,axiom,
sF0 = c_Lambda_OdB_OApp(v_s____,v_ta____),
introduced(definition) ).
cnf(t233,plain,
c_Lambda_OdB_OApp(v_s____,v_ta____) = sF0,
inference(orient,[status(thm)],[t222]) ).
cnf(t3113,plain,
sF2 = ifeq(c_InductTermi_OIT(sF0),true,false,true),
inference(step,[status(thm)],[t224,t233]) ).
cnf(f361,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f361_nnf,plain,
~ c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),
inference(nnf_transformation,[status(thm)],[f361]) ).
fof(f361_sk,plain,
~ c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),
inference(skolemisation,[status(esa)],[f361_nnf]) ).
cnf(c361,plain,
~ c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),
inference(cnf_transformation,[status(esa)],[f361_sk]) ).
cnf(t10,plain,
c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)) = false,
inference(equality_encoding,[status(esa)],[c361]) ).
cnf(t3057,plain,
c_InductTermi_OIT(sF0) = false,
inference(step,[status(thm)],[t10,t233]) ).
cnf(t235,plain,
c_InductTermi_OIT(sF0) = false,
inference(orient,[status(thm)],[t3057]) ).
cnf(t223,axiom,
sF1 = c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)),
introduced(definition) ).
cnf(t3058,plain,
sF1 = c_InductTermi_OIT(sF0),
inference(step,[status(thm)],[t223,t233]) ).
cnf(t3059,plain,
sF1 = false,
inference(step,[status(thm)],[t3058,t235]) ).
cnf(t240,plain,
false = sF1,
inference(orient,[status(thm)],[t3059]) ).
cnf(t3064,plain,
c_InductTermi_OIT(sF0) = sF1,
inference(step,[status(thm)],[t235,t240]) ).
cnf(t245,plain,
c_InductTermi_OIT(sF0) = sF1,
inference(orient,[status(thm)],[t3064]) ).
cnf(t3114,plain,
sF2 = ifeq(sF1,true,false,true),
inference(step,[status(thm)],[t3113,t245]) ).
cnf(t3115,plain,
sF2 = ifeq(sF1,true,sF1,true),
inference(step,[status(thm)],[t3114,t240]) ).
cnf(f289,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f289_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f289]) ).
fof(f289_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f289_nnf]) ).
cnf(c289,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(t69,plain,
ifeq(c_HOL_Oord__class_Oless(X1,X1,tc_nat),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c289]) ).
cnf(t8,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = false,
inference(equality_encoding,[status(esa)],[c289]) ).
cnf(t234,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = false,
inference(orient,[status(thm)],[t8]) ).
cnf(t3062,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = sF1,
inference(step,[status(thm)],[t234,t240]) ).
cnf(t243,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = sF1,
inference(orient,[status(thm)],[t3062]) ).
cnf(t3093,plain,
ifeq(sF1,true,false,true) = true,
inference(step,[status(thm)],[t69,t243]) ).
cnf(t3094,plain,
ifeq(sF1,true,sF1,true) = true,
inference(step,[status(thm)],[t3093,t240]) ).
cnf(t473,plain,
ifeq(sF1,true,sF1,true) = true,
inference(orient,[status(thm)],[t3094]) ).
cnf(t3116,plain,
sF2 = true,
inference(step,[status(thm)],[t3115,t473]) ).
cnf(t524,plain,
true = sF2,
inference(orient,[status(thm)],[t3116]) ).
cnf(f360,axiom,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OApp(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Olift(v_ta____,c_HOL_Ozero__class_Ozero(tc_nat))),v_s____,c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f360_nnf,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OApp(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Olift(v_ta____,c_HOL_Ozero__class_Ozero(tc_nat))),v_s____,c_HOL_Ozero__class_Ozero(tc_nat))),
inference(nnf_transformation,[status(thm)],[f360]) ).
cnf(c360,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OApp(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Olift(v_ta____,c_HOL_Ozero__class_Ozero(tc_nat))),v_s____,c_HOL_Ozero__class_Ozero(tc_nat))),
inference(cnf_transformation,[status(esa)],[f360_nnf]) ).
cnf(t126,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OApp(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),c_Lambda_Olift(v_ta____,c_HOL_Ozero__class_Ozero(tc_nat))),v_s____,c_HOL_Ozero__class_Ozero(tc_nat))) = true,
inference(equality_encoding,[status(esa)],[c360]) ).
cnf(f342,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubst(V_t,V_s,V_k),c_Lambda_Osubst(V_u,V_s,V_k)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__App_0) ).
fof(f342_nnf,plain,
! [V_t,V_u,V_s,V_k] : c_Lambda_Osubst(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubst(V_t,V_s,V_k),c_Lambda_Osubst(V_u,V_s,V_k)),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
! [V_t,V_u,V_s,V_k] : c_Lambda_Osubst(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubst(V_t,V_s,V_k),c_Lambda_Osubst(V_u,V_s,V_k)),
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
c_Lambda_Osubst(c_Lambda_OdB_OApp(X0,X1),X2,X3) = c_Lambda_OdB_OApp(c_Lambda_Osubst(X0,X2,X3),c_Lambda_Osubst(X1,X2,X3)),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(t138,plain,
c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X2,X3),c_Lambda_Osubst(X4,X2,X3)) = c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,X4),X2,X3),
inference(equality_encoding,[status(esa)],[c342]) ).
cnf(t1460,plain,
c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X2,X3),c_Lambda_Osubst(X4,X2,X3)) = c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,X4),X2,X3),
inference(orient,[status(thm)],[t138]) ).
cnf(f323,axiom,
c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__lift_0) ).
fof(f323_nnf,plain,
! [V_t,V_k,V_s] : c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t,
inference(nnf_transformation,[status(thm)],[f323]) ).
fof(f323_sk,plain,
! [V_t,V_k,V_s] : c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t,
inference(skolemisation,[status(esa)],[f323_nnf]) ).
cnf(c323,plain,
c_Lambda_Osubst(c_Lambda_Olift(X0,X1),X2,X1) = X0,
inference(cnf_transformation,[status(esa)],[f323_sk]) ).
cnf(t38,plain,
c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
inference(equality_encoding,[status(esa)],[c323]) ).
cnf(t281,plain,
c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(t1464,plain,
c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,c_Lambda_Olift(X2,X3)),X4,X3) = c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X4,X3),X2),
inference(cp,[status(thm)],[t1460,t281]) ).
cnf(t1506,plain,
c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,c_Lambda_Olift(X2,X3)),X4,X3) = c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X4,X3),X2),
inference(orient,[status(thm)],[t1464]) ).
cnf(t3420,plain,
c_InductTermi_OIT(c_Lambda_OdB_OApp(c_Lambda_Osubst(c_Lambda_OdB_OVar(c_HOL_Ozero__class_Ozero(tc_nat)),v_s____,c_HOL_Ozero__class_Ozero(tc_nat)),v_ta____)) = true,
inference(step,[status(thm)],[t126,t1506]) ).
cnf(f339,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__eq_0) ).
fof(f339_nnf,plain,
! [V_k,V_u] : c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u,
inference(nnf_transformation,[status(thm)],[f339]) ).
fof(f339_sk,plain,
! [V_k,V_u] : c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u,
inference(skolemisation,[status(esa)],[f339_nnf]) ).
cnf(c339,plain,
c_Lambda_Osubst(c_Lambda_OdB_OVar(X0),X1,X0) = X1,
inference(cnf_transformation,[status(esa)],[f339_sk]) ).
cnf(t24,plain,
c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
inference(equality_encoding,[status(esa)],[c339]) ).
cnf(t261,plain,
c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
inference(orient,[status(thm)],[t24]) ).
cnf(t3421,plain,
c_InductTermi_OIT(c_Lambda_OdB_OApp(v_s____,v_ta____)) = true,
inference(step,[status(thm)],[t3420,t261]) ).
cnf(t3422,plain,
c_InductTermi_OIT(sF0) = true,
inference(step,[status(thm)],[t3421,t233]) ).
cnf(t3423,plain,
sF1 = true,
inference(step,[status(thm)],[t3422,t245]) ).
cnf(t3424,plain,
sF1 = sF2,
inference(step,[status(thm)],[t3423,t524]) ).
cnf(t2561,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t3424]) ).
cnf(t3473,plain,
true = sF1,
inference(step,[status(thm)],[t524,t2561]) ).
cnf(t2610,plain,
true = sF1,
inference(orient,[status(thm)],[t3473]) ).
cnf(f96,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(f96_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)],[f96]) ).
fof(f96_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)],[f96_nnf]) ).
cnf(c96,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)],[f96_sk]) ).
cnf(f112,axiom,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,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_of__nat__less__0__iff_0) ).
fof(f112_nnf,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
! [T_a,V_m] :
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f112_nnf]) ).
cnf(c112,plain,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
cnf(f148,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(f148_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)],[f148]) ).
fof(f148_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)],[f148_nnf]) ).
cnf(c148,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)],[f148_sk]) ).
cnf(f171,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(f171_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)],[f171]) ).
fof(f171_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)],[f171_nnf]) ).
cnf(c171,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)],[f171_sk]) ).
cnf(f210,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f210_nnf,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c210,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(f211,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f211_nnf,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f256,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(f256_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)],[f256]) ).
fof(f256_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)],[f256_nnf]) ).
cnf(c256,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)],[f256_sk]) ).
cnf(f257,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(f257_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)],[f257]) ).
fof(f257_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)],[f257_nnf]) ).
cnf(c257,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)],[f257_sk]) ).
cnf(f258,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(f258_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)],[f258]) ).
fof(f258_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)],[f258_nnf]) ).
cnf(c258,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)],[f258_sk]) ).
cnf(f259,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(f259_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)],[f259]) ).
fof(f259_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)],[f259_nnf]) ).
cnf(c259,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)],[f259_sk]) ).
cnf(f264,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f264_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f264]) ).
fof(f264_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f264_nnf]) ).
cnf(c264,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f264_sk]) ).
cnf(f265,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f265_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c265,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f268,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f268_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c268,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(f276,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f276_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f276]) ).
fof(f276_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f276_nnf]) ).
cnf(c276,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f276_sk]) ).
cnf(f277,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f277_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c277,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
cnf(f286,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(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(f287,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(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f287_sk]) ).
cnf(f288,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(f288_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)],[f288]) ).
fof(f288_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)],[f288_nnf]) ).
cnf(c288,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
cnf(f290,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f290_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f290]) ).
fof(f290_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f290_nnf]) ).
cnf(c290,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
cnf(f298,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f298_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c298,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f299,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f299_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f299]) ).
fof(f299_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f299_nnf]) ).
cnf(c299,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f299_sk]) ).
cnf(f306,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f306_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f306]) ).
fof(f306_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f306_nnf]) ).
cnf(c306,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
cnf(f307,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f307_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f307]) ).
fof(f307_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f307_nnf]) ).
cnf(c307,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f307_sk]) ).
cnf(f313,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f313_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f313]) ).
fof(f313_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f313_nnf]) ).
cnf(c313,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
cnf(f330,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f330_nnf,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f330]) ).
fof(f330_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f330_nnf]) ).
cnf(c330,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f330_sk]) ).
cnf(f334,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f334_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c334,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(f341,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f341_nnf,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f341]) ).
fof(f341_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f341_nnf]) ).
cnf(c341,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f341_sk]) ).
cnf(f343,axiom,
c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f343_nnf,plain,
! [V_dB1,V_dB2,V_dB_H] : c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f343]) ).
fof(f343_sk,plain,
! [V_dB1,V_dB2,V_dB_H] : c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f343_nnf]) ).
cnf(c343,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f343_sk]) ).
cnf(f344,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f344_nnf,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(f347,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f347_nnf,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
inference(skolemisation,[status(esa)],[f347_nnf]) ).
cnf(c347,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(f359,axiom,
c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f359_nnf,plain,
! [V_dB1_H,V_dB2_H,V_nat] : c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f359]) ).
fof(f359_sk,plain,
! [V_dB1_H,V_dB2_H,V_nat] : c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f359_nnf]) ).
cnf(c359,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c96,c112,c148,c171,c210,c211,c256,c257,c258,c259,c264,c265,c268,c276,c277,c286,c287,c288,c289,c290,c298,c299,c306,c307,c313,c330,c334,c341,c343,c344,c347,c359,c361]) ).
cnf(g0_0,plain,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t2610]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t240]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL855-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/10.42 % Computer : n007.cluster.edu
% 0.15/10.42 % Model : x86_64 x86_64
% 0.15/10.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/10.42 % Memory : 8046.5625MB
% 0.15/10.42 % OS : Linux 6.8.0-71-generic
% 0.15/10.42 % CPULimit : 300
% 0.15/10.42 % WCLimit : 300
% 0.15/10.42 % DateTime : Thu Sep 24 00:34:18 UTC 2026
% 0.15/10.43 % CPUTime :
% 0.15/10.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 17.94/12.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.94/12.80 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------