%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV959-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:51 PM UTC 2026
% Result : Unsatisfiable 0.15s 10.69s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 11
% Syntax : Number of formulae : 50 ( 8 unt; 0 def)
% Number of atoms : 160 ( 2 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 216 ( 106 ~; 110 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 8 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-6 aty)
% Number of functors : 24 ( 24 usr; 13 con; 0-8 aty)
% Number of variables : 173 ( 173 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,axiom,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,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__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,axiom,
v_T____ = c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f350,axiom,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f356,axiom,
! [V_P,V_h,V_E,V_e,V_v,V_D,V_F,V_T] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,axiom,
! [V_T_092_060_094isub_0622,V_TF,V_C] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)
| ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),V_TF))
| 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_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f381,axiom,
! [V_T_092_060_094isub_0622,V_TF,V_C] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)
| ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),V_TF))
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,axiom,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| 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_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f383,axiom,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f384,negated_conjecture,
! [V_x] :
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,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/sandbox/benchmark/theBenchmark.p') ).
fof(f387,plain,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f388,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7)
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X4,X2,X5,X0,X3,X1,X6)))
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT) ),
inference(cnf_transformation,[status(thm)],[f387]) ).
fof(f395,plain,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_TypeRel_Ohas__field(V_P,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_F,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v),V_D,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f396,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7)
| c_TypeRel_Ohas__field(X0,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(X4,X2,X5,X0,X3,X1,X6),X5,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X3,X1,X6),X4,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT) ),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f786,plain,
! [V_P,V_h,V_E,V_e,V_D,V_F,V_v] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,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__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(V_D,V_E,V_F,V_P,V_e,V_h,V_v)))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
inference(miniscoping,[status(thm)],[f323]) ).
fof(f787,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X5,X4,X6,tc_List_Olist(tc_String_Ochar)),X7)
| 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__8__3(X4,X2,X5,X0,X3,X1,X6)),c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X4,X2,X5,X0,X3,X1,X6)))
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT) ),
inference(cnf_transformation,[status(thm)],[f786]) ).
fof(f789,plain,
v_T____ = c_Type_Oty_OVoid,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f823,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_T____),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f831,plain,
! [V_P,V_h,V_E,V_e,V_v,V_D,V_F] :
( ! [V_T] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e,V_F,V_D,V_v,tc_List_Olist(tc_String_Ochar)),V_T)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_v,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(V_D,V_E,V_F,V_P,V_e,V_h,V_v))
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,c_Type_Oty_ONT) ),
inference(miniscoping,[status(thm)],[f356]) ).
fof(f832,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X6,X5,X4,tc_List_Olist(tc_String_Ochar)),X7)
| c_WellTypeRT_OWTrt(X0,X1,X2,X4,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X5,X2,X6,X0,X3,X1,X4))
| c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT) ),
inference(cnf_transformation,[status(thm)],[f831]) ).
fof(f865,plain,
! [V_C] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C))
| ! [V_T_092_060_094isub_0622] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)
| ! [V_TF] :
( ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),V_TF))
| 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_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ) ) ),
inference(miniscoping,[status(thm)],[f380]) ).
fof(f866,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),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__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
inference(cnf_transformation,[status(thm)],[f865]) ).
fof(f867,plain,
! [V_C] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(V_C))
| ! [V_T_092_060_094isub_0622] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,V_T_092_060_094isub_0622)
| ! [V_TF] :
( ~ c_TypeRel_Ohas__field(v_P,V_C,v_F____,V_TF,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),V_TF))
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ) ) ),
inference(miniscoping,[status(thm)],[f381]) ).
fof(f868,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),X1))
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f869,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| 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_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f870,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,v_T____,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
inference(cnf_transformation,[status(thm)],[f383]) ).
fof(f871,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),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____)) ),
inference(cnf_transformation,[status(thm)],[f384]) ).
fof(f876,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid),
inference(forward_demodulation,[status(thm)],[f789,f823]) ).
fof(f881,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),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__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
inference(forward_demodulation,[status(thm)],[f789,f866]) ).
fof(f882,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),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__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),c_Type_Oty_OVoid)) ),
inference(forward_demodulation,[status(thm)],[f789,f881]) ).
fof(f883,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),X1))
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
inference(forward_demodulation,[status(thm)],[f789,f868]) ).
fof(f884,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| 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_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),v_T____)) ),
inference(forward_demodulation,[status(thm)],[f789,f869]) ).
fof(f885,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| 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_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)),c_Type_Oty_OVoid)) ),
inference(forward_demodulation,[status(thm)],[f789,f884]) ).
fof(f886,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____)) ),
inference(forward_demodulation,[status(thm)],[f789,f870]) ).
fof(f887,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),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_Type_Oty_OVoid)) ),
inference(forward_demodulation,[status(thm)],[f789,f871]) ).
fof(f1084,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),X1)) ),
inference(resolution,[status(thm)],[f882,f887]) ).
fof(f1092,plain,
! [X0,X1,X2] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X2))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,X0)
| ~ c_TypeRel_Ohas__field(v_P,X2,v_F____,X1,v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar))))
| ~ 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),X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1084,f883]) ).
fof(f1106,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(v_P,X5,X2,c_Expr_Oexp_OFAss(X4,X3,X1,X6,tc_List_Olist(tc_String_Ochar)),X7)
| c_WellTypeRT_OWTrt(v_P,X5,X2,X4,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(X0))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(X1,X2,X3,v_P,X4,X5,X6))
| ~ c_TypeRel_Ohas__field(v_P,X0,v_F____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__2(X1,X2,X3,v_P,X4,X5,X6),v_D____,tc_prod(tc_List_Olist(tc_List_Olist(tc_String_Ochar)),tc_Expr_Oexp(tc_List_Olist(tc_String_Ochar)))) ),
inference(resolution,[status(thm)],[f1092,f787]) ).
fof(f1113,plain,
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,c_Expr_Oexp_OFAss(v_e_Ha____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),v_sko__CHAINED__1(v_D____,v_E____,v_F____,v_P,c_Type_Oty_OVoid,v_e_Ha____,v_e_092_060_094isub_0622____,v_h_Ha____))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT) ),
inference(resolution,[status(thm)],[f885,f887]) ).
fof(f1122,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT),
inference(forward_subsumption_resolution,[status(thm)],[f1113,f886]) ).
fof(f1132,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_WellTypeRT_OWTrt(v_P,X2,X0,c_Expr_Oexp_OFAss(X1,v_F____,v_D____,X3,tc_List_Olist(tc_String_Ochar)),X5)
| c_WellTypeRT_OWTrt(v_P,X2,X0,X1,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,X2,X0,c_Expr_Oexp_OFAss(X1,v_F____,v_D____,X3,tc_List_Olist(tc_String_Ochar)),X4)
| c_WellTypeRT_OWTrt(v_P,X2,X0,X1,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,X0,v_F____,v_P,X1,X2,X3)))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,X0,v_F____,v_P,X1,X2,X3)) ),
inference(resolution,[status(thm)],[f1106,f396]) ).
fof(f1133,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_WellTypeRT_OWTrt(v_P,X2,X0,c_Expr_Oexp_OFAss(X1,v_F____,v_D____,X3,tc_List_Olist(tc_String_Ochar)),X5)
| ~ c_WellTypeRT_OWTrt(v_P,X2,X0,c_Expr_Oexp_OFAss(X1,v_F____,v_D____,X3,tc_List_Olist(tc_String_Ochar)),X4)
| c_WellTypeRT_OWTrt(v_P,X2,X0,X1,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_OClass(c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__1(v_D____,X0,v_F____,v_P,X1,X2,X3)))
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,X0,v_F____,v_P,X1,X2,X3)) ),
inference(duplicate_literals_removal,[status(thm)],[f1132]) ).
fof(f1135,plain,
! [X0,X1,X2,X3] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X3)
| c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X2)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X1)
| c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,X0)) ),
inference(resolution,[status(thm)],[f1133,f388]) ).
fof(f1137,plain,
! [X0,X1,X2,X3] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X3)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X2)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X1)
| c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f1135]) ).
fof(f1138,plain,
! [X0,X1,X2,X3] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X3)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X2)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,X0,tc_List_Olist(tc_String_Ochar)),X1)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_e_092_060_094isub_0622____,c_WellTypeRT_Osko__WellTypeRT__XWTrt__elim__cases__8__3(v_D____,v_E____,v_F____,v_P,v_ea____,v_ha____,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1137,f1122]) ).
fof(f1143,plain,
! [X0,X1,X2,X3] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X3)
| c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,v_ea____,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X2)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X1)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X0) ),
inference(resolution,[status(thm)],[f1138,f832]) ).
fof(f1144,plain,
! [X0,X1,X2,X3] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X3)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X2)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X1)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1143,f1122]) ).
fof(f1145,plain,
! [X0] : ~ c_WellTypeRT_OWTrt(v_P,v_ha____,v_E____,c_Expr_Oexp_OFAss(v_ea____,v_F____,v_D____,v_e_092_060_094isub_0622____,tc_List_Olist(tc_String_Ochar)),X0),
inference(resolution,[status(thm)],[f1144,f876]) ).
fof(f1171,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f876,f1145]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV959-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.38 % Computer : n010.cluster.edu
% 0.10/10.38 % Model : x86_64 x86_64
% 0.10/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.38 % Memory : 8046.5625MB
% 0.10/10.38 % OS : Linux 6.8.0-71-generic
% 0.10/10.38 % CPULimit : 300
% 0.10/10.38 % WCLimit : 300
% 0.10/10.38 % DateTime : Mon Sep 21 09:34:50 UTC 2026
% 0.10/10.38 % CPUTime :
% 0.15/10.42 % Drodi V4.1.1
% 0.15/10.69 % Refutation found
% 0.15/10.69 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/10.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/10.73 % Elapsed time: 0.329367 seconds
% 0.15/10.73 % CPU time: 2.169213 seconds
% 0.15/10.73 % Total memory used: 181.772 MB
% 0.15/10.73 % Net memory used: 179.850 MB
%------------------------------------------------------------------------------