CSE_E---1.7.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : LCL858-1 : TPTP v9.2.1. Released v4.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n023.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 04:45:16 PM UTC 2026

% Result   : Unsatisfiable 0.36s 1.62s
% Output   : CNFRefutation 0.36s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_205)

% Comments : 
%------------------------------------------------------------------------------
cnf(cls_apps__preserves__beta2_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__preserves__beta2_0) ).

cnf(cls_reflcl__tranclp_0,axiom,
    c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))) = c_Transitive__Closure_Ortranclp(X1,X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_reflcl__tranclp_0) ).

cnf(cls_rtranclp__converseD_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X4),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__converseD_0) ).

cnf(cls_rtranclp__trans_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__trans_0) ).

cnf(cls_rtrancl__beta__App_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtrancl__beta__App_0) ).

cnf(cls_rtranclp__converseI_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X4),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__converseI_0) ).

cnf(cls_rtranclp__sup__rtranclp_0,axiom,
    c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Ortranclp(X1,X2),c_Transitive__Closure_Ortranclp(X3,X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2) = c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_fun(X2,tc_bool))),X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__sup__rtranclp_0) ).

cnf(cls_subst__preserves__beta2_H_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__preserves__beta2_H_0) ).

cnf(cls_subst__preserves__beta_H_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X4,X2,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__preserves__beta_H_0) ).

cnf(cls_converse__rtranclp__into__rtranclp_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_converse__rtranclp__into__rtranclp_0) ).

cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp_Ortrancl__into__rtrancl_0) ).

cnf(cls_rtrancl__beta__AppR_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtrancl__beta__AppR_0) ).

cnf(cls_rtrancl__beta__AppL_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtrancl__beta__AppL_0) ).

cnf(cls_lift__preserves__beta_H_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Olift(X1,X2)),c_Lambda_Olift(X3,X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift__preserves__beta_H_0) ).

cnf(cls_rtrancl__beta__Abs_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_OdB_OAbs(X1)),c_Lambda_OdB_OAbs(X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtrancl__beta__Abs_0) ).

cnf(cls_tranclp__rtranclp__tranclp_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__rtranclp__tranclp_0) ).

cnf(cls_rtranclp__tranclp__tranclp_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__tranclp__tranclp_0) ).

cnf(cls_rtranclp__into__tranclp2_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__into__tranclp2_0) ).

cnf(cls_rtranclp__into__tranclp1_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__into__tranclp1_0) ).

cnf(cls_accp__downwards_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__downwards_0) ).

cnf(cls_accp__downwards__aux_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__downwards__aux_0) ).

cnf(cls_rtranclpD_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclpD_0) ).

cnf(cls_Nitpick_Ortranclp__def_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nitpick_Ortranclp__def_0) ).

cnf(cls_subject__reduction_H_0,axiom,
    ( c_Type_Otyping(X1,X2,X3)
    | ~ c_Type_Otyping(X1,X4,X3)
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X4),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subject__reduction_H_0) ).

cnf(cls_subst__preserves__beta2_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X2),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__preserves__beta2_0) ).

cnf(cls_Nitpick_Ortranclp__def_2,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nitpick_Ortranclp__def_2) ).

cnf(cls_r__into__rtranclp_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_r__into__rtranclp_0) ).

cnf(cls_Nitpick_Ortranclp__def_1,axiom,
    hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X3)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nitpick_Ortranclp__def_1) ).

cnf(cls_rtranclp_Ortrancl__refl_0,axiom,
    hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X3)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp_Ortrancl__refl_0) ).

cnf(cls_rtranclp__idemp_0,axiom,
    c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(X1,X2),X2) = c_Transitive__Closure_Ortranclp(X1,X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__idemp_0) ).

cnf(cls_rtranclp__reflcl_0,axiom,
    c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2) = c_Transitive__Closure_Ortranclp(X1,X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rtranclp__reflcl_0) ).

cnf(cls_head__Var__reduction_1,axiom,
    ( X1 = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(X2,X3,X1),tc_Lambda_OdB,tc_Lambda_OdB)
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_head__Var__reduction_1) ).

cnf(cls_head__Var__reduction_0,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),X1),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(X2,X1,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X1,tc_Lambda_OdB,tc_Lambda_OdB)),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_head__Var__reduction_0) ).

cnf(cls_double__induction__lemma_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_double__induction__lemma_0) ).

cnf(cls_apps__preserves__betas_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__preserves__betas_0) ).

cnf(cls_apps__preserves__beta_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__preserves__beta_0) ).

cnf(cls_Beta_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X2))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Beta_0) ).

cnf(cls_pred__comp_Ointros_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Opred__comp(X1,X2,X3,X4,X5),X6),X7))
    | ~ hBOOL(hAPP(hAPP(X2,X8),X7))
    | ~ hBOOL(hAPP(hAPP(X1,X6),X8)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_pred__comp_Ointros_0) ).

cnf(cls_var__app__type__eq_0,axiom,
    ( X1 = X2
    | ~ c_Type_Otyping(X3,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X4),X5,tc_Lambda_OdB,tc_Lambda_OdB),X2)
    | ~ c_Type_Otyping(X3,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X4),X5,tc_Lambda_OdB,tc_Lambda_OdB),X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_var__app__type__eq_0) ).

cnf(cls_IT_OVar_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ c_List_Olistsp(c_InductTermi_OIT,X2,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_IT_OVar_0) ).

cnf(cls_converse__pred__comp_0,axiom,
    c_Predicate_Oconversep(c_Predicate_Opred__comp(X1,X2,X3,X4,X5),X3,X5) = c_Predicate_Opred__comp(c_Predicate_Oconversep(X2,X4,X5),c_Predicate_Oconversep(X1,X3,X4),X5,X4,X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_converse__pred__comp_0) ).

cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__apps__eq__Abs__apps__conv_0) ).

cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__eq__Var__apps__conv_0) ).

cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom,
    ( X2 = X4
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__apps__eq__Abs__apps__conv_1) ).

cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom,
    ( X2 = X4
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__eq__Var__apps__conv_1) ).

cnf(cls_Var__apps__neq__Abs__apps_0,axiom,
    c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).

cnf(cls_apps__eq__tail__conv_0,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__eq__tail__conv_0) ).

cnf(cls_App__eq__foldl__conv_2,axiom,
    ( X1 = c_List_Ofoldl(c_Lambda_OdB_OApp,X3,c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(X1,X2,X3,X4),tc_Lambda_OdB,tc_Lambda_OdB)
    | X4 = c_List_Olist_ONil(tc_Lambda_OdB)
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_App__eq__foldl__conv_2) ).

cnf(cls_foldl__Cons_0,axiom,
    c_List_Ofoldl(X1,X2,c_List_Olist_OCons(X3,X4,X5),X6,X5) = c_List_Ofoldl(X1,hAPP(hAPP(X1,X2),X3),X4,X6,X5),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldl__Cons_0) ).

cnf(cls_tranclp__converseD_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__converseD_0) ).

cnf(cls_tranclp__converseI_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__converseI_0) ).

cnf(cls_App__eq__foldl__conv_0,axiom,
    ( hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) = X3
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_App__eq__foldl__conv_0) ).

cnf(cls_Abs__App__neq__Var__apps_0,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).

cnf(cls_Abs__eq__apps__conv_0,axiom,
    ( c_Lambda_OdB_OAbs(X1) = X2
    | c_Lambda_OdB_OAbs(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__eq__apps__conv_0) ).

cnf(cls_Var__eq__apps__conv_0,axiom,
    ( c_Lambda_OdB_OVar(X1) = X2
    | c_Lambda_OdB_OVar(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__eq__apps__conv_0) ).

cnf(cls_apps__eq__Abs__conv_0,axiom,
    ( X1 = c_Lambda_OdB_OAbs(X3)
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__eq__Abs__conv_0) ).

cnf(cls_apps__eq__Abs__conv_1,axiom,
    ( X2 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__eq__Abs__conv_1) ).

cnf(cls_Abs__eq__apps__conv_1,axiom,
    ( X3 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_Lambda_OdB_OAbs(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__eq__apps__conv_1) ).

cnf(cls_Var__eq__apps__conv_1,axiom,
    ( X3 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_Lambda_OdB_OVar(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__eq__apps__conv_1) ).

cnf(cls_sup2E_0,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X4,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X4,X1,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup2E_0) ).

cnf(cls_inf2E_0,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,X4,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf2E_0) ).

cnf(cls_inf2E_1,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X4,X1,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf2E_1) ).

cnf(cls_Cons__step1__Cons_1,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),X4))
    | hBOOL(hAPP(hAPP(X1,X5),X6))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X5,X3,X2)),c_List_Olist_OCons(X6,X4,X2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_1) ).

cnf(cls_Cons__step1__Cons_3,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),X4))
    | X4 = X3
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X5,X3,X2)),c_List_Olist_OCons(X6,X4,X2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_3) ).

cnf(cls_Cons__step1__Cons_0,axiom,
    ( X1 = X2
    | hBOOL(hAPP(hAPP(X3,X2),X1))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X3,X4),c_List_Olist_OCons(X2,X5,X4)),c_List_Olist_OCons(X1,X6,X4))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_0) ).

cnf(cls_inf2I_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X2,X5),X6))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X6)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf2I_0) ).

cnf(cls_App__eq__foldl__conv_4,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_App__eq__foldl__conv_4) ).

cnf(cls_Cons__step1__Cons_2,axiom,
    ( X1 = X2
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X5,X6),c_List_Olist_OCons(X2,X4,X6)),c_List_Olist_OCons(X1,X3,X6))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_2) ).

cnf(cls_subst__type__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(X1,X2,X3)))
    | ~ c_Type_Otyping(X4,X2,X5)
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X2))
    | ~ c_Type_Otyping(c_Type_Oshift(X4,X3,X5,tc_Type_Otype),X1,X6)
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__type__IT_0) ).

cnf(cls_sup2CI_1,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X6)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup2CI_1) ).

cnf(cls_sup2CI_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X2,X5),X6)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup2CI_0) ).

cnf(cls_apps__eq__Abs__conv_2,axiom,
    c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) = c_Lambda_OdB_OAbs(X1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_apps__eq__Abs__conv_2) ).

cnf(cls_Abs__eq__apps__conv_2,axiom,
    c_Lambda_OdB_OAbs(X1) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__eq__apps__conv_2) ).

cnf(cls_Var__eq__apps__conv_2,axiom,
    c_Lambda_OdB_OVar(X1) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__eq__apps__conv_2) ).

cnf(cls_foldl__Nil_0,axiom,
    c_List_Ofoldl(X1,X2,c_List_Olist_ONil(X3),X4,X3) = X2,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldl__Nil_0) ).

cnf(cls_Cons__step1__Cons_5,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X3,X4,X2)),c_List_Olist_OCons(X3,X5,X2)))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X4),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_5) ).

cnf(cls_subst__lemma_0,axiom,
    ( c_Type_Otyping(X1,c_Lambda_Osubst(X5,X2,X4),X6)
    | ~ c_Type_Otyping(X1,X2,X3)
    | ~ c_Type_Otyping(c_Type_Oshift(X1,X4,X3,tc_Type_Otype),X5,X6) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__lemma_0) ).

cnf(cls_Cons__step1__Cons_4,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X4),c_List_Olist_OCons(X2,X5,X4)),c_List_Olist_OCons(X3,X5,X4)))
    | ~ hBOOL(hAPP(hAPP(X1,X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__step1__Cons_4) ).

cnf(cls_Abs_0,axiom,
    ( c_Type_Otyping(X1,c_Lambda_OdB_OAbs(X2),c_Type_Otype_OFun(X3,X4))
    | ~ c_Type_Otyping(c_Type_Oshift(X1,c_HOL_Ozero__class_Ozero(tc_nat),X3,tc_Type_Otype),X2,X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs_0) ).

cnf(cls_Cons__acc__step1I_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),c_List_Olist_OCons(X3,X4,X2)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Cons__acc__step1I_0) ).

cnf(cls_conversepD_0,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X4,X5),X3),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversepD_0) ).

cnf(cls_conversep_Ocases_0,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X4,X5),X3),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversep_Ocases_0) ).

cnf(cls_subst__preserves__beta_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X4,X2,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__preserves__beta_0) ).

cnf(cls_tranclp__trans_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__trans_0) ).

cnf(cls_termi__implies__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,X1))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_termi__implies__IT_0) ).

cnf(cls_conjecture_0,negated_conjecture,
    ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),v_t)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).

cnf(cls_beta_0,axiom,
    hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2)),c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta_0) ).

cnf(cls_lift__type_0,axiom,
    ( c_Type_Otyping(c_Type_Oshift(X1,X2,X3,tc_Type_Otype),c_Lambda_Olift(X4,X2),X5)
    | ~ c_Type_Otyping(X1,X4,X5) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift__type_0) ).

cnf(cls_accp__induct__rule_1,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X4,X5)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,X5),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct__rule_1) ).

cnf(cls_accp__induct_1,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X4,X5)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,X5),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct_1) ).

cnf(cls_converse__join_0,axiom,
    c_Predicate_Oconversep(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(c_Predicate_Oconversep(X1,X3,X4),c_Predicate_Oconversep(X2,X3,X4),tc_fun(X4,tc_fun(X3,tc_bool))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_converse__join_0) ).

cnf(cls_converse__meet_0,axiom,
    c_Predicate_Oconversep(c_Lattices_Olower__semilattice__class_Oinf(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X3,X4) = c_Lattices_Olower__semilattice__class_Oinf(c_Predicate_Oconversep(X1,X3,X4),c_Predicate_Oconversep(X2,X3,X4),tc_fun(X4,tc_fun(X3,tc_bool))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_converse__meet_0) ).

cnf(cls_conversep__iff_1,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X2,X3),X4),X5))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversep__iff_1) ).

cnf(cls_conversep_Ointros_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X2,X3),X4),X5))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversep_Ointros_0) ).

cnf(cls_appR_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X2),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_appR_0) ).

cnf(cls_appL_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_appL_0) ).

cnf(cls_tranclp__into__tranclp2_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__into__tranclp2_0) ).

cnf(cls_tranclp_Otrancl__into__trancl_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp_Otrancl__into__trancl_0) ).

cnf(cls_accpI_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__XaccpI__1__1(X1,X3,X2)),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accpI_0) ).

cnf(cls_accp_OaccI_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__Xintros__1__1(X1,X3,X2)),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_OaccI_0) ).

cnf(cls_not__accp__down_0,axiom,
    ( hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xnot__accp__down__1__1(X1,X2,X3)),X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X3),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__accp__down_0) ).

cnf(cls_accpI_1,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__XaccpI__1__1(X1,X3,X2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accpI_1) ).

cnf(cls_accp_OaccI_1,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__Xaccp__Xintros__1__1(X1,X3,X2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_OaccI_1) ).

cnf(cls_not__accp__down_1,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__Xnot__accp__down__1__1(X1,X3,X2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__accp__down_1) ).

cnf(cls_accp__induct__rule_2,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct__rule_2) ).

cnf(cls_accp__induct_2,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct_2) ).

cnf(cls_IT__implies__termi_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X1))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_IT__implies__termi_0) ).

cnf(cls_shift__eq_0,axiom,
    hAPP(c_Type_Oshift(X1,X2,X3,X4),X2) = X3,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_shift__eq_0) ).

cnf(cls_subst__App_0,axiom,
    c_Lambda_Osubst(hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),X3,X4) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X3,X4)),c_Lambda_Osubst(X2,X3,X4)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__App_0) ).

cnf(cls_accp__induct__rule_0,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct__rule_0) ).

cnf(cls_accp__induct_0,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__induct_0) ).

cnf(cls_accp_Oinduct_0,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X4))
    | ~ hBOOL(hAPP(hAPP(X3,X4),v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinduct_0) ).

cnf(cls_accp_Oinducts_0,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X4))
    | ~ hBOOL(hAPP(hAPP(X3,X4),v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinducts_0) ).

cnf(cls_sup__inf__distrib2_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__inf__distrib2_0) ).

cnf(cls_inf__sup__distrib2_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__distrib2_0) ).

cnf(cls_sup__inf__distrib1_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__inf__distrib1_0) ).

cnf(cls_inf__sup__distrib1_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__distrib1_0) ).

cnf(cls_lists__accI_0,axiom,
    ( c_List_Olistsp(c_Wellfounded_Oaccp(X1,X2),X3,X2)
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lists__accI_0) ).

cnf(cls_accp_Oinduct_1,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinduct_1) ).

cnf(cls_accp_Oinducts_1,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinducts_1) ).

cnf(cls_lift__preserves__beta_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(X1,X2)),c_Lambda_Olift(X3,X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift__preserves__beta_0) ).

cnf(cls_accp_Ocases_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Ocases_0) ).

cnf(cls_accp__downward_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__downward_0) ).

cnf(cls_App_0,axiom,
    ( c_Type_Otyping(X1,hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),X4)
    | ~ c_Type_Otyping(X1,X3,X5)
    | ~ c_Type_Otyping(X1,X2,c_Type_Otype_OFun(X5,X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_App_0) ).

cnf(cls_lists__accD_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X3))
    | ~ c_List_Olistsp(c_Wellfounded_Oaccp(X1,X2),X3,X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lists__accD_0) ).

cnf(cls_not__Nil__step1_0,axiom,
    ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_ONil(X2)),X3)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).

cnf(cls_sup__assoc_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__assoc_0) ).

cnf(cls_inf__sup__aci_I6_J_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I6_J_0) ).

cnf(cls_inf__assoc_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__assoc_0) ).

cnf(cls_inf__sup__aci_I2_J_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I2_J_0) ).

cnf(cls_sup__left__commute_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__left__commute_0) ).

cnf(cls_inf__sup__aci_I7_J_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I7_J_0) ).

cnf(cls_inf__left__commute_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__left__commute_0) ).

cnf(cls_inf__sup__aci_I3_J_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I3_J_0) ).

cnf(cls_tranclp_Or__into__trancl_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp_Or__into__trancl_0) ).

cnf(cls_not__step1__Nil_0,axiom,
    ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),c_List_Olist_ONil(X2))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).

cnf(cls_subst__Var__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(X1,c_Lambda_OdB_OVar(X2),X3)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__Var__IT_0) ).

cnf(cls_accp_Oinduct_2,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinduct_2) ).

cnf(cls_accp_Oinducts_2,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp_Oinducts_2) ).

cnf(cls_subject__reduction_0,axiom,
    ( c_Type_Otyping(X1,X2,X3)
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X4),X2))
    | ~ c_Type_Otyping(X1,X4,X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subject__reduction_0) ).

cnf(cls_app__Var__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,X1),c_Lambda_OdB_OVar(X2))))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_app__Var__IT_0) ).

cnf(cls_abs_0,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(X1)),c_Lambda_OdB_OAbs(X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_abs_0) ).

cnf(cls_sup__left__idem_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__left__idem_0) ).

cnf(cls_inf__sup__aci_I8_J_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I8_J_0) ).

cnf(cls_inf__left__idem_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__left__idem_0) ).

cnf(cls_inf__sup__aci_I4_J_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I4_J_0) ).

cnf(cls_tranclp__converse_0,axiom,
    c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2) = c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_tranclp__converse_0) ).

cnf(cls_lift_Osimps_I2_J_0,axiom,
    c_Lambda_Olift(hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),X3) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Olift(X1,X3)),c_Lambda_Olift(X2,X3)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift_Osimps_I2_J_0) ).

cnf(cls_list_Oinject_0,axiom,
    ( X1 = X4
    | c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_OCons(X4,X5,X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Oinject_0) ).

cnf(cls_list_Oinject_1,axiom,
    ( X2 = X5
    | c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_OCons(X4,X5,X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Oinject_1) ).

cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom,
    ( X1 = X2
    | ~ hBOOL(hAPP(hAPP(c_fequal(X3),X1),X2)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_Ofequal__imp__equal_0) ).

cnf(cls_sup__inf__absorb_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = X2
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__inf__absorb_0) ).

cnf(cls_inf__sup__absorb_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = X2
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__absorb_0) ).

cnf(cls_conversep__conversep_0,axiom,
    c_Predicate_Oconversep(c_Predicate_Oconversep(X1,X2,X3),X3,X2) = X1,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversep__conversep_0) ).

cnf(cls_beta__cases_I1_J_0,axiom,
    ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X1)),X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).

cnf(cls_lift__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(X1,X2)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_lift__IT_0) ).

cnf(cls_dB_Osimps_I2_J_0,axiom,
    ( X1 = X3
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I2_J_0) ).

cnf(cls_dB_Osimps_I2_J_1,axiom,
    ( X2 = X4
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I2_J_1) ).

cnf(cls_sup__commute_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__commute_0) ).

cnf(cls_inf__sup__aci_I5_J_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I5_J_0) ).

cnf(cls_inf__commute_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__commute_0) ).

cnf(cls_inf__sup__aci_I1_J_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X1)
    | ~ class_Lattices_Olattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__sup__aci_I1_J_0) ).

cnf(cls_type__implies__IT_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,X1))
    | ~ c_Type_Otyping(X2,X1,X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type__implies__IT_0) ).

cnf(cls_typing__elims_I1_J_0,axiom,
    ( hAPP(X1,X2) = X3
    | ~ c_Type_Otyping(X1,c_Lambda_OdB_OVar(X2),X3) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_typing__elims_I1_J_0) ).

cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom,
    hBOOL(hAPP(hAPP(c_fequal(X1),X2),X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_Oequal__imp__fequal_0) ).

cnf(cls_accp__wfPD_0,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ c_Wellfounded_OwfP(X1,X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_accp__wfPD_0) ).

cnf(cls_list_Osimps_I3_J_0,axiom,
    c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_ONil(X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).

cnf(cls_neq__Nil__conv_1,axiom,
    c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_ONil(X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).

cnf(cls_list_Osimps_I2_J_0,axiom,
    c_List_Olist_ONil(X1) != c_List_Olist_OCons(X2,X3,X1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).

cnf(cls_not__Cons__self2_0,axiom,
    c_List_Olist_OCons(X1,X2,X3) != X2,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).

cnf(cls_not__Cons__self_0,axiom,
    X1 != c_List_Olist_OCons(X2,X1,X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).

cnf(cls_typing_OVar_0,axiom,
    c_Type_Otyping(X1,c_Lambda_OdB_OVar(X2),hAPP(X1,X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_typing_OVar_0) ).

cnf(cls_Lambda_0,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(X1)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Lambda_0) ).

cnf(cls_subst__lift_0,axiom,
    c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__lift_0) ).

cnf(cls_conversep__eq_0,axiom,
    c_Predicate_Oconversep(c_fequal(X1),X1,X1) = c_fequal(X1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conversep__eq_0) ).

cnf(cls_dB_Osimps_I8_J_0,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_Lambda_OdB_OAbs(X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).

cnf(cls_dB_Osimps_I5_J_0,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_Lambda_OdB_OVar(X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).

cnf(cls_dB_Osimps_I9_J_0,axiom,
    c_Lambda_OdB_OAbs(X1) != hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).

cnf(cls_dB_Osimps_I4_J_0,axiom,
    c_Lambda_OdB_OVar(X1) != hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).

cnf(cls_wfP__trancl_0,axiom,
    ( c_Wellfounded_OwfP(c_Transitive__Closure_Otranclp(X1,X2),X2)
    | ~ c_Wellfounded_OwfP(X1,X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wfP__trancl_0) ).

cnf(cls_sup__idem_0,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X2,X1) = X2
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__idem_0) ).

cnf(cls_inf__idem_0,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X2,X1) = X2
    | ~ class_Lattices_Olower__semilattice(X1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__idem_0) ).

cnf(cls_subst__eq_0,axiom,
    c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__eq_0) ).

cnf(cls_listsp_ONil_0,axiom,
    c_List_Olistsp(X1,c_List_Olist_ONil(X2),X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_listsp_ONil_0) ).

cnf(cls_type_Osimps_I2_J_0,axiom,
    ( X1 = X3
    | c_Type_Otype_OFun(X1,X2) != c_Type_Otype_OFun(X3,X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I2_J_0) ).

cnf(cls_type_Osimps_I2_J_1,axiom,
    ( X2 = X4
    | c_Type_Otype_OFun(X1,X2) != c_Type_Otype_OFun(X3,X4) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_type_Osimps_I2_J_1) ).

cnf(cls_Var__IT_0,axiom,
    hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(X1))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__IT_0) ).

cnf(clsarity_fun__Lattices_Odistrib__lattice,axiom,
    ( class_Lattices_Odistrib__lattice(tc_fun(X1,X2))
    | ~ class_Lattices_Odistrib__lattice(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_fun__Lattices_Odistrib__lattice) ).

cnf(clsarity_fun__Lattices_Olower__semilattice,axiom,
    ( class_Lattices_Olower__semilattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_fun__Lattices_Olower__semilattice) ).

cnf(clsarity_fun__Lattices_Oupper__semilattice,axiom,
    ( class_Lattices_Oupper__semilattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_fun__Lattices_Oupper__semilattice) ).

cnf(clsarity_fun__Lattices_Olattice,axiom,
    ( class_Lattices_Olattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_fun__Lattices_Olattice) ).

cnf(cls_CHAINED_0,axiom,
    hBOOL(hAPP(c_InductTermi_OIT,v_t)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).

cnf(cls_dB_Osimps_I3_J_0,axiom,
    ( X1 = X2
    | c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OAbs(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I3_J_0) ).

cnf(cls_dB_Osimps_I1_J_0,axiom,
    ( X1 = X2
    | c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OVar(X2) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I1_J_0) ).

cnf(cls_dB_Osimps_I7_J_0,axiom,
    c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OVar(X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).

cnf(cls_dB_Osimps_I6_J_0,axiom,
    c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OAbs(X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).

cnf(clsarity_bool__Lattices_Odistrib__lattice,axiom,
    class_Lattices_Odistrib__lattice(tc_bool),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Odistrib__lattice) ).

cnf(clsarity_nat__Lattices_Odistrib__lattice,axiom,
    class_Lattices_Odistrib__lattice(tc_nat),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Lattices_Odistrib__lattice) ).

cnf(clsarity_bool__Lattices_Olower__semilattice,axiom,
    class_Lattices_Olower__semilattice(tc_bool),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olower__semilattice) ).

cnf(clsarity_nat__Lattices_Olower__semilattice,axiom,
    class_Lattices_Olower__semilattice(tc_nat),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Lattices_Olower__semilattice) ).

cnf(clsarity_bool__Lattices_Oupper__semilattice,axiom,
    class_Lattices_Oupper__semilattice(tc_bool),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Oupper__semilattice) ).

cnf(clsarity_nat__Lattices_Oupper__semilattice,axiom,
    class_Lattices_Oupper__semilattice(tc_nat),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Lattices_Oupper__semilattice) ).

cnf(clsarity_bool__Lattices_Olattice,axiom,
    class_Lattices_Olattice(tc_bool),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olattice) ).

cnf(clsarity_nat__Lattices_Olattice,axiom,
    class_Lattices_Olattice(tc_nat),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Lattices_Olattice) ).

cnf(i_0_204,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    cls_apps__preserves__beta2_0 ).

cnf(i_0_205,axiom,
    c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))) = c_Transitive__Closure_Ortranclp(X1,X2),
    cls_reflcl__tranclp_0 ).

cnf(i_0_206,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X4),X3)) ),
    cls_rtranclp__converseD_0 ).

cnf(i_0_207,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    cls_rtranclp__trans_0 ).

cnf(i_0_208,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    cls_rtrancl__beta__App_0 ).

cnf(i_0_209,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X4),X3)) ),
    cls_rtranclp__converseI_0 ).

cnf(i_0_210,axiom,
    c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Ortranclp(X1,X2),c_Transitive__Closure_Ortranclp(X3,X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2) = c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_fun(X2,tc_bool))),X2),
    cls_rtranclp__sup__rtranclp_0 ).

cnf(i_0_211,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X4)) ),
    cls_subst__preserves__beta2_H_0 ).

cnf(i_0_212,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X4,X2,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X4)) ),
    cls_subst__preserves__beta_H_0 ).

cnf(i_0_213,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    cls_converse__rtranclp__into__rtranclp_0 ).

cnf(i_0_214,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    cls_rtranclp_Ortrancl__into__rtrancl_0 ).

cnf(i_0_215,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X2),X3)) ),
    cls_rtrancl__beta__AppR_0 ).

cnf(i_0_216,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    cls_rtrancl__beta__AppL_0 ).

cnf(i_0_217,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Olift(X1,X2)),c_Lambda_Olift(X3,X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X3)) ),
    cls_lift__preserves__beta_H_0 ).

cnf(i_0_218,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_OdB_OAbs(X1)),c_Lambda_OdB_OAbs(X2)))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X1),X2)) ),
    cls_rtrancl__beta__Abs_0 ).

cnf(i_0_219,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    cls_tranclp__rtranclp__tranclp_0 ).

cnf(i_0_220,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    cls_rtranclp__tranclp__tranclp_0 ).

cnf(i_0_221,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    cls_rtranclp__into__tranclp2_0 ).

cnf(i_0_222,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X5)) ),
    cls_rtranclp__into__tranclp1_0 ).

cnf(i_0_223,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    cls_accp__downwards_0 ).

cnf(i_0_224,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    cls_accp__downwards__aux_0 ).

cnf(i_0_225,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    cls_rtranclpD_0 ).

cnf(i_0_226,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4)) ),
    cls_Nitpick_Ortranclp__def_0 ).

cnf(i_0_227,axiom,
    ( c_Type_Otyping(X1,X2,X3)
    | ~ c_Type_Otyping(X1,X4,X3)
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),X4),X2)) ),
    cls_subject__reduction_H_0 ).

cnf(i_0_228,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X2),X4)) ),
    cls_subst__preserves__beta2_0 ).

cnf(i_0_229,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4)) ),
    cls_Nitpick_Ortranclp__def_2 ).

cnf(i_0_230,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4)) ),
    cls_r__into__rtranclp_0 ).

cnf(i_0_231,axiom,
    hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X3)),
    cls_Nitpick_Ortranclp__def_1 ).

cnf(i_0_232,axiom,
    hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X3)),
    cls_rtranclp_Ortrancl__refl_0 ).

cnf(i_0_233,axiom,
    c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(X1,X2),X2) = c_Transitive__Closure_Ortranclp(X1,X2),
    cls_rtranclp__idemp_0 ).

cnf(i_0_234,axiom,
    c_Transitive__Closure_Ortranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2) = c_Transitive__Closure_Ortranclp(X1,X2),
    cls_rtranclp__reflcl_0 ).

cnf(i_0_235,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_204,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_236,axiom,
    ( X1 = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(X2,X3,X1),tc_Lambda_OdB,tc_Lambda_OdB)
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X1)) ),
    cls_head__Var__reduction_1,
    [final] ).

cnf(i_0_237,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),X1),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(X2,X1,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X1,tc_Lambda_OdB,tc_Lambda_OdB)),X3)) ),
    cls_head__Var__reduction_0,
    [final] ).

cnf(i_0_238,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X2)) ),
    cls_double__induction__lemma_0,
    [final] ).

cnf(i_0_239,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),X2),X3)) ),
    cls_apps__preserves__betas_0,
    [final] ).

cnf(i_0_240,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    cls_apps__preserves__beta_0,
    [final] ).

cnf(i_0_241,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2),X3,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X2))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB))) ),
    cls_Beta_0,
    [final] ).

cnf(i_0_242,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Opred__comp(X1,X2,X3,X4,X5),X6),X7))
    | ~ hBOOL(hAPP(hAPP(X2,X8),X7))
    | ~ hBOOL(hAPP(hAPP(X1,X6),X8)) ),
    cls_pred__comp_Ointros_0,
    [final] ).

cnf(i_0_243,axiom,
    ( X1 = X2
    | ~ c_Type_Otyping(X3,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X4),X5,tc_Lambda_OdB,tc_Lambda_OdB),X2)
    | ~ c_Type_Otyping(X3,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X4),X5,tc_Lambda_OdB,tc_Lambda_OdB),X1) ),
    cls_var__app__type__eq_0,
    [final] ).

cnf(i_0_244,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X4),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_206,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_245,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X5)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_207,c_0_205]),c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_246,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_208,c_0_205]),c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_247,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X4),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_209,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_248,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB)))
    | ~ c_List_Olistsp(c_InductTermi_OIT,X2,tc_Lambda_OdB) ),
    cls_IT_OVar_0,
    [final] ).

cnf(i_0_249,axiom,
    c_Predicate_Oconversep(c_Predicate_Opred__comp(X1,X2,X3,X4,X5),X3,X5) = c_Predicate_Opred__comp(c_Predicate_Oconversep(X2,X4,X5),c_Predicate_Oconversep(X1,X3,X4),X5,X4,X3),
    cls_converse__pred__comp_0,
    [final] ).

cnf(i_0_250,plain,
    c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X3,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),tc_fun(X2,tc_fun(X2,tc_bool))),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_fun(X2,tc_bool))),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_210,c_0_205]),c_0_205]),c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_251,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Abs__apps__eq__Abs__apps__conv_0,
    [final] ).

cnf(i_0_252,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Var__apps__eq__Var__apps__conv_0,
    [final] ).

cnf(i_0_253,axiom,
    ( X2 = X4
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Abs__apps__eq__Abs__apps__conv_1,
    [final] ).

cnf(i_0_254,axiom,
    ( X2 = X4
    | c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Var__apps__eq__Var__apps__conv_1,
    [final] ).

cnf(i_0_255,axiom,
    c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB),
    cls_Var__apps__neq__Abs__apps_0,
    [final] ).

cnf(i_0_256,axiom,
    ( X1 = X3
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X2,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_apps__eq__tail__conv_0,
    [final] ).

cnf(i_0_257,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X2),X4)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_211,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_258,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X4,X2,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X4)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_212,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_259,axiom,
    ( X1 = c_List_Ofoldl(c_Lambda_OdB_OApp,X3,c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(X1,X2,X3,X4),tc_Lambda_OdB,tc_Lambda_OdB)
    | X4 = c_List_Olist_ONil(tc_Lambda_OdB)
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X4,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_App__eq__foldl__conv_2,
    [final] ).

cnf(i_0_260,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X5),X4)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_213,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_261,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X5)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_214,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_262,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X2),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_215,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_263,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_216,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_264,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_Lambda_Olift(X1,X2)),c_Lambda_Olift(X3,X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X3)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_217,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_265,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_Lambda_OdB_OAbs(X1)),c_Lambda_OdB_OAbs(X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X1),X2)) ),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_218,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_266,axiom,
    c_List_Ofoldl(X1,X2,c_List_Olist_OCons(X3,X4,X5),X6,X5) = c_List_Ofoldl(X1,hAPP(hAPP(X1,X2),X3),X4,X6,X5),
    cls_foldl__Cons_0,
    [final] ).

cnf(i_0_267,plain,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X5),X4)) ),
    inference(rw,[status(thm)],[i_0_219,c_0_205]),
    [final] ).

cnf(i_0_268,plain,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X5)) ),
    inference(rw,[status(thm)],[i_0_220,c_0_205]),
    [final] ).

cnf(i_0_269,plain,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X5),X4)) ),
    inference(rw,[status(thm)],[i_0_221,c_0_205]),
    [final] ).

cnf(i_0_270,plain,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X5)) ),
    inference(rw,[status(thm)],[i_0_222,c_0_205]),
    [final] ).

cnf(i_0_271,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4)) ),
    cls_tranclp__converseD_0,
    [final] ).

cnf(i_0_272,plain,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4)) ),
    inference(rw,[status(thm)],[i_0_223,c_0_205]),
    [final] ).

cnf(i_0_273,plain,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4)) ),
    inference(rw,[status(thm)],[i_0_224,c_0_205]),
    [final] ).

cnf(i_0_274,plain,
    ( X3 = X4
    | hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4)) ),
    inference(rw,[status(thm)],[i_0_225,c_0_205]),
    [final] ).

cnf(i_0_275,plain,
    ( X3 = X4
    | hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4)) ),
    inference(rw,[status(thm)],[i_0_226,c_0_205]),
    [final] ).

cnf(i_0_276,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),X3),X4)) ),
    cls_tranclp__converseI_0,
    [final] ).

cnf(i_0_277,plain,
    ( c_Type_Otyping(X1,X2,X3)
    | ~ c_Type_Otyping(X1,X4,X3)
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),X4),X2)) ),
    inference(rw,[status(thm)],[i_0_227,c_0_205]),
    [final] ).

cnf(i_0_278,axiom,
    ( hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) = X3
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,X3,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_App__eq__foldl__conv_0,
    [final] ).

cnf(i_0_279,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X3),X4,tc_Lambda_OdB,tc_Lambda_OdB),
    cls_Abs__App__neq__Var__apps_0,
    [final] ).

cnf(i_0_280,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_fequal(tc_Lambda_OdB),tc_fun(tc_Lambda_OdB,tc_fun(tc_Lambda_OdB,tc_bool))),c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X1,X4,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X2),X4)) ),
    inference(rw,[status(thm)],[i_0_228,c_0_205]),
    [final] ).

cnf(i_0_281,axiom,
    ( c_Lambda_OdB_OAbs(X1) = X2
    | c_Lambda_OdB_OAbs(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Abs__eq__apps__conv_0,
    [final] ).

cnf(i_0_282,axiom,
    ( c_Lambda_OdB_OVar(X1) = X2
    | c_Lambda_OdB_OVar(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Var__eq__apps__conv_0,
    [final] ).

cnf(i_0_283,axiom,
    ( X1 = c_Lambda_OdB_OAbs(X3)
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(X3) ),
    cls_apps__eq__Abs__conv_0,
    [final] ).

cnf(i_0_284,axiom,
    ( X2 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(X3) ),
    cls_apps__eq__Abs__conv_1,
    [final] ).

cnf(i_0_285,axiom,
    ( X3 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_Lambda_OdB_OAbs(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Abs__eq__apps__conv_1,
    [final] ).

cnf(i_0_286,axiom,
    ( X3 = c_List_Olist_ONil(tc_Lambda_OdB)
    | c_Lambda_OdB_OVar(X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,X2,X3,tc_Lambda_OdB,tc_Lambda_OdB) ),
    cls_Var__eq__apps__conv_1,
    [final] ).

cnf(i_0_287,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X4,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X4,X1,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    cls_sup2E_0,
    [final] ).

cnf(i_0_288,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,X4,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    cls_inf2E_0,
    [final] ).

cnf(i_0_289,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X4,X1,tc_fun(X5,tc_fun(X6,tc_bool))),X2),X3)) ),
    cls_inf2E_1,
    [final] ).

cnf(i_0_290,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4)) ),
    inference(rw,[status(thm)],[i_0_229,c_0_205]),
    [final] ).

cnf(i_0_291,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),X4))
    | hBOOL(hAPP(hAPP(X1,X5),X6))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X5,X3,X2)),c_List_Olist_OCons(X6,X4,X2))) ),
    cls_Cons__step1__Cons_1,
    [final] ).

cnf(i_0_292,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),X4))
    | X4 = X3
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X5,X3,X2)),c_List_Olist_OCons(X6,X4,X2))) ),
    cls_Cons__step1__Cons_3,
    [final] ).

cnf(i_0_293,plain,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4)) ),
    inference(rw,[status(thm)],[i_0_230,c_0_205]),
    [final] ).

cnf(i_0_294,axiom,
    ( X1 = X2
    | hBOOL(hAPP(hAPP(X3,X2),X1))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X3,X4),c_List_Olist_OCons(X2,X5,X4)),c_List_Olist_OCons(X1,X6,X4))) ),
    cls_Cons__step1__Cons_0,
    [final] ).

cnf(i_0_295,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X2,X5),X6))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X6)) ),
    cls_inf2I_0,
    [final] ).

cnf(i_0_296,plain,
    hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X3)),
    inference(rw,[status(thm)],[i_0_231,c_0_205]),
    [final] ).

cnf(i_0_297,plain,
    hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X3),X3)),
    inference(rw,[status(thm)],[i_0_232,c_0_205]),
    [final] ).

cnf(i_0_298,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    cls_App__eq__foldl__conv_4,
    [final] ).

cnf(i_0_299,axiom,
    ( X1 = X2
    | X3 = X4
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X5,X6),c_List_Olist_OCons(X2,X4,X6)),c_List_Olist_OCons(X1,X3,X6))) ),
    cls_Cons__step1__Cons_2,
    [final] ).

cnf(i_0_300,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(X1,X2,X3)))
    | ~ c_Type_Otyping(X4,X2,X5)
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X2))
    | ~ c_Type_Otyping(c_Type_Oshift(X4,X3,X5,tc_Type_Otype),X1,X6)
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_subst__type__IT_0,
    [final] ).

cnf(i_0_301,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X6)) ),
    cls_sup2CI_1,
    [final] ).

cnf(i_0_302,axiom,
    ( hBOOL(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X5),X6))
    | ~ hBOOL(hAPP(hAPP(X2,X5),X6)) ),
    cls_sup2CI_0,
    [final] ).

cnf(i_0_303,axiom,
    c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) = c_Lambda_OdB_OAbs(X1),
    cls_apps__eq__Abs__conv_2,
    [final] ).

cnf(i_0_304,axiom,
    c_Lambda_OdB_OAbs(X1) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    cls_Abs__eq__apps__conv_2,
    [final] ).

cnf(i_0_305,axiom,
    c_Lambda_OdB_OVar(X1) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X1),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
    cls_Var__eq__apps__conv_2,
    [final] ).

cnf(i_0_306,axiom,
    c_List_Ofoldl(X1,X2,c_List_Olist_ONil(X3),X4,X3) = X2,
    cls_foldl__Nil_0,
    [final] ).

cnf(i_0_307,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_OCons(X3,X4,X2)),c_List_Olist_OCons(X3,X5,X2)))
    | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X4),X5)) ),
    cls_Cons__step1__Cons_5,
    [final] ).

cnf(i_0_308,axiom,
    ( c_Type_Otyping(X1,c_Lambda_Osubst(X5,X2,X4),X6)
    | ~ c_Type_Otyping(X1,X2,X3)
    | ~ c_Type_Otyping(c_Type_Oshift(X1,X4,X3,tc_Type_Otype),X5,X6) ),
    cls_subst__lemma_0,
    [final] ).

cnf(i_0_309,axiom,
    ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X4),c_List_Olist_OCons(X2,X5,X4)),c_List_Olist_OCons(X3,X5,X4)))
    | ~ hBOOL(hAPP(hAPP(X1,X2),X3)) ),
    cls_Cons__step1__Cons_4,
    [final] ).

cnf(i_0_310,axiom,
    ( c_Type_Otyping(X1,c_Lambda_OdB_OAbs(X2),c_Type_Otype_OFun(X3,X4))
    | ~ c_Type_Otyping(c_Type_Oshift(X1,c_HOL_Ozero__class_Ozero(tc_nat),X3,tc_Type_Otype),X2,X4) ),
    cls_Abs_0,
    [final] ).

cnf(i_0_311,plain,
    c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_233,c_0_205]),c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_312,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),c_List_Olist_OCons(X3,X4,X2)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3)) ),
    cls_Cons__acc__step1I_0,
    [final] ).

cnf(i_0_313,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X4,X5),X3),X2)) ),
    cls_conversepD_0,
    [final] ).

cnf(i_0_314,axiom,
    ( hBOOL(hAPP(hAPP(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X4,X5),X3),X2)) ),
    cls_conversep_Ocases_0,
    [final] ).

cnf(i_0_315,plain,
    c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(c_Lattices_Oupper__semilattice__class_Osup(X1,c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))) = c_Lattices_Oupper__semilattice__class_Osup(c_Transitive__Closure_Otranclp(X1,X2),c_fequal(X2),tc_fun(X2,tc_fun(X2,tc_bool))),
    inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_234,c_0_205]),c_0_205]),
    [final] ).

cnf(i_0_316,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Osubst(X1,X2,X3)),c_Lambda_Osubst(X4,X2,X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X4)) ),
    cls_subst__preserves__beta_0,
    [final] ).

cnf(i_0_317,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    cls_tranclp__trans_0,
    [final] ).

cnf(i_0_318,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,X1))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X1)) ),
    cls_termi__implies__IT_0,
    [final] ).

cnf(i_0_319,negated_conjecture,
    ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),v_t)),
    cls_conjecture_0,
    [final] ).

cnf(i_0_320,axiom,
    hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X1)),X2)),c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat)))),
    cls_beta_0,
    [final] ).

cnf(i_0_321,axiom,
    ( c_Type_Otyping(c_Type_Oshift(X1,X2,X3,tc_Type_Otype),c_Lambda_Olift(X4,X2),X5)
    | ~ c_Type_Otyping(X1,X4,X5) ),
    cls_lift__type_0,
    [final] ).

cnf(i_0_322,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X4,X5)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,X5),X2)) ),
    cls_accp__induct__rule_1,
    [final] ).

cnf(i_0_323,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X4,X5)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,X5),X2)) ),
    cls_accp__induct_1,
    [final] ).

cnf(i_0_324,axiom,
    c_Predicate_Oconversep(c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(c_Predicate_Oconversep(X1,X3,X4),c_Predicate_Oconversep(X2,X3,X4),tc_fun(X4,tc_fun(X3,tc_bool))),
    cls_converse__join_0,
    [final] ).

cnf(i_0_325,axiom,
    c_Predicate_Oconversep(c_Lattices_Olower__semilattice__class_Oinf(X1,X2,tc_fun(X3,tc_fun(X4,tc_bool))),X3,X4) = c_Lattices_Olower__semilattice__class_Oinf(c_Predicate_Oconversep(X1,X3,X4),c_Predicate_Oconversep(X2,X3,X4),tc_fun(X4,tc_fun(X3,tc_bool))),
    cls_converse__meet_0,
    [final] ).

cnf(i_0_326,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X2,X3),X4),X5))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4)) ),
    cls_conversep__iff_1,
    [final] ).

cnf(i_0_327,axiom,
    ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(X1,X2,X3),X4),X5))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4)) ),
    cls_conversep_Ointros_0,
    [final] ).

cnf(i_0_328,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X2),X3)) ),
    cls_appR_0,
    [final] ).

cnf(i_0_329,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2)),hAPP(hAPP(c_Lambda_OdB_OApp,X3),X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    cls_appL_0,
    [final] ).

cnf(i_0_330,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X5),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X5)) ),
    cls_tranclp__into__tranclp2_0,
    [final] ).

cnf(i_0_331,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X5),X4))
    | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X5)) ),
    cls_tranclp_Otrancl__into__trancl_0,
    [final] ).

cnf(i_0_332,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__XaccpI__1__1(X1,X3,X2)),X3)) ),
    cls_accpI_0,
    [final] ).

cnf(i_0_333,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__Xintros__1__1(X1,X3,X2)),X3)) ),
    cls_accp_OaccI_0,
    [final] ).

cnf(i_0_334,axiom,
    ( hBOOL(hAPP(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xnot__accp__down__1__1(X1,X2,X3)),X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X3),X2)) ),
    cls_not__accp__down_0,
    [final] ).

cnf(i_0_335,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__XaccpI__1__1(X1,X3,X2))) ),
    cls_accpI_1,
    [final] ).

cnf(i_0_336,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__Xaccp__Xintros__1__1(X1,X3,X2))) ),
    cls_accp_OaccI_1,
    [final] ).

cnf(i_0_337,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),c_ATP__Linkup_Osko__Wellfounded__Xnot__accp__down__1__1(X1,X3,X2))) ),
    cls_not__accp__down_1,
    [final] ).

cnf(i_0_338,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    cls_accp__induct__rule_2,
    [final] ).

cnf(i_0_339,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    cls_accp__induct_2,
    [final] ).

cnf(i_0_340,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),X1))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_IT__implies__termi_0,
    [final] ).

cnf(i_0_341,axiom,
    hAPP(c_Type_Oshift(X1,X2,X3,X4),X2) = X3,
    cls_shift__eq_0,
    [final] ).

cnf(i_0_342,axiom,
    c_Lambda_Osubst(hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),X3,X4) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubst(X1,X3,X4)),c_Lambda_Osubst(X2,X3,X4)),
    cls_subst__App_0,
    [final] ).

cnf(i_0_343,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__rule__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    cls_accp__induct__rule_0,
    [final] ).

cnf(i_0_344,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),c_ATP__Linkup_Osko__Wellfounded__Xaccp__induct__1__1(X1,X3,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X4),X2)) ),
    cls_accp__induct_0,
    [final] ).

cnf(i_0_345,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X4))
    | ~ hBOOL(hAPP(hAPP(X3,X4),v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    cls_accp_Oinduct_0,
    [final] ).

cnf(i_0_346,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X4))
    | ~ hBOOL(hAPP(hAPP(X3,X4),v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    cls_accp_Oinducts_0,
    [final] ).

cnf(i_0_347,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    cls_sup__inf__distrib2_0,
    [final] ).

cnf(i_0_348,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    cls_inf__sup__distrib2_0,
    [final] ).

cnf(i_0_349,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    cls_sup__inf__distrib1_0,
    [final] ).

cnf(i_0_350,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Odistrib__lattice(X1) ),
    cls_inf__sup__distrib1_0,
    [final] ).

cnf(i_0_351,axiom,
    ( c_List_Olistsp(c_Wellfounded_Oaccp(X1,X2),X3,X2)
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X3)) ),
    cls_lists__accI_0,
    [final] ).

cnf(i_0_352,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,t_a),X2)) ),
    cls_accp_Oinduct_1,
    [final] ).

cnf(i_0_353,axiom,
    ( hBOOL(hAPP(X1,X2))
    | hBOOL(hAPP(X1,X3))
    | ~ hBOOL(hAPP(hAPP(X4,X3),v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X4)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X4,t_a),X2)) ),
    cls_accp_Oinducts_1,
    [final] ).

cnf(i_0_354,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(X1,X2)),c_Lambda_Olift(X3,X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X3)) ),
    cls_lift__preserves__beta_0,
    [final] ).

cnf(i_0_355,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    cls_accp_Ocases_0,
    [final] ).

cnf(i_0_356,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X4)) ),
    cls_accp__downward_0,
    [final] ).

cnf(i_0_357,axiom,
    ( c_Type_Otyping(X1,hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),X4)
    | ~ c_Type_Otyping(X1,X3,X5)
    | ~ c_Type_Otyping(X1,X2,c_Type_Otype_OFun(X5,X4)) ),
    cls_App_0,
    [final] ).

cnf(i_0_358,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(X1,X2),tc_List_Olist(X2)),X3))
    | ~ c_List_Olistsp(c_Wellfounded_Oaccp(X1,X2),X3,X2) ),
    cls_lists__accD_0,
    [final] ).

cnf(i_0_359,axiom,
    ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),c_List_Olist_ONil(X2)),X3)),
    cls_not__Nil__step1_0,
    [final] ).

cnf(i_0_360,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    cls_sup__assoc_0,
    [final] ).

cnf(i_0_361,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I6_J_0,
    [final] ).

cnf(i_0_362,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    cls_inf__assoc_0,
    [final] ).

cnf(i_0_363,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I2_J_0,
    [final] ).

cnf(i_0_364,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    cls_sup__left__commute_0,
    [final] ).

cnf(i_0_365,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,c_Lattices_Oupper__semilattice__class_Osup(X2,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I7_J_0,
    [final] ).

cnf(i_0_366,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    cls_inf__left__commute_0,
    [final] ).

cnf(i_0_367,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,c_Lattices_Olower__semilattice__class_Oinf(X2,X4,X1),X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I3_J_0,
    [final] ).

cnf(i_0_368,axiom,
    ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Otranclp(X1,X2),X3),X4))
    | ~ hBOOL(hAPP(hAPP(X1,X3),X4)) ),
    cls_tranclp_Or__into__trancl_0,
    [final] ).

cnf(i_0_369,axiom,
    ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X1,X2),X3),c_List_Olist_ONil(X2))),
    cls_not__step1__Nil_0,
    [final] ).

cnf(i_0_370,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(X1,c_Lambda_OdB_OVar(X2),X3)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_subst__Var__IT_0,
    [final] ).

cnf(i_0_371,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,v_sko__Wellfounded__Xaccp__Xinduct__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    cls_accp_Oinduct_2,
    [final] ).

cnf(i_0_372,axiom,
    ( hBOOL(hAPP(X1,X2))
    | ~ hBOOL(hAPP(X1,v_sko__Wellfounded__Xaccp__Xinducts__1(X1,X3)))
    | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X3,t_a),X2)) ),
    cls_accp_Oinducts_2,
    [final] ).

cnf(i_0_373,axiom,
    ( c_Type_Otyping(X1,X2,X3)
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X4),X2))
    | ~ c_Type_Otyping(X1,X4,X3) ),
    cls_subject__reduction_0,
    [final] ).

cnf(i_0_374,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,X1),c_Lambda_OdB_OVar(X2))))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_app__Var__IT_0,
    [final] ).

cnf(i_0_375,axiom,
    ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(X1)),c_Lambda_OdB_OAbs(X2)))
    | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,X1),X2)) ),
    cls_abs_0,
    [final] ).

cnf(i_0_376,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    cls_sup__left__idem_0,
    [final] ).

cnf(i_0_377,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I8_J_0,
    [final] ).

cnf(i_0_378,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    cls_inf__left__idem_0,
    [final] ).

cnf(i_0_379,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I4_J_0,
    [final] ).

cnf(i_0_380,axiom,
    c_Transitive__Closure_Otranclp(c_Predicate_Oconversep(X1,X2,X2),X2) = c_Predicate_Oconversep(c_Transitive__Closure_Otranclp(X1,X2),X2,X2),
    cls_tranclp__converse_0,
    [final] ).

cnf(i_0_381,axiom,
    c_Lambda_Olift(hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),X3) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Olift(X1,X3)),c_Lambda_Olift(X2,X3)),
    cls_lift_Osimps_I2_J_0,
    [final] ).

cnf(i_0_382,axiom,
    ( X1 = X4
    | c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_OCons(X4,X5,X3) ),
    cls_list_Oinject_0,
    [final] ).

cnf(i_0_383,axiom,
    ( X2 = X5
    | c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_OCons(X4,X5,X3) ),
    cls_list_Oinject_1,
    [final] ).

cnf(i_0_384,axiom,
    ( X1 = X2
    | ~ hBOOL(hAPP(hAPP(c_fequal(X3),X1),X2)) ),
    cls_ATP__Linkup_Ofequal__imp__equal_0,
    [final] ).

cnf(i_0_385,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1),X1) = X2
    | ~ class_Lattices_Olattice(X1) ),
    cls_sup__inf__absorb_0,
    [final] ).

cnf(i_0_386,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1),X1) = X2
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__absorb_0,
    [final] ).

cnf(i_0_387,axiom,
    c_Predicate_Oconversep(c_Predicate_Oconversep(X1,X2,X3),X3,X2) = X1,
    cls_conversep__conversep_0,
    [final] ).

cnf(i_0_388,axiom,
    ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X1)),X2)),
    cls_beta__cases_I1_J_0,
    [final] ).

cnf(i_0_389,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(X1,X2)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_lift__IT_0,
    [final] ).

cnf(i_0_390,axiom,
    ( X1 = X3
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4) ),
    cls_dB_Osimps_I2_J_0,
    [final] ).

cnf(i_0_391,axiom,
    ( X2 = X4
    | hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != hAPP(hAPP(c_Lambda_OdB_OApp,X3),X4) ),
    cls_dB_Osimps_I2_J_1,
    [final] ).

cnf(i_0_392,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X1)
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    cls_sup__commute_0,
    [final] ).

cnf(i_0_393,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I5_J_0,
    [final] ).

cnf(i_0_394,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X1)
    | ~ class_Lattices_Olower__semilattice(X1) ),
    cls_inf__commute_0,
    [final] ).

cnf(i_0_395,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X1)
    | ~ class_Lattices_Olattice(X1) ),
    cls_inf__sup__aci_I1_J_0,
    [final] ).

cnf(i_0_396,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,X1))
    | ~ c_Type_Otyping(X2,X1,X3) ),
    cls_type__implies__IT_0,
    [final] ).

cnf(i_0_397,axiom,
    ( hAPP(X1,X2) = X3
    | ~ c_Type_Otyping(X1,c_Lambda_OdB_OVar(X2),X3) ),
    cls_typing__elims_I1_J_0,
    [final] ).

cnf(i_0_398,axiom,
    hBOOL(hAPP(hAPP(c_fequal(X1),X2),X2)),
    cls_ATP__Linkup_Oequal__imp__fequal_0,
    [final] ).

cnf(i_0_399,axiom,
    ( hBOOL(hAPP(c_Wellfounded_Oaccp(X1,X2),X3))
    | ~ c_Wellfounded_OwfP(X1,X2) ),
    cls_accp__wfPD_0,
    [final] ).

cnf(i_0_400,axiom,
    c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_ONil(X3),
    cls_list_Osimps_I3_J_0,
    [final] ).

cnf(i_0_401,axiom,
    c_List_Olist_OCons(X1,X2,X3) != c_List_Olist_ONil(X3),
    cls_neq__Nil__conv_1,
    [final] ).

cnf(i_0_402,axiom,
    c_List_Olist_ONil(X1) != c_List_Olist_OCons(X2,X3,X1),
    cls_list_Osimps_I2_J_0,
    [final] ).

cnf(i_0_403,axiom,
    c_List_Olist_OCons(X1,X2,X3) != X2,
    cls_not__Cons__self2_0,
    [final] ).

cnf(i_0_404,axiom,
    X1 != c_List_Olist_OCons(X2,X1,X3),
    cls_not__Cons__self_0,
    [final] ).

cnf(i_0_405,axiom,
    c_Type_Otyping(X1,c_Lambda_OdB_OVar(X2),hAPP(X1,X2)),
    cls_typing_OVar_0,
    [final] ).

cnf(i_0_406,axiom,
    ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(X1)))
    | ~ hBOOL(hAPP(c_InductTermi_OIT,X1)) ),
    cls_Lambda_0,
    [final] ).

cnf(i_0_407,axiom,
    c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
    cls_subst__lift_0,
    [final] ).

cnf(i_0_408,axiom,
    c_Predicate_Oconversep(c_fequal(X1),X1,X1) = c_fequal(X1),
    cls_conversep__eq_0,
    [final] ).

cnf(i_0_409,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_Lambda_OdB_OAbs(X3),
    cls_dB_Osimps_I8_J_0,
    [final] ).

cnf(i_0_410,axiom,
    hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2) != c_Lambda_OdB_OVar(X3),
    cls_dB_Osimps_I5_J_0,
    [final] ).

cnf(i_0_411,axiom,
    c_Lambda_OdB_OAbs(X1) != hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),
    cls_dB_Osimps_I9_J_0,
    [final] ).

cnf(i_0_412,axiom,
    c_Lambda_OdB_OVar(X1) != hAPP(hAPP(c_Lambda_OdB_OApp,X2),X3),
    cls_dB_Osimps_I4_J_0,
    [final] ).

cnf(i_0_413,axiom,
    ( c_Wellfounded_OwfP(c_Transitive__Closure_Otranclp(X1,X2),X2)
    | ~ c_Wellfounded_OwfP(X1,X2) ),
    cls_wfP__trancl_0,
    [final] ).

cnf(i_0_414,axiom,
    ( c_Lattices_Oupper__semilattice__class_Osup(X2,X2,X1) = X2
    | ~ class_Lattices_Oupper__semilattice(X1) ),
    cls_sup__idem_0,
    [final] ).

cnf(i_0_415,axiom,
    ( c_Lattices_Olower__semilattice__class_Oinf(X2,X2,X1) = X2
    | ~ class_Lattices_Olower__semilattice(X1) ),
    cls_inf__idem_0,
    [final] ).

cnf(i_0_416,axiom,
    c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
    cls_subst__eq_0,
    [final] ).

cnf(i_0_417,axiom,
    c_List_Olistsp(X1,c_List_Olist_ONil(X2),X2),
    cls_listsp_ONil_0,
    [final] ).

cnf(i_0_418,axiom,
    ( X1 = X3
    | c_Type_Otype_OFun(X1,X2) != c_Type_Otype_OFun(X3,X4) ),
    cls_type_Osimps_I2_J_0,
    [final] ).

cnf(i_0_419,axiom,
    ( X2 = X4
    | c_Type_Otype_OFun(X1,X2) != c_Type_Otype_OFun(X3,X4) ),
    cls_type_Osimps_I2_J_1,
    [final] ).

cnf(i_0_420,axiom,
    hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(X1))),
    cls_Var__IT_0,
    [final] ).

cnf(i_0_421,axiom,
    ( class_Lattices_Odistrib__lattice(tc_fun(X1,X2))
    | ~ class_Lattices_Odistrib__lattice(X2) ),
    clsarity_fun__Lattices_Odistrib__lattice,
    [final] ).

cnf(i_0_422,axiom,
    ( class_Lattices_Olower__semilattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    clsarity_fun__Lattices_Olower__semilattice,
    [final] ).

cnf(i_0_423,axiom,
    ( class_Lattices_Oupper__semilattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    clsarity_fun__Lattices_Oupper__semilattice,
    [final] ).

cnf(i_0_424,axiom,
    ( class_Lattices_Olattice(tc_fun(X1,X2))
    | ~ class_Lattices_Olattice(X2) ),
    clsarity_fun__Lattices_Olattice,
    [final] ).

cnf(i_0_425,axiom,
    hBOOL(hAPP(c_InductTermi_OIT,v_t)),
    cls_CHAINED_0,
    [final] ).

cnf(i_0_426,axiom,
    ( X1 = X2
    | c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OAbs(X2) ),
    cls_dB_Osimps_I3_J_0,
    [final] ).

cnf(i_0_427,axiom,
    ( X1 = X2
    | c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OVar(X2) ),
    cls_dB_Osimps_I1_J_0,
    [final] ).

cnf(i_0_428,axiom,
    c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OVar(X2),
    cls_dB_Osimps_I7_J_0,
    [final] ).

cnf(i_0_429,axiom,
    c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OAbs(X2),
    cls_dB_Osimps_I6_J_0,
    [final] ).

cnf(i_0_430,axiom,
    class_Lattices_Odistrib__lattice(tc_bool),
    clsarity_bool__Lattices_Odistrib__lattice,
    [final] ).

cnf(i_0_431,axiom,
    class_Lattices_Odistrib__lattice(tc_nat),
    clsarity_nat__Lattices_Odistrib__lattice,
    [final] ).

cnf(i_0_432,axiom,
    class_Lattices_Olower__semilattice(tc_bool),
    clsarity_bool__Lattices_Olower__semilattice,
    [final] ).

cnf(i_0_433,axiom,
    class_Lattices_Olower__semilattice(tc_nat),
    clsarity_nat__Lattices_Olower__semilattice,
    [final] ).

cnf(i_0_434,axiom,
    class_Lattices_Oupper__semilattice(tc_bool),
    clsarity_bool__Lattices_Oupper__semilattice,
    [final] ).

cnf(i_0_435,axiom,
    class_Lattices_Oupper__semilattice(tc_nat),
    clsarity_nat__Lattices_Oupper__semilattice,
    [final] ).

cnf(i_0_436,axiom,
    class_Lattices_Olattice(tc_bool),
    clsarity_bool__Lattices_Olattice,
    [final] ).

cnf(i_0_437,axiom,
    class_Lattices_Olattice(tc_nat),
    clsarity_nat__Lattices_Olattice,
    [final] ).

cnf(i_0_438,axiom,
    X1 = X1 ).

cnf(i_0_439,axiom,
    ( X1 = X2
    | X2 != X1 ) ).

cnf(i_0_440,axiom,
    ( X1 = X2
    | X1 != X3
    | X3 != X2 ) ).

cnf(i_0_441,axiom,
    ( X1 != X2
    | hAPP(X1,X3) = hAPP(X2,X3) ) ).

cnf(i_0_442,axiom,
    ( X1 != X2
    | hAPP(X3,X1) = hAPP(X3,X2) ) ).

cnf(i_0_443,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X1,X3,X4) = c_Predicate_Oconversep(X2,X3,X4) ) ).

cnf(i_0_444,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X3,X1,X4) = c_Predicate_Oconversep(X3,X2,X4) ) ).

cnf(i_0_445,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X3,X4,X1) = c_Predicate_Oconversep(X3,X4,X2) ) ).

cnf(i_0_446,axiom,
    ( X1 != X2
    | c_Lambda_OdB_OAbs(X1) = c_Lambda_OdB_OAbs(X2) ) ).

cnf(i_0_447,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X1,X3,X4) = c_Lambda_Osubst(X2,X3,X4) ) ).

cnf(i_0_448,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X3,X1,X4) = c_Lambda_Osubst(X3,X2,X4) ) ).

cnf(i_0_449,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X3,X4,X1) = c_Lambda_Osubst(X3,X4,X2) ) ).

cnf(i_0_450,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X1,X3,X4,X5,X6) = c_Predicate_Opred__comp(X2,X3,X4,X5,X6) ) ).

cnf(i_0_451,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X1,X4,X5,X6) = c_Predicate_Opred__comp(X3,X2,X4,X5,X6) ) ).

cnf(i_0_452,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X1,X5,X6) = c_Predicate_Opred__comp(X3,X4,X2,X5,X6) ) ).

cnf(i_0_453,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X5,X1,X6) = c_Predicate_Opred__comp(X3,X4,X5,X2,X6) ) ).

cnf(i_0_454,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X5,X6,X1) = c_Predicate_Opred__comp(X3,X4,X5,X6,X2) ) ).

cnf(i_0_455,axiom,
    ( X1 != X2
    | c_List_Olist_ONil(X1) = c_List_Olist_ONil(X2) ) ).

cnf(i_0_456,axiom,
    ( X1 != X2
    | c_Lambda_Olift(X1,X3) = c_Lambda_Olift(X2,X3) ) ).

cnf(i_0_457,axiom,
    ( X1 != X2
    | c_Lambda_Olift(X3,X1) = c_Lambda_Olift(X3,X2) ) ).

cnf(i_0_458,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X1,X3,X4) = c_List_Olist_OCons(X2,X3,X4) ) ).

cnf(i_0_459,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X3,X1,X4) = c_List_Olist_OCons(X3,X2,X4) ) ).

cnf(i_0_460,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X3,X4,X1) = c_List_Olist_OCons(X3,X4,X2) ) ).

cnf(i_0_461,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X1,X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X4) ) ).

cnf(i_0_462,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X3,X1,X4) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X4) ) ).

cnf(i_0_463,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X2) ) ).

cnf(i_0_464,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X1,X3,X4) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X4) ) ).

cnf(i_0_465,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X3,X1,X4) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X4) ) ).

cnf(i_0_466,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X2) ) ).

cnf(i_0_467,axiom,
    ( X1 != X2
    | c_Type_Otype_OFun(X1,X3) = c_Type_Otype_OFun(X2,X3) ) ).

cnf(i_0_468,axiom,
    ( X1 != X2
    | c_Type_Otype_OFun(X3,X1) = c_Type_Otype_OFun(X3,X2) ) ).

cnf(i_0_469,axiom,
    ( X1 != X2
    | c_Transitive__Closure_Otranclp(X1,X3) = c_Transitive__Closure_Otranclp(X2,X3) ) ).

cnf(i_0_470,axiom,
    ( X1 != X2
    | c_Transitive__Closure_Otranclp(X3,X1) = c_Transitive__Closure_Otranclp(X3,X2) ) ).

cnf(i_0_471,axiom,
    ( X1 != X2
    | c_fequal(X1) = c_fequal(X2) ) ).

cnf(i_0_472,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X1,X3,X4,X5,X6) = c_List_Ofoldl(X2,X3,X4,X5,X6) ) ).

cnf(i_0_473,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X1,X4,X5,X6) = c_List_Ofoldl(X3,X2,X4,X5,X6) ) ).

cnf(i_0_474,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X1,X5,X6) = c_List_Ofoldl(X3,X4,X2,X5,X6) ) ).

cnf(i_0_475,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X5,X1,X6) = c_List_Ofoldl(X3,X4,X5,X2,X6) ) ).

cnf(i_0_476,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X5,X6,X1) = c_List_Ofoldl(X3,X4,X5,X6,X2) ) ).

cnf(i_0_477,axiom,
    ( X1 != X2
    | c_Lambda_OdB_OVar(X1) = c_Lambda_OdB_OVar(X2) ) ).

cnf(i_0_478,axiom,
    ( X1 != X2
    | ~ hBOOL(X1)
    | hBOOL(X2) ) ).

cnf(i_0_479,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X1,X3,X4)
    | c_Type_Otyping(X2,X3,X4) ) ).

cnf(i_0_480,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X3,X1,X4)
    | c_Type_Otyping(X3,X2,X4) ) ).

cnf(i_0_481,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X3,X4,X1)
    | c_Type_Otyping(X3,X4,X2) ) ).

cnf(i_0_482,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X1,X3,X4)
    | c_List_Olistsp(X2,X3,X4) ) ).

cnf(i_0_483,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X3,X1,X4)
    | c_List_Olistsp(X3,X2,X4) ) ).

cnf(i_0_484,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X3,X4,X1)
    | c_List_Olistsp(X3,X4,X2) ) ).

cnf(i_0_485,axiom,
    ( X1 != X2
    | ~ class_Lattices_Odistrib__lattice(X1)
    | class_Lattices_Odistrib__lattice(X2) ) ).

cnf(i_0_486,axiom,
    ( X1 != X2
    | ~ class_Lattices_Oupper__semilattice(X1)
    | class_Lattices_Oupper__semilattice(X2) ) ).

cnf(i_0_487,axiom,
    ( X1 != X2
    | ~ class_Lattices_Olattice(X1)
    | class_Lattices_Olattice(X2) ) ).

cnf(i_0_488,axiom,
    ( X1 != X2
    | ~ class_Lattices_Olower__semilattice(X1)
    | class_Lattices_Olower__semilattice(X2) ) ).

cnf(i_0_489,axiom,
    ( X1 != X2
    | ~ c_Wellfounded_OwfP(X1,X3)
    | c_Wellfounded_OwfP(X2,X3) ) ).

cnf(i_0_490,axiom,
    ( X1 != X2
    | ~ c_Wellfounded_OwfP(X3,X1)
    | c_Wellfounded_OwfP(X3,X2) ) ).

cnf(i_0_438_001,axiom,
    X1 = X1 ).

cnf(i_0_439_002,axiom,
    ( X1 = X2
    | X2 != X1 ) ).

cnf(i_0_440_003,axiom,
    ( X1 = X2
    | X1 != X3
    | X3 != X2 ) ).

cnf(i_0_441_004,axiom,
    ( X1 != X2
    | hAPP(X1,X3) = hAPP(X2,X3) ) ).

cnf(i_0_442_005,axiom,
    ( X1 != X2
    | hAPP(X3,X1) = hAPP(X3,X2) ) ).

cnf(i_0_443_006,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X1,X3,X4) = c_Predicate_Oconversep(X2,X3,X4) ) ).

cnf(i_0_444_007,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X3,X1,X4) = c_Predicate_Oconversep(X3,X2,X4) ) ).

cnf(i_0_445_008,axiom,
    ( X1 != X2
    | c_Predicate_Oconversep(X3,X4,X1) = c_Predicate_Oconversep(X3,X4,X2) ) ).

cnf(i_0_446_009,axiom,
    ( X1 != X2
    | c_Lambda_OdB_OAbs(X1) = c_Lambda_OdB_OAbs(X2) ) ).

cnf(i_0_447_010,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X1,X3,X4) = c_Lambda_Osubst(X2,X3,X4) ) ).

cnf(i_0_448_011,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X3,X1,X4) = c_Lambda_Osubst(X3,X2,X4) ) ).

cnf(i_0_449_012,axiom,
    ( X1 != X2
    | c_Lambda_Osubst(X3,X4,X1) = c_Lambda_Osubst(X3,X4,X2) ) ).

cnf(i_0_450_013,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X1,X3,X4,X5,X6) = c_Predicate_Opred__comp(X2,X3,X4,X5,X6) ) ).

cnf(i_0_451_014,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X1,X4,X5,X6) = c_Predicate_Opred__comp(X3,X2,X4,X5,X6) ) ).

cnf(i_0_452_015,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X1,X5,X6) = c_Predicate_Opred__comp(X3,X4,X2,X5,X6) ) ).

cnf(i_0_453_016,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X5,X1,X6) = c_Predicate_Opred__comp(X3,X4,X5,X2,X6) ) ).

cnf(i_0_454_017,axiom,
    ( X1 != X2
    | c_Predicate_Opred__comp(X3,X4,X5,X6,X1) = c_Predicate_Opred__comp(X3,X4,X5,X6,X2) ) ).

cnf(i_0_455_018,axiom,
    ( X1 != X2
    | c_List_Olist_ONil(X1) = c_List_Olist_ONil(X2) ) ).

cnf(i_0_456_019,axiom,
    ( X1 != X2
    | c_Lambda_Olift(X1,X3) = c_Lambda_Olift(X2,X3) ) ).

cnf(i_0_457_020,axiom,
    ( X1 != X2
    | c_Lambda_Olift(X3,X1) = c_Lambda_Olift(X3,X2) ) ).

cnf(i_0_458_021,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X1,X3,X4) = c_List_Olist_OCons(X2,X3,X4) ) ).

cnf(i_0_459_022,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X3,X1,X4) = c_List_Olist_OCons(X3,X2,X4) ) ).

cnf(i_0_460_023,axiom,
    ( X1 != X2
    | c_List_Olist_OCons(X3,X4,X1) = c_List_Olist_OCons(X3,X4,X2) ) ).

cnf(i_0_461_024,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X1,X3,X4) = c_Lattices_Oupper__semilattice__class_Osup(X2,X3,X4) ) ).

cnf(i_0_462_025,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X3,X1,X4) = c_Lattices_Oupper__semilattice__class_Osup(X3,X2,X4) ) ).

cnf(i_0_463_026,axiom,
    ( X1 != X2
    | c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X1) = c_Lattices_Oupper__semilattice__class_Osup(X3,X4,X2) ) ).

cnf(i_0_464_027,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X1,X3,X4) = c_Lattices_Olower__semilattice__class_Oinf(X2,X3,X4) ) ).

cnf(i_0_465_028,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X3,X1,X4) = c_Lattices_Olower__semilattice__class_Oinf(X3,X2,X4) ) ).

cnf(i_0_466_029,axiom,
    ( X1 != X2
    | c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X1) = c_Lattices_Olower__semilattice__class_Oinf(X3,X4,X2) ) ).

cnf(i_0_467_030,axiom,
    ( X1 != X2
    | c_Type_Otype_OFun(X1,X3) = c_Type_Otype_OFun(X2,X3) ) ).

cnf(i_0_468_031,axiom,
    ( X1 != X2
    | c_Type_Otype_OFun(X3,X1) = c_Type_Otype_OFun(X3,X2) ) ).

cnf(i_0_469_032,axiom,
    ( X1 != X2
    | c_Transitive__Closure_Otranclp(X1,X3) = c_Transitive__Closure_Otranclp(X2,X3) ) ).

cnf(i_0_470_033,axiom,
    ( X1 != X2
    | c_Transitive__Closure_Otranclp(X3,X1) = c_Transitive__Closure_Otranclp(X3,X2) ) ).

cnf(i_0_471_034,axiom,
    ( X1 != X2
    | c_fequal(X1) = c_fequal(X2) ) ).

cnf(i_0_472_035,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X1,X3,X4,X5,X6) = c_List_Ofoldl(X2,X3,X4,X5,X6) ) ).

cnf(i_0_473_036,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X1,X4,X5,X6) = c_List_Ofoldl(X3,X2,X4,X5,X6) ) ).

cnf(i_0_474_037,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X1,X5,X6) = c_List_Ofoldl(X3,X4,X2,X5,X6) ) ).

cnf(i_0_475_038,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X5,X1,X6) = c_List_Ofoldl(X3,X4,X5,X2,X6) ) ).

cnf(i_0_476_039,axiom,
    ( X1 != X2
    | c_List_Ofoldl(X3,X4,X5,X6,X1) = c_List_Ofoldl(X3,X4,X5,X6,X2) ) ).

cnf(i_0_477_040,axiom,
    ( X1 != X2
    | c_Lambda_OdB_OVar(X1) = c_Lambda_OdB_OVar(X2) ) ).

cnf(i_0_478_041,axiom,
    ( X1 != X2
    | ~ hBOOL(X1)
    | hBOOL(X2) ) ).

cnf(i_0_479_042,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X1,X3,X4)
    | c_Type_Otyping(X2,X3,X4) ) ).

cnf(i_0_480_043,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X3,X1,X4)
    | c_Type_Otyping(X3,X2,X4) ) ).

cnf(i_0_481_044,axiom,
    ( X1 != X2
    | ~ c_Type_Otyping(X3,X4,X1)
    | c_Type_Otyping(X3,X4,X2) ) ).

cnf(i_0_482_045,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X1,X3,X4)
    | c_List_Olistsp(X2,X3,X4) ) ).

cnf(i_0_483_046,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X3,X1,X4)
    | c_List_Olistsp(X3,X2,X4) ) ).

cnf(i_0_484_047,axiom,
    ( X1 != X2
    | ~ c_List_Olistsp(X3,X4,X1)
    | c_List_Olistsp(X3,X4,X2) ) ).

cnf(i_0_485_048,axiom,
    ( X1 != X2
    | ~ class_Lattices_Odistrib__lattice(X1)
    | class_Lattices_Odistrib__lattice(X2) ) ).

cnf(i_0_486_049,axiom,
    ( X1 != X2
    | ~ class_Lattices_Oupper__semilattice(X1)
    | class_Lattices_Oupper__semilattice(X2) ) ).

cnf(i_0_487_050,axiom,
    ( X1 != X2
    | ~ class_Lattices_Olattice(X1)
    | class_Lattices_Olattice(X2) ) ).

cnf(i_0_488_051,axiom,
    ( X1 != X2
    | ~ class_Lattices_Olower__semilattice(X1)
    | class_Lattices_Olower__semilattice(X2) ) ).

cnf(i_0_489_052,axiom,
    ( X1 != X2
    | ~ c_Wellfounded_OwfP(X1,X3)
    | c_Wellfounded_OwfP(X2,X3) ) ).

cnf(i_0_490_053,axiom,
    ( X1 != X2
    | ~ c_Wellfounded_OwfP(X3,X1)
    | c_Wellfounded_OwfP(X3,X2) ) ).

cnf(i_0_491,plain,
    X1 = X1,
    inference(equality_inference,[],[251]) ).

cnf(i_0_492,plain,
    X1 = X1,
    inference(equality_inference,[],[252]) ).

cnf(i_0_493,plain,
    X1 = X1,
    inference(equality_inference,[],[253]) ).

cnf(i_0_494,plain,
    X1 = X1,
    inference(equality_inference,[],[254]) ).

cnf(i_0_495,plain,
    X1 = X1,
    inference(equality_inference,[],[256]) ).

cnf(i_0_496,plain,
    X1 = X1,
    inference(equality_inference,[],[382]) ).

cnf(i_0_497,plain,
    X1 = X1,
    inference(equality_inference,[],[383]) ).

cnf(i_0_498,plain,
    X1 = X1,
    inference(equality_inference,[],[390]) ).

cnf(i_0_499,plain,
    X1 = X1,
    inference(equality_inference,[],[391]) ).

cnf(i_0_500,plain,
    X1 = X1,
    inference(equality_inference,[],[418]) ).

cnf(i_0_501,plain,
    X1 = X1,
    inference(equality_inference,[],[419]) ).

cnf(i_0_502,plain,
    X1 = X1,
    inference(equality_inference,[],[426]) ).

cnf(i_0_503,plain,
    X1 = X1,
    inference(equality_inference,[],[427]) ).

cnf(i_0_504,plain,
    $false,
    inference(scs_inference,[],[i_0_319,i_0_425,i_0_340]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : LCL858-1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33  % Computer : n023.cluster.edu
% 0.15/0.33  % Model    : x86_64 x86_64
% 0.15/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33  % Memory   : 8042.1875MB
% 0.15/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33  % CPULimit   : 300
% 0.15/0.33  % WCLimit    : 300
% 0.15/0.33  % DateTime   : Mon May  4 23:13:24 EDT 2026
% 0.15/0.33  % CPUTime    : 
% 0.15/0.35  % start to proof: theBenchmark
% 0.36/1.62  % Version  : CSE_E---1.7
% 0.36/1.62  % Problem  : theBenchmark.p
% 0.36/1.62  % SZS status Unsatisfiable for theBenchmark.p
% 0.36/1.62  % SZS output start CNFRefutation
% See solution above
% 0.36/1.66  % Total time : 1.273s
%------------------------------------------------------------------------------