%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV892-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 : n003.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:44 PM UTC 2026
% Result : Unsatisfiable 39.30s 5.50s
% Output : CNFRefutation 38.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 23
% Syntax : Number of formulae : 80 ( 23 unt; 8 def)
% Number of atoms : 145 ( 44 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 127 ( 62 ~; 57 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 10 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-4 aty)
% Number of variables : 110 ( 110 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f176,axiom,
! [V_P,T_a,T_b,V_Q] : hAPP(c_COMBK(V_P,T_a,T_b),V_Q) = V_P,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f249,axiom,
! [T_a,V_c,V_A,V_B] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A))
| hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,axiom,
! [V_a_H,T_a] : c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f345,axiom,
! [V_P] :
( ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P))
| hAPP(c_Com_Obody,V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f408,axiom,
! [V_m,V_n,T_b,T_a,V_k] :
( hAPP(V_m,V_k) = c_Option_Ooption_ONone(T_a)
| hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k) != c_Option_Ooption_ONone(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f636,axiom,
! [V_pn] :
( hAPP(c_Com_Obody,V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f639,axiom,
! [V_x,T_a] : c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a) = V_x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f660,axiom,
! [V_l1,V_l2,T_a,T_b,V_m] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_m),c_Map_Odom(V_l2,T_a,T_b)))
| hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m) = hAPP(V_l2,V_m) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f661,axiom,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f662,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(f664,axiom,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f665,axiom,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f667,negated_conjecture,
c_Com_OWT__bodies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f669,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f670,negated_conjecture,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f977,plain,
! [X0,X1,X2,X3] : hAPP(c_COMBK(X0,X1,X2),X3) = X0,
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f1091,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A))
| ! [V_B] : hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)))) ),
inference(miniscoping,[status(thm)],[f249]) ).
fof(f1092,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2))
| hBOOL(hAPP(hAPP(c_in(X0),X1),c_Lattices_Oupper__semilattice__class_Osup(X2,X3,tc_fun(X0,tc_bool)))) ),
inference(cnf_transformation,[status(thm)],[f1091]) ).
fof(f1207,plain,
! [X0,X1] : c_Option_Ooption_OSome(X0,X1) != c_Option_Ooption_ONone(X1),
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f1236,plain,
! [X0] :
( ~ c_Com_OWT(c_Com_Ocom_OBODY(X0))
| hAPP(c_Com_Obody,X0) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X0),tc_Com_Ocom) ),
inference(cnf_transformation,[status(thm)],[f345]) ).
fof(f1330,plain,
! [V_m,T_a,V_k] :
( hAPP(V_m,V_k) = c_Option_Ooption_ONone(T_a)
| ! [V_n,T_b] : hAPP(c_Map_Omap__add(V_m,V_n,T_b,T_a),V_k) != c_Option_Ooption_ONone(T_a) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f1331,plain,
! [X0,X1,X2,X3,X4] :
( hAPP(X0,X4) = c_Option_Ooption_ONone(X3)
| hAPP(c_Map_Omap__add(X0,X1,X2,X3),X4) != c_Option_Ooption_ONone(X3) ),
inference(cnf_transformation,[status(thm)],[f1330]) ).
fof(f1714,plain,
! [X0] :
( hAPP(c_Com_Obody,X0) = c_Option_Ooption_ONone(tc_Com_Ocom)
| c_Com_OWT(c_Com_Ocom_OBODY(X0)) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f1717,plain,
! [X0,X1] : c_Option_Othe(c_Option_Ooption_OSome(X0,X1),X1) = X0,
inference(cnf_transformation,[status(thm)],[f639]) ).
fof(f1756,plain,
! [V_l2,T_a,T_b,V_m] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_m),c_Map_Odom(V_l2,T_a,T_b)))
| ! [V_l1] : hAPP(c_Map_Omap__add(V_l1,V_l2,T_a,T_b),V_m) = hAPP(V_l2,V_m) ),
inference(miniscoping,[status(thm)],[f660]) ).
fof(f1757,plain,
! [X0,X1,X2,X3,X4] :
( ~ hBOOL(hAPP(hAPP(c_in(X2),X4),c_Map_Odom(X1,X2,X3)))
| hAPP(c_Map_Omap__add(X0,X1,X2,X3),X4) = hAPP(X1,X4) ),
inference(cnf_transformation,[status(thm)],[f1756]) ).
fof(f1758,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f661]) ).
fof(f1759,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)],[f662]) ).
fof(f1760,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)],[f1759]) ).
fof(f1763,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(miniscoping,[status(thm)],[f664]) ).
fof(f1764,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f1763]) ).
fof(f1765,plain,
! [V_S,V_x] :
( ! [T_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f665]) ).
fof(f1766,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f1765]) ).
fof(f1768,plain,
c_Com_OWT__bodies,
inference(cnf_transformation,[status(thm)],[f667]) ).
fof(f1770,plain,
hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom))),
inference(cnf_transformation,[status(thm)],[f669]) ).
fof(f1771,plain,
~ c_Com_OWT(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom)),
inference(cnf_transformation,[status(thm)],[f670]) ).
fof(f1833,definition,
! [X0,X1] :
( sQ4_spl
<=> ( c_Com_OWT(X1)
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1834,plain,
! [X0,X1] :
( ~ sQ4_spl
| c_Com_OWT(X1)
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(X1,tc_Com_Ocom) ),
inference(component_clause,[status(thm)],[f1833]) ).
fof(f1836,definition,
( sQ5_spl
<=> c_Com_OWT__bodies ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1838,plain,
( sQ5_spl
| ~ c_Com_OWT__bodies ),
inference(component_clause,[status(thm)],[f1836]) ).
fof(f1839,plain,
( ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1760,f1833,f1836]) ).
fof(f1844,plain,
! [X0] :
( ~ sQ4_spl
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom),tc_Com_Ocom) ),
inference(resolution,[status(thm)],[f1834,f1771]) ).
fof(f1876,plain,
! [X0,X1,X2,X3,X4] :
( ~ hBOOL(hAPP(c_Map_Odom(X1,X2,X3),X4))
| hAPP(c_Map_Omap__add(X0,X1,X2,X3),X4) = hAPP(X1,X4) ),
inference(resolution,[status(thm)],[f1757,f1764]) ).
fof(f3221,plain,
hBOOL(hAPP(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_pn)),
inference(resolution,[status(thm)],[f1766,f1770]) ).
fof(f3418,plain,
! [X0] : hAPP(c_Map_Omap__add(X0,c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),v_pn) = hAPP(c_Com_Obody,v_pn),
inference(resolution,[status(thm)],[f1876,f3221]) ).
fof(f9779,plain,
! [X0] : hBOOL(hAPP(hAPP(c_in(tc_Com_Opname),v_pn),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),X0,tc_fun(tc_Com_Opname,tc_bool)))),
inference(resolution,[status(thm)],[f1092,f1770]) ).
fof(f9804,plain,
! [X0] : hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),X0,tc_fun(tc_Com_Opname,tc_bool)),v_pn)),
inference(resolution,[status(thm)],[f9779,f1766]) ).
fof(f12501,definition,
! [X2] :
( sQ82_spl
<=> X2 = c_Option_Ooption_ONone(tc_Com_Ocom) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f12502,plain,
! [X0] :
( ~ sQ82_spl
| X0 = c_Option_Ooption_ONone(tc_Com_Ocom) ),
inference(component_clause,[status(thm)],[f12501]) ).
fof(f12731,plain,
( ~ sQ82_spl
| $false ),
inference(resolution,[status(thm)],[f12502,f1207]) ).
fof(f12736,plain,
~ sQ82_spl,
inference(contradiction_clause,[status(thm)],[f12731]) ).
fof(f13299,plain,
! [X0] :
( hAPP(c_Com_Obody,X0) = c_Option_Ooption_ONone(tc_Com_Ocom)
| hAPP(c_Com_Obody,X0) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(X0),tc_Com_Ocom) ),
inference(resolution,[status(thm)],[f1236,f1714]) ).
fof(f13817,definition,
( sQ101_spl
<=> hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f13818,plain,
( ~ sQ101_spl
| hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) ),
inference(component_clause,[status(thm)],[f13817]) ).
fof(f14272,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1838,f1768]) ).
fof(f14273,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f14272]) ).
fof(f14348,plain,
( ~ sQ101_spl
| c_Option_Othe(hAPP(c_Com_Obody,v_pn),tc_Com_Ocom) = c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn) ),
inference(paramodulation,[status(thm)],[f13818,f1717]) ).
fof(f14439,definition,
! [X3] :
( sQ160_spl
<=> ~ hBOOL(hAPP(X3,v_pn)) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f14440,plain,
! [X0] :
( ~ sQ160_spl
| ~ hBOOL(hAPP(X0,v_pn)) ),
inference(component_clause,[status(thm)],[f14439]) ).
fof(f14448,plain,
( ~ sQ160_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f9804,f14440]) ).
fof(f14501,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f14448]) ).
fof(f14624,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ101_spl
| hAPP(c_Com_Obody,X0) != c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) ),
inference(backward_demodulation,[status(thm)],[f14348,f1844]) ).
fof(f14628,plain,
! [X0] :
( ~ sQ4_spl
| ~ sQ101_spl
| hAPP(c_Com_Obody,X0) != hAPP(c_Com_Obody,v_pn) ),
inference(forward_demodulation,[status(thm)],[f13818,f14624]) ).
fof(f14649,definition,
( sQ164_spl
<=> c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f14651,plain,
( sQ164_spl
| ~ c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) ),
inference(component_clause,[status(thm)],[f14649]) ).
fof(f14660,plain,
( sQ164_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f14651,f1758]) ).
fof(f14661,plain,
sQ164_spl,
inference(contradiction_clause,[status(thm)],[f14660]) ).
fof(f14768,plain,
( ~ sQ4_spl
| ~ sQ101_spl
| $false ),
inference(equality_resolution,[status(thm)],[f14628]) ).
fof(f14769,plain,
( ~ sQ4_spl
| ~ sQ101_spl ),
inference(contradiction_clause,[status(thm)],[f14768]) ).
fof(f16457,definition,
( sQ177_spl
<=> hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition]) ).
fof(f16459,plain,
( sQ177_spl
| hAPP(c_Com_Obody,v_pn) != c_Option_Ooption_ONone(tc_Com_Ocom) ),
inference(component_clause,[status(thm)],[f16457]) ).
fof(f16463,plain,
! [X0] :
( hAPP(X0,v_pn) = c_Option_Ooption_ONone(tc_Com_Ocom)
| hAPP(c_Com_Obody,v_pn) != c_Option_Ooption_ONone(tc_Com_Ocom) ),
inference(paramodulation,[status(thm)],[f3418,f1331]) ).
fof(f16472,definition,
! [X0] :
( sQ178_spl
<=> hAPP(X0,v_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition]) ).
fof(f16473,plain,
! [X0] :
( ~ sQ178_spl
| hAPP(X0,v_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ),
inference(component_clause,[status(thm)],[f16472]) ).
fof(f16475,plain,
( sQ178_spl
| ~ sQ177_spl ),
inference(split_clause,[status(thm)],[f16463,f16457,f16472]) ).
fof(f16476,plain,
( sQ177_spl
| hAPP(c_Com_Obody,v_pn) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(v_pn),tc_Com_Ocom) ),
inference(resolution,[status(thm)],[f16459,f13299]) ).
fof(f16478,plain,
( sQ177_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f16476,f13817,f16457]) ).
fof(f16591,plain,
! [X0] :
( ~ sQ178_spl
| X0 = c_Option_Ooption_ONone(tc_Com_Ocom) ),
inference(paramodulation,[status(thm)],[f977,f16473]) ).
fof(f16795,plain,
( ~ sQ178_spl
| sQ82_spl ),
inference(split_clause,[status(thm)],[f16591,f12501,f16472]) ).
fof(f16818,plain,
$false,
inference(sat_refutation,[status(thm)],[f1839,f12736,f14273,f14501,f14661,f14769,f16475,f16478,f16795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV892-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:31:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 39.30/5.50 % Refutation found
% 39.30/5.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 39.30/5.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 38.87/5.60 % Elapsed time: 5.214629 seconds
% 38.87/5.60 % CPU time: 40.503438 seconds
% 38.87/5.60 % Total memory used: 469.656 MB
% 38.87/5.60 % Net memory used: 432.406 MB
%------------------------------------------------------------------------------