%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV901-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 : n012.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:45 PM UTC 2026
% Result : Unsatisfiable 0.13s 5.55s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 15 unt; 0 def)
% Number of atoms : 62 ( 6 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 68 ( 37 ~; 31 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-5 aty)
% Number of variables : 32 ( 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f556,axiom,
! [V_pn,V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f560,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/sandbox/benchmark/theBenchmark.p') ).
fof(f594,axiom,
! [V_G,V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f614,axiom,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f666,negated_conjecture,
c_Hoare__Mirabelle_Ostate__not__singleton,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f667,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f671,negated_conjecture,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f672,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),v_Fa,tc_Com_Ostate),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f673,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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/sandbox/benchmark/theBenchmark.p') ).
fof(f1579,plain,
! [V_b] :
( c_Com_OWT(V_b)
| ~ c_Com_OWT__bodies
| ! [V_pn] : hAPP(c_Com_Obody,V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) ),
inference(miniscoping,[status(thm)],[f556]) ).
fof(f1580,plain,
! [X0,X1] :
( c_Com_OWT(X1)
| ~ c_Com_OWT__bodies
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ),
inference(cnf_transformation,[status(thm)],[f1579]) ).
fof(f1584,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)],[f560]) ).
fof(f1585,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)],[f1584]) ).
fof(f1642,plain,
! [V_ts,T_a,V_G_H] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ! [V_G] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ) ),
inference(miniscoping,[status(thm)],[f594]) ).
fof(f1643,plain,
! [X0,X1,X2,X3] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X3,X1,X2)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X3,X2)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1642]) ).
fof(f1669,plain,
! [X0,X1] : c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool)),X1),
inference(cnf_transformation,[status(thm)],[f614]) ).
fof(f1753,plain,
c_Hoare__Mirabelle_Ostate__not__singleton,
inference(cnf_transformation,[status(thm)],[f666]) ).
fof(f1754,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f1758,plain,
hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(v_y,tc_Com_Ocom),
inference(cnf_transformation,[status(thm)],[f671]) ).
fof(f1759,plain,
c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),v_Fa,tc_Com_Ostate),
inference(cnf_transformation,[status(thm)],[f672]) ).
fof(f1760,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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)],[f673]) ).
fof(f1869,plain,
! [X0,X1] :
( c_Com_OWT(X1)
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ),
inference(forward_subsumption_resolution,[status(thm)],[f1580,f1754]) ).
fof(f1870,plain,
c_Com_OWT(v_y),
inference(resolution,[status(thm)],[f1869,f1758]) ).
fof(f1872,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,X0,tc_Com_Ostate)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X0,tc_Com_Ostate) ),
inference(resolution,[status(thm)],[f1643,f1759]) ).
fof(f1893,plain,
! [X0,X1] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,tc_Com_Ostate)
| c_Hoare__Mirabelle_Ohoare__derivs(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_Com_Ocom_OBODY,tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),X1,tc_Com_Ostate)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,X0,tc_Com_Ostate) ),
inference(resolution,[status(thm)],[f1872,f1643]) ).
fof(f2083,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(hAPP(c_Hoare__Mirabelle_OMGT,v_y),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)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,X0,tc_Com_Ostate) ),
inference(resolution,[status(thm)],[f1893,f1760]) ).
fof(f2823,plain,
! [X0] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ 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(forward_subsumption_resolution,[status(thm)],[f1585,f1754]) ).
fof(f2827,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate)
| ~ c_Hoare__Mirabelle_Ostate__not__singleton
| ~ c_Com_OWT(v_y) ),
inference(resolution,[status(thm)],[f2823,f2083]) ).
fof(f2834,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate)
| ~ c_Hoare__Mirabelle_Ostate__not__singleton ),
inference(forward_subsumption_resolution,[status(thm)],[f2827,f1870]) ).
fof(f2892,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_Fa,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_bool)),tc_Com_Ostate),
inference(forward_subsumption_resolution,[status(thm)],[f2834,f1753]) ).
fof(f2893,plain,
$false,
inference(resolution,[status(thm)],[f2892,f1669]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV901-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n012.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 09:30:45 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.13/5.41 % Drodi V4.1.1
% 0.13/5.55 % Refutation found
% 0.13/5.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.57 % Elapsed time: 0.202854 seconds
% 0.13/5.57 % CPU time: 1.172100 seconds
% 0.13/5.57 % Total memory used: 165.217 MB
% 0.13/5.57 % Net memory used: 164.133 MB
%------------------------------------------------------------------------------