%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW364+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 : n001.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:01 PM UTC 2026
% Result : Theorem 219.57s 29.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW364+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.46 % Computer : n001.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 09:54:45 UTC 2026
% 0.19/0.46 % CPUTime :
% 1.27/1.55 % Drodi V4.1.1
% 219.57/29.31 % Refutation found
% 219.57/29.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 219.57/29.31 % SZS output start CNFRefutation for theBenchmark
% 219.57/29.31 fof(f2,axiom,(
% 219.57/29.31 (! [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) ) )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f7,axiom,(
% 219.57/29.31 (! [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)) )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f37,axiom,(
% 219.57/29.31 (! [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 ) )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f60,axiom,(
% 219.57/29.31 (! [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))) ) )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f3275,axiom,(
% 219.57/29.31 (! [V_Pa_2,T_b] : hAPP(c_Set_OCollect(T_b),V_Pa_2) = V_Pa_2 )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f3288,axiom,(
% 219.57/29.31 (! [V_a_2,T_b] : hAPP(c_Set_OCollect(T_b),hAPP(c_fequal,V_a_2)) = hAPP(hAPP(c_Set_Oinsert(T_b),V_a_2),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_HOL_Obool))) )),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f5230,hypothesis,(
% 219.57/29.31 hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G)) ),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f5231,conjecture,(
% 219.57/29.31 v_P(v_G,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)))) ),
% 219.57/29.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 219.57/29.31 fof(f5232,negated_conjecture,(
% 219.57/29.31 ~(v_P(v_G,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)))) )),
% 219.57/29.31 inference(negated_conjecture,[status(cth)],[f5231])).
% 219.57/29.31 fof(f5236,plain,(
% 219.57/29.31 ![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))),
% 219.57/29.31 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 219.57/29.31 fof(f5237,plain,(
% 219.57/29.31 ![X0,X1]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),X1))|v_P(X1,X0))),
% 219.57/29.31 inference(cnf_transformation,[status(thm)],[f5236])).
% 219.57/29.31 fof(f5253,plain,(
% 219.57/29.31 ![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)))),
% 219.57/29.31 inference(cnf_transformation,[status(thm)],[f7])).
% 219.57/29.31 fof(f5342,plain,(
% 219.57/29.31 ![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)),
% 219.57/29.31 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 219.57/29.31 fof(f5343,plain,(
% 219.57/29.31 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hAPP(hAPP(c_Set_Oinsert(X0),X1),X2)=X2)),
% 219.57/29.31 inference(cnf_transformation,[status(thm)],[f5342])).
% 219.57/29.31 fof(f5415,plain,(
% 219.57/29.31 ![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))))),
% 219.57/29.31 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 219.57/29.31 fof(f5416,plain,(
% 219.57/29.31 ![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)))))),
% 219.57/29.31 inference(miniscoping,[status(thm)],[f5415])).
% 219.57/29.31 fof(f5417,plain,(
% 219.57/29.31 ![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))))),
% 214.22/29.57 inference(cnf_transformation,[status(thm)],[f5416])).
% 214.22/29.57 fof(f15161,plain,(
% 214.22/29.57 ![X0,X1]: (hAPP(c_Set_OCollect(X0),X1)=X1)),
% 214.22/29.57 inference(cnf_transformation,[status(thm)],[f3275])).
% 214.22/29.57 fof(f15186,plain,(
% 214.22/29.57 ![X0,X1]: (hAPP(c_Set_OCollect(X0),hAPP(c_fequal,X1))=hAPP(hAPP(c_Set_Oinsert(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool))))),
% 214.22/29.57 inference(cnf_transformation,[status(thm)],[f3288])).
% 214.22/29.57 fof(f20153,plain,(
% 214.22/29.57 hBOOL(hAPP(hAPP(c_member(t_a),hAPP(v_mgt__call,v_pn)),v_G))),
% 214.22/29.57 inference(cnf_transformation,[status(thm)],[f5230])).
% 214.22/29.57 fof(f20154,plain,(
% 214.22/29.57 ~v_P(v_G,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))))),
% 214.22/29.57 inference(cnf_transformation,[status(thm)],[f5232])).
% 214.22/29.57 fof(f22641,plain,(
% 214.22/29.57 ![X0,X1]: (hAPP(c_fequal,X0)=hAPP(hAPP(c_Set_Oinsert(X1),X0),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))))),
% 214.22/29.57 inference(forward_demodulation,[status(thm)],[f15161,f15186])).
% 214.22/29.57 fof(f24149,plain,(
% 214.22/29.57 ~v_P(v_G,hAPP(c_fequal,hAPP(v_mgt__call,v_pn)))),
% 214.22/29.57 inference(forward_demodulation,[status(thm)],[f22641,f20154])).
% 214.22/29.57 fof(f24953,plain,(
% 214.22/29.57 hAPP(hAPP(c_Set_Oinsert(t_a),hAPP(v_mgt__call,v_pn)),v_G)=v_G),
% 214.22/29.57 inference(resolution,[status(thm)],[f5343,f20153])).
% 214.22/29.57 fof(f25139,plain,(
% 214.22/29.57 ![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)))),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))))),
% 214.22/29.57 inference(resolution,[status(thm)],[f5417,f5253])).
% 214.22/29.57 fof(f25141,plain,(
% 214.22/29.57 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),hAPP(c_fequal,X1)),hAPP(hAPP(c_Set_Oinsert(X0),X1),X2))))),
% 214.22/29.57 inference(forward_demodulation,[status(thm)],[f22641,f25139])).
% 214.22/29.57 fof(f25142,plain,(
% 214.22/29.57 ![X0,X1]: (v_P(hAPP(hAPP(c_Set_Oinsert(t_a),X0),X1),hAPP(c_fequal,X0)))),
% 214.22/29.57 inference(resolution,[status(thm)],[f25141,f5237])).
% 214.22/29.57 fof(f25151,plain,(
% 214.22/29.57 v_P(v_G,hAPP(c_fequal,hAPP(v_mgt__call,v_pn)))),
% 214.22/29.57 inference(paramodulation,[status(thm)],[f24953,f25142])).
% 214.22/29.57 fof(f25155,plain,(
% 214.22/29.57 $false),
% 214.22/29.57 inference(forward_subsumption_resolution,[status(thm)],[f25151,f24149])).
% 214.22/29.57 % SZS output end CNFRefutation for theBenchmark.p
% 49.33/29.60 % Elapsed time: 29.111641 seconds
% 49.33/29.60 % CPU time: 221.807021 seconds
% 49.33/29.60 % Total memory used: 1.819 GB
% 49.33/29.60 % Net memory used: 1.700 GB
%------------------------------------------------------------------------------