%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV906-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 : n002.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:46 PM UTC 2026
% Result : Unsatisfiable 0.23s 5.58s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of formulae : 36 ( 17 unt; 3 def)
% Number of atoms : 64 ( 7 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 57 ( 29 ~; 25 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 8 con; 0-3 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f247,axiom,
! [V_xa,T_a] : c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f436,axiom,
! [V_pn] :
( hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(hAPP(c_Com_Ocom_OBODY,V_pn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f451,axiom,
! [V_c] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(V_c)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f470,axiom,
! [V_G,V_t,T_a,V_ts] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f474,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f475,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f477,negated_conjecture,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f479,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f898,plain,
! [X0,X1] : c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f1171,plain,
! [X0] :
( hAPP(c_Com_Obody,X0) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(hAPP(c_Com_Ocom_OBODY,X0)) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f1194,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ! [V_c] :
( ~ c_Com_OWT(V_c)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,V_c),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
inference(miniscoping,[status(thm)],[f451]) ).
fof(f1195,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT__bodies
| ~ c_Com_OWT(X0)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
inference(cnf_transformation,[status(thm)],[f1194]) ).
fof(f1224,plain,
! [V_G,V_t,T_a] :
( ! [V_ts] : ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a) ),
inference(miniscoping,[status(thm)],[f470]) ).
fof(f1225,plain,
! [X0,X1,X2,X3] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(X1,X3,tc_Hoare__Mirabelle_Otriple(X2)),X2)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),tc_Hoare__Mirabelle_Otriple(X2)),X2) ),
inference(cnf_transformation,[status(thm)],[f1224]) ).
fof(f1230,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(cnf_transformation,[status(thm)],[f474]) ).
fof(f1231,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(thm)],[f475]) ).
fof(f1233,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
inference(cnf_transformation,[status(thm)],[f477]) ).
fof(f1235,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(cnf_transformation,[status(thm)],[f479]) ).
fof(f1286,definition,
( sQ1_spl
<=> c_Hoare__Mirabelle_Ostate__not__singleton ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1288,plain,
( sQ1_spl
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
inference(component_clause,[status(thm)],[f1286]) ).
fof(f1293,definition,
( sQ3_spl
<=> c_Com_OWT__bodies ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1295,plain,
( sQ3_spl
| ~ c_Com_OWT__bodies ),
inference(component_clause,[status(thm)],[f1293]) ).
fof(f1309,definition,
! [X0] :
( sQ7_spl
<=> ( ~ c_Com_OWT(X0)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1310,plain,
! [X0] :
( ~ sQ7_spl
| ~ c_Com_OWT(X0)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,X0),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate) ),
inference(component_clause,[status(thm)],[f1309]) ).
fof(f1312,plain,
( ~ sQ1_spl
| ~ sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f1195,f1309,f1293,f1286]) ).
fof(f1317,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1295,f1231]) ).
fof(f1318,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f1317]) ).
fof(f1319,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1288,f1230]) ).
fof(f1320,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f1319]) ).
fof(f1688,plain,
hAPP(c_Com_Obody,v_pn) != c_Option_Ooption_ONone(tc_Com_Ocom),
inference(paramodulation,[status(thm)],[f1233,f898]) ).
fof(f2290,plain,
! [X0] : ~ c_Hoare__Mirabelle_Ohoare__derivs(c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pn)),X0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Com_Ostate),
inference(resolution,[status(thm)],[f1225,f1235]) ).
fof(f2406,plain,
( ~ sQ7_spl
| ~ c_Com_OWT(hAPP(c_Com_Ocom_OBODY,v_pn)) ),
inference(resolution,[status(thm)],[f1310,f2290]) ).
fof(f2448,plain,
c_Com_OWT(hAPP(c_Com_Ocom_OBODY,v_pn)),
inference(resolution,[status(thm)],[f1171,f1688]) ).
fof(f2459,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2448,f2406]) ).
fof(f2460,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f2459]) ).
fof(f2461,plain,
$false,
inference(sat_refutation,[status(thm)],[f1312,f1318,f1320,f2460]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV906-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.45 % Computer : n002.cluster.edu
% 0.16/5.45 % Model : x86_64 x86_64
% 0.16/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.45 % Memory : 8046.5625MB
% 0.16/5.45 % OS : Linux 6.8.0-71-generic
% 0.16/5.45 % CPULimit : 300
% 0.16/5.45 % WCLimit : 300
% 0.16/5.45 % DateTime : Mon Sep 21 09:33:52 UTC 2026
% 0.16/5.45 % CPUTime :
% 0.16/5.48 % Drodi V4.1.1
% 0.23/5.58 % Refutation found
% 0.23/5.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/5.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/5.65 % Elapsed time: 0.176323 seconds
% 0.23/5.65 % CPU time: 0.729233 seconds
% 0.23/5.65 % Total memory used: 135.942 MB
% 0.23/5.65 % Net memory used: 135.565 MB
%------------------------------------------------------------------------------