%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW384+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 03:07:45 PM UTC 2026
% Result : Theorem 103.93s 14.47s
% Output : CNFRefutation 101.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 56 ( 25 unt; 0 def)
% Number of atoms : 100 ( 56 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 83 ( 39 ~; 28 |; 8 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 9 con; 0-3 aty)
% Number of variables : 171 ( 171 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [V_G_2,V_ts_2,T_a] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)),V_ts_2),V_G_2))
=> c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,V_ts_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [V_ts_2,V_t_2,V_G_2,T_a] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),V_ts_2))
=> ( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,V_ts_2)
& c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [V_a_2,T_a] : ~ hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [T_b,V_y_2,T_a,V_x_2,V_f_2] :
( hAPP(V_f_2,V_x_2) = hAPP(c_Option_Ooption_OSome(T_a),V_y_2)
=> hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),c_Map_Odom(T_b,T_a,V_f_2)) = c_Map_Odom(T_b,T_a,V_f_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [T_a,V_B_2,V_A_2] :
( V_A_2 = V_B_2
=> ~ ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_A_2),V_B_2))
=> ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_B_2),V_A_2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [V_A_2,V_g_2,T_c,V_f_2,T_a,T_b] : hAPP(c_Set_Oimage(T_b,T_a,V_f_2),hAPP(c_Set_Oimage(T_c,T_b,V_g_2),V_A_2)) = hAPP(c_Set_Oimage(T_c,T_a,hAPP(hAPP(c_COMBB(T_b,T_a,T_c),V_f_2),V_g_2)),V_A_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [V_A_2,V_a_2,T_a] :
( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2))
=> hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2) = V_A_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [V_A_2,V_a_2,T_a] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [V_B_2,V_a_2,V_f_2,T_a,T_b] : hAPP(c_Set_Oimage(T_b,T_a,V_f_2),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_B_2)) = hAPP(hAPP(c_Set_Oinsert(T_a),hAPP(V_f_2,V_a_2)),hAPP(c_Set_Oimage(T_b,T_a,V_f_2),V_B_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1113,axiom,
! [V_m_2,T_b,V_a_2,T_a] :
( hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2)))
<=> hAPP(V_m_2,V_a_2) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1197,axiom,
! [V_f_2,T_b,T_a] :
( c_Map_Odom(T_a,T_b,V_f_2) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))
<=> V_f_2 = hAPP(c_COMBK(tc_Option_Ooption(T_b),T_a),c_Option_Ooption_ONone(T_b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5249,hypothesis,
hAPP(c_Com_Obody,v_pna) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_ya),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5250,conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(hAPP(c_COMBB(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Hoare__Mirabelle_OMGT),c_Com_Ocom_OBODY)),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pna))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5251,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(hAPP(c_COMBB(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Hoare__Mirabelle_OMGT),c_Com_Ocom_OBODY)),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pna))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))),
inference(negated_conjecture,[status(cth)],[f5250]) ).
fof(f5257,plain,
! [V_G_2,V_ts_2,T_a] :
( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,V_ts_2)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)),V_ts_2),V_G_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f5258,plain,
! [X0,X1,X2] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X2,X1)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool)),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f5257]) ).
fof(f5271,plain,
! [V_ts_2,V_t_2,V_G_2,T_a] :
( ( c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,V_ts_2)
& c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_HOL_Obool)))) )
| ~ c_Hoare__Mirabelle_Ohoare__derivs(T_a,V_G_2,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t_2),V_ts_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f5272,plain,
! [X0,X1,X2,X3] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X0),tc_HOL_Obool))))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(X0)),X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f5271]) ).
fof(f5295,plain,
! [X0,X1] : ~ hBOOL(hAPP(hAPP(c_member(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f5303,plain,
! [T_b,V_y_2,T_a,V_x_2,V_f_2] :
( hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),c_Map_Odom(T_b,T_a,V_f_2)) = c_Map_Odom(T_b,T_a,V_f_2)
| hAPP(V_f_2,V_x_2) != hAPP(c_Option_Ooption_OSome(T_a),V_y_2) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f5304,plain,
! [T_a,V_x_2,V_f_2] :
( ! [T_b] : hAPP(hAPP(c_Set_Oinsert(T_b),V_x_2),c_Map_Odom(T_b,T_a,V_f_2)) = c_Map_Odom(T_b,T_a,V_f_2)
| ! [V_y_2] : hAPP(V_f_2,V_x_2) != hAPP(c_Option_Ooption_OSome(T_a),V_y_2) ),
inference(miniscoping,[status(thm)],[f5303]) ).
fof(f5305,plain,
! [X0,X1,X2,X3,X4] :
( hAPP(hAPP(c_Set_Oinsert(X4),X1),c_Map_Odom(X4,X2,X0)) = c_Map_Odom(X4,X2,X0)
| hAPP(X0,X1) != hAPP(c_Option_Ooption_OSome(X2),X3) ),
inference(cnf_transformation,[status(thm)],[f5304]) ).
fof(f5344,plain,
! [T_a,V_B_2,V_A_2] :
( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_B_2),V_A_2))
& hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_A_2),V_B_2)) )
| V_A_2 != V_B_2 ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f5345,plain,
! [V_B_2,V_A_2] :
( ( ! [T_a] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_B_2),V_A_2))
& ! [T_a] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,tc_HOL_Obool)),V_A_2),V_B_2)) )
| V_A_2 != V_B_2 ),
inference(miniscoping,[status(thm)],[f5344]) ).
fof(f5346,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool)),X0),X1))
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f5345]) ).
fof(f5363,plain,
! [X0,X1,X2,X3,X4,X5] : hAPP(c_Set_Oimage(X0,X1,X2),hAPP(c_Set_Oimage(X3,X0,X4),X5)) = hAPP(c_Set_Oimage(X3,X1,hAPP(hAPP(c_COMBB(X0,X1,X3),X2),X4)),X5),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f5378,plain,
! [V_A_2,V_a_2,T_a] :
( hAPP(hAPP(c_Set_Oinsert(T_a),V_a_2),V_A_2) = V_A_2
| ~ hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),V_A_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f5379,plain,
! [X0,X1,X2] :
( hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) = X2
| ~ hBOOL(hAPP(hAPP(c_member(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f5378]) ).
fof(f5427,plain,
! [X0,X1,X2] : hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f5458,plain,
! [X0,X1,X2,X3,X4] : hAPP(c_Set_Oimage(X0,X1,X2),hAPP(hAPP(c_Set_Oinsert(X0),X3),X4)) = hAPP(hAPP(c_Set_Oinsert(X1),hAPP(X2,X3)),hAPP(c_Set_Oimage(X0,X1,X2),X4)),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f8486,plain,
! [V_m_2,T_b,V_a_2,T_a] :
( ( hAPP(V_m_2,V_a_2) = c_Option_Ooption_ONone(T_b)
| hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))) )
& ( hAPP(V_m_2,V_a_2) != c_Option_Ooption_ONone(T_b)
| ~ hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))) ) ),
inference(NNF_transformation,[status(thm)],[f1113]) ).
fof(f8487,plain,
( ! [V_m_2,T_b,V_a_2] :
( hAPP(V_m_2,V_a_2) = c_Option_Ooption_ONone(T_b)
| ! [T_a] : hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))) )
& ! [V_m_2,T_b,V_a_2] :
( hAPP(V_m_2,V_a_2) != c_Option_Ooption_ONone(T_b)
| ! [T_a] : ~ hBOOL(hAPP(hAPP(c_member(T_a),V_a_2),c_Map_Odom(T_a,T_b,V_m_2))) ) ),
inference(miniscoping,[status(thm)],[f8486]) ).
fof(f8489,plain,
! [X0,X1,X2,X3] :
( hAPP(X3,X1) = c_Option_Ooption_ONone(X2)
| hBOOL(hAPP(hAPP(c_member(X0),X1),c_Map_Odom(X0,X2,X3))) ),
inference(cnf_transformation,[status(thm)],[f8487]) ).
fof(f8809,plain,
! [V_f_2,T_b,T_a] :
( ( V_f_2 != hAPP(c_COMBK(tc_Option_Ooption(T_b),T_a),c_Option_Ooption_ONone(T_b))
| c_Map_Odom(T_a,T_b,V_f_2) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) )
& ( V_f_2 = hAPP(c_COMBK(tc_Option_Ooption(T_b),T_a),c_Option_Ooption_ONone(T_b))
| c_Map_Odom(T_a,T_b,V_f_2) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) ) ),
inference(NNF_transformation,[status(thm)],[f1197]) ).
fof(f8810,plain,
( ! [V_f_2,T_b,T_a] :
( V_f_2 != hAPP(c_COMBK(tc_Option_Ooption(T_b),T_a),c_Option_Ooption_ONone(T_b))
| c_Map_Odom(T_a,T_b,V_f_2) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) )
& ! [V_f_2,T_b,T_a] :
( V_f_2 = hAPP(c_COMBK(tc_Option_Ooption(T_b),T_a),c_Option_Ooption_ONone(T_b))
| c_Map_Odom(T_a,T_b,V_f_2) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)) ) ),
inference(miniscoping,[status(thm)],[f8809]) ).
fof(f8812,plain,
! [X0,X1,X2] :
( X2 != hAPP(c_COMBK(tc_Option_Ooption(X1),X0),c_Option_Ooption_ONone(X1))
| c_Map_Odom(X0,X1,X2) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)) ),
inference(cnf_transformation,[status(thm)],[f8810]) ).
fof(f19919,plain,
hAPP(c_Com_Obody,v_pna) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_ya),
inference(cnf_transformation,[status(thm)],[f5249]) ).
fof(f19920,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(hAPP(c_COMBB(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Hoare__Mirabelle_OMGT),c_Com_Ocom_OBODY)),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pna))),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_HOL_Obool)))),
inference(cnf_transformation,[status(thm)],[f5251]) ).
fof(f20207,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X1)),
inference(destructive_equality_resolution,[status(thm)],[f5346]) ).
fof(f20329,plain,
! [X0,X1] : c_Map_Odom(X0,X1,hAPP(c_COMBK(tc_Option_Ooption(X1),X0),c_Option_Ooption_ONone(X1))) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)),
inference(destructive_equality_resolution,[status(thm)],[f8812]) ).
fof(f20702,plain,
! [X0] : ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),hAPP(hAPP(c_COMBB(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Hoare__Mirabelle_OMGT),c_Com_Ocom_OBODY)),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody)),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pna))),X0)),
inference(resolution,[status(thm)],[f5272,f19920]) ).
fof(f20721,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Set_Oinsert(X3),X1),c_Map_Odom(X3,X2,X0)) = c_Map_Odom(X3,X2,X0)
| hAPP(X0,X1) = c_Option_Ooption_ONone(X2) ),
inference(resolution,[status(thm)],[f8489,f5379]) ).
fof(f20729,plain,
! [X0,X1,X2] :
( hAPP(hAPP(c_COMBK(tc_Option_Ooption(X2),X0),c_Option_Ooption_ONone(X2)),X1) = c_Option_Ooption_ONone(X2)
| hBOOL(hAPP(hAPP(c_member(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) ),
inference(paramodulation,[status(thm)],[f20329,f8489]) ).
fof(f20730,plain,
! [X0,X1,X2] : hAPP(hAPP(c_COMBK(tc_Option_Ooption(X0),X1),c_Option_Ooption_ONone(X0)),X2) = c_Option_Ooption_ONone(X0),
inference(forward_subsumption_resolution,[status(thm)],[f20729,f5295]) ).
fof(f20782,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Set_Oinsert(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))) = c_Map_Odom(X1,X0,hAPP(c_COMBK(tc_Option_Ooption(X0),X1),c_Option_Ooption_ONone(X0)))
| hAPP(hAPP(c_COMBK(tc_Option_Ooption(X0),X1),c_Option_Ooption_ONone(X0)),X2) != hAPP(c_Option_Ooption_OSome(X0),X3) ),
inference(paramodulation,[status(thm)],[f20329,f5305]) ).
fof(f20783,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Set_Oinsert(X2),X3),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))) = c_Map_Odom(X2,X0,hAPP(c_COMBK(tc_Option_Ooption(X0),X2),c_Option_Ooption_ONone(X0)))
| c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f20730,f20782]) ).
fof(f20784,plain,
! [X0,X1,X2,X3] :
( hAPP(hAPP(c_Set_Oinsert(X2),X3),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))
| c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f20329,f20783]) ).
fof(f20785,plain,
! [X0,X1] : c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1),
inference(forward_subsumption_resolution,[status(thm)],[f20784,f5427]) ).
fof(f20998,plain,
! [X0] : ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Ocom,c_Com_Ocom_OBODY),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),hAPP(c_Hoare__Mirabelle_OMGT,hAPP(c_Com_Ocom_OBODY,v_pna))),X0)),
inference(paramodulation,[status(thm)],[f5363,f20702]) ).
fof(f21232,plain,
! [X0,X1] : c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X1),
inference(resolution,[status(thm)],[f20207,f5258]) ).
fof(f23090,plain,
! [X0,X1] : ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Ocom,c_Com_Ocom_OBODY),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),hAPP(c_Set_Oimage(X0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(hAPP(c_Set_Oinsert(X0),hAPP(c_Com_Ocom_OBODY,v_pna)),X1))),
inference(paramodulation,[status(thm)],[f5458,f20998]) ).
fof(f23158,plain,
! [X0,X1,X2] : ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Ocom,c_Com_Ocom_OBODY),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),hAPP(c_Set_Oimage(X0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(X1,X0,c_Com_Ocom_OBODY),hAPP(hAPP(c_Set_Oinsert(X1),v_pna),X2)))),
inference(paramodulation,[status(thm)],[f5458,f23090]) ).
fof(f23176,plain,
! [X0,X1,X2,X3] :
( hAPP(X3,v_pna) = c_Option_Ooption_ONone(X2)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(tc_Com_Ostate,hAPP(c_Set_Oimage(tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Ocom,c_Com_Ocom_OBODY),c_Map_Odom(tc_Com_Opname,tc_Com_Ocom,c_Com_Obody))),hAPP(c_Set_Oimage(X0,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),c_Hoare__Mirabelle_OMGT),hAPP(c_Set_Oimage(X1,X0,c_Com_Ocom_OBODY),c_Map_Odom(X1,X2,X3)))) ),
inference(paramodulation,[status(thm)],[f20721,f23158]) ).
fof(f23424,plain,
hAPP(c_Com_Obody,v_pna) = c_Option_Ooption_ONone(tc_Com_Ocom),
inference(resolution,[status(thm)],[f23176,f21232]) ).
fof(f57414,plain,
c_Option_Ooption_ONone(tc_Com_Ocom) = hAPP(c_Option_Ooption_OSome(tc_Com_Ocom),v_ya),
inference(forward_demodulation,[status(thm)],[f23424,f19919]) ).
fof(f57415,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f57414,f20785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW384+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n020.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 09:51:17 UTC 2026
% 0.18/0.44 % CPUTime :
% 1.17/1.48 % Drodi V4.1.1
% 103.93/14.47 % Refutation found
% 103.93/14.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 103.93/14.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 17.52/14.66 % Elapsed time: 14.201442 seconds
% 17.52/14.66 % CPU time: 104.739649 seconds
% 17.52/14.66 % Total memory used: 1.370 GB
% 17.52/14.66 % Net memory used: 1.329 GB
%------------------------------------------------------------------------------