%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL784-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 : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:03:01 PM UTC 2026
% Result : Unsatisfiable 9.57s 1.62s
% Output : Proof 9.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 38
% Syntax : Number of formulae : 192 ( 164 unt; 0 def)
% Number of atoms : 236 ( 124 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 206 ( 162 ~; 44 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 23 ( 23 usr; 16 con; 0-5 aty)
% Number of variables : 323 ( 96 sgn 150 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f296,negated_conjecture,
~ hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f296_nnf,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____))),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____))),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c296,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____))),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
cnf(t110,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____))) = false,
inference(equality_encoding,[status(esa)],[c296]) ).
cnf(f244,axiom,
c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_foldl__Nil_0) ).
fof(f244_nnf,plain,
! [V_f,V_a,T_b,T_a] : c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a,
inference(nnf_transformation,[status(thm)],[f244]) ).
fof(f244_sk,plain,
! [V_f,V_a,T_b,T_a] : c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a,
inference(skolemisation,[status(esa)],[f244_nnf]) ).
cnf(c244,plain,
c_List_Ofoldl(X0,X1,c_List_Olist_ONil(X2),X3,X2) = X1,
inference(cnf_transformation,[status(esa)],[f244_sk]) ).
cnf(t31,plain,
c_List_Ofoldl(X1,X2,c_List_Olist_ONil(X3),X4,X3) = X2,
inference(equality_encoding,[status(esa)],[c244]) ).
cnf(t209,plain,
c_List_Ofoldl(X1,X2,c_List_Olist_ONil(X3),X4,X3) = X2,
inference(orient,[status(thm)],[t31]) ).
cnf(f273,axiom,
v_rs____ = c_List_Olist_ONil(tc_Lambda_OdB),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nil_0) ).
fof(f273_nnf,plain,
v_rs____ = c_List_Olist_ONil(tc_Lambda_OdB),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c273,plain,
v_rs____ = c_List_Olist_ONil(tc_Lambda_OdB),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(t2,plain,
c_List_Olist_ONil(tc_Lambda_OdB) = v_rs____,
inference(equality_encoding,[status(esa)],[c273]) ).
cnf(t174,plain,
c_List_Olist_ONil(tc_Lambda_OdB) = v_rs____,
inference(orient,[status(thm)],[t2]) ).
cnf(t210,plain,
X1 = c_List_Ofoldl(X2,X1,v_rs____,X3,tc_Lambda_OdB),
inference(cp,[status(thm)],[t209,t174]) ).
cnf(t211,plain,
c_List_Ofoldl(X1,X2,v_rs____,X3,tc_Lambda_OdB) = X2,
inference(orient,[status(thm)],[t210]) ).
cnf(t873,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_n____)),v_u____),v_i____))) = false,
inference(step,[status(thm)],[t110,t211]) ).
cnf(t165,axiom,
sF0 = c_Lambda_OdB_OVar(v_n____),
introduced(definition) ).
cnf(t175,plain,
c_Lambda_OdB_OVar(v_n____) = sF0,
inference(orient,[status(thm)],[t165]) ).
cnf(t874,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,sF0),v_u____),v_i____))) = false,
inference(step,[status(thm)],[t873,t175]) ).
cnf(t167,axiom,
sF2 = hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),
introduced(definition) ).
cnf(t781,plain,
sF2 = hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_n____)),
inference(step,[status(thm)],[t167,t211]) ).
cnf(t782,plain,
sF2 = hAPP(c_Lambda_Osubst,sF0),
inference(step,[status(thm)],[t781,t175]) ).
cnf(t324,plain,
hAPP(c_Lambda_Osubst,sF0) = sF2,
inference(orient,[status(thm)],[t782]) ).
cnf(t875,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(sF2,v_u____),v_i____))) = false,
inference(step,[status(thm)],[t874,t324]) ).
cnf(t169,axiom,
sF4 = hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),v_i____),
introduced(definition) ).
cnf(t844,plain,
sF4 = hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_n____)),v_u____),v_i____),
inference(step,[status(thm)],[t169,t211]) ).
cnf(t845,plain,
sF4 = hAPP(hAPP(hAPP(c_Lambda_Osubst,sF0),v_u____),v_i____),
inference(step,[status(thm)],[t844,t175]) ).
cnf(t846,plain,
sF4 = hAPP(hAPP(sF2,v_u____),v_i____),
inference(step,[status(thm)],[t845,t324]) ).
cnf(t168,axiom,
sF3 = hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_u____),
introduced(definition) ).
cnf(t805,plain,
sF3 = hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_n____)),v_u____),
inference(step,[status(thm)],[t168,t211]) ).
cnf(t806,plain,
sF3 = hAPP(hAPP(c_Lambda_Osubst,sF0),v_u____),
inference(step,[status(thm)],[t805,t175]) ).
cnf(t807,plain,
sF3 = hAPP(sF2,v_u____),
inference(step,[status(thm)],[t806,t324]) ).
cnf(t427,plain,
hAPP(sF2,v_u____) = sF3,
inference(orient,[status(thm)],[t807]) ).
cnf(t847,plain,
sF4 = hAPP(sF3,v_i____),
inference(step,[status(thm)],[t846,t427]) ).
cnf(f247,axiom,
v_n____ = v_i____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_True_0) ).
fof(f247_nnf,plain,
v_n____ = v_i____,
inference(nnf_transformation,[status(thm)],[f247]) ).
cnf(c247,plain,
v_n____ = v_i____,
inference(cnf_transformation,[status(esa)],[f247_nnf]) ).
cnf(t0,plain,
v_n____ = v_i____,
inference(equality_encoding,[status(esa)],[c247]) ).
cnf(t173,plain,
v_i____ = v_n____,
inference(orient,[status(thm)],[t0]) ).
cnf(t848,plain,
sF4 = hAPP(sF3,v_n____),
inference(step,[status(thm)],[t847,t173]) ).
cnf(f220,axiom,
hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_k)),V_u),V_k) = V_u,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__eq_0) ).
fof(f220_nnf,plain,
! [V_k,V_u] : hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_k)),V_u),V_k) = V_u,
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [V_k,V_u] : hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_k)),V_u),V_k) = V_u,
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0)),X1),X0) = X1,
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(t47,plain,
hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(X1)),X2),X1) = X2,
inference(equality_encoding,[status(esa)],[c220]) ).
cnf(t268,plain,
hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(X1)),X2),X1) = X2,
inference(orient,[status(thm)],[t47]) ).
cnf(t269,plain,
X1 = hAPP(hAPP(hAPP(c_Lambda_Osubst,sF0),X1),v_n____),
inference(cp,[status(thm)],[t268,t175]) ).
cnf(t272,plain,
hAPP(hAPP(hAPP(c_Lambda_Osubst,sF0),X1),v_n____) = X1,
inference(orient,[status(thm)],[t269]) ).
cnf(t783,plain,
hAPP(hAPP(sF2,X1),v_n____) = X1,
inference(step,[status(thm)],[t272,t324]) ).
cnf(t325,plain,
hAPP(hAPP(sF2,X1),v_n____) = X1,
inference(rw,[status(thm)],[t783]) ).
cnf(t328,plain,
hAPP(hAPP(sF2,X1),v_n____) = X1,
inference(orient,[status(thm)],[t325]) ).
cnf(t429,plain,
v_u____ = hAPP(sF3,v_n____),
inference(cp,[status(thm)],[t328,t427]) ).
cnf(t433,plain,
hAPP(sF3,v_n____) = v_u____,
inference(orient,[status(thm)],[t429]) ).
cnf(t849,plain,
sF4 = v_u____,
inference(step,[status(thm)],[t848,t433]) ).
cnf(t553,plain,
v_u____ = sF4,
inference(orient,[status(thm)],[t849]) ).
cnf(t876,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(sF2,sF4),v_i____))) = false,
inference(step,[status(thm)],[t875,t553]) ).
cnf(t851,plain,
hAPP(sF2,sF4) = sF3,
inference(step,[status(thm)],[t427,t553]) ).
cnf(t555,plain,
hAPP(sF2,sF4) = sF3,
inference(rw,[status(thm)],[t851]) ).
cnf(t570,plain,
hAPP(sF2,sF4) = sF3,
inference(orient,[status(thm)],[t555]) ).
cnf(t877,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(sF3,v_i____))) = false,
inference(step,[status(thm)],[t876,t570]) ).
cnf(t878,plain,
hBOOL(hAPP(c_InductTermi_OIT,hAPP(sF3,v_n____))) = false,
inference(step,[status(thm)],[t877,t173]) ).
cnf(t852,plain,
hAPP(sF3,v_n____) = sF4,
inference(step,[status(thm)],[t433,t553]) ).
cnf(t556,plain,
hAPP(sF3,v_n____) = sF4,
inference(orient,[status(thm)],[t852]) ).
cnf(t879,plain,
hBOOL(hAPP(c_InductTermi_OIT,sF4)) = false,
inference(step,[status(thm)],[t878,t556]) ).
cnf(f282,axiom,
hBOOL(hAPP(c_InductTermi_OIT,v_u____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_uIT_0) ).
fof(f282_nnf,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_u____)),
inference(nnf_transformation,[status(thm)],[f282]) ).
cnf(c282,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_u____)),
inference(cnf_transformation,[status(esa)],[f282_nnf]) ).
cnf(t11,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_u____)) = true,
inference(equality_encoding,[status(esa)],[c282]) ).
cnf(t182,plain,
hBOOL(hAPP(c_InductTermi_OIT,v_u____)) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t850,plain,
hBOOL(hAPP(c_InductTermi_OIT,sF4)) = true,
inference(step,[status(thm)],[t182,t553]) ).
cnf(t554,plain,
hBOOL(hAPP(c_InductTermi_OIT,sF4)) = true,
inference(rw,[status(thm)],[t850]) ).
cnf(t571,plain,
hBOOL(hAPP(c_InductTermi_OIT,sF4)) = true,
inference(orient,[status(thm)],[t554]) ).
cnf(t880,plain,
true = false,
inference(step,[status(thm)],[t879,t571]) ).
cnf(t668,plain,
false = true,
inference(orient,[status(thm)],[t880]) ).
cnf(f49,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f49_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(f50,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f50_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f74,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(f74_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)],[f74]) ).
fof(f74_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)],[f74_nnf]) ).
cnf(c74,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(f75,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(f75_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)],[f75]) ).
fof(f75_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)],[f75_nnf]) ).
cnf(c75,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil(X2),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f84,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(f84_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)],[f84]) ).
fof(f84_sk,plain,
! [V_x,V_t,T_a] : c_List_Olist_OCons(V_x,V_t,T_a) != V_t,
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
c_List_Olist_OCons(X0,X1,X2) != X1,
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f85,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(f85_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)],[f85]) ).
fof(f85_sk,plain,
! [V_xs,V_x,T_a] : V_xs != c_List_Olist_OCons(V_x,V_xs,T_a),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c85,plain,
X0 != c_List_Olist_OCons(X1,X0,X2),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(f113,axiom,
~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Nil__step1_0) ).
fof(f113_nnf,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [V_r,T_a,V_xs] : ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
~ c_ListOrder_Ostep1(X0,c_List_Olist_ONil(X1),X2,X1),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(f114,axiom,
~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__step1__Nil_0) ).
fof(f114_nnf,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
! [V_r,V_xs,T_a] : ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c114,plain,
~ c_ListOrder_Ostep1(X0,X1,c_List_Olist_ONil(X2),X2),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(f131,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f131_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f131]) ).
fof(f131_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f131_nnf]) ).
cnf(c131,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f131_sk]) ).
cnf(f132,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f132_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c132,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(f133,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f133_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f133]) ).
fof(f133_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f133_nnf]) ).
cnf(c133,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f133_sk]) ).
cnf(f134,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f134_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f134_nnf]) ).
cnf(c134,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(f135,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f135_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c135,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(f152,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(f152_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)],[f152]) ).
fof(f152_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)],[f152_nnf]) ).
cnf(c152,plain,
c_List_Olist_ONil(X0) != c_List_Olist_OCons(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
cnf(f162,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f162_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c162,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(f201,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f201_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f201]) ).
fof(f201_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f201_nnf]) ).
cnf(c201,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f201_sk]) ).
cnf(f204,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f204_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f204]) ).
fof(f204_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f204_nnf]) ).
cnf(c204,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
cnf(f205,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f205_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f205]) ).
fof(f205_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f205_nnf]) ).
cnf(c205,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f205_sk]) ).
cnf(f206,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f206_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f206]) ).
fof(f206_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c206,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(f211,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(f211_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)],[f211]) ).
fof(f211_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f212,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(f212_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)],[f212]) ).
fof(f212_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)],[f212_nnf]) ).
cnf(c212,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
cnf(f217,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(f217_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)],[f217]) ).
fof(f217_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)],[f217_nnf]) ).
cnf(c217,plain,
c_Lambda_OdB_OAbs(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f217_sk]) ).
cnf(f227,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(f227_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)],[f227]) ).
fof(f227_sk,plain,
! [V_i,V_t] : ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)),
inference(skolemisation,[status(esa)],[f227_nnf]) ).
cnf(c227,plain,
~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(X0)),X1)),
inference(cnf_transformation,[status(esa)],[f227_sk]) ).
cnf(f241,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(f241_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)],[f241]) ).
fof(f241_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)],[f241_nnf]) ).
cnf(c241,plain,
c_Lambda_OdB_OVar(X0) != hAPP(hAPP(c_Lambda_OdB_OApp,X1),X2),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f242,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(f242_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)],[f242]) ).
fof(f242_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)],[f242_nnf]) ).
cnf(c242,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)],[f242_sk]) ).
cnf(f248,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(f248_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)],[f248]) ).
fof(f248_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f248_nnf]) ).
cnf(c248,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(f289,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(f289_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)],[f289]) ).
fof(f289_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)],[f289_nnf]) ).
cnf(c289,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)],[f289_sk]) ).
cnf(f292,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(f292_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)],[f292]) ).
fof(f292_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)],[f292_nnf]) ).
cnf(c292,plain,
hAPP(hAPP(c_Lambda_OdB_OApp,X0),X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c49,c50,c74,c75,c84,c85,c113,c114,c131,c132,c133,c134,c135,c152,c162,c201,c204,c205,c206,c211,c212,c217,c227,c241,c242,c248,c289,c292,c296]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t668]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL784-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 00:35:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 9.57/1.62 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.57/1.62 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------