%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV963-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 : n018.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 02:53:24 PM UTC 2026
% Result : Unsatisfiable 4.87s 1.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV963-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n018.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 09:36:29 UTC 2026
% 0.01/0.36 % CPUTime :
% 0.24/0.50 % Drodi V4.1.1
% 4.87/1.84 % Refutation found
% 4.87/1.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.87/1.84 % SZS output start CNFRefutation for theBenchmark
% 4.87/1.84 fof(f408,axiom,(
% 4.87/1.84 c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f434,axiom,(
% 4.87/1.84 (![V_E,V_T]: (( c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(V_E,v_P,V_T,v_e_092_060_094isub_0622_H____,v_h_Ha____))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_e_092_060_094isub_0622____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f437,axiom,(
% 4.87/1.84 (![V_E,V_T]: (( hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(V_E,v_P,V_T,v_e_092_060_094isub_0622_H____,v_h_Ha____)),V_T))| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_e_092_060_094isub_0622____,V_T)| ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))) ) ))),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f439,axiom,(
% 4.87/1.84 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____) ),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f455,axiom,(
% 4.87/1.84 (![V_T_092_060_094isub_0622_H]: (( v_thesis____| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),V_T_092_060_094isub_0622_H),v_T_092_060_094isub_0622____))| ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,V_T_092_060_094isub_0622_H) ) ))),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f461,negated_conjecture,(
% 4.87/1.84 ~ v_thesis____ ),
% 4.87/1.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.84 fof(f1039,plain,(
% 4.87/1.84 c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f408])).
% 4.87/1.84 fof(f1082,plain,(
% 4.87/1.84 ![V_E]: ((![V_T]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,V_E,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(V_E,v_P,V_T,v_e_092_060_094isub_0622_H____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_e_092_060_094isub_0622____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 4.87/1.84 inference(miniscoping,[status(thm)],[f434])).
% 4.87/1.84 fof(f1083,plain,(
% 4.87/1.84 ![X0,X1]: (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,X0,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(X0,v_P,X1,v_e_092_060_094isub_0622_H____,v_h_Ha____))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_e_092_060_094isub_0622____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f1082])).
% 4.87/1.84 fof(f1088,plain,(
% 4.87/1.84 ![V_E]: ((![V_T]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(V_E,v_P,V_T,v_e_092_060_094isub_0622_H____,v_h_Ha____)),V_T))|~c_WellTypeRT_OWTrt(v_P,v_ha____,V_E,v_e_092_060_094isub_0622____,V_T)))|~c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 4.87/1.84 inference(miniscoping,[status(thm)],[f437])).
% 4.87/1.84 fof(f1089,plain,(
% 4.87/1.84 ![X0,X1]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(X0,v_P,X1,v_e_092_060_094isub_0622_H____,v_h_Ha____)),X1))|~c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_e_092_060_094isub_0622____,X1)|~c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f1088])).
% 4.87/1.84 fof(f1092,plain,(
% 4.87/1.84 c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____)),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f439])).
% 4.87/1.84 fof(f1117,plain,(
% 4.87/1.84 ![X0]: (v_thesis____|~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),v_T_092_060_094isub_0622____))|~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,X0))),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f455])).
% 4.87/1.84 fof(f1124,plain,(
% 4.87/1.84 ~v_thesis____),
% 4.87/1.84 inference(cnf_transformation,[status(thm)],[f461])).
% 4.87/1.84 fof(f1129,definition,(
% 4.87/1.84 sQ0_spl <=> (v_thesis____)),
% 4.87/1.84 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 4.87/1.84 fof(f1130,plain,(
% 4.87/1.84 v_thesis____|~sQ0_spl),
% 4.87/1.84 inference(component_clause,[status(thm)],[f1129])).
% 4.87/1.84 fof(f1132,definition,(
% 4.87/1.84 ![X0]: (sQ1_spl <=> (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),v_T_092_060_094isub_0622____))|~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,X0)))),
% 4.87/1.84 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 4.87/1.84 fof(f1133,plain,(
% 4.87/1.84 ![X0]: (~hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X0),v_T_092_060_094isub_0622____))|~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,X0)|~sQ1_spl)),
% 4.87/1.84 inference(component_clause,[status(thm)],[f1132])).
% 4.87/1.84 fof(f1135,plain,(
% 4.87/1.84 sQ0_spl|sQ1_spl),
% 4.87/1.84 inference(split_clause,[status(thm)],[f1117,f1129,f1132])).
% 4.87/1.84 fof(f1137,plain,(
% 4.87/1.84 $false|~sQ0_spl),
% 4.87/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1130,f1124])).
% 4.87/1.84 fof(f1138,plain,(
% 4.87/1.84 ~sQ0_spl),
% 4.87/1.84 inference(contradiction_clause,[status(thm)],[f1137])).
% 4.87/1.84 fof(f3599,plain,(
% 4.87/1.84 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),
% 4.87/1.84 inference(resolution,[status(thm)],[f1083,f1092])).
% 4.87/1.84 fof(f3600,definition,(
% 4.87/1.84 sQ10_spl <=> (c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____)))),
% 4.87/1.84 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 4.87/1.84 fof(f3601,plain,(
% 4.87/1.84 c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____))|~sQ10_spl),
% 4.87/1.84 inference(component_clause,[status(thm)],[f3600])).
% 4.87/1.84 fof(f3603,definition,(
% 4.87/1.84 sQ11_spl <=> (c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval)))))),
% 4.87/1.84 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 4.87/1.84 fof(f3605,plain,(
% 4.87/1.84 ~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))|sQ11_spl),
% 4.87/1.84 inference(component_clause,[status(thm)],[f3603])).
% 4.87/1.84 fof(f3606,plain,(
% 4.87/1.84 sQ10_spl|~sQ11_spl),
% 4.87/1.84 inference(split_clause,[status(thm)],[f3599,f3600,f3603])).
% 4.87/1.84 fof(f3646,plain,(
% 4.87/1.84 $false|sQ11_spl),
% 4.87/1.84 inference(forward_subsumption_resolution,[status(thm)],[f3605,f1039])).
% 4.87/1.84 fof(f3647,plain,(
% 4.87/1.84 sQ11_spl),
% 4.87/1.84 inference(contradiction_clause,[status(thm)],[f3646])).
% 4.87/1.84 fof(f3655,plain,(
% 4.87/1.84 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____)),v_T_092_060_094isub_0622____))|~c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_ha____,v_la____,tc_fun(tc_nat,tc_Option_Ooption(tc_prod(tc_List_Olist(tc_String_Ochar),tc_fun(tc_prod(tc_List_Olist(tc_String_Ochar),tc_List_Olist(tc_String_Ochar)),tc_Option_Ooption(tc_Value_Oval))))),tc_fun(tc_List_Olist(tc_String_Ochar),tc_Option_Ooption(tc_Value_Oval))))),
% 4.87/1.84 inference(resolution,[status(thm)],[f1089,f1092])).
% 4.87/1.84 fof(f3656,definition,(
% 4.87/1.84 sQ14_spl <=> (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____)),v_T_092_060_094isub_0622____)))),
% 4.87/1.84 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 4.87/1.84 fof(f3657,plain,(
% 4.87/1.84 hBOOL(hAPP(hAPP(c_TypeRel_Owiden(v_P,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____)),v_T_092_060_094isub_0622____))|~sQ14_spl),
% 4.87/1.84 inference(component_clause,[status(thm)],[f3656])).
% 4.87/1.84 fof(f3659,plain,(
% 4.87/1.84 sQ14_spl|~sQ11_spl),
% 4.87/1.84 inference(split_clause,[status(thm)],[f3655,f3656,f3603])).
% 4.87/1.84 fof(f3698,plain,(
% 4.87/1.84 ~c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622_H____,v_sko__local__XFAssRed2__Xhyps__2__1(v_E____,v_P,v_T_092_060_094isub_0622____,v_e_092_060_094isub_0622_H____,v_h_Ha____))|~sQ14_spl|~sQ1_spl),
% 4.87/1.84 inference(resolution,[status(thm)],[f3657,f1133])).
% 4.87/1.84 fof(f3707,plain,(
% 4.87/1.84 $false|~sQ10_spl|~sQ14_spl|~sQ1_spl),
% 4.87/1.84 inference(forward_subsumption_resolution,[status(thm)],[f3698,f3601])).
% 4.87/1.84 fof(f3708,plain,(
% 4.87/1.84 ~sQ10_spl|~sQ14_spl|~sQ1_spl),
% 4.87/1.84 inference(contradiction_clause,[status(thm)],[f3707])).
% 4.87/1.84 fof(f3709,plain,(
% 4.87/1.84 $false),
% 4.87/1.84 inference(sat_refutation,[status(thm)],[f1135,f1138,f3606,f3647,f3659,f3708])).
% 4.87/1.89 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/2.04 % Elapsed time: 1.664861 seconds
% 1.30/2.04 % CPU time: 11.170145 seconds
% 1.30/2.04 % Total memory used: 364.193 MB
% 1.30/2.04 % Net memory used: 358.837 MB
%------------------------------------------------------------------------------