%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV982-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:26 PM UTC 2026
% Result : Unsatisfiable 95.22s 12.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV982-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n006.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 09:35:27 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 95.22/12.64 % Refutation found
% 95.22/12.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 95.22/12.64 % SZS output start CNFRefutation for theBenchmark
% 95.22/12.64 fof(f179,axiom,(
% 95.22/12.64 (![V_P,V_h,V_E,V_e_092_060_094isub_0621,V_C,V_T,V_V,V_e_092_060_094isub_0622]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__5__1(V_C,V_E,V_P,V_T,V_V,V_e_092_060_094isub_0621,V_e_092_060_094isub_0622,V_h))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OTryCatch(V_e_092_060_094isub_0621,V_C,V_V,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f383,axiom,(
% 95.22/12.64 (![V_E,V_P,V_e,V_h,V_T]: (( c_Type_Ois__refT(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(V_E,V_P,V_e,V_h))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f411,axiom,(
% 95.22/12.64 (![V_P,V_h,V_E,V_e,V_T,V_T_092_060_094isub_062r]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T)| ~ c_Type_Ois__refT(V_T_092_060_094isub_062r)| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T_092_060_094isub_062r) ) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f412,axiom,(
% 95.22/12.64 (![V_P,V_h,V_E,V_e,V_T]: (( c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(V_E,V_P,V_e,V_h))| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T) ) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f415,axiom,(
% 95.22/12.64 c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_OTryCatch(c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),v_C______,v_V______,v_e_092_060_094isub_0622______,tc_List_Olist(tc_String_Ochar)),v_T____) ),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f420,axiom,(
% 95.22/12.64 (![V_P,T_a,V_T]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_T),V_T)) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f427,negated_conjecture,(
% 95.22/12.64 (![V_x]: (( ~ 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_x),v_T____))| ~ c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),V_x) ) ))),
% 95.22/12.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 95.22/12.64 fof(f653,plain,(
% 95.22/12.64 ![X0,X1,X2,X3,X4,X5,X6,X7]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__5__1(X4,X2,X0,X5,X6,X3,X7,X1))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OTryCatch(X3,X4,X6,X7,tc_List_Olist(tc_String_Ochar)),X5))),
% 95.22/12.64 inference(cnf_transformation,[status(thm)],[f179])).
% 95.22/12.64 fof(f908,plain,(
% 95.22/12.64 ![V_E,V_P,V_e,V_h]: (c_Type_Ois__refT(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(V_E,V_P,V_e,V_h))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 95.22/12.64 inference(miniscoping,[status(thm)],[f383])).
% 95.22/12.64 fof(f909,plain,(
% 95.22/12.64 ![X0,X1,X2,X3,X4]: (c_Type_Ois__refT(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(X0,X1,X2,X3))|~c_WellTypeRT_OWTrt(X1,X3,X0,c_Expr_Oexp_Othrow(X2,tc_List_Olist(tc_String_Ochar)),X4))),
% 95.22/12.64 inference(cnf_transformation,[status(thm)],[f908])).
% 95.22/12.64 fof(f947,plain,(
% 95.22/12.64 ![V_P,V_h,V_E,V_e,V_T_092_060_094isub_062r]: (((![V_T]: c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T))|~c_Type_Ois__refT(V_T_092_060_094isub_062r))|~c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T_092_060_094isub_062r))),
% 95.22/12.64 inference(miniscoping,[status(thm)],[f411])).
% 95.22/12.64 fof(f948,plain,(
% 95.22/12.64 ![X0,X1,X2,X3,X4,X5]: (c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_Othrow(X3,tc_List_Olist(tc_String_Ochar)),X4)|~c_Type_Ois__refT(X5)|~c_WellTypeRT_OWTrt(X0,X1,X2,X3,X5))),
% 95.22/12.64 inference(cnf_transformation,[status(thm)],[f947])).
% 95.22/12.64 fof(f949,plain,(
% 95.22/12.64 ![V_P,V_h,V_E,V_e]: (c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(V_E,V_P,V_e,V_h))|(![V_T]: ~c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_Othrow(V_e,tc_List_Olist(tc_String_Ochar)),V_T)))),
% 95.22/12.68 inference(miniscoping,[status(thm)],[f412])).
% 95.22/12.68 fof(f950,plain,(
% 95.22/12.68 ![X0,X1,X2,X3,X4]: (c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(X2,X0,X3,X1))|~c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_Othrow(X3,tc_List_Olist(tc_String_Ochar)),X4))),
% 95.22/12.68 inference(cnf_transformation,[status(thm)],[f949])).
% 95.22/12.68 fof(f953,plain,(
% 95.22/12.68 c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_OTryCatch(c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),v_C______,v_V______,v_e_092_060_094isub_0622______,tc_List_Olist(tc_String_Ochar)),v_T____)),
% 95.22/12.68 inference(cnf_transformation,[status(thm)],[f415])).
% 95.22/12.68 fof(f960,plain,(
% 95.22/12.68 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X2)))),
% 95.22/12.68 inference(cnf_transformation,[status(thm)],[f420])).
% 95.22/12.68 fof(f968,plain,(
% 95.22/12.68 ![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____))|~c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),X0))),
% 95.22/12.68 inference(cnf_transformation,[status(thm)],[f427])).
% 95.22/12.68 fof(f975,plain,(
% 95.22/12.68 ~c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),v_T____)),
% 95.22/12.68 inference(resolution,[status(thm)],[f960,f968])).
% 95.22/12.68 fof(f1833,plain,(
% 95.22/12.68 c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__5__1(v_C______,v_E____,v_P,v_T____,v_V______,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),v_e_092_060_094isub_0622______,v_a______))),
% 95.22/12.68 inference(resolution,[status(thm)],[f953,f653])).
% 95.22/12.68 fof(f7313,plain,(
% 95.22/12.68 c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(v_E____,v_P,c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),v_a______))),
% 95.22/12.68 inference(resolution,[status(thm)],[f1833,f950])).
% 95.22/12.68 fof(f7314,plain,(
% 95.22/12.68 c_Type_Ois__refT(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(v_E____,v_P,c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),v_a______))),
% 95.22/12.68 inference(resolution,[status(thm)],[f1833,f909])).
% 95.22/12.68 fof(f7616,plain,(
% 95.22/12.68 ![X0,X1,X2,X3,X4]: (c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_Othrow(X3,tc_List_Olist(tc_String_Ochar)),X4)|~c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__4__1(v_E____,v_P,c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),v_a______)))),
% 95.22/12.68 inference(resolution,[status(thm)],[f7314,f948])).
% 95.22/12.68 fof(f7959,plain,(
% 95.22/12.68 ![X0]: (c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_Othrow(c_Expr_Oexp_OVal(c_Value_Oval_OAddr(v_aa______),tc_List_Olist(tc_String_Ochar)),tc_List_Olist(tc_String_Ochar)),X0))),
% 95.22/12.68 inference(resolution,[status(thm)],[f7616,f7313])).
% 95.22/12.68 fof(f7963,plain,(
% 95.22/12.68 $false),
% 95.22/12.68 inference(backward_subsumption_resolution,[status(thm)],[f975,f7959])).
% 95.22/12.68 % SZS output end CNFRefutation for theBenchmark.p
% 36.82/12.79 % Elapsed time: 12.360321 seconds
% 36.82/12.79 % CPU time: 97.062746 seconds
% 36.82/12.79 % Total memory used: 1.172 GB
% 36.82/12.79 % Net memory used: 1.163 GB
%------------------------------------------------------------------------------