%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL786-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:08:48 PM UTC 2026
% Result : Unsatisfiable 2.43s 0.78s
% Output : CNFRefutation 2.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of formulae : 36 ( 14 unt; 3 def)
% Number of atoms : 66 ( 6 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 65 ( 35 ~; 27 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-5 aty)
% Number of variables : 36 ( 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f298,axiom,
! [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),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f432,axiom,
v_n____ = v_i____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f439,axiom,
! [V_e,V_t,V_T,V_ts] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_T))
| hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t),c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xlist__app__typeE__1__1(V_T,V_e,V_t,V_ts),V_T,tc_Type_Otype,tc_Type_Otype))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f441,axiom,
! [V_Ts] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,V_Ts,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,V_Ts)
| v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f443,axiom,
hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f449,axiom,
! [V_e,V_ts,V_T,V_t] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_T))
| c_Type_Otypings(V_e,V_ts,c_Type_Osko__Type__Xlist__app__typeE__1__1(V_T,V_e,V_t,V_ts)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f465,axiom,
v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f475,negated_conjecture,
~ v_thesis____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f932,plain,
! [X0,X1,X2,X3,X4,X5] : 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(thm)],[f298]) ).
fof(f1131,plain,
v_n____ = v_i____,
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f1138,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(X0),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X3,tc_Lambda_OdB,tc_Lambda_OdB)),X2))
| hBOOL(hAPP(hAPP(c_Type_Otyping(X0),X1),c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xlist__app__typeE__1__1(X2,X0,X1,X3),X2,tc_Type_Otype,tc_Type_Otype))) ),
inference(cnf_transformation,[status(thm)],[f439]) ).
fof(f1140,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,X0,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,X0)
| v_thesis____ ),
inference(cnf_transformation,[status(thm)],[f441]) ).
fof(f1142,plain,
hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f1149,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(X0),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X1,tc_Lambda_OdB,tc_Lambda_OdB)),X2))
| c_Type_Otypings(X0,X1,c_Type_Osko__Type__Xlist__app__typeE__1__1(X2,X0,X3,X1)) ),
inference(cnf_transformation,[status(thm)],[f449]) ).
fof(f1173,plain,
v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),
inference(cnf_transformation,[status(thm)],[f465]) ).
fof(f1186,plain,
~ v_thesis____,
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f1212,definition,
( sQ0_spl
<=> v_thesis____ ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1213,plain,
( ~ sQ0_spl
| v_thesis____ ),
inference(component_clause,[status(thm)],[f1212]) ).
fof(f1215,definition,
! [X0] :
( sQ1_spl
<=> ( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,X0,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1216,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,X0,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,X0) ),
inference(component_clause,[status(thm)],[f1215]) ).
fof(f1218,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1140,f1212,f1215]) ).
fof(f1219,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1213,f1186]) ).
fof(f1220,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f1219]) ).
fof(f1221,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,X0,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,X0) ),
inference(backward_demodulation,[status(thm)],[f1131,f1216]) ).
fof(f1222,plain,
! [X0] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,X0,v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_as____,X0) ),
inference(forward_demodulation,[status(thm)],[f1131,f1221]) ).
fof(f4731,plain,
hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)),
inference(forward_demodulation,[status(thm)],[f1131,f1142]) ).
fof(f4860,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____)),c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xlist__app__typeE__1__1(X1,c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),X0,v_as____),v_T_H____,tc_Type_Otype,tc_Type_Otype)))
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,X0,v_as____,tc_Lambda_OdB,tc_Lambda_OdB)),X1)) ),
inference(resolution,[status(thm)],[f1149,f1222]) ).
fof(f4924,plain,
( ~ sQ1_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____))
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)) ),
inference(resolution,[status(thm)],[f4860,f1138]) ).
fof(f4925,definition,
( sQ63_spl
<=> hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f4927,plain,
( sQ63_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)) ),
inference(component_clause,[status(thm)],[f4925]) ).
fof(f4928,plain,
( ~ sQ1_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f4924,f4925,f1215]) ).
fof(f4929,plain,
( sQ63_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)) ),
inference(paramodulation,[status(thm)],[f932,f4927]) ).
fof(f4930,plain,
( sQ63_spl
| ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype)),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB)),v_T_H____)) ),
inference(forward_demodulation,[status(thm)],[f1173,f4929]) ).
fof(f4931,plain,
( sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4930,f4731]) ).
fof(f4932,plain,
sQ63_spl,
inference(contradiction_clause,[status(thm)],[f4931]) ).
fof(f4933,plain,
$false,
inference(sat_refutation,[status(thm)],[f1218,f1220,f4928,f4932]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL786-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n019.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 01:04:20 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 2.43/0.78 % Refutation found
% 2.43/0.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.43/0.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.06/0.84 % Elapsed time: 0.466465 seconds
% 2.06/0.84 % CPU time: 2.962750 seconds
% 2.06/0.84 % Total memory used: 170.449 MB
% 2.06/0.84 % Net memory used: 168.149 MB
%------------------------------------------------------------------------------