%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW473+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 72.80s 9.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW473+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 09:58:10 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.22/0.53 % Drodi V4.1.1
% 72.80/9.79 % Refutation found
% 72.80/9.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 72.80/9.79 % SZS output start CNFRefutation for theBenchmark
% 72.80/9.79 fof(f146,axiom,(
% 72.80/9.79 (! [X_b,X_1,A_3] :( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))<=> hBOOL(hAPP(X_b,bool,A_3,X_1)) ) )),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f165,axiom,(
% 72.80/9.79 (! [X_c,X_b,F,X_1,A_3] :( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))=> hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),hAPP(X_b,X_c,F,X_1)),hAPP(fun(X_b,bool),fun(X_c,bool),hAPP(fun(X_b,X_c),fun(fun(X_b,bool),fun(X_c,bool)),image(X_b,X_c),F),A_3))) ) )),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f174,axiom,(
% 72.80/9.79 (! [X_b,X_1,A_3,B_1] :( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),X_1),A_3)),B_1))<=> ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B_1))& hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),A_3),B_1)) ) ) )),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f1196,hypothesis,(
% 72.80/9.79 hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),g),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u))) ),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f1199,hypothesis,(
% 72.80/9.79 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u)) ),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f1201,conjecture,(
% 72.80/9.79 hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),hAPP(fun(x_a,bool),fun(x_a,bool),hAPP(x_a,fun(fun(x_a,bool),fun(x_a,bool)),insert(x_a),hAPP(pname,x_a,mgt_call,pn)),g)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u))) ),
% 72.80/9.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.80/9.79 fof(f1202,negated_conjecture,(
% 72.80/9.79 ~(hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),hAPP(fun(x_a,bool),fun(x_a,bool),hAPP(x_a,fun(fun(x_a,bool),fun(x_a,bool)),insert(x_a),hAPP(pname,x_a,mgt_call,pn)),g)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u))) )),
% 72.80/9.79 inference(negated_conjecture,[status(cth)],[f1201])).
% 72.80/9.79 fof(f1497,plain,(
% 72.80/9.79 ![X_b,X_1,A_3]: ((~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|hBOOL(hAPP(X_b,bool,A_3,X_1)))&(hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|~hBOOL(hAPP(X_b,bool,A_3,X_1))))),
% 72.80/9.79 inference(NNF_transformation,[status(thm)],[f146])).
% 72.80/9.79 fof(f1498,plain,(
% 72.80/9.79 (![X_b,X_1,A_3]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|hBOOL(hAPP(X_b,bool,A_3,X_1))))&(![X_b,X_1,A_3]: (hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|~hBOOL(hAPP(X_b,bool,A_3,X_1))))),
% 72.80/9.79 inference(miniscoping,[status(thm)],[f1497])).
% 72.80/9.79 fof(f1499,plain,(
% 72.80/9.79 ![X0,X1,X2]: (~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))|hBOOL(hAPP(X0,bool,X2,X1)))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1498])).
% 72.80/9.79 fof(f1500,plain,(
% 72.80/9.79 ![X0,X1,X2]: (hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))|~hBOOL(hAPP(X0,bool,X2,X1)))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1498])).
% 72.80/9.79 fof(f1555,plain,(
% 72.80/9.79 ![X_c,X_b,F,X_1,A_3]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),hAPP(X_b,X_c,F,X_1)),hAPP(fun(X_b,bool),fun(X_c,bool),hAPP(fun(X_b,X_c),fun(fun(X_b,bool),fun(X_c,bool)),image(X_b,X_c),F),A_3))))),
% 72.80/9.79 inference(pre_NNF_transformation,[status(thm)],[f165])).
% 72.80/9.79 fof(f1556,plain,(
% 72.80/9.79 ![X_b,X_1,A_3]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_3))|(![X_c,F]: hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),hAPP(X_b,X_c,F,X_1)),hAPP(fun(X_b,bool),fun(X_c,bool),hAPP(fun(X_b,X_c),fun(fun(X_b,bool),fun(X_c,bool)),image(X_b,X_c),F),A_3)))))),
% 72.80/9.79 inference(miniscoping,[status(thm)],[f1555])).
% 72.80/9.79 fof(f1557,plain,(
% 72.80/9.79 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))|hBOOL(hAPP(fun(X3,bool),bool,hAPP(X3,fun(fun(X3,bool),bool),member(X3),hAPP(X0,X3,X4,X1)),hAPP(fun(X0,bool),fun(X3,bool),hAPP(fun(X0,X3),fun(fun(X0,bool),fun(X3,bool)),image(X0,X3),X4),X2))))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1556])).
% 72.80/9.79 fof(f1577,plain,(
% 72.80/9.79 ![X_b,X_1,A_3,B_1]: ((~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),X_1),A_3)),B_1))|(hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B_1))&hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),A_3),B_1))))&(hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),X_1),A_3)),B_1))|(~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B_1))|~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),A_3),B_1)))))),
% 72.80/9.79 inference(NNF_transformation,[status(thm)],[f174])).
% 72.80/9.79 fof(f1578,plain,(
% 72.80/9.79 (![X_b,X_1,A_3,B_1]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),X_1),A_3)),B_1))|(hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B_1))&hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),A_3),B_1)))))&(![X_b,X_1,A_3,B_1]: (hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),X_1),A_3)),B_1))|(~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B_1))|~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,bool),fun(fun(X_b,bool),bool),ord_less_eq(fun(X_b,bool)),A_3),B_1)))))),
% 72.80/9.79 inference(miniscoping,[status(thm)],[f1577])).
% 72.80/9.79 fof(f1581,plain,(
% 72.80/9.79 ![X0,X1,X2,X3]: (hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),X2)),X3))|~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X3))|~hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X2),X3)))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1578])).
% 72.80/9.79 fof(f4481,plain,(
% 72.80/9.79 hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),g),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u)))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1196])).
% 72.80/9.79 fof(f4484,plain,(
% 72.80/9.79 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1199])).
% 72.80/9.79 fof(f4486,plain,(
% 72.80/9.79 ~hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),hAPP(fun(x_a,bool),fun(x_a,bool),hAPP(x_a,fun(fun(x_a,bool),fun(x_a,bool)),insert(x_a),hAPP(pname,x_a,mgt_call,pn)),g)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u)))),
% 72.80/9.79 inference(cnf_transformation,[status(thm)],[f1202])).
% 72.80/9.79 fof(f5108,plain,(
% 72.80/9.79 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(X0,bool,X1,X2))|hBOOL(hAPP(fun(X3,bool),bool,hAPP(X3,fun(fun(X3,bool),bool),member(X3),hAPP(X0,X3,X4,X2)),hAPP(fun(X0,bool),fun(X3,bool),hAPP(fun(X0,X3),fun(fun(X0,bool),fun(X3,bool)),image(X0,X3),X4),X1))))),
% 72.80/9.88 inference(resolution,[status(thm)],[f1500,f1557])).
% 72.80/9.88 fof(f5125,plain,(
% 72.80/9.88 ~hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),hAPP(pname,x_a,mgt_call,pn)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u)))|~hBOOL(hAPP(fun(x_a,bool),bool,hAPP(fun(x_a,bool),fun(fun(x_a,bool),bool),ord_less_eq(fun(x_a,bool)),g),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u)))),
% 72.80/9.88 inference(resolution,[status(thm)],[f1581,f4486])).
% 72.80/9.88 fof(f5126,plain,(
% 72.80/9.88 ~hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),hAPP(pname,x_a,mgt_call,pn)),hAPP(fun(pname,bool),fun(x_a,bool),hAPP(fun(pname,x_a),fun(fun(pname,bool),fun(x_a,bool)),image(pname,x_a),mgt_call),u)))),
% 72.80/9.88 inference(forward_subsumption_resolution,[status(thm)],[f5125,f4481])).
% 72.80/9.88 fof(f5149,plain,(
% 72.80/9.88 ~hBOOL(hAPP(pname,bool,u,pn))),
% 72.80/9.88 inference(resolution,[status(thm)],[f5126,f5108])).
% 72.80/9.88 fof(f6137,plain,(
% 72.80/9.88 hBOOL(hAPP(pname,bool,u,pn))),
% 72.80/9.88 inference(resolution,[status(thm)],[f4484,f1499])).
% 72.80/9.88 fof(f6142,plain,(
% 72.80/9.88 $false),
% 72.80/9.88 inference(forward_subsumption_resolution,[status(thm)],[f6137,f5149])).
% 72.80/9.88 % SZS output end CNFRefutation for theBenchmark.p
% 16.48/9.99 % Elapsed time: 9.623204 seconds
% 16.48/9.99 % CPU time: 74.487419 seconds
% 16.48/9.99 % Total memory used: 1.172 GB
% 16.48/9.99 % Net memory used: 1.154 GB
%------------------------------------------------------------------------------