%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW365+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 14.33s 3.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW365+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.50 % Computer : n015.cluster.edu
% 0.19/0.50 % Model : x86_64 x86_64
% 0.19/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.50 % Memory : 8046.5625MB
% 0.19/0.50 % OS : Linux 6.8.0-71-generic
% 0.19/0.50 % CPULimit : 300
% 0.19/0.50 % WCLimit : 300
% 0.19/0.50 % DateTime : Mon Sep 21 09:52:36 UTC 2026
% 0.19/0.50 % CPUTime :
% 1.14/1.54 % Drodi V4.1.1
% 14.33/3.29 % Refutation found
% 14.33/3.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.33/3.29 % SZS output start CNFRefutation for theBenchmark
% 14.33/3.29 fof(f7,axiom,(
% 14.33/3.29 (! [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)) )),
% 14.33/3.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.33/3.29 fof(f69,axiom,(
% 14.33/3.29 (! [V_B_2,V_A_2,V_x_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_x_2),V_A_2)),V_B_2))<=> ( hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_B_2))& hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)) ) ) )),
% 14.33/3.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.33/3.29 fof(f5230,hypothesis,(
% 14.33/3.29 hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G)) ),
% 14.33/3.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.33/3.29 fof(f5231,conjecture,(
% 14.33/3.29 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)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)) ),
% 14.33/3.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 14.33/3.29 fof(f5232,negated_conjecture,(
% 14.33/3.29 ~(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)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G)) )),
% 14.33/3.29 inference(negated_conjecture,[status(cth)],[f5231])).
% 14.33/3.29 fof(f5253,plain,(
% 14.33/3.29 ![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)))),
% 14.33/3.29 inference(cnf_transformation,[status(thm)],[f7])).
% 14.33/3.29 fof(f5444,plain,(
% 14.33/3.29 ![V_B_2,V_A_2,V_x_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_x_2),V_A_2)),V_B_2))|(hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_B_2))&hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_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_x_2),V_A_2)),V_B_2))|(~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_B_2))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)))))),
% 14.33/3.29 inference(NNF_transformation,[status(thm)],[f69])).
% 14.33/3.29 fof(f5445,plain,(
% 14.33/3.29 (![V_B_2,V_A_2,V_x_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_x_2),V_A_2)),V_B_2))|(hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_B_2))&hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)))))&(![V_B_2,V_A_2,V_x_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_x_2),V_A_2)),V_B_2))|(~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_B_2))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)))))),
% 14.33/3.29 inference(miniscoping,[status(thm)],[f5444])).
% 14.33/3.29 fof(f5448,plain,(
% 14.33/3.29 ![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),X1),X2)),X3))|~hBOOL(hAPP(hAPP(c_member(X0),X1),X3))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X2),X3)))),
% 14.33/3.29 inference(cnf_transformation,[status(thm)],[f5445])).
% 14.33/3.29 fof(f20153,plain,(
% 14.33/3.29 hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G))),
% 14.33/3.29 inference(cnf_transformation,[status(thm)],[f5230])).
% 14.33/3.29 fof(f20154,plain,(
% 14.33/3.29 ~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)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G))),
% 14.33/3.29 inference(cnf_transformation,[status(thm)],[f5232])).
% 14.33/3.29 fof(f21176,plain,(
% 14.33/3.29 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)))),X2))|~hBOOL(hAPP(hAPP(c_member(X0),X1),X2)))),
% 14.33/3.29 inference(resolution,[status(thm)],[f5448,f5253])).
% 14.33/3.29 fof(f22296,plain,(
% 14.33/3.29 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)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_HOL_Obool)))),v_G))),
% 14.33/3.33 inference(resolution,[status(thm)],[f21176,f20153])).
% 14.33/3.33 fof(f22308,plain,(
% 14.33/3.33 $false),
% 14.33/3.33 inference(forward_subsumption_resolution,[status(thm)],[f22296,f20154])).
% 14.33/3.33 % SZS output end CNFRefutation for theBenchmark.p
% 2.65/3.48 % Elapsed time: 2.952306 seconds
% 2.65/3.48 % CPU time: 15.003745 seconds
% 2.65/3.48 % Total memory used: 745.062 MB
% 2.65/3.48 % Net memory used: 734.983 MB
%------------------------------------------------------------------------------