%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW473+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:14 PM UTC 2026
% Result : Theorem 1.25s 0.68s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW473+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:58:41 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.43 % Drodi V4.1.1
% 1.25/0.68 % Refutation found
% 1.25/0.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.25/0.68 % SZS output start CNFRefutation for theBenchmark
% 1.25/0.68 fof(f372,axiom,(
% 1.25/0.68 (! [A_1] : hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),A_1)) )),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f402,axiom,(
% 1.25/0.68 (! [C_6,A_1,B_6] :( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))=> ( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,B_6),C_6))=> hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),C_6)) ) ) )),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f437,axiom,(
% 1.25/0.68 (! [A_3,C_6,D_1] :( hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_6),D_1))=> hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_3,C_6)),insert_a(A_3,D_1))) ) )),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f441,axiom,(
% 1.25/0.68 (! [F,A_3,B_6] : image_pname_a(F,insert_pname(A_3,B_6)) = insert_a(hAPP_pname_a(F,A_3),image_pname_a(F,B_6)) )),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f447,axiom,(
% 1.25/0.68 (! [F,X_3,A_1] :( hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1))=> insert_a(hAPP_pname_a(F,X_3),image_pname_a(F,A_1)) = image_pname_a(F,A_1) ) )),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f912,hypothesis,(
% 1.25/0.68 hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u))) ),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f915,hypothesis,(
% 1.25/0.68 hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u)) ),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f917,conjecture,(
% 1.25/0.68 hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))) ),
% 1.25/0.68 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.25/0.68 fof(f918,negated_conjecture,(
% 1.25/0.68 ~(hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u))) )),
% 1.25/0.68 inference(negated_conjecture,[status(cth)],[f917])).
% 1.25/0.68 fof(f2061,plain,(
% 1.25/0.68 ![X0]: (hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X0)))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f372])).
% 1.25/0.68 fof(f2144,plain,(
% 1.25/0.68 ![C_6,A_1,B_6]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))|(~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,B_6),C_6))|hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),C_6))))),
% 1.25/0.68 inference(pre_NNF_transformation,[status(thm)],[f402])).
% 1.25/0.68 fof(f2145,plain,(
% 1.25/0.68 ![A_1,B_6]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),B_6))|(![C_6]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,B_6),C_6))|hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,A_1),C_6)))))),
% 1.25/0.68 inference(miniscoping,[status(thm)],[f2144])).
% 1.25/0.68 fof(f2146,plain,(
% 1.25/0.68 ![X0,X1,X2]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X2)))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f2145])).
% 1.25/0.68 fof(f2248,plain,(
% 1.25/0.68 ![A_3,C_6,D_1]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_6),D_1))|hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_3,C_6)),insert_a(A_3,D_1))))),
% 1.25/0.68 inference(pre_NNF_transformation,[status(thm)],[f437])).
% 1.25/0.68 fof(f2249,plain,(
% 1.25/0.68 ![C_6,D_1]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,C_6),D_1))|(![A_3]: hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(A_3,C_6)),insert_a(A_3,D_1)))))),
% 1.25/0.68 inference(miniscoping,[status(thm)],[f2248])).
% 1.25/0.68 fof(f2250,plain,(
% 1.25/0.68 ![X0,X1,X2]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X2,X0)),insert_a(X2,X1))))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f2249])).
% 1.25/0.68 fof(f2254,plain,(
% 1.25/0.68 ![X0,X1,X2]: (image_pname_a(X0,insert_pname(X1,X2))=insert_a(hAPP_pname_a(X0,X1),image_pname_a(X0,X2)))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f441])).
% 1.25/0.68 fof(f2270,plain,(
% 1.25/0.68 ![F,X_3,A_1]: (~hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1))|insert_a(hAPP_pname_a(F,X_3),image_pname_a(F,A_1))=image_pname_a(F,A_1))),
% 1.25/0.68 inference(pre_NNF_transformation,[status(thm)],[f447])).
% 1.25/0.68 fof(f2271,plain,(
% 1.25/0.68 ![X_3,A_1]: (~hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X_3),A_1))|(![F]: insert_a(hAPP_pname_a(F,X_3),image_pname_a(F,A_1))=image_pname_a(F,A_1)))),
% 1.25/0.68 inference(miniscoping,[status(thm)],[f2270])).
% 1.25/0.68 fof(f2272,plain,(
% 1.25/0.68 ![X0,X1,X2]: (~hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1))|insert_a(hAPP_pname_a(X2,X0),image_pname_a(X2,X1))=image_pname_a(X2,X1))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f2271])).
% 1.25/0.68 fof(f3557,plain,(
% 1.25/0.68 hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,g),image_pname_a(mgt_call,u)))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f912])).
% 1.25/0.68 fof(f3560,plain,(
% 1.25/0.68 hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,pn),u))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f915])).
% 1.25/0.68 fof(f3562,plain,(
% 1.25/0.68 ~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),image_pname_a(mgt_call,u)))),
% 1.25/0.68 inference(cnf_transformation,[status(thm)],[f918])).
% 1.25/0.68 fof(f3808,plain,(
% 1.25/0.68 ![X0]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),image_pname_a(mgt_call,u))))),
% 1.25/0.68 inference(resolution,[status(thm)],[f2146,f3562])).
% 1.25/0.68 fof(f3811,plain,(
% 1.25/0.68 ![X0,X1]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),image_pname_a(mgt_call,u))))),
% 1.25/0.68 inference(resolution,[status(thm)],[f3808,f2146])).
% 1.25/0.68 fof(f3813,plain,(
% 1.25/0.68 ![X0,X1,X2]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),image_pname_a(mgt_call,u))))),
% 1.25/0.68 inference(resolution,[status(thm)],[f3811,f2146])).
% 1.25/0.68 fof(f3815,plain,(
% 1.25/0.68 ![X0,X1,X2,X3]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),X3))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),image_pname_a(mgt_call,u))))),
% 1.25/0.68 inference(resolution,[status(thm)],[f3813,f2146])).
% 1.25/0.68 fof(f3817,plain,(
% 1.25/0.68 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),g)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),X3))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),X4))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X4),image_pname_a(mgt_call,u))))),
% 1.25/0.68 inference(resolution,[status(thm)],[f3815,f2146])).
% 1.25/0.69 fof(f3928,plain,(
% 1.25/0.69 ![X0]: (hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(X0,g)),insert_a(X0,image_pname_a(mgt_call,u)))))),
% 1.25/0.69 inference(resolution,[status(thm)],[f2250,f3557])).
% 1.25/0.69 fof(f3933,plain,(
% 1.25/0.69 ![X0,X1,X2]: (~hBOOL(hAPP_f1664156314l_bool(hAPP_p338031245l_bool(member_pname,X0),X1))|image_pname_a(X2,insert_pname(X0,X1))=image_pname_a(X2,X1))),
% 1.25/0.69 inference(forward_demodulation,[status(thm)],[f2254,f2272])).
% 1.25/0.69 fof(f3934,plain,(
% 1.25/0.69 ![X0]: (image_pname_a(X0,insert_pname(pn,u))=image_pname_a(X0,u))),
% 1.25/0.69 inference(resolution,[status(thm)],[f3933,f3560])).
% 1.25/0.69 fof(f5198,plain,(
% 1.25/0.69 ![X0,X1,X2,X3]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,insert_a(hAPP_pname_a(mgt_call,pn),image_pname_a(mgt_call,u))),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),X3))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(resolution,[status(thm)],[f3928,f3817])).
% 1.25/0.69 fof(f5206,plain,(
% 1.25/0.69 ![X0,X1,X2,X3]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,insert_pname(pn,u))),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),X3))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(forward_demodulation,[status(thm)],[f2254,f5198])).
% 1.25/0.69 fof(f5207,plain,(
% 1.25/0.69 ![X0,X1,X2,X3]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),X3))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X3),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(forward_demodulation,[status(thm)],[f3934,f5206])).
% 1.25/0.69 fof(f5227,plain,(
% 1.25/0.69 ![X0,X1,X2]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),X2))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X2),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(resolution,[status(thm)],[f5207,f2061])).
% 1.25/0.69 fof(f5359,plain,(
% 1.25/0.69 ![X0,X1]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),X1))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X1),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(resolution,[status(thm)],[f5227,f2061])).
% 1.25/0.69 fof(f5405,plain,(
% 1.25/0.69 ![X0]: (~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),X0))|~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,X0),image_pname_a(mgt_call,u))))),
% 1.25/0.69 inference(resolution,[status(thm)],[f5359,f2061])).
% 1.25/0.69 fof(f5408,plain,(
% 1.25/0.69 ~hBOOL(hAPP_fun_a_bool_bool(hAPP_f1631501043l_bool(ord_le1311769555a_bool,image_pname_a(mgt_call,u)),image_pname_a(mgt_call,u)))),
% 1.25/0.69 inference(resolution,[status(thm)],[f5405,f2061])).
% 1.25/0.69 fof(f5409,plain,(
% 1.25/0.69 $false),
% 1.25/0.69 inference(forward_subsumption_resolution,[status(thm)],[f5408,f2061])).
% 1.25/0.69 % SZS output end CNFRefutation for theBenchmark.p
% 1.25/0.72 % Elapsed time: 0.349801 seconds
% 1.25/0.72 % CPU time: 1.970048 seconds
% 1.25/0.72 % Total memory used: 212.597 MB
% 1.25/0.72 % Net memory used: 210.593 MB
%------------------------------------------------------------------------------