%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL789-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 : n017.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:02 PM UTC 2026
% Result : Unsatisfiable 8.53s 1.65s
% Output : Proof 8.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 24
% Syntax : Number of formulae : 108 ( 108 unt; 0 def)
% Number of atoms : 108 ( 85 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 81 ( 81 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-5 aty)
% Number of variables : 254 ( 94 sgn 118 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f281,axiom,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_varT_0) ).
fof(f281_nnf,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(nnf_transformation,[status(thm)],[f281]) ).
cnf(c281,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(cnf_transformation,[status(esa)],[f281_nnf]) ).
cnf(t127,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) = true,
inference(equality_encoding,[status(esa)],[c281]) ).
cnf(f273,axiom,
c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldr_Osimps_I2_J_0) ).
fof(f273_nnf,plain,
! [V_f,V_x,V_xs,T_b,V_a,T_a] : c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [V_f,V_x,V_xs,T_b,V_a,T_a] : c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
c_List_Ofoldr(X0,c_List_Olist_OCons(X1,X2,X3),X4,X3,X5) = hAPP(hAPP(X0,X1),c_List_Ofoldr(X0,X2,X4,X3,X5)),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(t128,plain,
hAPP(hAPP(X1,X2),c_List_Ofoldr(X1,X3,X4,X5,X6)) = c_List_Ofoldr(X1,c_List_Olist_OCons(X2,X3,X5),X4,X5,X6),
inference(equality_encoding,[status(esa)],[c273]) ).
cnf(t255,plain,
c_List_Ofoldr(X1,c_List_Olist_OCons(X2,X3,X4),X5,X4,X6) = hAPP(hAPP(X1,X2),c_List_Ofoldr(X1,X3,X5,X4,X6)),
inference(orient,[status(thm)],[t128]) ).
cnf(t654,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,v_Ts____,tc_Type_Otype),v_T_H____,tc_Type_Otype,tc_Type_Otype)) = true,
inference(step,[status(thm)],[t127,t255]) ).
cnf(f287,axiom,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_T_0) ).
fof(f287_nnf,plain,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
inference(nnf_transformation,[status(thm)],[f287]) ).
cnf(c287,plain,
v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)),
inference(cnf_transformation,[status(esa)],[f287_nnf]) ).
cnf(t59,plain,
hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) = v_T____,
inference(equality_encoding,[status(esa)],[c287]) ).
cnf(t651,plain,
c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,v_Ts____,tc_Type_Otype),v_T_H____,tc_Type_Otype,tc_Type_Otype) = v_T____,
inference(step,[status(thm)],[t59,t255]) ).
cnf(t333,plain,
c_List_Ofoldr(c_Type_Otype_OFun,c_List_Olist_OCons(v_T_H_H____,v_Ts____,tc_Type_Otype),v_T_H____,tc_Type_Otype,tc_Type_Otype) = v_T____,
inference(orient,[status(thm)],[t651]) ).
cnf(t655,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_T____) = true,
inference(step,[status(thm)],[t654,t333]) ).
cnf(t625,plain,
c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_T____) = true,
inference(orient,[status(thm)],[t655]) ).
cnf(f268,axiom,
c_Type_Otyping(v_e____,v_u____,v_T____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_uT_0) ).
fof(f268_nnf,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(nnf_transformation,[status(thm)],[f268]) ).
cnf(c268,plain,
c_Type_Otyping(v_e____,v_u____,v_T____),
inference(cnf_transformation,[status(esa)],[f268_nnf]) ).
cnf(t12,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(equality_encoding,[status(esa)],[c268]) ).
cnf(t638,plain,
c_Type_Otyping(v_e____,v_u____,v_T____) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t24,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t190,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t24]) ).
cnf(f35,axiom,
~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f35_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)],[f35]) ).
fof(f35_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)],[f35_nnf]) ).
cnf(c35,plain,
~ c_ListOrder_Ostep1(X0,c_List_Olist_ONil(X1),X2,X1),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f36,axiom,
~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f36_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)],[f36]) ).
fof(f36_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)],[f36_nnf]) ).
cnf(c36,plain,
~ c_ListOrder_Ostep1(X0,X1,c_List_Olist_ONil(X2),X2),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f186,axiom,
hAPP(hAPP(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(f186_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)],[f186]) ).
fof(f186_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)],[f186_nnf]) ).
cnf(c186,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(f190,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/sandbox2/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).
fof(f190_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)],[f190]) ).
fof(f190_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)],[f190_nnf]) ).
cnf(c190,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)],[f190_sk]) ).
cnf(f194,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f194_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)],[f194]) ).
fof(f194_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c194,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
cnf(f195,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f195_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)],[f195]) ).
fof(f195_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(f202,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f202_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)],[f202]) ).
fof(f202_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)],[f202_nnf]) ).
cnf(c202,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
cnf(f203,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f203_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)],[f203]) ).
fof(f203_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)],[f203_nnf]) ).
cnf(c203,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(f223,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(f223_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)],[f223]) ).
fof(f223_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f227,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/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).
fof(f227_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)],[f227]) ).
fof(f227_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)],[f227_nnf]) ).
cnf(c227,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)],[f227_sk]) ).
cnf(f233,axiom,
c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f233_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)],[f233]) ).
fof(f233_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)],[f233_nnf]) ).
cnf(c233,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f243,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f243_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)],[f243]) ).
fof(f243_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)],[f243_nnf]) ).
cnf(c243,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f243_sk]) ).
cnf(f244,axiom,
~ hBOOL(hAPP(hAPP(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(f244_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)],[f244]) ).
fof(f244_sk,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(skolemisation,[status(esa)],[f244_nnf]) ).
cnf(c244,plain,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X0)),X1)),
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(f255,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f255_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)],[f255]) ).
fof(f255_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)],[f255_nnf]) ).
cnf(c255,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f255_sk]) ).
cnf(f258,axiom,
hAPP(hAPP(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(f258_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)],[f258]) ).
fof(f258_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)],[f258_nnf]) ).
cnf(c258,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f259,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(f259_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)],[f259]) ).
fof(f259_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f259_nnf]) ).
cnf(c259,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f259_sk]) ).
cnf(f267,axiom,
hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I4_J_0) ).
fof(f267_nnf,plain,
! [V_type1_H,V_type2_H,V_nat] : hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
inference(nnf_transformation,[status(thm)],[f267]) ).
fof(f267_sk,plain,
! [V_type1_H,V_type2_H,V_nat] : hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c267,plain,
hAPP(hAPP(c_Type_Otype_OFun,X0),X1) != c_Type_Otype_OAtom(X2),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f293,axiom,
c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I3_J_0) ).
fof(f293_nnf,plain,
! [V_nat,V_type1_H,V_type2_H] : c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
! [V_nat,V_type1_H,V_type2_H] : c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H),
inference(skolemisation,[status(esa)],[f293_nnf]) ).
cnf(c293,plain,
c_Type_Otype_OAtom(X0) != hAPP(hAPP(c_Type_Otype_OFun,X1),X2),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f299,negated_conjecture,
~ c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f299_nnf,plain,
~ c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(nnf_transformation,[status(thm)],[f299]) ).
fof(f299_sk,plain,
~ c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(skolemisation,[status(esa)],[f299_nnf]) ).
cnf(c299,plain,
~ c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
inference(cnf_transformation,[status(esa)],[f299_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c35,c36,c186,c190,c194,c195,c202,c203,c223,c227,c233,c243,c244,c255,c258,c259,c267,c293,c299]) ).
cnf(g0_0,plain,
true != ifeq(c_Type_Otyping(v_e____,v_u____,v_T____),true,false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(c_Type_Otyping(v_e____,v_u____,v_T____),true,false,c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_T____)),
inference(rw,[status(thm)],[g0_0,t625]) ).
cnf(g0_2,plain,
true != ifeq(c_Type_Otyping(v_e____,v_u____,v_T____),c_Type_Otyping(v_e____,v_u____,v_T____),false,c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_T____)),
inference(rw,[status(thm)],[g0_1,t638]) ).
cnf(g0_3,plain,
true != false,
inference(rw,[status(thm)],[g0_2,t190]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL789-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 00:25:31 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.53/1.65 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.53/1.65 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------