%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW473+5 : 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 : n009.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 10.20s 1.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW473+5 : 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.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:57:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 10.20/1.74 % Refutation found
% 10.20/1.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.20/1.74 % SZS output start CNFRefutation for theBenchmark
% 10.20/1.74 fof(f21,axiom,(
% 10.20/1.74 (! [X_c,X_a,B_1_1,B_2] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2)) = hAPP(X_a,X_c,B_1_1,B_2) )),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f80,axiom,(
% 10.20/1.74 (! [X_b,X_c,A_1,B_1,F,X_2] :( ti(X_b,B_1) = hAPP(X_c,X_b,F,X_2)=> ( hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),X_2),A_1))=> hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),B_1),hAPP(fun(X_c,bool),fun(X_b,bool),hAPP(fun(X_c,X_b),fun(fun(X_c,bool),fun(X_b,bool)),image(X_c,X_b),F),A_1))) ) ) )),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f82,axiom,(
% 10.20/1.74 (! [X_b,C_1,A_1,B] :( 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_1),B))=> ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),A_1))=> hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),B)) ) ) )),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f84,axiom,(
% 10.20/1.74 (! [X_b,A_2,B_1,A_1] :( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),A_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),B_1),A_1)))=> ( ti(X_b,A_2) != ti(X_b,B_1)=> hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),A_2),A_1)) ) ) )),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f123,axiom,(
% 10.20/1.74 (! [X_b,B,A_1] :( (! [X_1] :( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_1))=> hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B)) ))=> 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_1),B)) ) )),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f156,hypothesis,(
% 10.20/1.74 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))) ),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f159,hypothesis,(
% 10.20/1.74 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u)) ),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f161,conjecture,(
% 10.20/1.74 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))) ),
% 10.20/1.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.20/1.74 fof(f162,negated_conjecture,(
% 10.20/1.74 ~(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))) )),
% 10.20/1.74 inference(negated_conjecture,[status(cth)],[f161])).
% 10.20/1.74 fof(f184,plain,(
% 10.20/1.74 ![X0,X1,X2,X3]: (ti(X0,hAPP(X1,X0,X2,X3))=hAPP(X1,X0,X2,X3))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f21])).
% 10.20/1.74 fof(f330,plain,(
% 10.20/1.74 ![X_b,X_c,A_1,B_1,F,X_2]: (~ti(X_b,B_1)=hAPP(X_c,X_b,F,X_2)|(~hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),X_2),A_1))|hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),B_1),hAPP(fun(X_c,bool),fun(X_b,bool),hAPP(fun(X_c,X_b),fun(fun(X_c,bool),fun(X_b,bool)),image(X_c,X_b),F),A_1)))))),
% 10.20/1.74 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 10.20/1.74 fof(f331,plain,(
% 10.20/1.74 ![X_b,X_c,B_1,F,X_2]: (~ti(X_b,B_1)=hAPP(X_c,X_b,F,X_2)|(![A_1]: (~hBOOL(hAPP(fun(X_c,bool),bool,hAPP(X_c,fun(fun(X_c,bool),bool),member(X_c),X_2),A_1))|hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),B_1),hAPP(fun(X_c,bool),fun(X_b,bool),hAPP(fun(X_c,X_b),fun(fun(X_c,bool),fun(X_b,bool)),image(X_c,X_b),F),A_1))))))),
% 10.20/1.74 inference(miniscoping,[status(thm)],[f330])).
% 10.20/1.74 fof(f332,plain,(
% 10.20/1.74 ![X0,X1,X2,X3,X4,X5]: (~ti(X0,X1)=hAPP(X2,X0,X3,X4)|~hBOOL(hAPP(fun(X2,bool),bool,hAPP(X2,fun(fun(X2,bool),bool),member(X2),X4),X5))|hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(fun(X2,bool),fun(X0,bool),hAPP(fun(X2,X0),fun(fun(X2,bool),fun(X0,bool)),image(X2,X0),X3),X5))))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f331])).
% 10.20/1.74 fof(f335,plain,(
% 10.20/1.74 ![X_b,C_1,A_1,B]: (~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_1),B))|(~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),A_1))|hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),B))))),
% 10.20/1.74 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 10.20/1.74 fof(f336,plain,(
% 10.20/1.74 ![X_b,A_1,B]: (~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_1),B))|(![C_1]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),A_1))|hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),C_1),B)))))),
% 10.20/1.74 inference(miniscoping,[status(thm)],[f335])).
% 10.20/1.74 fof(f337,plain,(
% 10.20/1.74 ![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(X0,fun(fun(X0,bool),bool),member(X0),X3),X1))|hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X3),X2)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f336])).
% 10.20/1.74 fof(f341,plain,(
% 10.20/1.74 ![X_b,A_2,B_1,A_1]: (~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),A_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),B_1),A_1)))|(ti(X_b,A_2)=ti(X_b,B_1)|hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),A_2),A_1))))),
% 10.20/1.74 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 10.20/1.74 fof(f342,plain,(
% 10.20/1.74 ![X0,X1,X2,X3]: (~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X2),X3)))|ti(X0,X1)=ti(X0,X2)|hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X3)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f341])).
% 10.20/1.74 fof(f450,plain,(
% 10.20/1.74 ![X_b,B,A_1]: ((?[X_1]: (hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_1))&~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),B))))|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_1),B)))),
% 10.20/1.74 inference(pre_NNF_transformation,[status(thm)],[f123])).
% 10.20/1.74 fof(f451,plain,(
% 10.20/1.74 ![X_b,B,A_1]: ((hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),sK7_skl(A_1,B,X_b)),A_1))&~hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),sK7_skl(A_1,B,X_b)),B)))|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_1),B)))),
% 10.20/1.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X_1,sK7_skl(A_1,B,X_b))],[f450])).
% 10.20/1.74 fof(f452,plain,(
% 10.20/1.74 ![X0,X1,X2]: (hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),sK7_skl(X1,X2,X0)),X1))|hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X1),X2)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f451])).
% 10.20/1.74 fof(f453,plain,(
% 10.20/1.74 ![X0,X1,X2]: (~hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),sK7_skl(X1,X2,X0)),X2))|hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X1),X2)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f451])).
% 10.20/1.74 fof(f516,plain,(
% 10.20/1.74 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)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f156])).
% 10.20/1.74 fof(f519,plain,(
% 10.20/1.74 hBOOL(hAPP(fun(pname,bool),bool,hAPP(pname,fun(fun(pname,bool),bool),member(pname),pn),u))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f159])).
% 10.20/1.74 fof(f521,plain,(
% 10.20/1.74 ~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)))),
% 10.20/1.74 inference(cnf_transformation,[status(thm)],[f162])).
% 10.20/1.74 fof(f556,plain,(
% 10.20/1.74 ![X0,X1,X2]: (~ti(X0,X1)=hAPP(pname,X0,X2,pn)|hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(fun(pname,bool),fun(X0,bool),hAPP(fun(pname,X0),fun(fun(pname,bool),fun(X0,bool)),image(pname,X0),X2),u))))),
% 10.20/1.74 inference(resolution,[status(thm)],[f332,f519])).
% 10.20/1.74 fof(f3162,plain,(
% 10.20/1.74 hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),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)))),
% 10.20/1.74 inference(resolution,[status(thm)],[f452,f521])).
% 10.20/1.74 fof(f3201,plain,(
% 10.20/1.74 ti(x_a,sK7_skl(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),x_a))=ti(x_a,hAPP(pname,x_a,mgt_call,pn))|hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),g))),
% 10.20/1.74 inference(resolution,[status(thm)],[f3162,f342])).
% 10.20/1.74 fof(f3214,plain,(
% 10.20/1.74 ti(x_a,sK7_skl(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),x_a))=hAPP(pname,x_a,mgt_call,pn)|hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),g))),
% 10.20/1.74 inference(forward_demodulation,[status(thm)],[f184,f3201])).
% 10.20/1.74 fof(f3222,plain,(
% 10.20/1.74 ![X0]: (ti(x_a,sK7_skl(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),x_a))=hAPP(pname,x_a,mgt_call,pn)|~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),X0))|hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),X0)))),
% 10.20/1.74 inference(resolution,[status(thm)],[f3214,f337])).
% 10.20/1.74 fof(f5991,plain,(
% 10.20/1.74 ti(x_a,sK7_skl(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),x_a))=hAPP(pname,x_a,mgt_call,pn)|hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),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)))),
% 10.20/1.74 inference(resolution,[status(thm)],[f3222,f516])).
% 10.20/1.74 fof(f5996,plain,(
% 10.20/1.74 hBOOL(hAPP(fun(x_a,bool),bool,hAPP(x_a,fun(fun(x_a,bool),bool),member(x_a),sK7_skl(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),x_a)),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)))),
% 10.20/1.74 inference(forward_subsumption_resolution,[status(thm)],[f5991,f556])).
% 10.20/1.74 fof(f6126,plain,(
% 10.20/1.74 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)))),
% 10.20/1.74 inference(resolution,[status(thm)],[f5996,f453])).
% 10.20/1.74 fof(f6154,plain,(
% 10.20/1.74 $false),
% 10.20/1.74 inference(forward_subsumption_resolution,[status(thm)],[f6126,f521])).
% 10.20/1.74 % SZS output end CNFRefutation for theBenchmark.p
% 10.20/1.77 % Elapsed time: 1.393505 seconds
% 10.20/1.77 % CPU time: 10.610733 seconds
% 10.20/1.77 % Total memory used: 326.264 MB
% 10.20/1.77 % Net memory used: 319.413 MB
%------------------------------------------------------------------------------