%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW367+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:09:02 PM UTC 2026
% Result : Theorem 149.44s 20.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW367+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 09:52:51 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.81/1.10 % Drodi V4.1.1
% 149.44/20.00 % Refutation found
% 149.44/20.00 % SZS status Theorem for theBenchmark: Theorem is valid
% 149.44/20.00 % SZS output start CNFRefutation for theBenchmark
% 149.44/20.00 fof(f46,axiom,(
% 149.44/20.00 (! [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))) ) )),
% 149.44/20.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 149.44/20.00 fof(f54,axiom,(
% 149.44/20.00 (! [V_f_2,T_c,V_A_2,V_x_2,T_b] :( hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))=> hAPP(hAPP(c_Set_Oinsert(T_c),hAPP(V_f_2,V_x_2)),hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2)) = hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2) ) )),
% 149.44/20.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 149.44/20.00 fof(f5225,hypothesis,(
% 149.44/20.00 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
% 149.44/20.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 149.44/20.00 fof(f5228,hypothesis,(
% 149.44/20.00 hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pn),v_U)) ),
% 149.44/20.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 149.44/20.00 fof(f5230,conjecture,(
% 149.44/20.00 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
% 149.44/20.00 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 149.44/20.00 fof(f5231,negated_conjecture,(
% 149.44/20.00 ~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) )),
% 149.44/20.00 inference(negated_conjecture,[status(cth)],[f5230])).
% 149.44/20.00 fof(f5374,plain,(
% 149.44/20.00 ![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))))),
% 149.44/20.00 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 149.44/20.00 fof(f5375,plain,(
% 149.44/20.00 ![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))|(![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)))))),
% 149.44/20.00 inference(miniscoping,[status(thm)],[f5374])).
% 149.44/20.00 fof(f5376,plain,(
% 149.44/20.00 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X2))|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))))),
% 149.44/20.00 inference(cnf_transformation,[status(thm)],[f5375])).
% 149.44/20.00 fof(f5401,plain,(
% 149.44/20.00 ![V_f_2,T_c,V_A_2,V_x_2,T_b]: (~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))|hAPP(hAPP(c_Set_Oinsert(T_c),hAPP(V_f_2,V_x_2)),hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2))=hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2))),
% 149.44/20.00 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 149.44/20.00 fof(f5402,plain,(
% 149.44/20.00 ![V_A_2,V_x_2,T_b]: (~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))|(![V_f_2,T_c]: hAPP(hAPP(c_Set_Oinsert(T_c),hAPP(V_f_2,V_x_2)),hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2))=hAPP(c_Set_Oimage(T_b,T_c,V_f_2),V_A_2)))),
% 149.44/20.00 inference(miniscoping,[status(thm)],[f5401])).
% 149.44/20.00 fof(f5403,plain,(
% 149.44/20.00 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(hAPP(c_Set_Oinsert(X3),hAPP(X4,X1)),hAPP(c_Set_Oimage(X0,X3,X4),X2))=hAPP(c_Set_Oimage(X0,X3,X4),X2))),
% 149.44/20.00 inference(cnf_transformation,[status(thm)],[f5402])).
% 149.44/20.00 fof(f20146,plain,(
% 149.44/20.00 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))),
% 149.44/20.00 inference(cnf_transformation,[status(thm)],[f5225])).
% 149.44/20.00 fof(f20149,plain,(
% 149.44/20.00 hBOOL(hAPP(hAPP(c_member(tc_Com_Opname),v_pn),v_U))),
% 149.44/20.00 inference(cnf_transformation,[status(thm)],[f5228])).
% 149.44/20.00 fof(f20151,plain,(
% 149.44/20.00 ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))),
% 127.44/20.20 inference(cnf_transformation,[status(thm)],[f5231])).
% 127.44/20.20 fof(f21248,plain,(
% 127.44/20.20 ![X0,X1]: (hAPP(hAPP(c_Set_Oinsert(X0),hAPP(X1,v_pn)),hAPP(c_Set_Oimage(tc_Com_Opname,X0,X1),v_U))=hAPP(c_Set_Oimage(tc_Com_Opname,X0,X1),v_U))),
% 127.44/20.20 inference(resolution,[status(thm)],[f5403,f20149])).
% 127.44/20.20 fof(f21412,plain,(
% 127.44/20.20 ![X0]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),X0),v_G)),hAPP(hAPP(c_Set_Oinsert(t_a),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))))),
% 127.44/20.20 inference(resolution,[status(thm)],[f5376,f20146])).
% 127.44/20.20 fof(f52001,plain,(
% 127.44/20.20 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))),
% 127.44/20.20 inference(paramodulation,[status(thm)],[f21248,f21412])).
% 127.44/20.20 fof(f52003,plain,(
% 127.44/20.20 $false),
% 127.44/20.20 inference(forward_subsumption_resolution,[status(thm)],[f52001,f20151])).
% 127.44/20.20 % SZS output end CNFRefutation for theBenchmark.p
% 6.31/20.36 % Elapsed time: 19.969092 seconds
% 6.31/20.36 % CPU time: 151.470196 seconds
% 6.31/20.36 % Total memory used: 1.477 GB
% 6.31/20.36 % Net memory used: 1.421 GB
%------------------------------------------------------------------------------