%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW470+7 : 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 : n006.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:11 PM UTC 2026
% Result : Theorem 0.46s 1.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.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:55:57 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.37/0.65 % Drodi V4.1.1
% 0.46/1.13 % Refutation found
% 0.46/1.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.46/1.13 % SZS output start CNFRefutation for theBenchmark
% 0.46/1.13 fof(f67,hypothesis,(
% 0.46/1.13 ti(bool,fFalse) = fFalse ),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f74,axiom,(
% 0.46/1.13 (! [X_a,X_c,B_1_1,B_2_1] : hAPP(X_a,X_c,ti(fun(X_a,X_c),B_1_1),B_2_1) = hAPP(X_a,X_c,B_1_1,B_2_1) )),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f88,axiom,(
% 0.46/1.13 (! [X_b,Ga,Ca,Q_3,Pa] :( (! [Z_4,S_3] :( hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_4),S_3))=> hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),S_3))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,Z_4)))),bot_bot(fun(hoare_2118899576triple(X_b),bool))))) ))=> hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool))))) ) )),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f1179,axiom,(
% 0.46/1.13 (! [X_b,X_a,P,Q] : hAPP(X_b,X_a,hAPP(X_a,fun(X_b,X_a),combk(X_a,X_b),P),Q) = ti(X_a,P) )),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f1187,axiom,(
% 0.46/1.13 ~ hBOOL(fFalse) ),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f1194,conjecture,(
% 0.46/1.13 hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))) ),
% 0.46/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.46/1.13 fof(f1195,negated_conjecture,(
% 0.46/1.13 ~(hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool))))) )),
% 0.46/1.13 inference(negated_conjecture,[status(cth)],[f1194])).
% 0.46/1.13 fof(f1292,plain,(
% 0.46/1.13 ti(bool,fFalse)=fFalse),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f67])).
% 0.46/1.13 fof(f1299,plain,(
% 0.46/1.13 ![X0,X1,X2,X3]: (hAPP(X0,X1,ti(fun(X0,X1),X2),X3)=hAPP(X0,X1,X2,X3))),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f74])).
% 0.46/1.13 fof(f1327,plain,(
% 0.46/1.13 ![X_b,Ga,Ca,Q_3,Pa]: ((?[Z_4,S_3]: (hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,Z_4),S_3))&~hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),S_3))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,Z_4)))),bot_bot(fun(hoare_2118899576triple(X_b),bool)))))))|hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool))))))),
% 0.46/1.13 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 0.46/1.13 fof(f1328,plain,(
% 0.46/1.13 ![X_b,Ga,Ca,Q_3,Pa]: ((hBOOL(hAPP(state,bool,hAPP(X_b,fun(state,bool),Pa,sK0_skl(Pa,Q_3,Ca,Ga,X_b)),sK1_skl(Pa,Q_3,Ca,Ga,X_b)))&~hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(state,fun(state,bool),hAPP(fun(state,fun(state,bool)),fun(state,fun(state,bool)),combc(state,state,bool),fequal(state)),sK1_skl(Pa,Q_3,Ca,Ga,X_b)))),Ca),hAPP(fun(state,bool),fun(X_b,fun(state,bool)),combk(fun(state,bool),X_b),hAPP(X_b,fun(state,bool),Q_3,sK0_skl(Pa,Q_3,Ca,Ga,X_b))))),bot_bot(fun(hoare_2118899576triple(X_b),bool))))))|hBOOL(hAPP(fun(hoare_2118899576triple(X_b),bool),bool,hAPP(fun(hoare_2118899576triple(X_b),bool),fun(fun(hoare_2118899576triple(X_b),bool),bool),hoare_1301688828derivs(X_b),Ga),hAPP(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool),hAPP(hoare_2118899576triple(X_b),fun(fun(hoare_2118899576triple(X_b),bool),fun(hoare_2118899576triple(X_b),bool)),insert(hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b),hAPP(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b)),hAPP(fun(X_b,fun(state,bool)),fun(com,fun(fun(X_b,fun(state,bool)),hoare_2118899576triple(X_b))),hoare_759811442triple(X_b),Pa),Ca),Q_3)),bot_bot(fun(hoare_2118899576triple(X_b),bool))))))),
% 0.46/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_4,sK0_skl(Pa,Q_3,Ca,Ga,X_b)),skolemize(S_3,sK1_skl(Pa,Q_3,Ca,Ga,X_b))],[f1327])).
% 0.46/1.13 fof(f1329,plain,(
% 0.46/1.13 ![X0,X1,X2,X3,X4]: (hBOOL(hAPP(state,bool,hAPP(X0,fun(state,bool),X1,sK0_skl(X1,X2,X3,X4,X0)),sK1_skl(X1,X2,X3,X4,X0)))|hBOOL(hAPP(fun(hoare_2118899576triple(X0),bool),bool,hAPP(fun(hoare_2118899576triple(X0),bool),fun(fun(hoare_2118899576triple(X0),bool),bool),hoare_1301688828derivs(X0),X4),hAPP(fun(hoare_2118899576triple(X0),bool),fun(hoare_2118899576triple(X0),bool),hAPP(hoare_2118899576triple(X0),fun(fun(hoare_2118899576triple(X0),bool),fun(hoare_2118899576triple(X0),bool)),insert(hoare_2118899576triple(X0)),hAPP(fun(X0,fun(state,bool)),hoare_2118899576triple(X0),hAPP(com,fun(fun(X0,fun(state,bool)),hoare_2118899576triple(X0)),hAPP(fun(X0,fun(state,bool)),fun(com,fun(fun(X0,fun(state,bool)),hoare_2118899576triple(X0))),hoare_759811442triple(X0),X1),X3),X2)),bot_bot(fun(hoare_2118899576triple(X0),bool))))))),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f1328])).
% 0.46/1.13 fof(f4495,plain,(
% 0.46/1.13 ![X0,X1,X2,X3]: (hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3)=ti(X1,X2))),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f1179])).
% 0.46/1.13 fof(f4508,plain,(
% 0.46/1.13 ~hBOOL(fFalse)),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f1187])).
% 0.46/1.13 fof(f4518,plain,(
% 0.46/1.13 ~hBOOL(hAPP(fun(hoare_2118899576triple(x_a),bool),bool,hAPP(fun(hoare_2118899576triple(x_a),bool),fun(fun(hoare_2118899576triple(x_a),bool),bool),hoare_1301688828derivs(x_a),g),hAPP(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool),hAPP(hoare_2118899576triple(x_a),fun(fun(hoare_2118899576triple(x_a),bool),fun(hoare_2118899576triple(x_a),bool)),insert(hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a),hAPP(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a)),hAPP(fun(x_a,fun(state,bool)),fun(com,fun(fun(x_a,fun(state,bool)),hoare_2118899576triple(x_a))),hoare_759811442triple(x_a),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse))),c),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)))),bot_bot(fun(hoare_2118899576triple(x_a),bool)))))),
% 0.46/1.13 inference(cnf_transformation,[status(thm)],[f1195])).
% 0.46/1.13 fof(f6263,plain,(
% 0.46/1.13 hBOOL(hAPP(state,bool,hAPP(x_a,fun(state,bool),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),sK0_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,g,x_a)),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,g,x_a)))),
% 0.46/1.16 inference(resolution,[status(thm)],[f1329,f4518])).
% 0.46/1.16 fof(f6291,plain,(
% 0.46/1.16 hBOOL(hAPP(state,bool,ti(fun(state,bool),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,g,x_a)))),
% 0.46/1.16 inference(forward_demodulation,[status(thm)],[f4495,f6263])).
% 0.46/1.16 fof(f6292,plain,(
% 0.46/1.16 hBOOL(hAPP(state,bool,hAPP(bool,fun(state,bool),combk(bool,state),fFalse),sK1_skl(hAPP(fun(state,bool),fun(x_a,fun(state,bool)),combk(fun(state,bool),x_a),hAPP(bool,fun(state,bool),combk(bool,state),fFalse)),hAPP(fun(state,bool),fun(x_a,fun(state,bool)),hAPP(fun(x_a,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(x_a,fun(state,bool))),combc(x_a,fun(state,bool),fun(state,bool)),hAPP(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool))),hAPP(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(x_a,fun(state,fun(bool,bool))),fun(x_a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),x_a),combs(state,bool,bool)),hAPP(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool))),hAPP(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(x_a,fun(state,bool)),fun(x_a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),x_a),hAPP(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fconj)),p))),hAPP(fun(state,bool),fun(state,bool),hAPP(fun(bool,bool),fun(fun(state,bool),fun(state,bool)),combb(bool,bool,state),fNot),b)),c,g,x_a)))),
% 0.46/1.16 inference(forward_demodulation,[status(thm)],[f1299,f6291])).
% 0.46/1.16 fof(f6293,plain,(
% 0.46/1.16 hBOOL(ti(bool,fFalse))),
% 0.46/1.16 inference(forward_demodulation,[status(thm)],[f4495,f6292])).
% 0.46/1.16 fof(f6294,plain,(
% 0.46/1.16 hBOOL(fFalse)),
% 0.46/1.16 inference(forward_demodulation,[status(thm)],[f1292,f6293])).
% 0.46/1.16 fof(f6295,plain,(
% 0.46/1.16 $false),
% 0.46/1.16 inference(forward_subsumption_resolution,[status(thm)],[f6294,f4508])).
% 0.46/1.16 % SZS output end CNFRefutation for theBenchmark.p
% 2.74/1.18 % Elapsed time: 0.816276 seconds
% 2.74/1.18 % CPU time: 4.152531 seconds
% 2.74/1.18 % Total memory used: 336.577 MB
% 2.74/1.18 % Net memory used: 334.646 MB
%------------------------------------------------------------------------------