%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW470+1 : 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 : n020.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:17 AM UTC 2026
% Result : Theorem 53.05s 8.19s
% Output : CNFRefutation 53.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 22
% Syntax : Number of formulae : 132 ( 60 unt; 0 def)
% Number of atoms : 230 ( 108 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 153 ( 55 ~; 79 |; 7 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 45 ( 45 usr; 16 con; 0-6 aty)
% Number of variables : 205 ( 42 sgn 63 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(gsy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____jfehddehev__Otriple,axiom,
! [B_1_1,B_2] : is_bool(finite520909254iple_a(B_1_1,B_2)),
file('theBenchmark.p',gsy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____jfehddehev__Otriple) ).
fof(gsy_c_hAPP_000tc__Com__Ostate_000tc__HOL__Obool,axiom,
! [B_1_1,B_2] : is_bool(hAPP_state_bool(B_1_1,B_2)),
file('theBenchmark.p',gsy_c_hAPP_000tc__Com__Ostate_000tc__HOL__Obool) ).
fof(gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool,axiom,
! [B_1_1,B_2] :
( is_bool(B_2)
=> is_bool(hAPP_bool_bool(B_1_1,B_2)) ),
file('theBenchmark.p',gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool) ).
fof(fact_12_singleton__conv2,axiom,
! [A_3] : collec1266446174iple_a(hAPP_H562195827a_bool(fequal1878252616iple_a,A_3)) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A_3),bot_bo1687970473a_bool),
file('theBenchmark.p',fact_12_singleton__conv2) ).
fof(fact_13_singleton__conv,axiom,
! [A_3] : collec1266446174iple_a(hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A_3)) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A_3),bot_bo1687970473a_bool),
file('theBenchmark.p',fact_13_singleton__conv) ).
fof(fact_17_Collect__empty__eq,axiom,
! [Pa] :
( collec1266446174iple_a(Pa) = bot_bo1687970473a_bool
<=> ! [X_2] : ~ hBOOL(hAPP_H1927961489a_bool(Pa,X_2)) ),
file('theBenchmark.p',fact_17_Collect__empty__eq) ).
fof(fact_23_insert__absorb,axiom,
! [A_3,A] :
( hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,A_3),A))
=> hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A_3),A) = A ),
file('theBenchmark.p',fact_23_insert__absorb) ).
fof(fact_60_conseq,axiom,
! [Q_1,Ga,Ca,Pa] :
( ! [Z_1,S] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_1),S))
=> ? [P_1,Q_2] :
( ! [S_1] :
( ! [Z_2] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(P_1,Z_2),S))
=> hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_2,Z_2),S_1)) )
=> hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_1,Z_1),S_1)) )
& hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(P_1,Ca,Q_2)),bot_bo1687970473a_bool))) ) )
=> hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool))) ),
file('theBenchmark.p',fact_60_conseq) ).
fof(fact_73_mem__def,axiom,
! [X_1,A] :
( hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,X_1),A))
<=> hBOOL(hAPP_H1927961489a_bool(A,X_1)) ),
file('theBenchmark.p',fact_73_mem__def) ).
fof(fact_74_Collect__def,axiom,
! [Pa] : collec1266446174iple_a(Pa) = Pa,
file('theBenchmark.p',fact_74_Collect__def) ).
fof(help_fNot_2_1_U,axiom,
! [P] :
( hBOOL(hAPP_bool_bool(fNot,P))
| hBOOL(P) ),
file('theBenchmark.p',help_fNot_2_1_U) ).
fof(help_fFalse_1_1_T,axiom,
! [P] :
( is_bool(P)
=> ( P = fFalse
| P = fTrue ) ),
file('theBenchmark.p',help_fFalse_1_1_T) ).
fof(help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U,axiom,
! [P,Q] :
( is_bool(P)
=> hAPP_state_bool(cOMBK_bool_state(P),Q) = P ),
file('theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) ).
fof(help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U,axiom,
! [P,Q] : hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(P),Q) = P,
file('theBenchmark.p',help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) ).
fof(help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____jfehddehev__,axiom,
! [P,Q] :
( is_bool(P)
=> hAPP_H1927961489a_bool(cOMBK_1150238960iple_a(P),Q) = P ),
file('theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____jfehddehev__) ).
fof(fact_42_bot__fun__def,axiom,
! [X_2] :
( hBOOL(hAPP_H1927961489a_bool(bot_bo1687970473a_bool,X_2))
<=> hBOOL(bot_bot_bool) ),
file('theBenchmark.p',fact_42_bot__fun__def) ).
fof(conj_0,conjecture,
hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool))),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool))),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool,axiom,
is_bool(bot_bot_bool),
file('theBenchmark.p',gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool) ).
cnf(c_139,plain,
is_bool(bot_bot_bool),
inference(clausify,[status(thm)],[gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool]) ).
cnf(c_144,plain,
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1927961489a_bool(bot_bo1687970473a_bool,A)) ),
inference(clausify,[status(thm)],[fact_42_bot__fun__def]) ).
cnf(c_162,plain,
is_bool(finite520909254iple_a(A,B)),
inference(clausify,[status(thm)],[gsy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____jfehddehev__Otriple]) ).
fof(gsy_c_fFalse,axiom,
is_bool(fFalse),
file('theBenchmark.p',gsy_c_fFalse) ).
cnf(c_164,plain,
is_bool(fFalse),
inference(clausify,[status(thm)],[gsy_c_fFalse]) ).
fof(gsy_c_fTrue,axiom,
is_bool(fTrue),
file('theBenchmark.p',gsy_c_fTrue) ).
cnf(c_165,plain,
is_bool(fTrue),
inference(clausify,[status(thm)],[gsy_c_fTrue]) ).
cnf(c_166,plain,
is_bool(hAPP_state_bool(A,B)),
inference(clausify,[status(thm)],[gsy_c_hAPP_000tc__Com__Ostate_000tc__HOL__Obool]) ).
cnf(c_167,plain,
( is_bool(hAPP_bool_bool(B,A))
| ~ is_bool(A) ),
inference(clausify,[status(thm)],[gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool]) ).
cnf(c_192,plain,
collec1266446174iple_a(hAPP_H562195827a_bool(fequal1878252616iple_a,A)) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),bot_bo1687970473a_bool),
inference(clausify,[status(thm)],[fact_12_singleton__conv2]) ).
cnf(c_193,plain,
collec1266446174iple_a(hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A)) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),bot_bo1687970473a_bool),
inference(clausify,[status(thm)],[fact_13_singleton__conv]) ).
cnf(c_200,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| collec1266446174iple_a(A) != bot_bo1687970473a_bool ),
inference(clausify,[status(thm)],[fact_17_Collect__empty__eq]) ).
fof(fact_22_empty__def,axiom,
bot_bo1687970473a_bool = collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse)),
file('theBenchmark.p',fact_22_empty__def) ).
cnf(c_209,plain,
bot_bo1687970473a_bool = collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse)),
inference(clausify,[status(thm)],[fact_22_empty__def]) ).
cnf(c_210,plain,
( hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),B) = B
| ~ hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,A),B)) ),
inference(clausify,[status(thm)],[fact_23_insert__absorb]) ).
fof(nnf_57,plain,
! [Q_1,Ga,Ca,Pa] :
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool)))
| ? [Z_1,S] :
( ! [P_1,Q_2] :
( ? [S_1] :
( ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_1,Z_1),S_1))
& ! [Z_2] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_2,Z_2),S_1))
| ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(P_1,Z_2),S)) ) )
| ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(P_1,Ca,Q_2)),bot_bo1687970473a_bool))) )
& hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_1),S)) ) ),
inference(fof_nnf,[status(thm)],[fact_60_conseq]) ).
fof(sk_fact_60_conseq_sk,plain,
! [Q_1,Ga,Ca,Pa] :
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool)))
| ( ! [P_1,Q_2] :
( ( ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_1,sK0(Q_1,Ga,Ca,Pa)),sK3(Q_1,Ga,Ca,Pa,P_1,Q_2)))
& ! [Z_2] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Q_2,Z_2),sK3(Q_1,Ga,Ca,Pa,P_1,Q_2)))
| ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(P_1,Z_2),sK1(Q_1,Ga,Ca,Pa))) ) )
| ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(P_1,Ca,Q_2)),bot_bo1687970473a_bool))) )
& hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,sK0(Q_1,Ga,Ca,Pa)),sK1(Q_1,Ga,Ca,Pa))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK3]),skolemize(Z_1,sK0(Q_1,Ga,Ca,Pa)),skolemize(S,sK1(Q_1,Ga,Ca,Pa)),skolemize(S_1,sK3(Q_1,Ga,Ca,Pa,P_1,Q_2))],[nnf_57]) ).
fof(sk_fact_60_conseq,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(VAR_0),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(VAR_5,VAR_2,VAR_4)),bot_bo1687970473a_bool)))
| ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(VAR_4,sK0(VAR_4,VAR_0,VAR_2,VAR_5)),sK3(VAR_4,VAR_0,VAR_2,VAR_5,VAR_1,VAR_3)))
| ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(VAR_0),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(VAR_1,VAR_2,VAR_3)),bot_bo1687970473a_bool))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(VAR_0),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(VAR_6,VAR_2,VAR_5)),bot_bo1687970473a_bool)))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(VAR_3,VAR_4),sK3(VAR_5,VAR_0,VAR_2,VAR_6,VAR_1,VAR_3)))
| ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(VAR_1,VAR_4),sK1(VAR_5,VAR_0,VAR_2,VAR_6)))
| ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(VAR_0),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(VAR_1,VAR_2,VAR_3)),bot_bo1687970473a_bool))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(VAR_2),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(VAR_0,VAR_3,VAR_1)),bot_bo1687970473a_bool)))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(VAR_0,sK0(VAR_1,VAR_2,VAR_3,VAR_0)),sK1(VAR_1,VAR_2,VAR_3,VAR_0))) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_60_conseq_sk]) ).
cnf(c_263,plain,
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(C),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(A,D,B)),bot_bo1687970473a_bool)))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(A,sK0(B,C,D,A)),sK1(B,C,D,A))) ),
inference(split_conjunct,[status(thm)],[sk_fact_60_conseq]) ).
cnf(c_264,plain,
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(C),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(A,D,B)),collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse)))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(A,sK0(B,C,D,A)),sK1(B,C,D,A))) ),
inference(paramod,[status(thm)],[c_209,c_263]) ).
cnf(c_300,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(B,A))
| hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,A),B)) ),
inference(clausify,[status(thm)],[fact_73_mem__def]) ).
cnf(c_301,plain,
collec1266446174iple_a(A) = A,
inference(clausify,[status(thm)],[fact_74_Collect__def]) ).
cnf(c_378,plain,
( hBOOL(hAPP_bool_bool(fNot,A))
| hBOOL(A) ),
inference(clausify,[status(thm)],[help_fNot_2_1_U]) ).
fof(help_fFalse_1_1_U,axiom,
~ hBOOL(fFalse),
file('theBenchmark.p',help_fFalse_1_1_U) ).
cnf(c_385,plain,
~ hBOOL(fFalse),
inference(clausify,[status(thm)],[help_fFalse_1_1_U]) ).
cnf(c_386,plain,
( A = fFalse
| A = fTrue
| ~ is_bool(A) ),
inference(clausify,[status(thm)],[help_fFalse_1_1_T]) ).
cnf(c_16599,plain,
( A = fFalse
| fTrue = A
| ~ is_bool(A) ),
inference(copy,[status(thm)],[c_386]) ).
cnf(c_387,plain,
( fFalse = A
| fTrue = A
| ~ is_bool(A) ),
inference(copy,[status(thm)],[c_16599]) ).
cnf(c_393,plain,
( hAPP_state_bool(cOMBK_bool_state(A),B) = A
| ~ is_bool(A) ),
inference(clausify,[status(thm)],[help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U]) ).
cnf(c_394,plain,
hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(A),B) = A,
inference(clausify,[status(thm)],[help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U]) ).
cnf(c_403,plain,
( hAPP_H1927961489a_bool(cOMBK_1150238960iple_a(A),B) = A
| ~ is_bool(A) ),
inference(clausify,[status(thm)],[help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____jfehddehev__]) ).
cnf(c_414,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool))),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_16600,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse))))),
inference(paramod,[status(thm)],[c_209,c_414]) ).
cnf(c_415,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),cOMBK_1150238960iple_a(fFalse)))),
inference(paramod,[status(thm)],[c_301,c_16600]) ).
cnf(c_16601,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| A != bot_bo1687970473a_bool ),
inference(paramod,[status(thm)],[c_301,c_200]) ).
cnf(c_16602,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| A != collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse)) ),
inference(paramod,[status(thm)],[c_209,c_16601]) ).
cnf(c_16603,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| A != cOMBK_1150238960iple_a(fFalse) ),
inference(paramod,[status(thm)],[c_301,c_16602]) ).
cnf(c_423,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| cOMBK_1150238960iple_a(fFalse) != A ),
inference(copy,[status(thm)],[c_16603]) ).
cnf(c_16604,plain,
hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),bot_bo1687970473a_bool),
inference(paramod,[status(thm)],[c_301,c_193]) ).
cnf(c_16605,plain,
hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse))),
inference(paramod,[status(thm)],[c_209,c_16604]) ).
cnf(c_16606,plain,
hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),cOMBK_1150238960iple_a(fFalse)),
inference(paramod,[status(thm)],[c_301,c_16605]) ).
cnf(c_429,plain,
hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),cOMBK_1150238960iple_a(fFalse)) = hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A),
inference(copy,[status(thm)],[c_16606]) ).
cnf(c_16607,plain,
hAPP_H562195827a_bool(fequal1878252616iple_a,A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),bot_bo1687970473a_bool),
inference(paramod,[status(thm)],[c_301,c_192]) ).
cnf(c_16608,plain,
hAPP_H562195827a_bool(fequal1878252616iple_a,A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse))),
inference(paramod,[status(thm)],[c_209,c_16607]) ).
cnf(c_16609,plain,
hAPP_H562195827a_bool(fequal1878252616iple_a,A) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),cOMBK_1150238960iple_a(fFalse)),
inference(paramod,[status(thm)],[c_301,c_16608]) ).
cnf(c_16610,plain,
hAPP_H562195827a_bool(fequal1878252616iple_a,A) = hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A),
inference(paramod,[status(thm)],[c_429,c_16609]) ).
cnf(c_430,plain,
hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),A) = hAPP_H562195827a_bool(fequal1878252616iple_a,A),
inference(copy,[status(thm)],[c_16610]) ).
cnf(c_16611,plain,
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1927961489a_bool(collec1266446174iple_a(cOMBK_1150238960iple_a(fFalse)),A)) ),
inference(paramod,[status(thm)],[c_209,c_144]) ).
cnf(c_448,plain,
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1927961489a_bool(cOMBK_1150238960iple_a(fFalse),A)) ),
inference(paramod,[status(thm)],[c_301,c_16611]) ).
cnf(c_16612,plain,
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(C),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(A,D,B)),cOMBK_1150238960iple_a(fFalse))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(A,sK0(B,C,D,A)),sK1(B,C,D,A))) ),
inference(paramod,[status(thm)],[c_301,c_264]) ).
cnf(c_16613,plain,
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(C),hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),hoare_1050552211iple_a(A,D,B))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(A,sK0(B,C,D,A)),sK1(B,C,D,A))) ),
inference(paramod,[status(thm)],[c_429,c_16612]) ).
cnf(c_470,plain,
( hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(C),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(A,D,B))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(A,sK0(B,C,D,A)),sK1(B,C,D,A))) ),
inference(paramod,[status(thm)],[c_430,c_16613]) ).
cnf(c_16614,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_H562195827a_bool(hAPP_f1915402821a_bool(cOMBC_2049287834a_bool,fequal1878252616iple_a),hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))))),
inference(paramod,[status(thm)],[c_429,c_415]) ).
cnf(c_493,negated_conjecture,
~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))))),
inference(paramod,[status(thm)],[c_430,c_16614]) ).
cnf(c_507,plain,
~ hBOOL(hAPP_H1927961489a_bool(cOMBK_1150238960iple_a(fFalse),A)),
inference(xxres,[status(thm)],[c_423]) ).
cnf(c_508,plain,
~ hBOOL(bot_bot_bool),
inference(resolve,[status(thm)],[c_507,c_448]) ).
cnf(c_16615,plain,
( fFalse = finite520909254iple_a(A,B)
| fTrue = finite520909254iple_a(A,B) ),
inference(resolve,[status(thm)],[c_387,c_162]) ).
cnf(c_16616,plain,
( fFalse = finite520909254iple_a(A,B)
| finite520909254iple_a(A,B) = fTrue ),
inference(copy,[status(thm)],[c_16615]) ).
cnf(c_510,plain,
( finite520909254iple_a(A,B) = fFalse
| finite520909254iple_a(A,B) = fTrue ),
inference(copy,[status(thm)],[c_16616]) ).
cnf(c_511,plain,
( fFalse = bot_bot_bool
| fTrue = bot_bot_bool ),
inference(resolve,[status(thm)],[c_387,c_139]) ).
cnf(c_16617,plain,
( fFalse = hAPP_state_bool(A,B)
| fTrue = hAPP_state_bool(A,B) ),
inference(resolve,[status(thm)],[c_166,c_387]) ).
cnf(c_16618,plain,
( fFalse = hAPP_state_bool(A,B)
| hAPP_state_bool(A,B) = fTrue ),
inference(copy,[status(thm)],[c_16617]) ).
cnf(c_533,plain,
( hAPP_state_bool(A,B) = fFalse
| hAPP_state_bool(A,B) = fTrue ),
inference(copy,[status(thm)],[c_16618]) ).
cnf(c_536,plain,
is_bool(hAPP_bool_bool(A,fFalse)),
inference(resolve,[status(thm)],[c_167,c_164]) ).
cnf(c_16619,plain,
( fFalse = hAPP_bool_bool(A,fFalse)
| fTrue = hAPP_bool_bool(A,fFalse) ),
inference(resolve,[status(thm)],[c_536,c_387]) ).
cnf(c_16620,plain,
( fFalse = hAPP_bool_bool(A,fFalse)
| hAPP_bool_bool(A,fFalse) = fTrue ),
inference(copy,[status(thm)],[c_16619]) ).
cnf(c_545,plain,
( hAPP_bool_bool(A,fFalse) = fFalse
| hAPP_bool_bool(A,fFalse) = fTrue ),
inference(copy,[status(thm)],[c_16620]) ).
cnf(c_581,plain,
( ~ hBOOL(finite520909254iple_a(A,B))
| finite520909254iple_a(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_510,c_385]) ).
cnf(c_604,plain,
( hAPP_state_bool(A,B) = bot_bot_bool
| fTrue = bot_bot_bool
| hAPP_state_bool(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_533,c_511]) ).
cnf(c_740,plain,
( ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(finite520909254iple_a(A,B))),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))
| finite520909254iple_a(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_510,c_493]) ).
cnf(c_741,plain,
( ~ hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(hAPP_state_bool(A,B))),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))
| hAPP_state_bool(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_533,c_493]) ).
cnf(c_16621,plain,
( hBOOL(fFalse)
| hBOOL(fFalse)
| hAPP_bool_bool(fNot,fFalse) = fTrue ),
inference(paramod,[status(thm)],[c_545,c_378]) ).
cnf(c_16622,plain,
( hBOOL(fFalse)
| hAPP_bool_bool(fNot,fFalse) = fTrue ),
inference(copy,[status(thm)],[c_16621]) ).
cnf(c_757,plain,
hAPP_bool_bool(fNot,fFalse) = fTrue,
inference(resolve,[status(thm)],[c_385,c_16622]) ).
cnf(c_16623,plain,
( hBOOL(fTrue)
| hBOOL(fFalse) ),
inference(paramod,[status(thm)],[c_757,c_378]) ).
cnf(c_776,plain,
hBOOL(fTrue),
inference(resolve,[status(thm)],[c_385,c_16623]) ).
cnf(c_2309,plain,
hAPP_state_bool(cOMBK_bool_state(hAPP_state_bool(A,B)),C) = hAPP_state_bool(A,B),
inference(resolve,[status(thm)],[c_393,c_166]) ).
cnf(c_2311,plain,
hAPP_state_bool(cOMBK_bool_state(fFalse),A) = fFalse,
inference(resolve,[status(thm)],[c_393,c_164]) ).
cnf(c_2313,plain,
hAPP_state_bool(cOMBK_bool_state(finite520909254iple_a(A,B)),C) = finite520909254iple_a(A,B),
inference(resolve,[status(thm)],[c_393,c_162]) ).
cnf(c_2314,plain,
hAPP_state_bool(cOMBK_bool_state(bot_bot_bool),A) = bot_bot_bool,
inference(resolve,[status(thm)],[c_393,c_139]) ).
cnf(c_16624,plain,
( hBOOL(bot_bot_bool)
| hAPP_state_bool(A,B) = bot_bot_bool
| hAPP_state_bool(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_604,c_776]) ).
cnf(c_2665,plain,
( hAPP_state_bool(A,B) = bot_bot_bool
| hAPP_state_bool(A,B) = fTrue ),
inference(resolve,[status(thm)],[c_508,c_16624]) ).
cnf(c_16625,plain,
( fTrue = fFalse
| hAPP_state_bool(cOMBK_bool_state(fFalse),A) = bot_bot_bool ),
inference(paramod,[status(thm)],[c_2665,c_2311]) ).
cnf(c_16626,plain,
( fTrue = fFalse
| fFalse = bot_bot_bool ),
inference(paramod,[status(thm)],[c_2311,c_16625]) ).
cnf(c_2708,plain,
( fFalse = fTrue
| fFalse = bot_bot_bool ),
inference(copy,[status(thm)],[c_16626]) ).
cnf(c_16627,plain,
( ~ hBOOL(fTrue)
| fFalse = bot_bot_bool ),
inference(paramod,[status(thm)],[c_2708,c_385]) ).
cnf(c_2744,plain,
fFalse = bot_bot_bool,
inference(resolve,[status(thm)],[c_776,c_16627]) ).
cnf(c_3162,plain,
( ~ hBOOL(hAPP_H1927961489a_bool(A,B))
| cOMBK_1150238960iple_a(bot_bot_bool) != A ),
inference(paramod,[status(thm)],[c_2744,c_423]) ).
cnf(c_4527,plain,
hAPP_H1927961489a_bool(cOMBK_1150238960iple_a(fTrue),A) = fTrue,
inference(resolve,[status(thm)],[c_403,c_165]) ).
cnf(c_16628,plain,
( ~ hBOOL(fTrue)
| hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,A),cOMBK_1150238960iple_a(fTrue))) ),
inference(paramod,[status(thm)],[c_4527,c_300]) ).
cnf(c_4591,plain,
hBOOL(hAPP_f1753944735l_bool(hAPP_H1926610125l_bool(member564727580iple_a,A),cOMBK_1150238960iple_a(fTrue))),
inference(resolve,[status(thm)],[c_776,c_16628]) ).
cnf(c_16629,plain,
( ~ hBOOL(fTrue)
| cOMBK_1150238960iple_a(bot_bot_bool) != cOMBK_1150238960iple_a(fTrue) ),
inference(paramod,[status(thm)],[c_4527,c_3162]) ).
cnf(c_16630,plain,
( ~ hBOOL(fTrue)
| cOMBK_1150238960iple_a(fTrue) != cOMBK_1150238960iple_a(bot_bot_bool) ),
inference(copy,[status(thm)],[c_16629]) ).
cnf(c_4592,plain,
cOMBK_1150238960iple_a(fTrue) != cOMBK_1150238960iple_a(bot_bot_bool),
inference(resolve,[status(thm)],[c_776,c_16630]) ).
cnf(c_4715,plain,
hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),cOMBK_1150238960iple_a(fTrue)) = cOMBK_1150238960iple_a(fTrue),
inference(resolve,[status(thm)],[c_4591,c_210]) ).
cnf(c_16631,plain,
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(cOMBK_bool_state(finite520909254iple_a(A,B))),sK0(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(finite520909254iple_a(A,B))))),sK1(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(finite520909254iple_a(A,B))))))
| finite520909254iple_a(A,B) = fTrue ),
inference(resolve,[status(thm)],[c_740,c_470]) ).
cnf(c_16632,plain,
( hBOOL(hAPP_state_bool(cOMBK_bool_state(finite520909254iple_a(A,B)),sK1(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(finite520909254iple_a(A,B))))))
| finite520909254iple_a(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_394,c_16631]) ).
cnf(c_15800,plain,
( hBOOL(finite520909254iple_a(A,B))
| finite520909254iple_a(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_2313,c_16632]) ).
cnf(c_16633,plain,
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(cOMBK_bool_state(hAPP_state_bool(A,B))),sK0(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(hAPP_state_bool(A,B))))),sK1(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(hAPP_state_bool(A,B))))))
| hAPP_state_bool(A,B) = fTrue ),
inference(resolve,[status(thm)],[c_741,c_470]) ).
cnf(c_16634,plain,
( hBOOL(hAPP_state_bool(cOMBK_bool_state(hAPP_state_bool(A,B)),sK1(hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),g,c,cOMBK_1458035955bool_a(cOMBK_bool_state(hAPP_state_bool(A,B))))))
| hAPP_state_bool(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_394,c_16633]) ).
cnf(c_15801,plain,
( hBOOL(hAPP_state_bool(A,B))
| hAPP_state_bool(A,B) = fTrue ),
inference(paramod,[status(thm)],[c_2309,c_16634]) ).
cnf(c_16635,plain,
( finite520909254iple_a(A,B) = fTrue
| finite520909254iple_a(A,B) = fTrue ),
inference(resolve,[status(thm)],[c_15800,c_581]) ).
cnf(c_16075,plain,
finite520909254iple_a(A,B) = fTrue,
inference(copy,[status(thm)],[c_16635]) ).
cnf(c_16179,plain,
cOMBK_1150238960iple_a(finite520909254iple_a(A,B)) != cOMBK_1150238960iple_a(bot_bot_bool),
inference(paramod,[status(thm)],[c_16075,c_4592]) ).
cnf(c_16636,plain,
hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A),cOMBK_1150238960iple_a(fTrue)) = cOMBK_1150238960iple_a(finite520909254iple_a(B,C)),
inference(paramod,[status(thm)],[c_16075,c_4715]) ).
cnf(c_16637,plain,
cOMBK_1150238960iple_a(fTrue) = cOMBK_1150238960iple_a(finite520909254iple_a(B,C)),
inference(paramod,[status(thm)],[c_4715,c_16636]) ).
cnf(c_16183,plain,
cOMBK_1150238960iple_a(finite520909254iple_a(A,B)) = cOMBK_1150238960iple_a(fTrue),
inference(copy,[status(thm)],[c_16637]) ).
cnf(c_16638,plain,
( hBOOL(bot_bot_bool)
| hAPP_state_bool(cOMBK_bool_state(bot_bot_bool),A) = fTrue ),
inference(paramod,[status(thm)],[c_2314,c_15801]) ).
cnf(c_16639,plain,
( hBOOL(bot_bot_bool)
| bot_bot_bool = fTrue ),
inference(paramod,[status(thm)],[c_2314,c_16638]) ).
cnf(c_16640,plain,
( hBOOL(bot_bot_bool)
| fTrue = bot_bot_bool ),
inference(copy,[status(thm)],[c_16639]) ).
cnf(c_16511,plain,
fTrue = bot_bot_bool,
inference(resolve,[status(thm)],[c_508,c_16640]) ).
cnf(c_16641,plain,
cOMBK_1150238960iple_a(finite520909254iple_a(A,B)) = cOMBK_1150238960iple_a(bot_bot_bool),
inference(paramod,[status(thm)],[c_16511,c_16183]) ).
cnf(c_16598,plain,
$false,
inference(resolve,[status(thm)],[c_16179,c_16641]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 26 15:58:34 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 1958929 was started by sandbox2 on n020,
% 0.11/0.37 % Sat Sep 26 15:58:34 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.40
% 0.11/0.40 % From the command line: assign(max_seconds, 300).
% 0.11/0.40
% 0.11/0.40 % SInE: 127 to sos, 16 to usable, of 143 axioms (tolerance 2.00, depth 0 fixpoint).
% 53.05/8.19
% 53.05/8.19 % given #500 (A,wt=43): 492 -hBOOL(hAPP_H1927961489a_bool(A,B)) | hAPP_f1400872321a_bool(hAPP_f1104866853a_bool(cOMBS_213702372l_bool,hAPP_f13210641l_bool(cOMBB_633860163iple_a(fconj),hAPP_H562195827a_bool(fequal1878252616iple_a,B))),A) = hAPP_H562195827a_bool(fequal1878252616iple_a,B). [back_rewrite(428),rewrite([429(15),430(14)])].
% 53.05/8.19
% 53.05/8.19 % SZS status Theorem for theBenchmark
% 53.05/8.19
% 53.05/8.19 % Proof 1 at 6.26 (+ 1.13) seconds.
% 53.05/8.19 % Length of proof is 80.
% 53.05/8.19 % Level of proof is 12.
% 53.05/8.19 % Maximum clause weight is 414.000.
% 53.05/8.19 % Given clauses 742.
% 53.05/8.19
% 53.05/8.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------