%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL814-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 : n016.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:07 PM UTC 2026
% Result : Unsatisfiable 29.22s 9.08s
% Output : Proof 29.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 53
% Syntax : Number of formulae : 226 ( 150 unt; 0 def)
% Number of atoms : 346 ( 103 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 438 ( 318 ~; 120 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 9 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-4 aty)
% Number of functors : 31 ( 31 usr; 14 con; 0-5 aty)
% Number of variables : 453 ( 96 sgn 216 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f615,axiom,
( ~ c_Type_Otyping(V_e,V_u,V_T)
| ~ c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_T,tc_Type_Otype),V_ts,V_Ts)
| c_Type_Otypings(V_e,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),V_u),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_substs__lemma_0) ).
fof(f615_nnf,plain,
! [V_e,V_u,V_i,V_ts,V_Ts,V_T] :
( ~ c_Type_Otyping(V_e,V_u,V_T)
| ~ c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_T,tc_Type_Otype),V_ts,V_Ts)
| c_Type_Otypings(V_e,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),V_u),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
inference(nnf_transformation,[status(thm)],[f615]) ).
fof(f615_sk,plain,
! [V_e,V_u,V_i,V_ts,V_Ts,V_T] :
( ~ c_Type_Otyping(V_e,V_u,V_T)
| ~ c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_T,tc_Type_Otype),V_ts,V_Ts)
| c_Type_Otypings(V_e,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),V_u),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) ),
inference(skolemisation,[status(esa)],[f615_nnf]) ).
cnf(c615,plain,
( ~ c_Type_Otyping(X0,X1,X5)
| ~ c_Type_Otypings(c_Type_Oshift(X0,X2,X5,tc_Type_Otype),X3,X4)
| c_Type_Otypings(X0,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),X4) ),
inference(cnf_transformation,[status(esa)],[f615_sk]) ).
cnf(t81,plain,
ifeq(c_Type_Otypings(c_Type_Oshift(X1,X2,X3,tc_Type_Otype),X4,X5),true,ifeq(c_Type_Otyping(X1,X6,X3),true,c_Type_Otypings(X1,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X6),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X2),X4,tc_Lambda_OdB,tc_Lambda_OdB),X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c615]) ).
cnf(t101,plain,
ifeq(c_Type_Otypings(c_Type_Oshift(X1,X2,X3,tc_Type_Otype),X4,X5),true,ifeq(c_Type_Otyping(X1,X6,X3),true,c_Type_Otypings(X1,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X6),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),X2),X4,tc_Lambda_OdB,tc_Lambda_OdB),X5),true),true) = true,
inference(orient,[status(thm)],[t81]) ).
cnf(f607,axiom,
c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_argsT_0) ).
fof(f607_nnf,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____),
inference(nnf_transformation,[status(thm)],[f607]) ).
cnf(c607,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____),
inference(cnf_transformation,[status(esa)],[f607_nnf]) ).
cnf(t32,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) = true,
inference(equality_encoding,[status(esa)],[c607]) ).
cnf(t119,plain,
c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(t121,plain,
true = ifeq(true,true,ifeq(c_Type_Otyping(v_e____,X1,v_T____),true,c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),true),true),
inference(cp,[status(thm)],[t101,t119]) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t85,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(t837,plain,
true = ifeq(c_Type_Otyping(v_e____,X1,v_T____),true,c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),true),
inference(step,[status(thm)],[t121,t85]) ).
cnf(t678,plain,
ifeq(c_Type_Otyping(v_e____,X1,v_T____),true,c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),true) = true,
inference(orient,[status(thm)],[t837]) ).
cnf(f590,axiom,
c_Type_Otyping(v_e____,v_u____,v_T____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_uT_0) ).
fof(f590_nnf,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(nnf_transformation,[status(thm)],[f590]) ).
cnf(c590,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(cnf_transformation,[status(esa)],[f590_nnf]) ).
cnf(t9,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(equality_encoding,[status(esa)],[c590]) ).
cnf(t132,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t679,plain,
true = ifeq(true,true,c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),true),
inference(cp,[status(thm)],[t678,t132]) ).
cnf(t838,plain,
true = c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(step,[status(thm)],[t679,t85]) ).
cnf(f628,negated_conjecture,
~ c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f628_nnf,plain,
~ c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(nnf_transformation,[status(thm)],[f628]) ).
fof(f628_sk,plain,
~ c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(skolemisation,[status(esa)],[f628_nnf]) ).
cnf(c628,plain,
~ c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____),
inference(cnf_transformation,[status(esa)],[f628_sk]) ).
cnf(t72,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = false,
inference(equality_encoding,[status(esa)],[c628]) ).
cnf(t223,plain,
c_Type_Otypings(v_e____,c_List_Omap(hAPP(c_COMBC(hAPP(c_COMBC(c_Lambda_Osubst,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_u____),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_i____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_Ts____) = false,
inference(orient,[status(thm)],[t72]) ).
cnf(t839,plain,
true = false,
inference(step,[status(thm)],[t838,t223]) ).
cnf(t681,plain,
false = true,
inference(orient,[status(thm)],[t839]) ).
cnf(f0,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f0_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f1,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f1_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f10,axiom,
~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f10_nnf,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
~ c_ListOrder_Ostep1(X0,X1,c_List_Olist_ONil(X2),X2),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f11,axiom,
~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f11_nnf,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
~ c_ListOrder_Ostep1(X0,c_List_Olist_ONil(X1),X2,X1),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f14,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f14_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)],[f14]) ).
fof(f14_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f49,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f49_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(f50,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f50_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f106,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f106_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c106,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
cnf(f107,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f107_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f107]) ).
fof(f107_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f107_nnf]) ).
cnf(c107,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f107_sk]) ).
cnf(f108,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(f108_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)],[f108]) ).
fof(f108_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)],[f108_nnf]) ).
cnf(c108,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(f109,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(f109_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)],[f109]) ).
fof(f109_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)],[f109_nnf]) ).
cnf(c109,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(f110,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(f110_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)],[f110]) ).
fof(f110_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)],[f110_nnf]) ).
cnf(c110,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(f114,axiom,
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f114_nnf,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c114,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(f139,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f139_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f139]) ).
fof(f139_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f139_nnf]) ).
cnf(c139,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f139_sk]) ).
cnf(f140,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f140_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f140]) ).
fof(f140_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f140_nnf]) ).
cnf(c140,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
cnf(f156,axiom,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).
fof(f156_nnf,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f156]) ).
fof(f156_sk,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(V_w,T_a),c_Int_Onumber__class_Onumber__of(V_v,T_a),T_a)
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f156_nnf]) ).
cnf(c156,plain,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X1,X0),X0)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(X1,X0),c_Int_Onumber__class_Onumber__of(X2,X0),X0)
| ~ class_Int_Onumber(X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f156_sk]) ).
cnf(f162,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/sandbox/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f162_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)],[f162]) ).
fof(f162_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)],[f162_nnf]) ).
cnf(c162,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)],[f162_sk]) ).
cnf(f168,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f168_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f178,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f178_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f178]) ).
fof(f178_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f178_nnf]) ).
cnf(c178,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f178_sk]) ).
cnf(f179,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f179_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c179,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(f194,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f194_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)],[f194]) ).
fof(f194_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f195,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f195_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)],[f195]) ).
fof(f195_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(f203,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(f203_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)],[f203]) ).
fof(f203_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)],[f203_nnf]) ).
cnf(c203,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(f205,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(f205_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)],[f205]) ).
fof(f205_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)],[f205_nnf]) ).
cnf(c205,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f207,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(f207_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)],[f207]) ).
fof(f207_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)],[f207_nnf]) ).
cnf(c207,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f207_sk]) ).
cnf(f209,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(f209_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)],[f209]) ).
fof(f209_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)],[f209_nnf]) ).
cnf(c209,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(f220,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f220_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(f240,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f240_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f240]) ).
fof(f240_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f240_nnf]) ).
cnf(c240,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f240_sk]) ).
cnf(f261,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/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f261_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)],[f261]) ).
fof(f261_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)],[f261_nnf]) ).
cnf(c261,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)],[f261_sk]) ).
cnf(f284,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_length__greater__0__conv_0) ).
fof(f284_nnf,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f284]) ).
fof(f284_sk,plain,
! [T_a] : ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f284_nnf]) ).
cnf(c284,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(X0),tc_List_Olist(X0)),tc_nat),
inference(cnf_transformation,[status(esa)],[f284_sk]) ).
cnf(f304,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f304_nnf,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(nnf_transformation,[status(thm)],[f304]) ).
fof(f304_sk,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(skolemisation,[status(esa)],[f304_nnf]) ).
cnf(c304,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
cnf(f307,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f307_nnf,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f307]) ).
fof(f307_sk,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f307_nnf]) ).
cnf(c307,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f307_sk]) ).
cnf(f308,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f308_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)],[f308]) ).
fof(f308_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f308_nnf]) ).
cnf(c308,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(f336,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(f336_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)],[f336]) ).
fof(f336_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)],[f336_nnf]) ).
cnf(c336,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)],[f336_sk]) ).
cnf(f339,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(f339_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)],[f339]) ).
fof(f339_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)],[f339_nnf]) ).
cnf(c339,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)],[f339_sk]) ).
cnf(f342,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(f342_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)],[f342]) ).
fof(f342_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)],[f342_nnf]) ).
cnf(c342,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)],[f342_sk]) ).
cnf(f343,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(f343_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)],[f343]) ).
fof(f343_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)],[f343_nnf]) ).
cnf(c343,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)],[f343_sk]) ).
cnf(f354,axiom,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_impossible__Cons_0) ).
fof(f354_nnf,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f354]) ).
fof(f354_sk,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f354_nnf]) ).
cnf(c354,plain,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)),c_Nat_Osize__class_Osize(X1,tc_List_Olist(X2)),tc_nat),
inference(cnf_transformation,[status(esa)],[f354_sk]) ).
cnf(f404,axiom,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).
fof(f404_nnf,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f404]) ).
fof(f404_sk,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f404_nnf]) ).
cnf(c404,plain,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X0),X1,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f404_sk]) ).
cnf(f407,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).
fof(f407_nnf,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f407]) ).
fof(f407_sk,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f407_nnf]) ).
cnf(c407,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X0)),X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f407_sk]) ).
cnf(f454,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f454_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f454]) ).
fof(f454_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f454_nnf]) ).
cnf(c454,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f454_sk]) ).
cnf(f455,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f455_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f455]) ).
fof(f455_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f455_nnf]) ).
cnf(c455,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f455_sk]) ).
cnf(f470,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f470_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f470]) ).
fof(f470_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f470_nnf]) ).
cnf(c470,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f470_sk]) ).
cnf(f471,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f471_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f471]) ).
fof(f471_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f471_nnf]) ).
cnf(c471,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f471_sk]) ).
cnf(f487,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f487_nnf,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c487,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
cnf(f529,axiom,
c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f529_nnf,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(nnf_transformation,[status(thm)],[f529]) ).
fof(f529_sk,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(skolemisation,[status(esa)],[f529_nnf]) ).
cnf(c529,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f529_sk]) ).
cnf(f539,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f539_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f539]) ).
fof(f539_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f539_nnf]) ).
cnf(c539,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f539_sk]) ).
cnf(f542,axiom,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f542_nnf,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(nnf_transformation,[status(thm)],[f542]) ).
fof(f542_sk,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(skolemisation,[status(esa)],[f542_nnf]) ).
cnf(c542,plain,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X0)),X1)),
inference(cnf_transformation,[status(esa)],[f542_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c10,c11,c14,c49,c50,c106,c107,c108,c109,c110,c114,c139,c140,c156,c162,c168,c178,c179,c194,c195,c203,c205,c207,c209,c220,c240,c261,c284,c304,c307,c308,c336,c339,c342,c343,c354,c404,c407,c454,c455,c470,c471,c487,c529,c539,c542,c628]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t681]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL814-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n016.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 00:37:01 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 29.22/9.08 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.22/9.08 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------