%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW359+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 : n006.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:43 PM UTC 2026
% Result : Theorem 106.42s 14.98s
% Output : CNFRefutation 103.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 40 ( 21 unt; 0 def)
% Number of atoms : 69 ( 9 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 50 ( 21 ~; 20 |; 3 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 92 ( 90 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V_G_2,V_c_2] :
( v_wt(V_c_2)
=> ( ! [B_x] :
( hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),B_x),v_U))
=> v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,B_x)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))) )
=> v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(V_c_2)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [V_B_2,V_a_2,V_f_2,T_b,T_c] : hAPP(c_Set_Oimage(T_c,T_b,V_f_2),hAPP(hAPP(c_Set_Oinsert(T_c),V_a_2),V_B_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),hAPP(V_f_2,V_a_2)),hAPP(c_Set_Oimage(T_c,T_b,V_f_2),V_B_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [V_G_2,V_ts_2] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),V_ts_2),V_G_2))
=> v_P(V_G_2,V_ts_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [V_f_2,T_b,T_c] : hAPP(c_Set_Oimage(T_c,T_b,V_f_2),c_Orderings_Obot__class_Obot(tc_fun(T_c,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [V_A_2,T_b] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))),V_A_2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [V_a_2,V_D_2,V_C_2,T_b] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [V_A_2,V_a_2,T_b] :
( hBOOL(hAPP(hAPP(c_member(T_b),V_a_2),V_A_2))
=> hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_A_2) = V_A_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5225,hypothesis,
v_wt(v_c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5227,conjecture,
v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(v_c)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5228,negated_conjecture,
~ v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(v_c)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(negated_conjecture,[status(cth)],[f5227]) ).
fof(f5232,plain,
! [V_G_2,V_c_2] :
( v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(V_c_2)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ? [B_x] :
( ~ v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,B_x)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
& hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),B_x),v_U)) )
| ~ v_wt(V_c_2) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f5233,plain,
! [V_c_2] :
( ! [V_G_2] :
( v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(V_c_2)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ? [B_x] :
( ~ v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,B_x)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
& hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),B_x),v_U)) ) )
| ~ v_wt(V_c_2) ),
inference(miniscoping,[status(thm)],[f5232]) ).
fof(f5234,plain,
! [V_c_2] :
( ! [V_G_2] :
( v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(V_c_2)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ( ~ v_P(V_G_2,hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,sK1_skl(V_G_2,V_c_2))),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
& hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),sK1_skl(V_G_2,V_c_2)),v_U)) ) )
| ~ v_wt(V_c_2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(B_x,sK1_skl(V_G_2,V_c_2))],[f5233]) ).
fof(f5235,plain,
! [X0,X1] :
( v_P(X1,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(X0)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),sK1_skl(X1,X0)),v_U))
| ~ v_wt(X0) ),
inference(cnf_transformation,[status(thm)],[f5234]) ).
fof(f5236,plain,
! [X0,X1] :
( v_P(X1,hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(X0)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ~ v_P(X1,hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,sK1_skl(X1,X0))),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ~ v_wt(X0) ),
inference(cnf_transformation,[status(thm)],[f5234]) ).
fof(f5246,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)],[f7]) ).
fof(f5247,plain,
! [V_G_2,V_ts_2] :
( v_P(V_G_2,V_ts_2)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),V_ts_2),V_G_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f5248,plain,
! [X0,X1] :
( v_P(X1,X0)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f5247]) ).
fof(f5253,plain,
! [X0,X1,X2] : hAPP(c_Set_Oimage(X0,X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f5265,plain,
! [X0,X1] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))),X1)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f5294,plain,
! [V_a_2,V_D_2,V_C_2,T_b] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f5295,plain,
! [V_D_2,V_C_2,T_b] :
( ! [V_a_2] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_C_2)),hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_D_2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_C_2),V_D_2)) ),
inference(miniscoping,[status(thm)],[f5294]) ).
fof(f5296,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X3),X1)),hAPP(hAPP(c_Set_Oinsert(X0),X3),X2)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X2)) ),
inference(cnf_transformation,[status(thm)],[f5295]) ).
fof(f5452,plain,
! [V_A_2,V_a_2,T_b] :
( hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),V_A_2) = V_A_2
| ~ hBOOL(hAPP(hAPP(c_member(T_b),V_a_2),V_A_2)) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f5453,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)],[f5452]) ).
fof(f20149,plain,
v_wt(v_c),
inference(cnf_transformation,[status(thm)],[f5225]) ).
fof(f20151,plain,
~ v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(v_c)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(cnf_transformation,[status(thm)],[f5228]) ).
fof(f20590,plain,
( hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),sK1_skl(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),v_c)),v_U))
| ~ v_wt(v_c) ),
inference(resolution,[status(thm)],[f5235,f20151]) ).
fof(f20591,plain,
hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),sK1_skl(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),v_c)),v_U)),
inference(forward_subsumption_resolution,[status(thm)],[f20590,f20149]) ).
fof(f20937,plain,
! [X0,X1,X2,X3] : hAPP(c_Set_Oimage(X0,X1,X2),hAPP(hAPP(c_Set_Oinsert(X0),X3),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))) = hAPP(hAPP(c_Set_Oinsert(X1),hAPP(X2,X3)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),
inference(paramodulation,[status(thm)],[f5253,f5246]) ).
fof(f21629,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(c_Set_Oimage(X2,X0,X3),hAPP(hAPP(c_Set_Oinsert(X2),X4),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool))))),hAPP(hAPP(c_Set_Oinsert(X0),hAPP(X3,X4)),X1)))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))),X1)) ),
inference(paramodulation,[status(thm)],[f20937,f5296]) ).
fof(f21647,plain,
! [X0,X1,X2,X3,X4] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(c_Set_Oimage(X1,X0,X2),hAPP(hAPP(c_Set_Oinsert(X1),X3),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))))),hAPP(hAPP(c_Set_Oinsert(X0),hAPP(X2,X3)),X4))),
inference(forward_subsumption_resolution,[status(thm)],[f21629,f5265]) ).
fof(f21834,plain,
! [X0,X1,X2,X3] : v_P(hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(X0,X1)),X2),hAPP(c_Set_Oimage(X3,t_a,X0),hAPP(hAPP(c_Set_Oinsert(X3),X1),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_HOL_Obool))))),
inference(resolution,[status(thm)],[f21647,f5248]) ).
fof(f21867,plain,
! [X0,X1,X2] : v_P(hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(X0,X1)),X2),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(X0,X1)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(forward_demodulation,[status(thm)],[f20937,f21834]) ).
fof(f21887,plain,
! [X0,X1,X2,X3] : v_P(hAPP(c_Set_Oimage(X0,t_a,X1),hAPP(hAPP(c_Set_Oinsert(X0),X2),X3)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(X1,X2)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(paramodulation,[status(thm)],[f5246,f21867]) ).
fof(f31586,plain,
hAPP(hAPP(c_Set_Oinsert(tc_Com_Opname),sK1_skl(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),v_c)),v_U) = v_U,
inference(resolution,[status(thm)],[f5453,f20591]) ).
fof(f31681,plain,
! [X0] : v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,X0),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(X0,sK1_skl(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),v_c))),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(paramodulation,[status(thm)],[f31586,f21887]) ).
fof(f32751,plain,
( v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(v_c)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool))))
| ~ v_wt(v_c) ),
inference(resolution,[status(thm)],[f31681,f5236]) ).
fof(f32752,plain,
v_P(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),hAPP(hAPP(c_Set_Oinsert(t_a),v_mgt(v_c)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),
inference(forward_subsumption_resolution,[status(thm)],[f32751,f20149]) ).
fof(f32753,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f32752,f20151]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW359+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n006.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 09:49:12 UTC 2026
% 0.19/0.46 % CPUTime :
% 1.25/1.50 % Drodi V4.1.1
% 106.42/14.98 % Refutation found
% 106.42/14.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 106.42/14.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 52.48/15.16 % Elapsed time: 14.686610 seconds
% 52.48/15.16 % CPU time: 107.757930 seconds
% 52.48/15.16 % Total memory used: 1.421 GB
% 52.48/15.16 % Net memory used: 1.382 GB
%------------------------------------------------------------------------------