%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV938-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 : n019.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 119.88s 15.75s
% Output : CNFRefutation 119.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 5
% Syntax : Number of formulae : 16 ( 8 unt; 0 def)
% Number of atoms : 27 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 27 ( 16 ~; 11 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 11 con; 0-5 aty)
% Number of variables : 44 ( 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f337,axiom,
! [T_b,T_a,V_g] : c_Map_Omap__le(c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),V_g,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f450,axiom,
! [V_P,V_h,V_E_H,V_e,V_T,V_E] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T)
| ~ c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E_H,V_e,V_T) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f459,axiom,
! [V_f,V_as,V_bs,T_a,T_b,V_g] :
( ~ c_Map_Omap__le(V_f,V_g,T_a,T_b)
| c_Map_Omap__le(c_Map_Omap__upds(V_f,V_as,V_bs,T_a,T_b),c_Map_Omap__upds(V_g,V_as,V_bs,T_a,T_b),T_a,T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f497,axiom,
c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f498,negated_conjecture,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1048,plain,
! [X0,X1,X2] : c_Map_Omap__le(c_COMBK(c_Option_Ooption_ONone(X0),tc_Option_Ooption(X0),X1),X2,X1,X0),
inference(cnf_transformation,[status(thm)],[f337]) ).
fof(f1215,plain,
! [V_P,V_h,V_e,V_T,V_E] :
( ~ c_WellTypeRT_OWTrt(V_P,V_h,V_E,V_e,V_T)
| ! [V_E_H] :
( ~ c_Map_Omap__le(V_E,V_E_H,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(V_P,V_h,V_E_H,V_e,V_T) ) ),
inference(miniscoping,[status(thm)],[f450]) ).
fof(f1216,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ c_Map_Omap__le(X2,X5,tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| c_WellTypeRT_OWTrt(X0,X1,X5,X3,X4)
| ~ c_WellTypeRT_OWTrt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f1215]) ).
fof(f1227,plain,
! [V_f,T_a,T_b,V_g] :
( ~ c_Map_Omap__le(V_f,V_g,T_a,T_b)
| ! [V_as,V_bs] : c_Map_Omap__le(c_Map_Omap__upds(V_f,V_as,V_bs,T_a,T_b),c_Map_Omap__upds(V_g,V_as,V_bs,T_a,T_b),T_a,T_b) ),
inference(miniscoping,[status(thm)],[f459]) ).
fof(f1228,plain,
! [X0,X1,X2,X3,X4,X5] :
( c_Map_Omap__le(c_Map_Omap__upds(X0,X4,X5,X2,X3),c_Map_Omap__upds(X1,X4,X5,X2,X3),X2,X3)
| ~ c_Map_Omap__le(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f1227]) ).
fof(f1281,plain,
c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(cnf_transformation,[status(thm)],[f497]) ).
fof(f1282,plain,
~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____),
inference(cnf_transformation,[status(thm)],[f498]) ).
fof(f10500,plain,
! [X0] :
( ~ c_Map_Omap__le(X0,c_Map_Omap__upds(v_E____,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty)
| ~ c_WellTypeRT_OWTrt(v_P,v_ha____,X0,v_body____,v_T_H_H____) ),
inference(resolution,[status(thm)],[f1216,f1282]) ).
fof(f10544,plain,
! [X0] :
( ~ c_WellTypeRT_OWTrt(v_P,v_ha____,c_Map_Omap__upds(X0,c_List_Olist_OCons(c_Type_Othis,v_pns____,tc_List_Olist(tc_String_Ochar)),c_List_Olist_OCons(c_Type_Oty_OClass(v_D____),v_Ts____,tc_Type_Oty),tc_List_Olist(tc_String_Ochar),tc_Type_Oty),v_body____,v_T_H_H____)
| ~ c_Map_Omap__le(X0,v_E____,tc_List_Olist(tc_String_Ochar),tc_Type_Oty) ),
inference(resolution,[status(thm)],[f10500,f1228]) ).
fof(f10630,plain,
~ c_Map_Omap__le(c_COMBK(c_Option_Ooption_ONone(tc_Type_Oty),tc_Option_Ooption(tc_Type_Oty),tc_List_Olist(tc_String_Ochar)),v_E____,tc_List_Olist(tc_String_Ochar),tc_Type_Oty),
inference(resolution,[status(thm)],[f10544,f1281]) ).
fof(f10926,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f10630,f1048]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV938-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.48 % Computer : n019.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Mon Sep 21 09:34:04 UTC 2026
% 0.22/0.49 % CPUTime :
% 0.26/0.56 % Drodi V4.1.1
% 119.88/15.75 % Refutation found
% 119.88/15.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 119.88/15.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.25/15.82 % Elapsed time: 15.324659 seconds
% 13.25/15.82 % CPU time: 120.417664 seconds
% 13.25/15.82 % Total memory used: 569.360 MB
% 13.25/15.82 % Net memory used: 527.102 MB
%------------------------------------------------------------------------------