%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL776-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:02:59 PM UTC 2026
% Result : Unsatisfiable 150.87s 19.86s
% Output : Proof 150.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 57
% Syntax : Number of formulae : 253 ( 169 unt; 0 def)
% Number of atoms : 393 ( 126 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 486 ( 346 ~; 140 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 11 con; 0-5 aty)
% Number of variables : 518 ( 100 sgn 236 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f767,axiom,
( ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,V_s))
| hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r)),V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Beta_0) ).
fof(f767_nnf,plain,
! [V_r,V_s,V_ss] :
( ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,V_s))
| hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r)),V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(nnf_transformation,[status(thm)],[f767]) ).
fof(f767_sk,plain,
! [V_r,V_s,V_ss] :
( ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,V_s))
| hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r)),V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(skolemisation,[status(esa)],[f767_nnf]) ).
cnf(c767,plain,
( ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X0,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X2,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X1))
| hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X0)),X1),X2,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(cnf_transformation,[status(esa)],[f767_sk]) ).
cnf(t167,plain,
ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB))),true,hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2)),X1),X3,tc_Lambda_OdB,tc_Lambda_OdB))),true),true) = true,
inference(equality_encoding,[status(esa)],[c767]) ).
cnf(t238,plain,
ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB))),true,hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2)),X1),X3,tc_Lambda_OdB,tc_Lambda_OdB))),true),true) = true,
inference(orient,[status(thm)],[t167]) ).
cnf(f736,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_ts,c_List_Olist_OCons(V_u,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_app__last_0) ).
fof(f736_nnf,plain,
! [V_t,V_ts,V_u] : hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_ts,c_List_Olist_OCons(V_u,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f736]) ).
fof(f736_sk,plain,
! [V_t,V_ts,V_u] : hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_ts,c_List_Olist_OCons(V_u,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f736_nnf]) ).
cnf(c736,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,X0,X1,tc_Lambda_OdB,tc_Lambda_OdB)),X2) = c_List_Ofoldl(c_Lambda_OdB_OApp,X0,c_List_Oappend(X1,c_List_Olist_OCons(X2,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f736_sk]) ).
cnf(t159,plain,
c_List_Ofoldl(c_Lambda_OdB_OApp,X1,c_List_Oappend(X2,c_List_Olist_OCons(X3,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) = hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),X3),
inference(equality_encoding,[status(esa)],[c736]) ).
cnf(t332,plain,
c_List_Ofoldl(c_Lambda_OdB_OApp,X1,c_List_Oappend(X2,c_List_Olist_OCons(X3,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) = hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X2,tc_Lambda_OdB,tc_Lambda_OdB)),X3),
inference(orient,[status(thm)],[t159]) ).
cnf(t349,plain,
true = ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true,hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2)),X1),c_List_Oappend(X3,c_List_Olist_OCons(X4,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),true),true),
inference(cp,[status(thm)],[t238,t332]) ).
cnf(t45306,plain,
true = ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2)),X1),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true),true),
inference(step,[status(thm)],[t349,t332]) ).
cnf(f778,axiom,
c_List_Ofoldl(V_f,V_a,c_List_Olist_OCons(V_x,V_xs,T_b),T_a,T_b) = c_List_Ofoldl(V_f,hAPP(hAPP(V_f,V_a),V_x),V_xs,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldl__Cons_0) ).
fof(f778_nnf,plain,
! [V_f,V_a,V_x,V_xs,T_b,T_a] : c_List_Ofoldl(V_f,V_a,c_List_Olist_OCons(V_x,V_xs,T_b),T_a,T_b) = c_List_Ofoldl(V_f,hAPP(hAPP(V_f,V_a),V_x),V_xs,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f778]) ).
fof(f778_sk,plain,
! [V_f,V_a,V_x,V_xs,T_b,T_a] : c_List_Ofoldl(V_f,V_a,c_List_Olist_OCons(V_x,V_xs,T_b),T_a,T_b) = c_List_Ofoldl(V_f,hAPP(hAPP(V_f,V_a),V_x),V_xs,T_a,T_b),
inference(skolemisation,[status(esa)],[f778_nnf]) ).
cnf(c778,plain,
c_List_Ofoldl(X0,X1,c_List_Olist_OCons(X2,X3,X4),X5,X4) = c_List_Ofoldl(X0,hAPP(hAPP(X0,X1),X2),X3,X5,X4),
inference(cnf_transformation,[status(esa)],[f778_sk]) ).
cnf(t149,plain,
c_List_Ofoldl(X1,hAPP(hAPP(X1,X2),X3),X4,X5,X6) = c_List_Ofoldl(X1,X2,c_List_Olist_OCons(X3,X4,X6),X5,X6),
inference(equality_encoding,[status(esa)],[c778]) ).
cnf(t684,plain,
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),
inference(orient,[status(thm)],[t149]) ).
cnf(t45307,plain,
true = ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2),c_List_Olist_OCons(X1,X3,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true),true),
inference(step,[status(thm)],[t45306,t684]) ).
cnf(t43383,plain,
ifeq(hBOOL(hAPP(c_InductTermi_OIT,X1)),true,ifeq(hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(X2,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X3,tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2),c_List_Olist_OCons(X1,X3,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),X4))),true),true) = true,
inference(orient,[status(thm)],[t45307]) ).
cnf(f800,negated_conjecture,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f800_nnf,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),
inference(nnf_transformation,[status(thm)],[f800]) ).
cnf(c800,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),
inference(cnf_transformation,[status(esa)],[f800_nnf]) ).
cnf(t151,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = true,
inference(equality_encoding,[status(esa)],[c800]) ).
cnf(t271,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r,v_s,c_HOL_Ozero__class_Ozero(tc_nat)),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = true,
inference(orient,[status(thm)],[t151]) ).
cnf(t43903,plain,
true = ifeq(hBOOL(hAPP(c_InductTermi_OIT,v_s)),true,ifeq(true,true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),true),true),
inference(cp,[status(thm)],[t43383,t271]) ).
cnf(f801,negated_conjecture,
hBOOL(hAPP(c_InductTermi_OIT,v_s)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f801_nnf,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_s)),
inference(nnf_transformation,[status(thm)],[f801]) ).
cnf(c801,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_s)),
inference(cnf_transformation,[status(esa)],[f801_nnf]) ).
cnf(t7,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_s)) = true,
inference(equality_encoding,[status(esa)],[c801]) ).
cnf(t288,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_s)) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t45308,plain,
true = ifeq(true,true,ifeq(true,true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),true),true),
inference(step,[status(thm)],[t43903,t288]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t169,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t45309,plain,
true = ifeq(true,true,hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),true),
inference(step,[status(thm)],[t45308,t169]) ).
cnf(t45310,plain,
true = hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))),
inference(step,[status(thm)],[t45309,t169]) ).
cnf(f803,negated_conjecture,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f803_nnf,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(nnf_transformation,[status(thm)],[f803]) ).
fof(f803_sk,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(skolemisation,[status(esa)],[f803_nnf]) ).
cnf(c803,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(cnf_transformation,[status(esa)],[f803_sk]) ).
cnf(t160,plain,
hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),c_List_Oappend(v_ss,c_List_Olist_OCons(c_Lambda_OdB_OVar(v_i),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))) = false,
inference(equality_encoding,[status(esa)],[c803]) ).
cnf(t44419,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = false,
inference(step,[status(thm)],[t160,t332]) ).
cnf(t647,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = false,
inference(orient,[status(thm)],[t44419]) ).
cnf(t699,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r)),v_s),v_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = false,
inference(rw,[status(thm)],[t647]) ).
cnf(t45201,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = false,
inference(step,[status(thm)],[t699,t684]) ).
cnf(t35231,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r),c_List_Olist_OCons(v_s,v_ss,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),c_Lambda_OdB_OVar(v_i)))) = false,
inference(orient,[status(thm)],[t45201]) ).
cnf(t45311,plain,
true = false,
inference(step,[status(thm)],[t45310,t35231]) ).
cnf(t43990,plain,
false = true,
inference(orient,[status(thm)],[t45311]) ).
cnf(f74,axiom,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_impossible__Cons_0) ).
fof(f74_nnf,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
! [V_x,V_ys,T_a] : ~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_ys,T_a),tc_List_Olist(T_a)),c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
~ c_lessequals(c_Nat_Osize__class_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)),c_Nat_Osize__class_Osize(X1,tc_List_Olist(X2)),tc_nat),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(f97,axiom,
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f97_nnf,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [T_a] :
( ~ c_lessequals(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c97,plain,
( ~ c_lessequals(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(f129,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f129_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f129_nnf]) ).
cnf(c129,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(f131,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f131_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f131]) ).
fof(f131_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f131_nnf]) ).
cnf(c131,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f131_sk]) ).
cnf(f133,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f133_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f133]) ).
fof(f133_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f133_nnf]) ).
cnf(c133,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f133_sk]) ).
cnf(f135,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f135_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c135,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(f172,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f172_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f172_nnf]) ).
cnf(c172,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(f236,axiom,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a)),c_Int_Onumber__class_Onumber__of(V_v,T_a)))
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__number__of__eq__not__less_0) ).
fof(f236_nnf,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a)),c_Int_Onumber__class_Onumber__of(V_v,T_a)))
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [T_a,V_w,V_v] :
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(V_v,T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a),T_a)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Int_Onumber__class_Onumber__of(V_w,T_a)),c_Int_Onumber__class_Onumber__of(V_v,T_a)))
| ~ class_Int_Onumber(T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
( ~ c_lessequals(c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X1,X0),X0)
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),c_Int_Onumber__class_Onumber__of(X1,X0)),c_Int_Onumber__class_Onumber__of(X2,X0)))
| ~ class_Int_Onumber(X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f246,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f246_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f246]) ).
fof(f246_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f246_nnf]) ).
cnf(c246,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f246_sk]) ).
cnf(f261,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f261_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f261]) ).
fof(f261_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f261_nnf]) ).
cnf(c261,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f261_sk]) ).
cnf(f262,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f262_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c262,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
cnf(f303,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f303_nnf,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
inference(skolemisation,[status(esa)],[f303_nnf]) ).
cnf(c303,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X1),c_Suc(X0)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
cnf(f373,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f373_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f373]) ).
fof(f373_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f373_nnf]) ).
cnf(c373,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f373_sk]) ).
cnf(f374,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f374_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f374]) ).
fof(f374_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f374_nnf]) ).
cnf(c374,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f374_sk]) ).
cnf(f379,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f379_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f379]) ).
fof(f379_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f379_nnf]) ).
cnf(c379,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
cnf(f380,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f380_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f380]) ).
fof(f380_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f380_nnf]) ).
cnf(c380,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f380_sk]) ).
cnf(f475,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f475_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f475]) ).
fof(f475_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f475_nnf]) ).
cnf(c475,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f475_sk]) ).
cnf(f547,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_length__greater__0__conv_0) ).
fof(f547_nnf,plain,
! [T_a] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)))),
inference(nnf_transformation,[status(thm)],[f547]) ).
fof(f547_sk,plain,
! [T_a] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)))),
inference(skolemisation,[status(esa)],[f547_nnf]) ).
cnf(c547,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Nat_Osize__class_Osize(c_List_Olist_ONil(X0),tc_List_Olist(X0)))),
inference(cnf_transformation,[status(esa)],[f547_sk]) ).
cnf(f567,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Oone__class_Oone(T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f567_nnf,plain,
! [T_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Oone__class_Oone(T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f567]) ).
fof(f567_sk,plain,
! [T_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Oone__class_Oone(T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f567_nnf]) ).
cnf(c567,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),c_HOL_Oone__class_Oone(X0)),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f567_sk]) ).
cnf(f568,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f568_nnf,plain,
! [T_a,V_m] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f568]) ).
fof(f568_sk,plain,
! [T_a,V_m] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f568_nnf]) ).
cnf(c568,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),c_Nat_Osemiring__1__class_Oof__nat(X1,X0)),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f568_sk]) ).
cnf(f596,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f596_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c596,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
cnf(f597,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f597_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f597]) ).
fof(f597_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f597_nnf]) ).
cnf(c597,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f597_sk]) ).
cnf(f637,axiom,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f637_nnf,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(nnf_transformation,[status(thm)],[f637]) ).
fof(f637_sk,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(skolemisation,[status(esa)],[f637_nnf]) ).
cnf(c637,plain,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X0)),X1)),
inference(cnf_transformation,[status(esa)],[f637_sk]) ).
cnf(f655,axiom,
~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_ONil(T_a)),V_xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f655_nnf,plain,
! [V_r,T_a,V_xs] : ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_ONil(T_a)),V_xs)),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [V_r,T_a,V_xs] : ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_ONil(T_a)),V_xs)),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X0,X1),c_List_Olist_ONil(X1)),X2)),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(f656,axiom,
~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_xs),c_List_Olist_ONil(T_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f656_nnf,plain,
! [V_r,T_a,V_xs] : ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_xs),c_List_Olist_ONil(T_a))),
inference(nnf_transformation,[status(thm)],[f656]) ).
fof(f656_sk,plain,
! [V_r,T_a,V_xs] : ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_xs),c_List_Olist_ONil(T_a))),
inference(skolemisation,[status(esa)],[f656_nnf]) ).
cnf(c656,plain,
~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(X0,X1),X2),c_List_Olist_ONil(X1))),
inference(cnf_transformation,[status(esa)],[f656_sk]) ).
cnf(f668,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f668_nnf,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(nnf_transformation,[status(thm)],[f668]) ).
fof(f668_sk,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(skolemisation,[status(esa)],[f668_nnf]) ).
cnf(c668,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(cnf_transformation,[status(esa)],[f668_sk]) ).
cnf(f669,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f669_nnf,plain,
! [V_m] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
! [V_m] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c669,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
cnf(f671,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f671_nnf,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(nnf_transformation,[status(thm)],[f671]) ).
fof(f671_sk,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(skolemisation,[status(esa)],[f671_nnf]) ).
cnf(c671,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(cnf_transformation,[status(esa)],[f671_sk]) ).
cnf(f680,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f680_nnf,plain,
! [V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
inference(nnf_transformation,[status(thm)],[f680]) ).
fof(f680_sk,plain,
! [V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
inference(skolemisation,[status(esa)],[f680_nnf]) ).
cnf(c680,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X0)),
inference(cnf_transformation,[status(esa)],[f680_sk]) ).
cnf(f681,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f681_nnf,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
inference(nnf_transformation,[status(thm)],[f681]) ).
fof(f681_sk,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
inference(skolemisation,[status(esa)],[f681_nnf]) ).
cnf(c681,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X0)),
inference(cnf_transformation,[status(esa)],[f681_sk]) ).
cnf(f682,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f682_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f682]) ).
fof(f682_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f682_nnf]) ).
cnf(c682,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f682_sk]) ).
cnf(f683,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f683_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f683]) ).
fof(f683_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f683_nnf]) ).
cnf(c683,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f683_sk]) ).
cnf(f684,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f684_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f684]) ).
fof(f684_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f684_nnf]) ).
cnf(c684,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f684_sk]) ).
cnf(f695,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f695_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f695]) ).
fof(f695_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f695_nnf]) ).
cnf(c695,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f695_sk]) ).
cnf(f696,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f696_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f696]) ).
fof(f696_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f696_nnf]) ).
cnf(c696,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f696_sk]) ).
cnf(f697,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f697_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c697,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
cnf(f698,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f698_nnf,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f698]) ).
fof(f698_sk,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f698_nnf]) ).
cnf(c698,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f698_sk]) ).
cnf(f733,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f733_nnf,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f733]) ).
fof(f733_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f733_nnf]) ).
cnf(c733,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f733_sk]) ).
cnf(f734,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f734_nnf,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f734]) ).
fof(f734_sk,plain,
! [V_dB1,V_dB2,V_dB_H] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f734_nnf]) ).
cnf(c734,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f734_sk]) ).
cnf(f737,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f737_nnf,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(nnf_transformation,[status(thm)],[f737]) ).
fof(f737_sk,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),
inference(skolemisation,[status(esa)],[f737_nnf]) ).
cnf(c737,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f737_sk]) ).
cnf(f750,axiom,
c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I2_J_0) ).
fof(f750_nnf,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f750]) ).
fof(f750_sk,plain,
! [T_a,V_a_H,V_list_H] : c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f750_nnf]) ).
cnf(c750,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f750_sk]) ).
cnf(f758,axiom,
c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f758_nnf,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(nnf_transformation,[status(thm)],[f758]) ).
fof(f758_sk,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H),
inference(skolemisation,[status(esa)],[f758_nnf]) ).
cnf(c758,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f758_sk]) ).
cnf(f765,axiom,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Var__apps__neq__Abs__apps_0) ).
fof(f765_nnf,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f765]) ).
fof(f765_sk,plain,
! [V_n,V_ts,V_r,V_ss] : c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f765_nnf]) ).
cnf(c765,plain,
c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X0),X1,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f765_sk]) ).
cnf(f768,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f768_nnf,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f768]) ).
fof(f768_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f768_nnf]) ).
cnf(c768,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f768_sk]) ).
cnf(f786,axiom,
c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq__Nil__conv_1) ).
fof(f786_nnf,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f786]) ).
fof(f786_sk,plain,
! [V_x,V_xa,T_a] : c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f786_nnf]) ).
cnf(c786,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f786_sk]) ).
cnf(f787,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_list_Osimps_I3_J_0) ).
fof(f787_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(nnf_transformation,[status(thm)],[f787]) ).
fof(f787_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a),
inference(skolemisation,[status(esa)],[f787_nnf]) ).
cnf(c787,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f787_sk]) ).
cnf(f791,axiom,
c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self2_0) ).
fof(f791_nnf,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(nnf_transformation,[status(thm)],[f791]) ).
fof(f791_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f791_nnf]) ).
cnf(c791,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f791_sk]) ).
cnf(f792,axiom,
V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Cons__self_0) ).
fof(f792_nnf,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f792]) ).
fof(f792_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f792_nnf]) ).
cnf(c792,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f792_sk]) ).
cnf(f796,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Abs__App__neq__Var__apps_0) ).
fof(f796_nnf,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f796]) ).
fof(f796_sk,plain,
! [V_s,V_t,V_n,V_ss] : hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),
inference(skolemisation,[status(esa)],[f796_nnf]) ).
cnf(c796,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(X0)),X1) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(X2),X3,tc_Lambda_OdB,tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f796_sk]) ).
cnf(f798,axiom,
hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f798_nnf,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f798]) ).
fof(f798_sk,plain,
! [V_dB1_H,V_dB2_H,V_nat] : hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f798_nnf]) ).
cnf(c798,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f798_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c74,c97,c129,c131,c133,c135,c172,c236,c246,c261,c262,c303,c373,c374,c379,c380,c475,c547,c567,c568,c596,c597,c637,c655,c656,c668,c669,c671,c680,c681,c682,c683,c684,c695,c696,c697,c698,c733,c734,c737,c750,c758,c765,c768,c786,c787,c791,c792,c796,c798,c803]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t43990]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL776-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 00:28:57 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 150.87/19.86 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 150.87/19.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------