%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV879-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 : n016.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:43 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.68s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 14 unt; 0 def)
% Number of atoms : 51 ( 2 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 28 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-4 aty)
% Number of variables : 59 ( 59 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f616,axiom,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f640,axiom,
! [V_G,V_ts] :
( ~ c_lessequals(V_ts,V_G,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,V_G),V_ts)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f647,axiom,
! [V_x,V_A,T_a,V_B] :
( ~ hBOOL(c_in(V_x,V_B,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f844,axiom,
! [V_x,V_S,T_a] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(c_in(V_x,V_S,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f845,axiom,
! [V_S,V_x,T_a] :
( ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f857,axiom,
! [V_x,V_A,T_aa,V_f,T_a] :
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f862,negated_conjecture,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f863,negated_conjecture,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f864,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1935,plain,
! [X0,X1] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(thm)],[f616]) ).
fof(f1973,plain,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f640]) ).
fof(f1983,plain,
! [V_x,T_a,V_B] :
( ~ hBOOL(c_in(V_x,V_B,T_a))
| ! [V_A] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ) ),
inference(miniscoping,[status(thm)],[f647]) ).
fof(f1984,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(c_in(X0,X3,X2))
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(thm)],[f1983]) ).
fof(f2281,plain,
! [V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| ! [T_a] : hBOOL(c_in(V_x,V_S,T_a)) ),
inference(miniscoping,[status(thm)],[f844]) ).
fof(f2282,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP(X1,X0))
| hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f2281]) ).
fof(f2283,plain,
! [V_S,V_x] :
( ! [T_a] : ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
inference(miniscoping,[status(thm)],[f845]) ).
fof(f2284,plain,
! [X0,X1,X2] :
( ~ hBOOL(c_in(X1,X0,X2))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f2283]) ).
fof(f2302,plain,
! [V_x,V_A,T_aa] :
( ! [V_f,T_a] : hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
inference(miniscoping,[status(thm)],[f857]) ).
fof(f2303,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(c_in(hAPP(X3,X0),c_Set_Oimage(X3,X1,X2,X4),X4))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f2302]) ).
fof(f2311,plain,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(cnf_transformation,[status(thm)],[f862]) ).
fof(f2312,plain,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
inference(cnf_transformation,[status(thm)],[f863]) ).
fof(f2313,plain,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(cnf_transformation,[status(thm)],[f864]) ).
fof(f2377,plain,
~ hBOOL(hAPP(hAPP(v_P,v_G),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(forward_demodulation,[status(thm)],[f2311,f2313]) ).
fof(f2932,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),v_G,tc_fun(t_a,tc_bool)),
inference(resolution,[status(thm)],[f1973,f2377]) ).
fof(f3759,plain,
( ~ hBOOL(c_in(hAPP(v_mgt__call,v_x),v_G,t_a))
| ~ c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),v_G,tc_fun(t_a,tc_bool)) ),
inference(resolution,[status(thm)],[f1984,f2932]) ).
fof(f3776,plain,
~ hBOOL(c_in(hAPP(v_mgt__call,v_x),v_G,t_a)),
inference(forward_subsumption_resolution,[status(thm)],[f3759,f1935]) ).
fof(f3908,plain,
~ hBOOL(hAPP(v_G,hAPP(v_mgt__call,v_x))),
inference(resolution,[status(thm)],[f3776,f2282]) ).
fof(f3965,plain,
! [X0,X1,X2,X3,X4] :
( hBOOL(hAPP(c_Set_Oimage(X3,X1,X2,X4),hAPP(X3,X0)))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f2303,f2284]) ).
fof(f3980,plain,
! [X0] :
( hBOOL(hAPP(v_G,hAPP(v_mgt__call,X0)))
| ~ hBOOL(c_in(X0,v_U,tc_Com_Opname)) ),
inference(paramodulation,[status(thm)],[f2311,f3965]) ).
fof(f3990,plain,
~ hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
inference(resolution,[status(thm)],[f3980,f3908]) ).
fof(f3991,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f3990,f2312]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV879-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.55 % Computer : n016.cluster.edu
% 0.08/0.55 % Model : x86_64 x86_64
% 0.08/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.55 % Memory : 8046.5625MB
% 0.08/0.55 % OS : Linux 6.8.0-71-generic
% 0.08/0.55 % CPULimit : 300
% 0.08/0.55 % WCLimit : 300
% 0.08/0.55 % DateTime : Mon Sep 21 09:34:39 UTC 2026
% 0.12/0.56 % CPUTime :
% 0.14/0.63 % Drodi V4.1.1
% 0.14/0.68 % Refutation found
% 0.14/0.68 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.72 % Elapsed time: 0.151767 seconds
% 0.14/0.72 % CPU time: 0.534903 seconds
% 0.14/0.72 % Total memory used: 130.061 MB
% 0.14/0.72 % Net memory used: 129.530 MB
%------------------------------------------------------------------------------