%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV948-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:49:49 PM UTC 2026
% Result : Unsatisfiable 155.86s 25.29s
% Output : CNFRefutation 72.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 17
% Syntax : Number of formulae : 66 ( 19 unt; 2 def)
% Number of atoms : 131 ( 11 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 131 ( 66 ~; 63 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-5 aty)
% Number of functors : 28 ( 28 usr; 14 con; 0-5 aty)
% Number of variables : 177 ( 177 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [V_E,V_v,V_T,V_P,V_h] :
( c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OVar(V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| hAPP(V_E,V_v) != c_Option_Ooption_OSome(V_T,tc_Type_Oty) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,axiom,
! [V_P,V_h,V_E,V_V,V_e,V_T_H,V_T] :
( ~ c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OVar(V_V,tc_List_Olist(tc_String_Ochar)),V_T)
| ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T_H)
| ~ 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_H),V_T))
| c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_V,V_e,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f300,axiom,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_a______,v_b______,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)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f303,axiom,
! [V_E,V_v,V_P,V_e,V_h,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| hAPP(V_E,V_v) = c_Option_Ooption_OSome(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(V_E,V_P,V_e,V_h,V_v),tc_Type_Oty) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f318,axiom,
! [V_T,V_P,V_h,V_E,V_v,V_e] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| V_T = c_Type_Oty_OVoid ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,axiom,
! [V_P,V_E,V_e,V_h,V_v,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),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)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(V_E,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(V_E,V_P,V_e,V_h,V_v))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f328,axiom,
! [V_P,V_h,V_E,V_e,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T)
| c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f329,axiom,
! [V_P,V_h,V_E,V_e,V_T] :
( ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f339,axiom,
! [V_P,V_h,V_E,V_e,V_v,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(V_E,V_P,V_e,V_h,V_v)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f340,axiom,
! [V_P,T_a,V_T] : hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_T),V_T)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f341,axiom,
! [V_P,T_a,V_S,V_T,V_U] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_S),V_U))
| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_U),V_T))
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_S),V_T)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f358,axiom,
c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_ea______,tc_List_Olist(tc_String_Ochar)),v_T____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f360,axiom,
! [V_E,V_T] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_a______,v_b______,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))))
| ~ c_WellTypeRT_OWTrt(v_P,v_a______,V_E,v_ea______,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__CHAINED__1(V_E,v_P,V_T,v_aa______,v_e_Ha______)),V_T)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f361,axiom,
! [V_E,V_T] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_a______,v_b______,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))))
| ~ c_WellTypeRT_OWTrt(v_P,v_a______,V_E,v_ea______,V_T)
| c_WellTypeRT_OWTrt(v_P,v_aa______,V_E,v_e_Ha______,v_sko__CHAINED__1(V_E,v_P,V_T,v_aa______,v_e_Ha______)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f363,negated_conjecture,
! [V_x] :
( ~ c_WellTypeRT_OWTrt(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),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____)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f366,plain,
! [V_E,V_v,V_T] :
( ! [V_P,V_h] : c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OVar(V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| hAPP(V_E,V_v) != c_Option_Ooption_OSome(V_T,tc_Type_Oty) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f367,plain,
! [X0,X1,X2,X3,X4] :
( c_Option_Ooption_OSome(X4,tc_Type_Oty) != hAPP(X2,X3)
| c_Progress_OWTrt_H(X0,X1,X2,c_Expr_Oexp_OVar(X3,tc_List_Olist(tc_String_Ochar)),X4) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f482,plain,
! [V_P,V_h,V_E,V_V,V_T] :
( ~ c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OVar(V_V,tc_List_Olist(tc_String_Ochar)),V_T)
| ! [V_e,V_T_H] :
( ~ c_Progress_OWTrt_H(V_P,V_h,V_E,V_e,V_T_H)
| ~ 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_H),V_T))
| c_Progress_OWTrt_H(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_V,V_e,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid) ) ),
inference(miniscoping,[status(thm)],[f95]) ).
fof(f483,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( c_Progress_OWTrt_H(X0,X1,X2,c_Expr_Oexp_OLAss(X3,X6,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid)
| ~ c_Progress_OWTrt_H(X0,X1,X2,X6,X5)
| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X5),X4))
| ~ c_Progress_OWTrt_H(X0,X1,X2,c_Expr_Oexp_OVar(X3,tc_List_Olist(tc_String_Ochar)),X4) ),
inference(cnf_transformation,[status(thm)],[f482]) ).
fof(f736,plain,
c_TypeSafe__Mirabelle_Osconf(v_P,v_E____,c_Pair(v_a______,v_b______,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)))),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f739,plain,
! [V_E,V_v,V_P,V_e,V_h] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| hAPP(V_E,V_v) = c_Option_Ooption_OSome(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(V_E,V_P,V_e,V_h,V_v),tc_Type_Oty) ),
inference(miniscoping,[status(thm)],[f303]) ).
fof(f740,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_WellTypeRT_OWTrt(X2,X4,X0,c_Expr_Oexp_OLAss(X1,X3,tc_List_Olist(tc_String_Ochar)),X5)
| hAPP(X0,X1) = c_Option_Ooption_OSome(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(X0,X2,X3,X4,X1),tc_Type_Oty) ),
inference(cnf_transformation,[status(thm)],[f739]) ).
fof(f761,plain,
! [V_T] :
( ! [V_P,V_h,V_E,V_v,V_e] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| V_T = c_Type_Oty_OVoid ),
inference(miniscoping,[status(thm)],[f318]) ).
fof(f762,plain,
! [X0,X1,X2,X3,X4,X5] :
( X5 = c_Type_Oty_OVoid
| ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OLAss(X3,X4,tc_List_Olist(tc_String_Ochar)),X5) ),
inference(cnf_transformation,[status(thm)],[f761]) ).
fof(f770,plain,
! [V_P,V_E,V_e,V_h,V_v] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),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)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(V_E,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(V_E,V_P,V_e,V_h,V_v))) ),
inference(miniscoping,[status(thm)],[f324]) ).
fof(f771,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_WellTypeRT_OWTrt(X0,X3,X1,c_Expr_Oexp_OLAss(X4,X2,tc_List_Olist(tc_String_Ochar)),X5)
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(X1,X0,X2,X3,X4)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(X1,X0,X2,X3,X4))) ),
inference(cnf_transformation,[status(thm)],[f770]) ).
fof(f776,plain,
! [X0,X1,X2,X3,X4] :
( c_Progress_OWTrt_H(X0,X1,X2,X3,X4)
| ~ c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f777,plain,
! [X0,X1,X2,X3,X4] :
( c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4)
| ~ c_Progress_OWTrt_H(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f789,plain,
! [V_P,V_h,V_E,V_e,V_v] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OLAss(V_v,V_e,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(V_E,V_P,V_e,V_h,V_v)) ),
inference(miniscoping,[status(thm)],[f339]) ).
fof(f790,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_WellTypeRT_OWTrt(X0,X1,X2,X4,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(X2,X0,X4,X1,X3))
| ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OLAss(X3,X4,tc_List_Olist(tc_String_Ochar)),X5) ),
inference(cnf_transformation,[status(thm)],[f789]) ).
fof(f791,plain,
! [X0,X1,X2] : hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X2)),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f792,plain,
! [V_P,T_a,V_S,V_U] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_S),V_U))
| ! [V_T] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_U),V_T))
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_S),V_T)) ) ),
inference(miniscoping,[status(thm)],[f341]) ).
fof(f793,plain,
! [X0,X1,X2,X3,X4] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X4))
| ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X4),X3))
| hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f792]) ).
fof(f817,plain,
c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_ea______,tc_List_Olist(tc_String_Ochar)),v_T____),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f819,plain,
! [V_E] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_a______,v_b______,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))))
| ! [V_T] :
( ~ c_WellTypeRT_OWTrt(v_P,v_a______,V_E,v_ea______,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__CHAINED__1(V_E,v_P,V_T,v_aa______,v_e_Ha______)),V_T)) ) ),
inference(miniscoping,[status(thm)],[f360]) ).
fof(f820,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,v_a______,X0,v_ea______,X1)
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_a______,v_b______,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))))
| 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__CHAINED__1(X0,v_P,X1,v_aa______,v_e_Ha______)),X1)) ),
inference(cnf_transformation,[status(thm)],[f819]) ).
fof(f821,plain,
! [V_E] :
( ~ c_TypeSafe__Mirabelle_Osconf(v_P,V_E,c_Pair(v_a______,v_b______,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))))
| ! [V_T] :
( ~ c_WellTypeRT_OWTrt(v_P,v_a______,V_E,v_ea______,V_T)
| c_WellTypeRT_OWTrt(v_P,v_aa______,V_E,v_e_Ha______,v_sko__CHAINED__1(V_E,v_P,V_T,v_aa______,v_e_Ha______)) ) ),
inference(miniscoping,[status(thm)],[f361]) ).
fof(f822,plain,
! [X0,X1] :
( ~ c_WellTypeRT_OWTrt(v_P,v_a______,X0,v_ea______,X1)
| c_WellTypeRT_OWTrt(v_P,v_aa______,X0,v_e_Ha______,v_sko__CHAINED__1(X0,v_P,X1,v_aa______,v_e_Ha______))
| ~ c_TypeSafe__Mirabelle_Osconf(v_P,X0,c_Pair(v_a______,v_b______,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)))) ),
inference(cnf_transformation,[status(thm)],[f821]) ).
fof(f824,plain,
! [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_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),X0) ),
inference(cnf_transformation,[status(thm)],[f363]) ).
fof(f831,plain,
~ c_WellTypeRT_OWTrt(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),v_T____),
inference(resolution,[status(thm)],[f824,f791]) ).
fof(f835,plain,
c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,v_ea______,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______)),
inference(resolution,[status(thm)],[f790,f817]) ).
fof(f873,plain,
c_Type_Oty_OVoid = v_T____,
inference(resolution,[status(thm)],[f762,f817]) ).
fof(f884,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))),X4),X6))
| ~ c_Progress_OWTrt_H(X0,X1,X2,c_Expr_Oexp_OVar(X5,tc_List_Olist(tc_String_Ochar)),X6)
| c_Progress_OWTrt_H(X0,X1,X2,c_Expr_Oexp_OLAss(X5,X3,tc_List_Olist(tc_String_Ochar)),v_T____)
| ~ c_Progress_OWTrt_H(X0,X1,X2,X3,X4) ),
inference(backward_demodulation,[status(thm)],[f873,f483]) ).
fof(f1429,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,v_ea______,X0)
| c_WellTypeRT_OWTrt(v_P,v_aa______,v_E____,v_e_Ha______,v_sko__CHAINED__1(v_E____,v_P,X0,v_aa______,v_e_Ha______)) ),
inference(resolution,[status(thm)],[f822,f736]) ).
fof(f1434,plain,
c_WellTypeRT_OWTrt(v_P,v_aa______,v_E____,v_e_Ha______,v_sko__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),
inference(resolution,[status(thm)],[f1429,f835]) ).
fof(f1436,plain,
c_Progress_OWTrt_H(v_P,v_aa______,v_E____,v_e_Ha______,v_sko__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),
inference(resolution,[status(thm)],[f1434,f776]) ).
fof(f1450,plain,
! [X0,X1] :
( c_Progress_OWTrt_H(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(X0,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),X1))
| ~ c_Progress_OWTrt_H(v_P,v_aa______,v_E____,c_Expr_Oexp_OVar(X0,tc_List_Olist(tc_String_Ochar)),X1) ),
inference(resolution,[status(thm)],[f1436,f884]) ).
fof(f1773,plain,
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)))),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______))),
inference(resolution,[status(thm)],[f771,f817]) ).
fof(f1779,plain,
! [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),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______)))
| ~ 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),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______))) ),
inference(resolution,[status(thm)],[f1773,f793]) ).
fof(f1788,plain,
! [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)))),v_sko__CHAINED__1(v_E____,v_P,X0,v_aa______,v_e_Ha______)),X0))
| ~ c_WellTypeRT_OWTrt(v_P,v_a______,v_E____,v_ea______,X0) ),
inference(resolution,[status(thm)],[f820,f736]) ).
fof(f1793,plain,
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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______))),
inference(resolution,[status(thm)],[f1788,f835]) ).
fof(f2122,plain,
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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______))),
inference(resolution,[status(thm)],[f1793,f1779]) ).
fof(f2523,plain,
c_Option_Ooption_OSome(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______),tc_Type_Oty) = hAPP(v_E____,v_V______),
inference(resolution,[status(thm)],[f740,f817]) ).
fof(f2535,plain,
! [X0,X1] : c_Progress_OWTrt_H(X0,X1,v_E____,c_Expr_Oexp_OVar(v_V______,tc_List_Olist(tc_String_Ochar)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______)),
inference(resolution,[status(thm)],[f2523,f367]) ).
fof(f2694,plain,
( c_Progress_OWTrt_H(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______))) ),
inference(resolution,[status(thm)],[f2535,f1450]) ).
fof(f2736,definition,
( sQ90_spl
<=> c_Progress_OWTrt_H(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),v_T____) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2737,plain,
( ~ sQ90_spl
| c_Progress_OWTrt_H(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),v_T____) ),
inference(component_clause,[status(thm)],[f2736]) ).
fof(f2755,definition,
( sQ95_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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______))) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f2757,plain,
( sQ95_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__CHAINED__1(v_E____,v_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__2(v_E____,v_P,v_ea______,v_a______,v_V______),v_aa______,v_e_Ha______)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__1__1(v_E____,v_P,v_ea______,v_a______,v_V______))) ),
inference(component_clause,[status(thm)],[f2755]) ).
fof(f2758,plain,
( sQ90_spl
| ~ sQ95_spl ),
inference(split_clause,[status(thm)],[f2694,f2755,f2736]) ).
fof(f2761,plain,
( sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2757,f2122]) ).
fof(f2762,plain,
sQ95_spl,
inference(contradiction_clause,[status(thm)],[f2761]) ).
fof(f2782,plain,
( ~ sQ90_spl
| c_WellTypeRT_OWTrt(v_P,v_aa______,v_E____,c_Expr_Oexp_OLAss(v_V______,v_e_Ha______,tc_List_Olist(tc_String_Ochar)),v_T____) ),
inference(resolution,[status(thm)],[f2737,f777]) ).
fof(f2784,plain,
( ~ sQ90_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2782,f831]) ).
fof(f2785,plain,
~ sQ90_spl,
inference(contradiction_clause,[status(thm)],[f2784]) ).
fof(f2786,plain,
$false,
inference(sat_refutation,[status(thm)],[f2758,f2762,f2785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV948-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n018.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Mon Sep 21 09:35:18 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.23/5.50 % Drodi V4.1.1
% 155.86/25.29 % Refutation found
% 155.86/25.29 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 155.86/25.29 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 72.51/25.37 % Elapsed time: 19.883075 seconds
% 72.51/25.37 % CPU time: 156.759794 seconds
% 72.51/25.37 % Total memory used: 825.448 MB
% 72.51/25.37 % Net memory used: 800.390 MB
%------------------------------------------------------------------------------