%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL787-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 : n015.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 67.41s 9.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL787-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n015.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 01:07:20 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 67.41/9.11 % Refutation found
% 67.41/9.11 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 67.41/9.11 % SZS output start CNFRefutation for theBenchmark
% 67.41/9.11 fof(f219,axiom,(
% 67.41/9.11 (![V_e,V_u,V_T,V_t]: (( c_Type_Otyping(V_e,V_u,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u))| ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ))),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f329,axiom,(
% 67.41/9.11 v_n____ = v_i____ ),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f335,axiom,(
% 67.41/9.11 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)) ),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f346,axiom,(
% 67.41/9.11 (![V_T_H_H]: (( v_thesis____| ~ c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,V_T_H_H)| ~ c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,V_T_H_H),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) ) ))),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f353,axiom,(
% 67.41/9.11 (![V_e,V_t,V_T,V_u]: (( c_Type_Otyping(V_e,V_t,hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)),V_T))| ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ))),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f356,negated_conjecture,(
% 67.41/9.11 ~ v_thesis____ ),
% 67.41/9.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 67.41/9.11 fof(f711,plain,(
% 67.41/9.11 ![X0,X1,X2,X3]: (c_Type_Otyping(X0,X1,c_Type_Osko__Type__Xtyping__elims__2__1(X2,X0,X3,X1))|~c_Type_Otyping(X0,hAPP(hAPP(c_Lambda_OdB_OApp,X3),X1),X2))),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f219])).
% 67.41/9.11 fof(f875,plain,(
% 67.41/9.11 v_n____=v_i____),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f329])).
% 67.41/9.11 fof(f881,plain,(
% 67.41/9.11 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))),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f335])).
% 67.41/9.11 fof(f893,plain,(
% 67.41/9.11 ![X0]: (v_thesis____|~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,X0)|~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,X0),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))))),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f346])).
% 67.41/9.11 fof(f903,plain,(
% 67.41/9.11 ![X0,X1,X2,X3]: (c_Type_Otyping(X0,X1,hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__2__1(X2,X0,X1,X3)),X2))|~c_Type_Otyping(X0,hAPP(hAPP(c_Lambda_OdB_OApp,X1),X3),X2))),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f353])).
% 67.41/9.11 fof(f906,plain,(
% 67.41/9.11 ~v_thesis____),
% 67.41/9.11 inference(cnf_transformation,[status(thm)],[f356])).
% 67.41/9.11 fof(f932,definition,(
% 67.41/9.11 sQ0_spl <=> (v_thesis____)),
% 67.41/9.11 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 67.41/9.11 fof(f933,plain,(
% 67.41/9.11 v_thesis____|~sQ0_spl),
% 67.41/9.11 inference(component_clause,[status(thm)],[f932])).
% 67.41/9.11 fof(f935,definition,(
% 67.41/9.11 ![X0]: (sQ1_spl <=> (~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,X0)|~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,X0),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)))))),
% 67.41/9.11 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 67.41/9.11 fof(f936,plain,(
% 67.41/9.11 ![X0]: (~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,X0)|~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,X0),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)))|~sQ1_spl)),
% 67.41/9.11 inference(component_clause,[status(thm)],[f935])).
% 67.41/9.11 fof(f938,plain,(
% 67.41/9.11 sQ0_spl|sQ1_spl),
% 67.41/9.11 inference(split_clause,[status(thm)],[f893,f932,f935])).
% 68.19/9.20 fof(f969,plain,(
% 68.19/9.20 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,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))),
% 68.19/9.20 inference(forward_demodulation,[status(thm)],[f875,f881])).
% 68.19/9.20 fof(f974,plain,(
% 68.19/9.20 $false|~sQ0_spl),
% 68.19/9.20 inference(forward_subsumption_resolution,[status(thm)],[f933,f906])).
% 68.19/9.20 fof(f975,plain,(
% 68.19/9.20 ~sQ0_spl),
% 68.19/9.20 inference(contradiction_clause,[status(thm)],[f974])).
% 68.19/9.20 fof(f979,plain,(
% 68.19/9.20 ![X0]: (~c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_a____,X0)|~c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,X0),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)))|~sQ1_spl)),
% 68.19/9.20 inference(forward_demodulation,[status(thm)],[f875,f936])).
% 68.19/9.20 fof(f980,plain,(
% 68.19/9.20 ![X0]: (~c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_a____,X0)|~c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,X0),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)))|~sQ1_spl)),
% 68.19/9.20 inference(forward_demodulation,[status(thm)],[f875,f979])).
% 68.19/9.20 fof(f2212,plain,(
% 68.19/9.20 c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_a____,c_Type_Osko__Type__Xtyping__elims__2__1(c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_a____))),
% 68.19/9.20 inference(resolution,[status(thm)],[f969,f711])).
% 68.19/9.20 fof(f2250,plain,(
% 68.19/9.20 c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__2__1(c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),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)))),
% 68.19/9.20 inference(resolution,[status(thm)],[f903,f969])).
% 68.19/9.20 fof(f14079,plain,(
% 68.19/9.20 ~c_Type_Otyping(c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),v_a____,c_Type_Osko__Type__Xtyping__elims__2__1(c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype),c_Type_Oshift(v_e____,v_n____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),v_a____))|~sQ1_spl),
% 68.19/9.20 inference(resolution,[status(thm)],[f2250,f980])).
% 68.19/9.20 fof(f14100,plain,(
% 68.19/9.20 $false|~sQ1_spl),
% 68.19/9.20 inference(forward_subsumption_resolution,[status(thm)],[f14079,f2212])).
% 68.19/9.20 fof(f14101,plain,(
% 68.19/9.20 ~sQ1_spl),
% 68.19/9.20 inference(contradiction_clause,[status(thm)],[f14100])).
% 68.19/9.20 fof(f14102,plain,(
% 68.19/9.20 $false),
% 68.19/9.20 inference(sat_refutation,[status(thm)],[f938,f975,f14101])).
% 68.19/9.20 % SZS output end CNFRefutation for theBenchmark.p
% 2.02/9.22 % Elapsed time: 8.776117 seconds
% 2.02/9.22 % CPU time: 68.772606 seconds
% 2.02/9.22 % Total memory used: 555.958 MB
% 2.02/9.22 % Net memory used: 531.392 MB
%------------------------------------------------------------------------------