%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL786-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:11:07 PM UTC 2026
% Result : Unsatisfiable 119.84s 15.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL786-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 01:04:20 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 119.84/15.79 % Refutation found
% 119.84/15.79 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 119.84/15.79 % SZS output start CNFRefutation for theBenchmark
% 119.84/15.79 fof(f298,axiom,(
% 119.84/15.79 (![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) ))),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f432,axiom,(
% 119.84/15.79 v_n____ = v_i____ ),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f439,axiom,(
% 119.84/15.79 (![V_e,V_t,V_T,V_ts]: (( 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)))| ~ 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)) ) ))),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f441,axiom,(
% 119.84/15.79 (![V_Ts]: (( v_thesis____| ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,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))) ) ))),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f443,axiom,(
% 119.84/15.79 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____)) ),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f449,axiom,(
% 119.84/15.79 (![V_e,V_ts,V_T,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))| ~ 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)) ) ))),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f465,axiom,(
% 119.84/15.79 v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB) ),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f475,negated_conjecture,(
% 119.84/15.79 ~ v_thesis____ ),
% 119.84/15.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 119.84/15.79 fof(f932,plain,(
% 119.84/15.79 ![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))),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f298])).
% 119.84/15.79 fof(f1131,plain,(
% 119.84/15.79 v_n____=v_i____),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f432])).
% 119.84/15.79 fof(f1138,plain,(
% 119.84/15.79 ![X0,X1,X2,X3]: (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)))|~hBOOL(hAPP(hAPP(c_Type_Otyping(X0),c_List_Ofoldl(c_Lambda_OdB_OApp,X1,X3,tc_Lambda_OdB,tc_Lambda_OdB)),X2)))),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f439])).
% 119.84/15.79 fof(f1140,plain,(
% 119.84/15.79 ![X0]: (v_thesis____|~c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,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))))),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f441])).
% 119.84/15.79 fof(f1142,plain,(
% 119.84/15.79 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____))),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f443])).
% 119.84/15.79 fof(f1149,plain,(
% 119.84/15.79 ![X0,X1,X2,X3]: (c_Type_Otypings(X0,X1,c_Type_Osko__Type__Xlist__app__typeE__1__1(X2,X0,X3,X1))|~hBOOL(hAPP(hAPP(c_Type_Otyping(X0),c_List_Ofoldl(c_Lambda_OdB_OApp,X3,X1,tc_Lambda_OdB,tc_Lambda_OdB)),X2)))),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f449])).
% 119.84/15.79 fof(f1173,plain,(
% 119.84/15.79 v_rs____=c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB)),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f465])).
% 119.84/15.79 fof(f1186,plain,(
% 119.84/15.79 ~v_thesis____),
% 119.84/15.79 inference(cnf_transformation,[status(thm)],[f475])).
% 119.84/15.79 fof(f1212,definition,(
% 119.84/15.79 sQ0_spl <=> (v_thesis____)),
% 119.84/15.79 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 119.84/15.80 fof(f1213,plain,(
% 119.84/15.80 v_thesis____|~sQ0_spl),
% 119.84/15.80 inference(component_clause,[status(thm)],[f1212])).
% 119.84/15.80 fof(f1215,definition,(
% 119.84/15.80 ![X0]: (sQ1_spl <=> (~c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,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)))))),
% 119.84/15.80 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 119.84/15.80 fof(f1216,plain,(
% 119.84/15.80 ![X0]: (~c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,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)))|~sQ1_spl)),
% 119.84/15.80 inference(component_clause,[status(thm)],[f1215])).
% 119.84/15.80 fof(f1218,plain,(
% 119.84/15.80 sQ0_spl|sQ1_spl),
% 119.84/15.80 inference(split_clause,[status(thm)],[f1140,f1212,f1215])).
% 119.84/15.80 fof(f1219,plain,(
% 119.84/15.80 $false|~sQ0_spl),
% 119.84/15.80 inference(forward_subsumption_resolution,[status(thm)],[f1213,f1186])).
% 119.84/15.80 fof(f1220,plain,(
% 119.84/15.80 ~sQ0_spl),
% 119.84/15.80 inference(contradiction_clause,[status(thm)],[f1219])).
% 119.84/15.80 fof(f1232,plain,(
% 119.84/15.80 ![X0]: (~c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,X0)|~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)))|~sQ1_spl)),
% 119.84/15.80 inference(backward_demodulation,[status(thm)],[f1131,f1216])).
% 119.84/15.80 fof(f1233,plain,(
% 119.84/15.80 ![X0]: (~c_Type_Otypings(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_as____,X0)|~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)))|~sQ1_spl)),
% 119.84/15.80 inference(forward_demodulation,[status(thm)],[f1131,f1232])).
% 119.84/15.80 fof(f35494,plain,(
% 119.84/15.80 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____))),
% 119.84/15.80 inference(forward_demodulation,[status(thm)],[f1131,f1142])).
% 119.84/15.80 fof(f35853,plain,(
% 119.84/15.80 ![X0,X1]: (~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))|~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)))|~sQ1_spl)),
% 119.84/15.80 inference(resolution,[status(thm)],[f1149,f1233])).
% 119.84/15.80 fof(f36037,definition,(
% 119.84/15.80 sQ414_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____)))),
% 119.84/15.80 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 119.84/15.80 fof(f36039,plain,(
% 119.84/15.80 ~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____))|sQ414_spl),
% 119.84/15.80 inference(component_clause,[status(thm)],[f36037])).
% 119.84/15.80 fof(f38419,plain,(
% 119.84/15.80 ~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____))|~sQ1_spl),
% 119.84/15.85 inference(resolution,[status(thm)],[f35853,f1138])).
% 119.84/15.85 fof(f38420,plain,(
% 119.84/15.85 ~sQ414_spl|~sQ1_spl),
% 119.84/15.85 inference(split_clause,[status(thm)],[f38419,f36037,f1215])).
% 119.84/15.85 fof(f38421,plain,(
% 119.84/15.85 ~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____))|sQ414_spl),
% 119.84/15.85 inference(paramodulation,[status(thm)],[f932,f36039])).
% 119.84/15.85 fof(f38422,plain,(
% 119.84/15.85 ~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____))|sQ414_spl),
% 119.84/15.85 inference(forward_demodulation,[status(thm)],[f1173,f38421])).
% 119.84/15.85 fof(f38423,plain,(
% 119.84/15.85 $false|sQ414_spl),
% 119.84/15.85 inference(forward_subsumption_resolution,[status(thm)],[f38422,f35494])).
% 119.84/15.85 fof(f38424,plain,(
% 119.84/15.85 sQ414_spl),
% 119.84/15.85 inference(contradiction_clause,[status(thm)],[f38423])).
% 119.84/15.85 fof(f38425,plain,(
% 119.84/15.85 $false),
% 119.84/15.85 inference(sat_refutation,[status(thm)],[f1218,f1220,f38420,f38424])).
% 119.84/15.85 % SZS output end CNFRefutation for theBenchmark.p
% 15.61/15.97 % Elapsed time: 15.563759 seconds
% 15.61/15.97 % CPU time: 122.443800 seconds
% 15.61/15.97 % Total memory used: 1.121 GB
% 15.61/15.97 % Net memory used: 1.066 GB
%------------------------------------------------------------------------------