%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 09:14:22 AM UTC 2026
% Result : Theorem 1.91s 0.73s
% Output : CNFRefutation 1.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 38 ( 27 unt; 0 def)
% Number of atoms : 60 ( 16 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 40 ( 18 ~; 15 |; 0 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 12 con; 0-4 aty)
% Number of variables : 49 ( 4 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_hAPP_res,axiom,
! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
file('theBenchmark.p',tsy_c_hAPP_res) ).
fof(fact_0_empty,axiom,
! [X_a,G] : hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),bot_bot(fun(hoare_509422987triple(X_a),bool)))),
file('theBenchmark.p',fact_0_empty) ).
fof(fact_4_cut,axiom,
! [X_a,G,G_2,Ts] :
( hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G_2),Ts))
=> ( hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),G_2))
=> hBOOL(hAPP(fun(hoare_509422987triple(X_a),bool),bool,hAPP(fun(hoare_509422987triple(X_a),bool),fun(fun(hoare_509422987triple(X_a),bool),bool),hoare_122391849derivs(X_a),G),Ts)) ) ),
file('theBenchmark.p',fact_4_cut) ).
fof(fact_19_MGF,axiom,
! [C_1] :
( hBOOL(hoare_1883395792gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP(com,bool,wt,C_1))
=> hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,C_1)),bot_bot(fun(hoare_509422987triple(state),bool))))) ) ) ),
file('theBenchmark.p',fact_19_MGF) ).
fof(fact_77_Collect__def,axiom,
! [X_a,P_1] : hAPP(fun(X_a,bool),fun(X_a,bool),collect(X_a),P_1) = ti(fun(X_a,bool),P_1),
file('theBenchmark.p',fact_77_Collect__def) ).
fof(fact_90_singleton__conv2,axiom,
! [X_a,A_3] : hAPP(fun(X_a,bool),fun(X_a,bool),collect(X_a),hAPP(X_a,fun(X_a,bool),fequal(X_a),A_3)) = hAPP(fun(X_a,bool),fun(X_a,bool),hAPP(X_a,fun(fun(X_a,bool),fun(X_a,bool)),insert(X_a),A_3),bot_bot(fun(X_a,bool))),
file('theBenchmark.p',fact_90_singleton__conv2) ).
fof(fact_92_WT__bodiesD,axiom,
! [Pn,B_2] :
( hBOOL(wT_bodies)
=> ( hAPP(pname,option(com),body,Pn) = hAPP(com,option(com),some(com),B_2)
=> hBOOL(hAPP(com,bool,wt,B_2)) ) ),
file('theBenchmark.p',fact_92_WT__bodiesD) ).
fof(conj_7,conjecture,
hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
file('theBenchmark.p',conj_7) ).
fof(conj_7_neg,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(assume_negation,[status(cth)],[conj_7]) ).
cnf(c_206,plain,
hAPP(A,B,C,D) = ti(B,hAPP(A,B,C,D)),
inference(clausify,[status(thm)],[tsy_c_hAPP_res]) ).
cnf(c_207,plain,
ti(A,hAPP(B,A,C,D)) = hAPP(B,A,C,D),
inference(copy,[status(thm)],[c_206]) ).
cnf(c_215,plain,
hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),B),bot_bot(fun(hoare_509422987triple(A),bool)))),
inference(clausify,[status(thm)],[fact_0_empty]) ).
cnf(c_219,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),D),C))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),D),B))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(A),bool),bool,hAPP(fun(hoare_509422987triple(A),bool),fun(fun(hoare_509422987triple(A),bool),bool),hoare_122391849derivs(A),B),C)) ),
inference(clausify,[status(thm)],[fact_4_cut]) ).
cnf(c_236,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,A)),bot_bot(fun(hoare_509422987triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,A))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1883395792gleton) ),
inference(clausify,[status(thm)],[fact_19_MGF]) ).
cnf(c_307,plain,
hAPP(fun(A,bool),fun(A,bool),collect(A),B) = ti(fun(A,bool),B),
inference(clausify,[status(thm)],[fact_77_Collect__def]) ).
cnf(c_334,plain,
hAPP(fun(A,bool),fun(A,bool),hAPP(A,fun(fun(A,bool),fun(A,bool)),insert(A),B),bot_bot(fun(A,bool))) = hAPP(fun(A,bool),fun(A,bool),collect(A),hAPP(A,fun(A,bool),fequal(A),B)),
inference(clausify,[status(thm)],[fact_90_singleton__conv2]) ).
cnf(c_677,plain,
hAPP(fun(A,bool),fun(A,bool),hAPP(A,fun(fun(A,bool),fun(A,bool)),insert(A),B),bot_bot(fun(A,bool))) = ti(fun(A,bool),hAPP(A,fun(A,bool),fequal(A),B)),
inference(paramod,[status(thm)],[c_307,c_334]) ).
cnf(c_335,plain,
hAPP(fun(A,bool),fun(A,bool),hAPP(A,fun(fun(A,bool),fun(A,bool)),insert(A),B),bot_bot(fun(A,bool))) = hAPP(A,fun(A,bool),fequal(A),B),
inference(paramod,[status(thm)],[c_207,c_677]) ).
cnf(c_340,plain,
( hBOOL(hAPP(com,bool,wt,B))
| hAPP(pname,option(com),body,A) != hAPP(com,option(com),some(com),B)
| ~ hBOOL(wT_bodies) ),
inference(clausify,[status(thm)],[fact_92_WT__bodiesD]) ).
fof(conj_0,axiom,
hBOOL(hoare_1883395792gleton),
file('theBenchmark.p',conj_0) ).
cnf(c_375,plain,
hBOOL(hoare_1883395792gleton),
inference(clausify,[status(thm)],[conj_0]) ).
fof(conj_1,axiom,
hBOOL(wT_bodies),
file('theBenchmark.p',conj_1) ).
cnf(c_376,plain,
hBOOL(wT_bodies),
inference(clausify,[status(thm)],[conj_1]) ).
fof(conj_5,axiom,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
file('theBenchmark.p',conj_5) ).
cnf(c_380,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(clausify,[status(thm)],[conj_5]) ).
cnf(c_381,plain,
hAPP(com,option(com),some(com),y) = hAPP(pname,option(com),body,pn),
inference(copy,[status(thm)],[c_380]) ).
cnf(c_383,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(clausify,[status(thm)],[conj_7_neg]) ).
cnf(c_384,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))),
inference(paramod,[status(thm)],[c_335,c_383]) ).
cnf(c_678,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,A))))
| ~ hBOOL(hAPP(com,bool,wt,A))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1883395792gleton) ),
inference(paramod,[status(thm)],[c_335,c_236]) ).
cnf(c_679,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,A))))
| ~ hBOOL(hAPP(com,bool,wt,A))
| ~ hBOOL(wT_bodies) ),
inference(resolve,[status(thm)],[c_375,c_678]) ).
cnf(c_413,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,A))))
| ~ hBOOL(hAPP(com,bool,wt,A)) ),
inference(resolve,[status(thm)],[c_376,c_679]) ).
cnf(c_424,plain,
( hBOOL(hAPP(com,bool,wt,B))
| hAPP(pname,option(com),body,A) != hAPP(com,option(com),some(com),B) ),
inference(resolve,[status(thm)],[c_376,c_340]) ).
cnf(c_680,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(copy,[status(thm)],[c_381]) ).
cnf(c_461,plain,
hBOOL(hAPP(com,bool,wt,y)),
inference(resolve,[status(thm)],[c_424,c_680]) ).
cnf(c_670,plain,
hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))),
inference(resolve,[status(thm)],[c_413,c_461]) ).
cnf(c_681,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),A),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y))))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),A),bot_bot(fun(hoare_509422987triple(state),bool)))) ),
inference(resolve,[status(thm)],[c_670,c_219]) ).
cnf(c_675,plain,
hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),A),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))),
inference(resolve,[status(thm)],[c_215,c_681]) ).
cnf(c_676,plain,
$false,
inference(resolve,[status(thm)],[c_675,c_384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 16:03:15 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 3681125 was started by sandbox2 on n010,
% 0.10/0.38 % Sat Sep 26 16:03:15 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.42
% 0.10/0.42 % From the command line: assign(max_seconds, 300).
% 0.10/0.42
% 0.10/0.42 % SInE: 150 to sos, 18 to usable, of 168 axioms (tolerance 2.00, depth 0 fixpoint).
% 1.91/0.73
% 1.91/0.73 % SZS status Theorem for theBenchmark
% 1.91/0.73
% 1.91/0.73 % Proof 1 at 0.17 (+ 0.04) seconds.
% 1.91/0.73 % Length of proof is 29.
% 1.91/0.73 % Level of proof is 7.
% 1.91/0.73 % Maximum clause weight is 161.000.
% 1.91/0.73 % Given clauses 248.
% 1.91/0.73
% 1.91/0.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------