%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW473+6 : 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 : n013.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 13.05s 2.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW473+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n013.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 09:57:20 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.22/0.58 % Drodi V4.1.1
% 13.05/2.58 % Refutation found
% 13.05/2.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.05/2.58 % SZS output start CNFRefutation for theBenchmark
% 13.05/2.58 fof(f142,axiom,(
% 13.05/2.58 (! [X_b,A_2,C_2,D_2] :( 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)),C_2),D_2))=> 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),A_2),C_2)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),A_2),D_2))) ) )),
% 13.05/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.05/2.58 fof(f144,axiom,(
% 13.05/2.58 (! [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))=> hAPP(fun(X_c,bool),fun(X_c,bool),hAPP(X_c,fun(fun(X_c,bool),fun(X_c,bool)),insert(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)) = 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) ) )),
% 13.05/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.05/2.58 fof(f604,hypothesis,(
% 13.05/2.58 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))) ),
% 13.05/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.05/2.58 fof(f607,hypothesis,(
% 13.05/2.58 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u)) ),
% 13.05/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.05/2.58 fof(f609,conjecture,(
% 13.05/2.58 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))) ),
% 13.05/2.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.05/2.58 fof(f610,negated_conjecture,(
% 13.05/2.58 ~(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))) )),
% 13.05/2.58 inference(negated_conjecture,[status(cth)],[f609])).
% 13.05/2.58 fof(f918,plain,(
% 13.05/2.58 ![X_b,A_2,C_2,D_2]: (~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)),C_2),D_2))|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),A_2),C_2)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),A_2),D_2))))),
% 13.05/2.58 inference(pre_NNF_transformation,[status(thm)],[f142])).
% 13.05/2.58 fof(f919,plain,(
% 13.05/2.58 ![X_b,C_2,D_2]: (~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)),C_2),D_2))|(![A_2]: 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),A_2),C_2)),hAPP(fun(X_b,bool),fun(X_b,bool),hAPP(X_b,fun(fun(X_b,bool),fun(X_b,bool)),insert(X_b),A_2),D_2)))))),
% 13.05/2.58 inference(miniscoping,[status(thm)],[f918])).
% 13.05/2.58 fof(f920,plain,(
% 13.05/2.58 ![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)),X1),X2))|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),X3),X1)),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X3),X2))))),
% 13.05/2.58 inference(cnf_transformation,[status(thm)],[f919])).
% 13.05/2.58 fof(f922,plain,(
% 13.05/2.58 ![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))|hAPP(fun(X_c,bool),fun(X_c,bool),hAPP(X_c,fun(fun(X_c,bool),fun(X_c,bool)),insert(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))=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))),
% 13.05/2.62 inference(pre_NNF_transformation,[status(thm)],[f144])).
% 13.05/2.62 fof(f923,plain,(
% 13.05/2.62 ![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]: hAPP(fun(X_c,bool),fun(X_c,bool),hAPP(X_c,fun(fun(X_c,bool),fun(X_c,bool)),insert(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))=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)))),
% 13.05/2.62 inference(miniscoping,[status(thm)],[f922])).
% 13.05/2.62 fof(f924,plain,(
% 13.05/2.62 ![X0,X1,X2,X3,X4]: (~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))|hAPP(fun(X3,bool),fun(X3,bool),hAPP(X3,fun(fun(X3,bool),fun(X3,bool)),insert(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))=hAPP(fun(X0,bool),fun(X3,bool),hAPP(fun(X0,X3),fun(fun(X0,bool),fun(X3,bool)),image(X0,X3),X4),X2))),
% 13.05/2.62 inference(cnf_transformation,[status(thm)],[f923])).
% 13.05/2.62 fof(f2247,plain,(
% 13.05/2.62 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)))),
% 13.05/2.62 inference(cnf_transformation,[status(thm)],[f604])).
% 13.05/2.62 fof(f2250,plain,(
% 13.05/2.62 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u))),
% 13.05/2.62 inference(cnf_transformation,[status(thm)],[f607])).
% 13.05/2.62 fof(f2252,plain,(
% 13.05/2.62 ~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)))),
% 13.05/2.62 inference(cnf_transformation,[status(thm)],[f610])).
% 13.05/2.62 fof(f2377,plain,(
% 13.05/2.62 ![X0,X1]: (hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),hAPP(pname,X0,X1,pn)),hAPP(fun(pname,bool),fun(X0,bool),hAPP(fun(pname,X0),fun(fun(pname,bool),fun(X0,bool)),image(pname,X0),X1),u))=hAPP(fun(pname,bool),fun(X0,bool),hAPP(fun(pname,X0),fun(fun(pname,bool),fun(X0,bool)),image(pname,X0),X1),u))),
% 13.05/2.62 inference(resolution,[status(thm)],[f924,f2250])).
% 13.05/2.62 fof(f2406,plain,(
% 13.05/2.62 ![X0]: (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),X0),g)),hAPP(fun(x_a,bool),fun(x_a,bool),hAPP(x_a,fun(fun(x_a,bool),fun(x_a,bool)),insert(x_a),X0),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)))))),
% 13.05/2.62 inference(resolution,[status(thm)],[f2247,f920])).
% 13.05/2.62 fof(f6767,plain,(
% 13.05/2.62 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)))),
% 13.05/2.62 inference(paramodulation,[status(thm)],[f2377,f2406])).
% 13.05/2.62 fof(f6771,plain,(
% 13.05/2.62 $false),
% 13.05/2.62 inference(forward_subsumption_resolution,[status(thm)],[f6767,f2252])).
% 13.05/2.62 % SZS output end CNFRefutation for theBenchmark.p
% 14.74/2.66 % Elapsed time: 2.212373 seconds
% 14.74/2.66 % CPU time: 16.266636 seconds
% 14.74/2.66 % Total memory used: 386.263 MB
% 14.74/2.66 % Net memory used: 381.977 MB
%------------------------------------------------------------------------------