%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL759-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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:08:18 PM UTC 2026
% Result : Unsatisfiable 2.34s 6.75s
% Output : CNFRefutation 2.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 32
% Syntax : Number of formulae : 64 ( 54 unt; 24 def)
% Number of atoms : 192 ( 32 equ)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 36 ( 20 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 28 ( 26 usr; 25 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-5 aty)
% Number of variables : 52 ( 0 sgn 52 !; 0 ?; 34 :)
% Comments :
%------------------------------------------------------------------------------
fof(f61,axiom,
! [X0] : c_Suc(X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f62,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)) = c_Suc(X0),
inference(reorient_equations,[],[f61]) ).
fof(f484,axiom,
! [X2,X0,X1] :
( ~ c_Type_Otyping(X0,c_Lambda_OdB_OVar(X1),X2)
| hAPP(X0,X1) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_typing__elims_I1_J_0) ).
fof(f485,axiom,
! [X0,X1] : c_Type_Otyping(X0,c_Lambda_OdB_OVar(X1),hAPP(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_typing_OVar_0) ).
fof(f701,axiom,
! [X0,X1] : c_Lambda_Osubstn(X0,X1,c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(hAPP(c_Lambda_Osubst,X0),X1),c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_substn__subst__0_0) ).
fof(f755,axiom,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(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))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Beta_0) ).
fof(f771,negated_conjecture,
! [X0,X1] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(c_Suc(X0))),c_Suc(X1))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1)),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f773,negated_conjecture,
! [X0,X1] : hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f774,negated_conjecture,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(c_Suc(v_ia))),c_Suc(v_ja)))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(v_ia)),v_ja)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_ia),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_ja,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f911,plain,
! [X0,X1] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1)),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(definition_unfolding,[],[f771,f62,f62]) ).
fof(f912,plain,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),v_ia),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),v_ja),c_HOL_Oone__class_Oone(tc_nat))))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(v_ia)),v_ja)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_ia),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_ja,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(definition_unfolding,[],[f774,f62,f62]) ).
tcf(c_1024,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( hAPP(X0,X1) = X2 )
| ~ c_Type_Otyping(X0,c_Lambda_OdB_OVar(X1),X2) ),
inference(cnf_transformation,[],[f484]) ).
tcf(c_1025,plain,
! [X0: $i,X1: $i] : c_Type_Otyping(X0,c_Lambda_OdB_OVar(X1),hAPP(X0,X1)),
inference(cnf_transformation,[],[f485]) ).
tcf(c_1168,plain,
! [X0: $i,X1: $i] : hAPP(hAPP(hAPP(c_Lambda_Osubst,X0),X1),c_HOL_Ozero__class_Ozero(tc_nat)) = c_Lambda_Osubstn(X0,X1,c_HOL_Ozero__class_Ozero(tc_nat)),
inference(cnf_transformation,[],[f701]) ).
tcf(c_1210,plain,
! [X0: $i,X1: $i,X2: $i] :
( 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)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X1))
| ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,X0),X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(cnf_transformation,[],[f755]) ).
tcf(c_1224,negated_conjecture,
! [X0: $i,X1: $i] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1)),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(cnf_transformation,[],[f911]) ).
tcf(c_1226,negated_conjecture,
! [X0: $i,X1: $i] : hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1))),
inference(cnf_transformation,[],[f773]) ).
tcf(c_1227,negated_conjecture,
~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),v_ia),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),v_ja),c_HOL_Oone__class_Oone(tc_nat))))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(v_ia)),v_ja)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(v_ia),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),v_ja,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(cnf_transformation,[],[f912]) ).
tcf(c_6756,plain,
! [X0: $i,X1: $i,X2: $i] :
( 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)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X1))
| ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(X0,X1,c_HOL_Ozero__class_Ozero(tc_nat)),X2,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(light_normalisation,[status(thm)],[c_1210,c_1168]) ).
tcf(c_6831,plain,
! [X0: $i,X1: $i] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(hAPP(hAPP(hAPP(c_Lambda_Osubst,v_ra),c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),c_HOL_Oone__class_Oone(tc_nat))),hAPP(hAPP(hAPP(c_Lambda_Osubst,v_s),c_Lambda_OdB_OVar(X0)),X1),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0),tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),X1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(demodulation,[status(thm)],[c_1224,c_1168]) ).
tcf(c_14111,definition,
iPr_def_10 = hAPP(c_Lambda_Osubst,v_ra),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_14112,definition,
iPr_def_11 = c_HOL_Oplus__class_Oplus(tc_nat),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_14113,definition,
iPr_def_12 = c_HOL_Oone__class_Oone(tc_nat),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_14114,definition,
iPr_def_13 = hAPP(c_Lambda_Osubst,v_s),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_14115,definition,
iPr_def_14 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_14116,definition,
iPr_def_15 = tc_fun(tc_nat,tc_Lambda_OdB),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_14120,definition,
iPr_def_19 = hAPP(iPr_def_11,v_ia),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_14121,definition,
iPr_def_20 = hAPP(iPr_def_19,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_14122,definition,
iPr_def_21 = c_Lambda_OdB_OVar(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_14123,definition,
iPr_def_22 = hAPP(iPr_def_10,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_14124,definition,
iPr_def_23 = hAPP(iPr_def_11,v_ja),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_14125,definition,
iPr_def_24 = hAPP(iPr_def_23,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_14126,definition,
iPr_def_25 = hAPP(iPr_def_22,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_14127,definition,
iPr_def_26 = c_Lambda_OdB_OAbs(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_14128,definition,
iPr_def_27 = hAPP(c_Lambda_OdB_OApp,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_14129,definition,
iPr_def_28 = c_Lambda_OdB_OVar(v_ia),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_14130,definition,
iPr_def_29 = hAPP(iPr_def_13,iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_14131,definition,
iPr_def_30 = hAPP(iPr_def_29,v_ja),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_14132,definition,
iPr_def_31 = hAPP(iPr_def_27,iPr_def_30),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_14133,definition,
iPr_def_32 = c_COMBC(c_Lambda_Osubst,iPr_def_28,tc_Lambda_OdB,tc_Lambda_OdB,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_32])],[]) ).
tcf(c_14134,definition,
iPr_def_33 = c_COMBC(iPr_def_32,v_ja,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),
introduced(definition,[new_symbols(definition,[iPr_def_33])],[]) ).
tcf(c_14135,definition,
iPr_def_34 = c_List_Omap(iPr_def_33,v_ss,tc_Lambda_OdB,tc_Lambda_OdB),
introduced(definition,[new_symbols(definition,[iPr_def_34])],[]) ).
tcf(c_14136,definition,
iPr_def_35 = c_List_Ofoldl(c_Lambda_OdB_OApp,iPr_def_31,iPr_def_34,tc_Lambda_OdB,tc_Lambda_OdB),
introduced(definition,[new_symbols(definition,[iPr_def_35])],[]) ).
tcf(c_14137,definition,
iPr_def_36 = hAPP(c_InductTermi_OIT,iPr_def_35),
introduced(definition,[new_symbols(definition,[iPr_def_36])],[]) ).
tcf(c_14139,plain,
! [X0: $i,X1: $i] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(hAPP(hAPP(iPr_def_10,c_Lambda_OdB_OVar(hAPP(hAPP(iPr_def_11,X0),iPr_def_12))),hAPP(hAPP(iPr_def_11,X1),iPr_def_12)),hAPP(hAPP(iPr_def_13,c_Lambda_OdB_OVar(X0)),X1),iPr_def_14),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,c_Lambda_OdB_OVar(X0),tc_Lambda_OdB,tc_Lambda_OdB,iPr_def_15),X1,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(demodulation,[status(thm)],[c_6831,c_14116,c_14115,c_14114,c_14113,c_14112,c_14111]) ).
tcf(c_14141,negated_conjecture,
~ hBOOL(iPr_def_36),
inference(demodulation,[status(thm)],[c_1227,c_14133,c_14134,c_14135,c_14129,c_14130,c_14131,c_14124,c_14125,c_14120,c_14121,c_14122,c_14123,c_14126,c_14127,c_14128,c_14132,c_14136,c_14137]) ).
tcf(c_14142,negated_conjecture,
! [X0: $i,X1: $i] : hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(iPr_def_13,c_Lambda_OdB_OVar(X0)),X1))),
inference(demodulation,[status(thm)],[c_1226]) ).
tcf(c_18915,plain,
! [X0: $i] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(hAPP(hAPP(iPr_def_10,c_Lambda_OdB_OVar(hAPP(hAPP(iPr_def_11,v_ia),iPr_def_12))),hAPP(hAPP(iPr_def_11,X0),iPr_def_12)),hAPP(hAPP(iPr_def_13,iPr_def_28),X0),iPr_def_14),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,iPr_def_28,tc_Lambda_OdB,tc_Lambda_OdB,iPr_def_15),X0,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(superposition,[status(thm)],[c_14129,c_14139]) ).
tcf(c_18916,plain,
! [X0: $i] : hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(iPr_def_13,iPr_def_28),X0))),
inference(superposition,[status(thm)],[c_14129,c_14142]) ).
tcf(c_18917,plain,
! [X0: $i] : hBOOL(hAPP(c_InductTermi_OIT,hAPP(iPr_def_29,X0))),
inference(light_normalisation,[status(thm)],[c_18916,c_14130]) ).
tcf(c_18918,plain,
! [X0: $i] : hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(hAPP(iPr_def_22,hAPP(hAPP(iPr_def_11,X0),iPr_def_12)),hAPP(iPr_def_29,X0),iPr_def_14),c_List_Omap(c_COMBC(iPr_def_32,X0,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(light_normalisation,[status(thm)],[c_18915,c_14120,c_14121,c_14122,c_14123,c_14130,c_14133]) ).
tcf(c_18978,plain,
hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(hAPP(iPr_def_22,hAPP(iPr_def_23,iPr_def_12)),hAPP(iPr_def_29,v_ja),iPr_def_14),c_List_Omap(c_COMBC(iPr_def_32,v_ja,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),v_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB))),
inference(superposition,[status(thm)],[c_14124,c_18918]) ).
tcf(c_18985,plain,
hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(iPr_def_25,iPr_def_30,iPr_def_14),iPr_def_34,tc_Lambda_OdB,tc_Lambda_OdB))),
inference(light_normalisation,[status(thm)],[c_18978,c_14125,c_14126,c_14131,c_14134,c_14135]) ).
tcf(c_19030,plain,
hBOOL(hAPP(c_InductTermi_OIT,iPr_def_30)),
inference(superposition,[status(thm)],[c_14131,c_18917]) ).
tcf(c_19066,plain,
c_Type_Otyping(iPr_def_27,c_Lambda_OdB_OVar(iPr_def_30),iPr_def_31),
inference(superposition,[status(thm)],[c_14132,c_1025]) ).
tcf(c_19067,plain,
c_Type_Otyping(c_InductTermi_OIT,c_Lambda_OdB_OVar(iPr_def_35),iPr_def_36),
inference(superposition,[status(thm)],[c_14137,c_1025]) ).
tcf(c_19238,plain,
! [X0: $i,X1: $i,X2: $i] :
( 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)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X1))
| ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(X0,X1,iPr_def_14),X2,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(light_normalisation,[status(thm)],[c_6756,c_14115]) ).
tcf(c_19248,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,iPr_def_26),X0),X1,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X0))
| ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(iPr_def_25,X0,iPr_def_14),X1,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(superposition,[status(thm)],[c_14127,c_19238]) ).
tcf(c_19250,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(iPr_def_27,X0),X1,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,X0))
| ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubstn(iPr_def_25,X0,iPr_def_14),X1,tc_Lambda_OdB,tc_Lambda_OdB))) ),
inference(light_normalisation,[status(thm)],[c_19248,c_14128]) ).
tcf(c_19718,plain,
hAPP(iPr_def_27,iPr_def_30) = iPr_def_31,
inference(superposition,[status(thm)],[c_19066,c_1024]) ).
tcf(c_19719,plain,
hAPP(c_InductTermi_OIT,iPr_def_35) = iPr_def_36,
inference(superposition,[status(thm)],[c_19067,c_1024]) ).
tcf(c_22099,plain,
( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(iPr_def_27,iPr_def_30),iPr_def_34,tc_Lambda_OdB,tc_Lambda_OdB)))
| ~ hBOOL(hAPP(c_InductTermi_OIT,iPr_def_30)) ),
inference(superposition,[status(thm)],[c_18985,c_19250]) ).
tcf(c_22101,plain,
( hBOOL(iPr_def_36)
| ~ hBOOL(hAPP(c_InductTermi_OIT,iPr_def_30)) ),
inference(light_normalisation,[status(thm)],[c_22099,c_14136,c_19718,c_19719]) ).
tcf(c_22102,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_22101,c_14141,c_19030]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL759-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/5.36 % Computer : n019.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Thu Sep 24 00:26:26 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.41 Running first-order theorem proving
% 0.14/5.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.42
% 0.14/5.42 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.42
% 0.14/5.42 % Detected problem language: tptp
% 0.14/5.43 % Proving...
% 2.34/6.75 % SZS status Started for theBenchmark.p
% 2.34/6.75 % SZS status Unsatisfiable for theBenchmark.p
% 2.34/6.75
% 2.34/6.75 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.34/6.75
% 2.34/6.75 % ------ iProver source info
% 2.34/6.75
% 2.34/6.75 % git: date: 2026-07-19 20:42:38 +0200
% 2.34/6.75 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.34/6.75 % git: non_committed_changes: false
% 2.34/6.75
% 2.34/6.75 % ------ Parsing...% successful
% 2.34/6.75
% 2.34/6.75
% 2.34/6.75 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.34/6.75
% 2.34/6.75 % ------ Preprocessing... sup_sim: 56 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 30 sf_s rm: 30 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 30 0s sf_e pe_s pe_e %
% 2.34/6.75
% 2.34/6.75 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.34/6.75
% 2.34/6.75 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.34/6.75 % ------ Proving...
% 2.34/6.75 % ------ Problem Properties
% 2.34/6.75
% 2.34/6.75 %
% 2.34/6.75 % clauses 339
% 2.34/6.75 % conjectures 3
% 2.34/6.75 % EPR 18
% 2.34/6.75 % Horn 291
% 2.34/6.75 % unary 146
% 2.34/6.75 % binary 115
% 2.34/6.75 % lits 616
% 2.34/6.75 % lits eq 285
% 2.34/6.75 % fd_pure 0
% 2.34/6.75 % fd_pseudo 0
% 2.34/6.75 % fd_cond 33
% 2.34/6.75 % fd_pseudo_cond 29
% 2.34/6.75 % AC symbols 0
% 2.34/6.75
% 2.34/6.75 % ------ Schedule dynamic 5 is on
% 2.34/6.75
% 2.34/6.75 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.34/6.75
% 2.34/6.75
% 2.34/6.75 % ------
% 2.34/6.75 % Current options:
% 2.34/6.75 % ------
% 2.34/6.75
% 2.34/6.75
% 2.34/6.75 %
% 2.34/6.75
% 2.34/6.75 % ------ Proving...
% 2.34/6.75 %
% 2.34/6.75
% 2.34/6.75 % SZS status Unsatisfiable for theBenchmark.p
% 2.34/6.75
% 2.34/6.75 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.34/6.76
% 2.34/6.76
%------------------------------------------------------------------------------