%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:53:18 PM UTC 2026
% Result : Unsatisfiable 4.35s 1.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV884-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n013.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 09:29:35 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.42 % Drodi V4.1.1
% 4.35/1.07 % Refutation found
% 4.35/1.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.35/1.07 % SZS output start CNFRefutation for theBenchmark
% 4.35/1.07 fof(f959,axiom,(
% 4.35/1.07 (![V_a,V_C,T_a,V_D]: (( c_lessequals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool))| ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool)) ) ))),
% 4.35/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.35/1.07 fof(f1037,axiom,(
% 4.35/1.07 (![V_f,V_x,V_A,T_a,T_b]: (( c_Set_Oinsert(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b) = c_Set_Oimage(V_f,V_A,T_a,T_b)| ~ c_in(V_x,V_A,T_a) ) ))),
% 4.35/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.35/1.07 fof(f1057,negated_conjecture,(
% 4.35/1.07 c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
% 4.35/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.35/1.07 fof(f1060,negated_conjecture,(
% 4.35/1.07 c_in(v_pn,v_U,tc_Com_Opname) ),
% 4.35/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.35/1.07 fof(f1062,negated_conjecture,(
% 4.35/1.07 ~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
% 4.35/1.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.35/1.07 fof(f2647,plain,(
% 4.35/1.07 ![V_C,T_a,V_D]: ((![V_a]: c_lessequals(c_Set_Oinsert(V_a,V_C,T_a),c_Set_Oinsert(V_a,V_D,T_a),tc_fun(T_a,tc_bool)))|~c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool)))),
% 4.35/1.07 inference(miniscoping,[status(thm)],[f959])).
% 4.35/1.07 fof(f2648,plain,(
% 4.35/1.07 ![X0,X1,X2,X3]: (c_lessequals(c_Set_Oinsert(X0,X1,X2),c_Set_Oinsert(X0,X3,X2),tc_fun(X2,tc_bool))|~c_lessequals(X1,X3,tc_fun(X2,tc_bool)))),
% 4.35/1.07 inference(cnf_transformation,[status(thm)],[f2647])).
% 4.35/1.07 fof(f2770,plain,(
% 4.35/1.07 ![V_x,V_A,T_a]: ((![V_f,T_b]: c_Set_Oinsert(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)=c_Set_Oimage(V_f,V_A,T_a,T_b))|~c_in(V_x,V_A,T_a))),
% 4.35/1.07 inference(miniscoping,[status(thm)],[f1037])).
% 4.35/1.07 fof(f2771,plain,(
% 4.35/1.07 ![X0,X1,X2,X3,X4]: (c_Set_Oinsert(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4)=c_Set_Oimage(X0,X2,X3,X4)|~c_in(X1,X2,X3))),
% 4.35/1.07 inference(cnf_transformation,[status(thm)],[f2770])).
% 4.35/1.07 fof(f2803,plain,(
% 4.35/1.07 c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))),
% 4.35/1.07 inference(cnf_transformation,[status(thm)],[f1057])).
% 4.35/1.07 fof(f2806,plain,(
% 4.35/1.07 c_in(v_pn,v_U,tc_Com_Opname)),
% 4.35/1.07 inference(cnf_transformation,[status(thm)],[f1060])).
% 4.35/1.07 fof(f2808,plain,(
% 4.35/1.07 ~c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))),
% 4.35/1.07 inference(cnf_transformation,[status(thm)],[f1062])).
% 4.35/1.07 fof(f3823,plain,(
% 4.35/1.07 ![X0]: (c_lessequals(c_Set_Oinsert(X0,v_G,t_a),c_Set_Oinsert(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_fun(t_a,tc_bool)))),
% 4.35/1.07 inference(resolution,[status(thm)],[f2648,f2803])).
% 4.35/1.07 fof(f4151,plain,(
% 4.35/1.07 ![X0,X1]: (c_Set_Oinsert(hAPP(X0,v_pn),c_Set_Oimage(X0,v_U,tc_Com_Opname,X1),X1)=c_Set_Oimage(X0,v_U,tc_Com_Opname,X1))),
% 4.35/1.07 inference(resolution,[status(thm)],[f2771,f2806])).
% 4.35/1.07 fof(f4203,plain,(
% 4.35/1.07 c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))),
% 4.35/1.07 inference(paramodulation,[status(thm)],[f4151,f3823])).
% 4.35/1.07 fof(f4211,plain,(
% 4.35/1.07 $false),
% 4.35/1.07 inference(forward_subsumption_resolution,[status(thm)],[f4203,f2808])).
% 4.35/1.07 % SZS output end CNFRefutation for theBenchmark.p
% 4.35/1.10 % Elapsed time: 0.736920 seconds
% 4.35/1.10 % CPU time: 4.934950 seconds
% 4.35/1.10 % Total memory used: 206.767 MB
% 4.35/1.10 % Net memory used: 204.081 MB
%------------------------------------------------------------------------------