%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV955-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 : 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 02:49:50 PM UTC 2026
% Result : Unsatisfiable 0.15s 0.65s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of formulae : 26 ( 12 unt; 2 def)
% Number of atoms : 43 ( 2 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 39 ( 22 ~; 15 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 12 con; 0-5 aty)
% Number of variables : 36 ( 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f308,axiom,
! [V_P,V_h,V_E,V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,axiom,
v_T____ = c_Type_Oty_OVoid,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f351,axiom,
! [V_P,T_a,V_T] : hBOOL(hAPP(hAPP(c_TypeRel_Owiden(V_P,T_a),V_T),V_T)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,axiom,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f381,axiom,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_ONT),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f382,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(f761,plain,
! [V_P,V_h,V_E,V_e_092_060_094isub_0621] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0621,c_Type_Oty_ONT)
| ! [V_e_092_060_094isub_0622] :
( ! [V_T_092_060_094isub_0622] : ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e_092_060_094isub_0622,V_T_092_060_094isub_0622)
| ! [V_F,V_D] : c_WellTypeRT_OWTrt(V_P,V_h,V_E,c_Expr_Oexp_OFAss(V_e_092_060_094isub_0621,V_F,V_D,V_e_092_060_094isub_0622,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid) ) ),
inference(miniscoping,[status(thm)],[f308]) ).
fof(f762,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ c_WellTypeRT_OWTrt(X0,X1,X2,X3,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(X0,X1,X2,X6,X7)
| c_WellTypeRT_OWTrt(X0,X1,X2,c_Expr_Oexp_OFAss(X3,X4,X5,X6,tc_List_Olist(tc_String_Ochar)),c_Type_Oty_OVoid) ),
inference(cnf_transformation,[status(thm)],[f761]) ).
fof(f787,plain,
v_T____ = c_Type_Oty_OVoid,
inference(cnf_transformation,[status(thm)],[f325]) ).
fof(f822,plain,
! [X0,X1,X2] : hBOOL(hAPP(hAPP(c_TypeRel_Owiden(X0,X1),X2),X2)),
inference(cnf_transformation,[status(thm)],[f351]) ).
fof(f863,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,v_T_092_060_094isub_0622____),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f864,plain,
c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_ONT),
inference(cnf_transformation,[status(thm)],[f381]) ).
fof(f865,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)],[f382]) ).
fof(f874,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)],[f787,f865]) ).
fof(f875,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)),c_Type_Oty_OVoid),
inference(resolution,[status(thm)],[f822,f874]) ).
fof(f1024,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_ONT)
| ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,X0) ),
inference(resolution,[status(thm)],[f762,f875]) ).
fof(f1026,definition,
! [X0] :
( sQ2_spl
<=> ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,X0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1027,plain,
! [X0] :
( ~ sQ2_spl
| ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_092_060_094isub_0622____,X0) ),
inference(component_clause,[status(thm)],[f1026]) ).
fof(f1029,definition,
( sQ3_spl
<=> c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_ONT) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1031,plain,
( sQ3_spl
| ~ c_WellTypeRT_OWTrt(v_P,v_h_Ha____,v_E____,v_e_Ha____,c_Type_Oty_ONT) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1032,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1024,f1026,f1029]) ).
fof(f1044,plain,
( ~ sQ2_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f863,f1027]) ).
fof(f1045,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f1044]) ).
fof(f1046,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1031,f864]) ).
fof(f1047,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1046]) ).
fof(f1048,plain,
$false,
inference(sat_refutation,[status(thm)],[f1032,f1045,f1047]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV955-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.55 % Computer : n015.cluster.edu
% 0.11/0.55 % Model : x86_64 x86_64
% 0.11/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.55 % Memory : 8046.5625MB
% 0.11/0.55 % OS : Linux 6.8.0-71-generic
% 0.11/0.55 % CPULimit : 300
% 0.11/0.55 % WCLimit : 300
% 0.11/0.55 % DateTime : Mon Sep 21 09:37:36 UTC 2026
% 0.11/0.55 % CPUTime :
% 0.15/0.59 % Drodi V4.1.1
% 0.15/0.65 % Refutation found
% 0.15/0.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.68 % Elapsed time: 0.116165 seconds
% 0.15/0.68 % CPU time: 0.478739 seconds
% 0.15/0.68 % Total memory used: 129.036 MB
% 0.15/0.68 % Net memory used: 128.723 MB
%------------------------------------------------------------------------------