%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SWW471_1 : TPTP v6.4.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n149.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 06:08:28 EDT 2016
% Result : Timeout 300.09s
% Output : None
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.03 % Problem : SWW471_1 : TPTP v6.4.0. Released v5.3.0.
% 0.01/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.23 % Computer : n149.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.75MB
% 0.02/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Sat Apr 9 01:58:24 CDT 2016
% 0.02/0.23 % CPUTime :
% 6.31/5.85 > val it = (): unit
% 6.90/6.50 Trying to find a model that refutes: (ALL X.
% 6.90/6.50 bnd_hBOOL
% 6.90/6.50 (bnd_hAPP_f1454306822l_bool
% 6.90/6.50 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 6.90/6.50 bnd_g)) -->
% 6.90/6.50 bnd_hBOOL
% 6.90/6.50 (bnd_hAPP_H1448631928a_bool (bnd_hoare_1572001082alid_a bnd_n, X))) -->
% 6.90/6.50 (ALL X.
% 6.90/6.50 bnd_hBOOL
% 6.90/6.50 (bnd_hAPP_f1454306822l_bool
% 6.90/6.50 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 6.90/6.50 bnd_image_68284913iple_a
% 6.90/6.50 (bnd_cOMBS_821474699iple_a
% 6.90/6.50 (bnd_cOMBS_1125763966iple_a
% 6.90/6.50 (bnd_cOMBB_1515136928_pname
% 6.90/6.50 (bnd_hoare_1652181356iple_a, bnd_p),
% 6.90/6.50 bnd_body),
% 6.90/6.50 bnd_q),
% 6.90/6.50 bnd_procs))) -->
% 6.90/6.50 bnd_hBOOL
% 6.90/6.50 (bnd_hAPP_H1448631928a_bool (bnd_hoare_1572001082alid_a bnd_n, X)))
% 14.42/13.92 Unfolded term: [| ALL N.
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_g,
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname
% 14.42/13.92 (bnd_hoare_1652181356iple_a, bnd_p),
% 14.42/13.92 bnd_body),
% 14.42/13.92 bnd_q),
% 14.42/13.92 bnd_procs)))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a N, X))) -->
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname
% 14.42/13.92 (bnd_hoare_1652181356iple_a, bnd_p),
% 14.42/13.92 bnd_cOMBB_923936821_pname (bnd_the_com, bnd_body_1)),
% 14.42/13.92 bnd_q),
% 14.42/13.92 bnd_procs))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (bnd_hoare_1572001082alid_a N, X)));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_p1788720341iple_a (bnd_cOMBB_1515136928_pname (P, Q), R) =
% 14.42/13.92 bnd_hAPP_f185596029iple_a (P, bnd_hAPP_p635540397e_bool (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_p1513881570iple_a (bnd_cOMBS_1125763966iple_a (P, Q), R) =
% 14.42/13.92 bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_p1788720341iple_a (P, R), bnd_hAPP_pname_com (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (bnd_cOMBC_862840740l_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_f1454306822l_bool (bnd_hAPP_H694056973l_bool (P, R), Q);
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_p824302401iple_a (bnd_cOMBS_821474699iple_a (P, Q), R) =
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_p1513881570iple_a (P, R),
% 14.42/13.92 bnd_hAPP_p635540397e_bool (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H963118037iple_a (bnd_cOMBB_1110279240iple_a (P, Q), R) =
% 14.42/13.92 bnd_hAPP_p824302401iple_a (P, bnd_hAPP_H2145880809_pname (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (bnd_cOMBC_671859290a_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (bnd_hAPP_H1027145665a_bool (P, R), Q);
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H1487873860l_bool (bnd_cOMBB_196465322iple_a (P, Q), R) =
% 14.42/13.92 bnd_hAPP_b589554111l_bool (P, bnd_hAPP_H1448631928a_bool (Q, R));
% 14.42/13.92 ALL P Q. bnd_hAPP_H963118037iple_a (bnd_cOMBK_2109678094iple_a P, Q) = P;
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_pname (bnd_cOMBB_1433562676_pname (P, Q), R) =
% 14.42/13.92 bnd_hAPP_H2145880809_pname (P, bnd_hAPP_p824302401iple_a (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (bnd_cOMBS_2061548107l_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_H1487873860l_bool (P, R),
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (bnd_cOMBB_213049548iple_a (P, Q), R) =
% 14.42/13.92 bnd_hAPP_bool_bool (P, bnd_hAPP_H1448631928a_bool (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_bool (bnd_cOMBC_1058051404l_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_f1664156314l_bool (bnd_hAPP_p338031245l_bool (P, R), Q);
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_p393069232l_bool (bnd_cOMBB_675860798_pname (P, Q), R) =
% 14.42/13.92 bnd_hAPP_b589554111l_bool (P, bnd_hAPP_pname_bool (Q, R));
% 14.42/13.92 ALL P Q. bnd_hAPP_p824302401iple_a (bnd_cOMBK_669226658_pname P, Q) = P;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 bnd_hAPP_H2145880809_pname (bnd_cOMBK_1495131898iple_a P, Q) = P;
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_com (bnd_cOMBB_923936821_pname (P, Q), R) =
% 14.42/13.92 bnd_hAPP_option_com_com (P, bnd_hAPP_p799580910on_com (Q, R));
% 14.42/13.92 ALL P Q. bnd_hAPP_H1448631928a_bool (bnd_cOMBK_712844119iple_a P, Q) = P;
% 14.42/13.92 ALL X_1 Y.
% 14.42/13.92 ~ X_1 = Y |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hAPP_H1027145665a_bool (bnd_fequal1440857775iple_a, X_1), Y));
% 14.42/13.92 ALL X_1 Y.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hAPP_H1027145665a_bool (bnd_fequal1440857775iple_a, X_1),
% 14.42/13.92 Y)) |
% 14.42/13.92 X_1 = Y;
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_bool (bnd_cOMBC_1149511130e_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_pname_bool (bnd_hAPP_p61793385e_bool (P, R), Q);
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_bool (bnd_cOMBS_568398431l_bool (P, Q), R) =
% 14.42/13.92 bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_p393069232l_bool (P, R), bnd_hAPP_pname_bool (Q, R));
% 14.42/13.92 ALL P Q R.
% 14.42/13.92 bnd_hAPP_pname_bool (bnd_cOMBB_647938656_pname (P, Q), R) =
% 14.42/13.92 bnd_hAPP_bool_bool (P, bnd_hAPP_pname_bool (Q, R));
% 14.42/13.92 ALL P Q. bnd_hAPP_pname_pname (bnd_cOMBK_pname_pname P, Q) = P;
% 14.42/13.92 ALL P Q. bnd_hAPP_pname_bool (bnd_cOMBK_bool_pname P, Q) = P;
% 14.42/13.92 ALL X_1 Y.
% 14.42/13.92 ~ X_1 = Y |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool
% 14.42/13.92 (bnd_hAPP_p61793385e_bool (bnd_fequal_pname, X_1), Y));
% 14.42/13.92 ALL X_1 Y.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool
% 14.42/13.92 (bnd_hAPP_p61793385e_bool (bnd_fequal_pname, X_1), Y)) |
% 14.42/13.92 X_1 = Y;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fimplies, P), Q)) |
% 14.42/13.92 ~ bnd_hBOOL P) |
% 14.42/13.92 bnd_hBOOL Q;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 ~ bnd_hBOOL Q |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fimplies, P), Q));
% 14.42/13.92 ALL Q P.
% 14.42/13.92 bnd_hBOOL P |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fimplies, P), Q));
% 14.42/13.92 ALL P. P = bnd_fTrue | P = bnd_fFalse; ~ bnd_hBOOL bnd_fFalse;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fdisj, P), Q)) |
% 14.42/13.92 bnd_hBOOL P) |
% 14.42/13.92 bnd_hBOOL Q;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 ~ bnd_hBOOL Q |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool (bnd_hAPP_b589554111l_bool (bnd_fdisj, P), Q));
% 14.42/13.92 ALL Q P.
% 14.42/13.92 ~ bnd_hBOOL P |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool (bnd_hAPP_b589554111l_bool (bnd_fdisj, P), Q));
% 14.42/13.92 ALL P Q.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fconj, P), Q)) |
% 14.42/13.92 bnd_hBOOL Q;
% 14.42/13.92 ALL P Q.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool
% 14.42/13.92 (bnd_hAPP_b589554111l_bool (bnd_fconj, P), Q)) |
% 14.42/13.92 bnd_hBOOL P;
% 14.42/13.92 ALL Q P.
% 14.42/13.92 (~ bnd_hBOOL P | ~ bnd_hBOOL Q) |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_bool_bool (bnd_hAPP_b589554111l_bool (bnd_fconj, P), Q));
% 14.42/13.92 ALL P. bnd_hBOOL P | bnd_hBOOL (bnd_hAPP_bool_bool (bnd_fNot, P));
% 14.42/13.92 ALL P. ~ bnd_hBOOL (bnd_hAPP_bool_bool (bnd_fNot, P)) | ~ bnd_hBOOL P;
% 14.42/13.92 ALL C X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 bnd_image_68284913iple_a (bnd_cOMBK_669226658_pname C, A) =
% 14.42/13.92 bnd_insert1434104874iple_a (C, bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL C X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 bnd_image_pname_pname (bnd_cOMBK_pname_pname C, A) =
% 14.42/13.92 bnd_insert_pname (C, bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL C X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_image_590713477iple_a (bnd_cOMBK_2109678094iple_a C, A) =
% 14.42/13.92 bnd_insert1434104874iple_a (C, bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL C X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_image_1389863321_pname (bnd_cOMBK_1495131898iple_a C, A) =
% 14.42/13.92 bnd_insert_pname (C, bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL C A.
% 14.42/13.92 (A = bnd_bot_bo844097828e_bool -->
% 14.42/13.92 bnd_image_68284913iple_a (bnd_cOMBK_669226658_pname C, A) =
% 14.42/13.92 bnd_bot_bo1208640912a_bool) &
% 14.42/13.92 (~ A = bnd_bot_bo844097828e_bool -->
% 14.42/13.92 bnd_image_68284913iple_a (bnd_cOMBK_669226658_pname C, A) =
% 14.42/13.92 bnd_insert1434104874iple_a (C, bnd_bot_bo1208640912a_bool));
% 14.42/13.92 ALL C A.
% 14.42/13.92 (A = bnd_bot_bo1208640912a_bool -->
% 14.42/13.92 bnd_image_1389863321_pname (bnd_cOMBK_1495131898iple_a C, A) =
% 14.42/13.92 bnd_bot_bo844097828e_bool) &
% 14.42/13.92 (~ A = bnd_bot_bo1208640912a_bool -->
% 14.42/13.92 bnd_image_1389863321_pname (bnd_cOMBK_1495131898iple_a C, A) =
% 14.42/13.92 bnd_insert_pname (C, bnd_bot_bo844097828e_bool));
% 14.42/13.92 ALL U C_1 S T.
% 14.42/13.92 bnd_hBOOL (bnd_evalc ((C_1, S), T)) -->
% 14.42/13.92 bnd_hBOOL (bnd_evalc ((C_1, S), U)) --> U = T;
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool) =
% 14.42/13.92 bnd_insert_pname (B, bnd_bot_bo844097828e_bool) -->
% 14.42/13.92 A_1 = B;
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool) =
% 14.42/13.92 bnd_insert1434104874iple_a (B, bnd_bot_bo1208640912a_bool) -->
% 14.42/13.92 A_1 = B;
% 14.42/13.92 ALL Ga T_1 Ts.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga, bnd_insert1434104874iple_a (T_1, Ts))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_insert1434104874iple_a (T_1, bnd_bot_bo1208640912a_bool))) &
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1617968510rivs_a (Ga, Ts));
% 14.42/13.92 ALL B A_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, B),
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool))) -->
% 14.42/13.92 B = A_1;
% 14.42/13.92 ALL B A_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, B),
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool))) -->
% 14.42/13.92 B = A_1;
% 14.42/13.92 ALL Ts Ga T_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_insert1434104874iple_a (T_1, bnd_bot_bo1208640912a_bool))) -->
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1617968510rivs_a (Ga, Ts)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga, bnd_insert1434104874iple_a (T_1, Ts)));
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), A)) -->
% 14.42/13.92 bnd_insert_pname (A_1, A) = A;
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, A) = A;
% 14.42/13.92 ALL B A_1 B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_insert_pname (B, B_1)));
% 14.42/13.92 ALL B A_1 B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_insert1434104874iple_a (B, B_1)));
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 A = bnd_bot_bo844097828e_bool -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), A));
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 A = bnd_bot_bo1208640912a_bool -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1), A));
% 14.42/13.92 ALL B_1 X_2 A.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), B_1)) -->
% 14.42/13.92 (bnd_insert_pname (X_2, A) = bnd_insert_pname (X_2, B_1)) = (A = B_1);
% 14.42/13.92 ALL B_1 X_2 A.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 (bnd_insert1434104874iple_a (X_2, A) =
% 14.42/13.92 bnd_insert1434104874iple_a (X_2, B_1)) =
% 14.42/13.92 (A = B_1);
% 14.42/13.92 ALL X Xa.
% 14.42/13.92 bnd_insert_pname (X, Xa) =
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fdisj, bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, X)),
% 14.42/13.92 bnd_cOMBC_1058051404l_bool (bnd_member_pname, Xa)));
% 14.42/13.92 ALL X Xa.
% 14.42/13.92 bnd_insert1434104874iple_a (X, Xa) =
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fdisj,
% 14.42/13.92 bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, X)),
% 14.42/13.92 bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, Xa)));
% 14.42/13.92 ALL Y_1 A X_2.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (bnd_insert_pname (Y_1, A), X_2)) =
% 14.42/13.92 (Y_1 = X_2 | bnd_hBOOL (bnd_hAPP_pname_bool (A, X_2)));
% 14.42/13.92 ALL Y_1 A X_2.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_insert1434104874iple_a (Y_1, A), X_2)) =
% 14.42/13.92 (Y_1 = X_2 | bnd_hBOOL (bnd_hAPP_H1448631928a_bool (A, X_2)));
% 14.42/13.92 ALL A_1 B C D.
% 14.42/13.92 (bnd_insert_pname
% 14.42/13.92 (A_1, bnd_insert_pname (B, bnd_bot_bo844097828e_bool)) =
% 14.42/13.92 bnd_insert_pname
% 14.42/13.92 (C, bnd_insert_pname (D, bnd_bot_bo844097828e_bool))) =
% 14.42/13.92 (A_1 = C & B = D | A_1 = D & B = C);
% 14.42/13.92 ALL A_1 B C D.
% 14.42/13.92 (bnd_insert1434104874iple_a
% 14.42/13.92 (A_1, bnd_insert1434104874iple_a (B, bnd_bot_bo1208640912a_bool)) =
% 14.42/13.92 bnd_insert1434104874iple_a
% 14.42/13.92 (C, bnd_insert1434104874iple_a (D, bnd_bot_bo1208640912a_bool))) =
% 14.42/13.92 (A_1 = C & B = D | A_1 = D & B = C);
% 14.42/13.92 ALL Pa.
% 14.42/13.92 (bnd_collec829051333iple_a Pa = bnd_bot_bo1208640912a_bool) =
% 14.42/13.92 (ALL X. ~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X)));
% 14.42/13.92 ALL Pa.
% 14.42/13.92 (bnd_collect_pname Pa = bnd_bot_bo844097828e_bool) =
% 14.42/13.92 (ALL X. ~ bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X)));
% 14.42/13.92 ALL A_1 B A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_insert_pname (B, A))) =
% 14.42/13.92 (A_1 = B |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), A)));
% 14.42/13.92 ALL A_1 B A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_insert1434104874iple_a (B, A))) =
% 14.42/13.92 (A_1 = B |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1), A)));
% 14.42/13.92 ALL X_2 Y_1 A.
% 14.42/13.92 bnd_insert_pname (X_2, bnd_insert_pname (Y_1, A)) =
% 14.42/13.92 bnd_insert_pname (Y_1, bnd_insert_pname (X_2, A));
% 14.42/13.92 ALL X_2 Y_1 A.
% 14.42/13.92 bnd_insert1434104874iple_a
% 14.42/13.92 (X_2, bnd_insert1434104874iple_a (Y_1, A)) =
% 14.42/13.92 bnd_insert1434104874iple_a (Y_1, bnd_insert1434104874iple_a (X_2, A));
% 14.42/13.92 ALL X_2 A.
% 14.42/13.92 bnd_insert_pname (X_2, bnd_insert_pname (X_2, A)) =
% 14.42/13.92 bnd_insert_pname (X_2, A);
% 14.42/13.92 ALL X_2 A.
% 14.42/13.92 bnd_insert1434104874iple_a
% 14.42/13.92 (X_2, bnd_insert1434104874iple_a (X_2, A)) =
% 14.42/13.92 bnd_insert1434104874iple_a (X_2, A);
% 14.42/13.92 ALL B A_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, B),
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool))) =
% 14.42/13.92 (B = A_1);
% 14.42/13.92 ALL B A_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, B),
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool))) =
% 14.42/13.92 (B = A_1);
% 14.42/13.92 ALL A_1 Pa.
% 14.42/13.92 bnd_insert_pname (A_1, bnd_collect_pname Pa) =
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fimplies,
% 14.42/13.92 bnd_cOMBB_647938656_pname
% 14.42/13.92 (bnd_fNot,
% 14.42/13.92 bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, A_1))),
% 14.42/13.92 Pa));
% 14.42/13.92 ALL A_1 Pa.
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_collec829051333iple_a Pa) =
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fimplies,
% 14.42/13.92 bnd_cOMBB_213049548iple_a
% 14.42/13.92 (bnd_fNot,
% 14.42/13.92 bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, A_1))),
% 14.42/13.92 Pa));
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 bnd_insert_pname (A_1, A) =
% 14.42/13.92 bnd_semila278973382e_bool
% 14.42/13.92 (bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool), A);
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, A) =
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool), A);
% 14.42/13.92 ALL A_1 B_1.
% 14.42/13.92 bnd_insert_pname (A_1, B_1) =
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fdisj, bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, A_1)),
% 14.42/13.92 bnd_cOMBC_1058051404l_bool (bnd_member_pname, B_1)));
% 14.42/13.92 ALL A_1 B_1.
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, B_1) =
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fdisj,
% 14.42/13.92 bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, A_1)),
% 14.42/13.92 bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, B_1)));
% 14.42/13.92 ALL Pa. bnd_collec829051333iple_a Pa = Pa;
% 14.42/13.92 ALL Pa. bnd_collect_pname Pa = Pa;
% 14.42/13.92 ALL X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) =
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (A, X_2));
% 14.42/13.92 ALL X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2), A)) =
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (A, X_2));
% 14.42/13.92 ALL C.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_bot_bo844097828e_bool));
% 14.42/13.92 ALL C.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_bot_bo1208640912a_bool));
% 14.42/13.92 ALL Pa.
% 14.42/13.92 (bnd_bot_bo1208640912a_bool = bnd_collec829051333iple_a Pa) =
% 14.42/13.92 (ALL X. ~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X)));
% 14.42/13.92 ALL Pa.
% 14.42/13.92 (bnd_bot_bo844097828e_bool = bnd_collect_pname Pa) =
% 14.42/13.92 (ALL X. ~ bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X)));
% 14.42/13.92 ALL Pa A_1.
% 14.42/13.92 (bnd_hBOOL (bnd_hAPP_pname_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fconj, bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool)) &
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_pname_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fconj, bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL Pa A_1.
% 14.42/13.92 (bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fconj,
% 14.42/13.92 bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool)) &
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fconj,
% 14.42/13.92 bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL Pa A_1.
% 14.42/13.92 (bnd_hBOOL (bnd_hAPP_pname_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fconj, bnd_hAPP_p61793385e_bool (bnd_fequal_pname, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool)) &
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_pname_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fconj, bnd_hAPP_p61793385e_bool (bnd_fequal_pname, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL Pa A_1.
% 14.42/13.92 (bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fconj,
% 14.42/13.92 bnd_hAPP_H1027145665a_bool (bnd_fequal1440857775iple_a, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool)) &
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, A_1)) -->
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fconj,
% 14.42/13.92 bnd_hAPP_H1027145665a_bool (bnd_fequal1440857775iple_a, A_1)),
% 14.42/13.92 Pa)) =
% 14.42/13.92 bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL A_1.
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBC_1149511130e_bool (bnd_fequal_pname, A_1)) =
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL A_1.
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBC_671859290a_bool (bnd_fequal1440857775iple_a, A_1)) =
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL A.
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A))) =
% 14.42/13.92 (~ A = bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL A.
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A))) =
% 14.42/13.92 (~ A = bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL A_1.
% 14.42/13.92 bnd_collect_pname (bnd_hAPP_p61793385e_bool (bnd_fequal_pname, A_1)) =
% 14.42/13.92 bnd_insert_pname (A_1, bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL A_1.
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_hAPP_H1027145665a_bool (bnd_fequal1440857775iple_a, A_1)) =
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL A.
% 14.42/13.92 (ALL X.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A))) =
% 14.42/13.92 (A = bnd_bot_bo844097828e_bool);
% 14.42/13.92 ALL A.
% 14.42/13.92 (ALL X.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A))) =
% 14.42/13.92 (A = bnd_bot_bo1208640912a_bool);
% 14.42/13.92 ALL A_1 B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_insert_pname (A_1, B_1)));
% 14.42/13.92 ALL A_1 B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_insert1434104874iple_a (A_1, B_1)));
% 14.42/13.92 bnd_bot_bo1208640912a_bool =
% 14.42/13.92 bnd_collec829051333iple_a (bnd_cOMBK_712844119iple_a bnd_fFalse);
% 14.42/13.92 bnd_bot_bo844097828e_bool =
% 14.42/13.92 bnd_collect_pname (bnd_cOMBK_bool_pname bnd_fFalse);
% 14.42/13.92 ALL X.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (bnd_bot_bo844097828e_bool, X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X),
% 14.42/13.92 bnd_bot_bo844097828e_bool));
% 14.42/13.92 ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (bnd_bot_bo1208640912a_bool, X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_bot_bo1208640912a_bool));
% 14.42/13.92 ALL A_1 A. ~ bnd_insert_pname (A_1, A) = bnd_bot_bo844097828e_bool;
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 ~ bnd_insert1434104874iple_a (A_1, A) = bnd_bot_bo1208640912a_bool;
% 14.42/13.92 ALL A_1 A. ~ bnd_bot_bo844097828e_bool = bnd_insert_pname (A_1, A);
% 14.42/13.92 ALL A_1 A.
% 14.42/13.92 ~ bnd_bot_bo1208640912a_bool = bnd_insert1434104874iple_a (A_1, A);
% 14.42/13.92 ALL P S S1.
% 14.42/13.92 bnd_hBOOL (bnd_evalc ((bnd_hAPP_pname_com (bnd_body, P), S), S1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_evalc
% 14.42/13.92 ((bnd_hAPP_option_com_com
% 14.42/13.92 (bnd_the_com, bnd_hAPP_p799580910on_com (bnd_body_1, P)),
% 14.42/13.92 S),
% 14.42/13.92 S1));
% 14.42/13.92 ALL B A_1 B_1.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), B_1)) -->
% 14.42/13.92 A_1 = B) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_insert_pname (B, B_1)));
% 14.42/13.92 ALL B A_1 B_1.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 A_1 = B) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_insert1434104874iple_a (B, B_1)));
% 14.42/13.92 ALL A_1 B A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_insert_pname (B, A))) -->
% 14.42/13.92 ~ A_1 = B -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1), A));
% 14.42/13.92 ALL A_1 B A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_insert1434104874iple_a (B, A))) -->
% 14.42/13.92 ~ A_1 = B -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1), A));
% 14.42/13.92 ALL A_1.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, A_1),
% 14.42/13.92 bnd_bot_bo844097828e_bool));
% 14.42/13.92 ALL A_1.
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, A_1),
% 14.42/13.92 bnd_bot_bo1208640912a_bool));
% 14.42/13.92 ALL Pn S0 S1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_evalc
% 14.42/13.92 ((bnd_hAPP_option_com_com
% 14.42/13.92 (bnd_the_com, bnd_hAPP_p799580910on_com (bnd_body_1, Pn)),
% 14.42/13.92 S0),
% 14.42/13.92 S1)) -->
% 14.42/13.92 bnd_hBOOL (bnd_evalc ((bnd_hAPP_pname_com (bnd_body, Pn), S0), S1));
% 14.42/13.92 ALL Pname_1 Pname.
% 14.42/13.92 (bnd_hAPP_pname_com (bnd_body, Pname_1) =
% 14.42/13.92 bnd_hAPP_pname_com (bnd_body, Pname)) =
% 14.42/13.92 (Pname_1 = Pname);
% 14.42/13.92 ALL Pa Pn_1 Qa.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a bnd_zero_zero_nat,
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_hAPP_pname_com (bnd_body, Pn_1)),
% 14.42/13.92 Qa)));
% 14.42/13.92 ALL F G M N_1.
% 14.42/13.92 M = N_1 -->
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), N_1)) -->
% 14.42/13.92 bnd_hAPP_p824302401iple_a (F, X) =
% 14.42/13.92 bnd_hAPP_p824302401iple_a (G, X)) -->
% 14.42/13.92 bnd_image_68284913iple_a (F, M) = bnd_image_68284913iple_a (G, N_1);
% 14.42/13.92 ALL F G M N_1.
% 14.42/13.92 M = N_1 -->
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 N_1)) -->
% 14.42/13.92 bnd_hAPP_H2145880809_pname (F, X) =
% 14.42/13.92 bnd_hAPP_H2145880809_pname (G, X)) -->
% 14.42/13.92 bnd_image_1389863321_pname (F, M) =
% 14.42/13.92 bnd_image_1389863321_pname (G, N_1);
% 14.42/13.92 ALL Pn_1 Ga Pa Qa Procsa.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (bnd_semila1525949746a_bool
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname
% 14.42/13.92 (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_body),
% 14.42/13.92 Qa),
% 14.42/13.92 Procsa)),
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_cOMBB_923936821_pname (bnd_the_com, bnd_body_1)),
% 14.42/13.92 Qa),
% 14.42/13.92 Procsa))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, Pn_1), Procsa)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_insert1434104874iple_a
% 14.42/13.92 (bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a
% 14.42/13.92 (bnd_hoare_1652181356iple_a,
% 14.42/13.92 bnd_hAPP_p635540397e_bool (Pa, Pn_1)),
% 14.42/13.92 bnd_hAPP_pname_com (bnd_body, Pn_1)),
% 14.42/13.92 bnd_hAPP_p635540397e_bool (Qa, Pn_1)),
% 14.42/13.92 bnd_bot_bo1208640912a_bool)));
% 14.42/13.92 ALL Y_1.
% 14.42/13.92 ~ (ALL Fun1 Com Fun2.
% 14.42/13.92 ~ Y_1 =
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a
% 14.42/13.92 (bnd_hoare_1652181356iple_a, Fun1),
% 14.42/13.92 Com),
% 14.42/13.92 Fun2));
% 14.42/13.92 ALL N_2 Pa Pn_1 Qa.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a N_2,
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_hAPP_option_com_com
% 14.42/13.92 (bnd_the_com, bnd_hAPP_p799580910on_com (bnd_body_1, Pn_1))),
% 14.42/13.92 Qa))) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a (bnd_suc N_2),
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_hAPP_pname_com (bnd_body, Pn_1)),
% 14.42/13.92 Qa)));
% 14.42/13.92 ALL B F A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, B),
% 14.42/13.92 bnd_image_68284913iple_a (F, A))) -->
% 14.42/13.92 ~ (ALL X.
% 14.42/13.92 B = bnd_hAPP_p824302401iple_a (F, X) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A)));
% 14.42/13.92 ALL B F A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, B),
% 14.42/13.92 bnd_image_1389863321_pname (F, A))) -->
% 14.42/13.92 ~ (ALL X.
% 14.42/13.92 B = bnd_hAPP_H2145880809_pname (F, X) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A)));
% 14.42/13.92 ALL Pa Qa.
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname (bnd_fdisj, Pa), Qa)) =
% 14.42/13.92 bnd_semila278973382e_bool
% 14.42/13.92 (bnd_collect_pname Pa, bnd_collect_pname Qa);
% 14.42/13.92 ALL Pa Qa.
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a (bnd_fdisj, Pa), Qa)) =
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_collec829051333iple_a Pa, bnd_collec829051333iple_a Qa);
% 14.42/13.92 ALL R_1 S_1 X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool
% 14.42/13.92 (bnd_semila278973382e_bool
% 14.42/13.92 (bnd_cOMBC_1058051404l_bool (bnd_member_pname, R_1),
% 14.42/13.92 bnd_cOMBC_1058051404l_bool (bnd_member_pname, S_1)),
% 14.42/13.92 X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X),
% 14.42/13.92 bnd_semila278973382e_bool (R_1, S_1)));
% 14.42/13.92 ALL R_1 S_1 X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, R_1),
% 14.42/13.92 bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, S_1)),
% 14.42/13.92 X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_semila1525949746a_bool (R_1, S_1)));
% 14.42/13.92 ALL F G A.
% 14.42/13.92 bnd_image_1389863321_pname (F, bnd_image_68284913iple_a (G, A)) =
% 14.42/13.92 bnd_image_pname_pname (bnd_cOMBB_1433562676_pname (F, G), A);
% 14.42/13.92 ALL F G A.
% 14.42/13.92 bnd_image_68284913iple_a (F, bnd_image_1389863321_pname (G, A)) =
% 14.42/13.92 bnd_image_590713477iple_a (bnd_cOMBB_1110279240iple_a (F, G), A);
% 14.42/13.92 ALL A. bnd_semila278973382e_bool (A, A) = A;
% 14.42/13.92 ALL A. bnd_semila1525949746a_bool (A, A) = A;
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1) =
% 14.42/13.92 bnd_collect_pname
% 14.42/13.92 (bnd_cOMBS_568398431l_bool
% 14.42/13.92 (bnd_cOMBB_675860798_pname
% 14.42/13.92 (bnd_fdisj, bnd_cOMBC_1058051404l_bool (bnd_member_pname, A)),
% 14.42/13.92 bnd_cOMBC_1058051404l_bool (bnd_member_pname, B_1)));
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1) =
% 14.42/13.92 bnd_collec829051333iple_a
% 14.42/13.92 (bnd_cOMBS_2061548107l_bool
% 14.42/13.92 (bnd_cOMBB_196465322iple_a
% 14.42/13.92 (bnd_fdisj,
% 14.42/13.92 bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, A)),
% 14.42/13.92 bnd_cOMBC_862840740l_bool (bnd_member127332739iple_a, B_1)));
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1) =
% 14.42/13.92 bnd_semila278973382e_bool (B_1, A);
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1) =
% 14.42/13.92 bnd_semila1525949746a_bool (B_1, A);
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila278973382e_bool (A, bnd_semila278973382e_bool (A, B_1)) =
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1);
% 14.42/13.92 ALL A B_1.
% 14.42/13.92 bnd_semila1525949746a_bool (A, bnd_semila1525949746a_bool (A, B_1)) =
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1);
% 14.42/13.92 ALL A B_1 C_2.
% 14.42/13.92 bnd_semila278973382e_bool (A, bnd_semila278973382e_bool (B_1, C_2)) =
% 14.42/13.92 bnd_semila278973382e_bool (B_1, bnd_semila278973382e_bool (A, C_2));
% 14.42/13.92 ALL A B_1 C_2.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (A, bnd_semila1525949746a_bool (B_1, C_2)) =
% 14.42/13.92 bnd_semila1525949746a_bool (B_1, bnd_semila1525949746a_bool (A, C_2));
% 14.42/13.92 ALL C A B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1))) =
% 14.42/13.92 (bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), A)) |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), B_1)));
% 14.42/13.92 ALL C A B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1))) =
% 14.42/13.92 (bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C), A)) |
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C), B_1)));
% 14.42/13.92 ALL A B_1 C_2.
% 14.42/13.92 bnd_semila278973382e_bool (bnd_semila278973382e_bool (A, B_1), C_2) =
% 14.42/13.92 bnd_semila278973382e_bool (A, bnd_semila278973382e_bool (B_1, C_2));
% 14.42/13.92 ALL A B_1 C_2.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (A, B_1), C_2) =
% 14.42/13.92 bnd_semila1525949746a_bool (A, bnd_semila1525949746a_bool (B_1, C_2));
% 14.42/13.92 ALL Pa A B_1.
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1))) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))) =
% 14.42/13.92 ((EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A)) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))) |
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), B_1)) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))));
% 14.42/13.92 ALL Pa A B_1.
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1))) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))) =
% 14.42/13.92 ((EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A)) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))) |
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 B_1)) &
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))));
% 14.42/13.92 ALL Pa A B_1.
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1))) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))) =
% 14.42/13.92 ((ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))) &
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), B_1)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (Pa, X))));
% 14.42/13.92 ALL Pa A B_1.
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1))) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))) =
% 14.42/13.92 ((ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))) &
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (Pa, X))));
% 14.42/13.92 ALL B_1 A X_2.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (A, X_2)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (A, B_1), X_2));
% 14.42/13.92 ALL B_1 A X_2.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (A, X_2)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (A, B_1), X_2));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (B_1, X_2)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (A, B_1), X_2));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (B_1, X_2)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (A, B_1), X_2));
% 14.42/13.92 ALL B_1 C A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1)));
% 14.42/13.92 ALL B_1 C A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C), A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1)));
% 14.42/13.92 ALL A C B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1)));
% 14.42/13.92 ALL A C B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1)));
% 14.42/13.92 ALL Z F A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, Z),
% 14.42/13.92 bnd_image_68284913iple_a (F, A))) =
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X), A)) &
% 14.42/13.92 Z = bnd_hAPP_p824302401iple_a (F, X));
% 14.42/13.92 ALL Z F A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, Z),
% 14.42/13.92 bnd_image_1389863321_pname (F, A))) =
% 14.42/13.92 (EX X. bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 A)) &
% 14.42/13.92 Z = bnd_hAPP_H2145880809_pname (F, X));
% 14.42/13.92 ALL F X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool
% 14.42/13.92 (bnd_member127332739iple_a, bnd_hAPP_p824302401iple_a (F, X_2)),
% 14.42/13.92 bnd_image_68284913iple_a (F, A)));
% 14.42/13.92 ALL F X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool
% 14.42/13.92 (bnd_member_pname, bnd_hAPP_H2145880809_pname (F, X_2)),
% 14.42/13.92 bnd_image_1389863321_pname (F, A)));
% 14.42/13.92 ALL B F X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 B = bnd_hAPP_p824302401iple_a (F, X_2) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, B),
% 14.42/13.92 bnd_image_68284913iple_a (F, A)));
% 14.42/13.92 ALL B F X_2 A.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 B = bnd_hAPP_H2145880809_pname (F, X_2) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, B),
% 14.42/13.92 bnd_image_1389863321_pname (F, A)));
% 14.42/13.92 ALL A_1.
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (A_1, A_1)) = bnd_hBOOL A_1;
% 14.42/13.92 ALL A_1. bnd_semila278973382e_bool (A_1, A_1) = A_1;
% 14.42/13.92 ALL A_1. bnd_semila1525949746a_bool (A_1, A_1) = A_1;
% 14.42/13.92 ALL X_2.
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (X_2, X_2)) = bnd_hBOOL X_2;
% 14.42/13.92 ALL X_2. bnd_semila278973382e_bool (X_2, X_2) = X_2;
% 14.42/13.92 ALL X_2. bnd_semila1525949746a_bool (X_2, X_2) = X_2;
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (A_1, B)) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (B, A_1));
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_semila278973382e_bool (A_1, B) =
% 14.42/13.92 bnd_semila278973382e_bool (B, A_1);
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_semila1525949746a_bool (A_1, B) =
% 14.42/13.92 bnd_semila1525949746a_bool (B, A_1);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (Y_1, X_2));
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila278973382e_bool (X_2, Y_1) =
% 14.42/13.92 bnd_semila278973382e_bool (Y_1, X_2);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, Y_1) =
% 14.42/13.92 bnd_semila1525949746a_bool (Y_1, X_2);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (Y_1, X_2));
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila278973382e_bool (X_2, Y_1) =
% 14.42/13.92 bnd_semila278973382e_bool (Y_1, X_2);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, Y_1) =
% 14.42/13.92 bnd_semila1525949746a_bool (Y_1, X_2);
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (A_1, bnd_semila1168014441p_bool (A_1, B))) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (A_1, B));
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_semila278973382e_bool (A_1, bnd_semila278973382e_bool (A_1, B)) =
% 14.42/13.92 bnd_semila278973382e_bool (A_1, B);
% 14.42/13.92 ALL A_1 B.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (A_1, bnd_semila1525949746a_bool (A_1, B)) =
% 14.42/13.92 bnd_semila1525949746a_bool (A_1, B);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (X_2, Y_1))) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (X_2, Y_1));
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila278973382e_bool
% 14.42/13.92 (X_2, bnd_semila278973382e_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_semila278973382e_bool (X_2, Y_1);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (X_2, bnd_semila1525949746a_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, Y_1);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (X_2, Y_1))) =
% 14.42/13.92 bnd_hBOOL (bnd_semila1168014441p_bool (X_2, Y_1));
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila278973382e_bool
% 14.42/13.92 (X_2, bnd_semila278973382e_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_semila278973382e_bool (X_2, Y_1);
% 14.42/13.92 ALL X_2 Y_1.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (X_2, bnd_semila1525949746a_bool (X_2, Y_1)) =
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, Y_1);
% 14.42/13.92 ALL B A_1 C.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (B, bnd_semila1168014441p_bool (A_1, C))) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (A_1, bnd_semila1168014441p_bool (B, C)));
% 14.42/13.92 ALL B A_1 C.
% 14.42/13.92 bnd_semila278973382e_bool (B, bnd_semila278973382e_bool (A_1, C)) =
% 14.42/13.92 bnd_semila278973382e_bool (A_1, bnd_semila278973382e_bool (B, C));
% 14.42/13.92 ALL B A_1 C.
% 14.42/13.92 bnd_semila1525949746a_bool (B, bnd_semila1525949746a_bool (A_1, C)) =
% 14.42/13.92 bnd_semila1525949746a_bool (A_1, bnd_semila1525949746a_bool (B, C));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (Y_1, Z))) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (Y_1, bnd_semila1168014441p_bool (X_2, Z)));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila278973382e_bool (X_2, bnd_semila278973382e_bool (Y_1, Z)) =
% 14.42/13.92 bnd_semila278973382e_bool (Y_1, bnd_semila278973382e_bool (X_2, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (X_2, bnd_semila1525949746a_bool (Y_1, Z)) =
% 14.42/13.92 bnd_semila1525949746a_bool (Y_1, bnd_semila1525949746a_bool (X_2, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (Y_1, Z))) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (Y_1, bnd_semila1168014441p_bool (X_2, Z)));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila278973382e_bool (X_2, bnd_semila278973382e_bool (Y_1, Z)) =
% 14.42/13.92 bnd_semila278973382e_bool (Y_1, bnd_semila278973382e_bool (X_2, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (X_2, bnd_semila1525949746a_bool (Y_1, Z)) =
% 14.42/13.92 bnd_semila1525949746a_bool (Y_1, bnd_semila1525949746a_bool (X_2, Z));
% 14.42/13.92 ALL A_1 B C.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_semila1168014441p_bool (A_1, B), C)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (A_1, bnd_semila1168014441p_bool (B, C)));
% 14.42/13.92 ALL A_1 B C.
% 14.42/13.92 bnd_semila278973382e_bool (bnd_semila278973382e_bool (A_1, B), C) =
% 14.42/13.92 bnd_semila278973382e_bool (A_1, bnd_semila278973382e_bool (B, C));
% 14.42/13.92 ALL A_1 B C.
% 14.42/13.92 bnd_semila1525949746a_bool (bnd_semila1525949746a_bool (A_1, B), C) =
% 14.42/13.92 bnd_semila1525949746a_bool (A_1, bnd_semila1525949746a_bool (B, C));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_semila1168014441p_bool (X_2, Y_1), Z)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (Y_1, Z)));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila278973382e_bool (bnd_semila278973382e_bool (X_2, Y_1), Z) =
% 14.42/13.92 bnd_semila278973382e_bool (X_2, bnd_semila278973382e_bool (Y_1, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (X_2, Y_1), Z) =
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, bnd_semila1525949746a_bool (Y_1, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_semila1168014441p_bool (X_2, Y_1), Z)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (X_2, bnd_semila1168014441p_bool (Y_1, Z)));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila278973382e_bool (bnd_semila278973382e_bool (X_2, Y_1), Z) =
% 14.42/13.92 bnd_semila278973382e_bool (X_2, bnd_semila278973382e_bool (Y_1, Z));
% 14.42/13.92 ALL X_2 Y_1 Z.
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (X_2, Y_1), Z) =
% 14.42/13.92 bnd_semila1525949746a_bool (X_2, bnd_semila1525949746a_bool (Y_1, Z));
% 14.42/13.92 ALL Ga G_1 Ts.
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1617968510rivs_a (G_1, Ts)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1617968510rivs_a (Ga, G_1)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1617968510rivs_a (Ga, Ts));
% 14.42/13.92 ALL F G X_2.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (F, G), X_2)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_hAPP_pname_bool (F, X_2), bnd_hAPP_pname_bool (G, X_2)));
% 14.42/13.92 ALL F G X_2.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (F, G), X_2)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (F, X_2),
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (G, X_2)));
% 14.42/13.92 ALL F G X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (F, G), X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_hAPP_pname_bool (F, X), bnd_hAPP_pname_bool (G, X)));
% 14.42/13.92 ALL F G X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (bnd_semila1525949746a_bool (F, G), X)) =
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_semila1168014441p_bool
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (F, X),
% 14.42/13.92 bnd_hAPP_H1448631928a_bool (G, X)));
% 14.42/13.92 ALL F A B_1.
% 14.42/13.92 bnd_image_1389863321_pname (F, bnd_semila1525949746a_bool (A, B_1)) =
% 14.42/13.92 bnd_semila278973382e_bool
% 14.42/13.92 (bnd_image_1389863321_pname (F, A),
% 14.42/13.92 bnd_image_1389863321_pname (F, B_1));
% 14.42/13.92 ALL F A B_1.
% 14.42/13.92 bnd_image_68284913iple_a (F, bnd_semila278973382e_bool (A, B_1)) =
% 14.42/13.92 bnd_semila1525949746a_bool
% 14.42/13.92 (bnd_image_68284913iple_a (F, A), bnd_image_68284913iple_a (F, B_1));
% 14.42/13.92 ALL A B F X_2.
% 14.42/13.92 B = bnd_hAPP_H2145880809_pname (F, X_2) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X_2),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, B),
% 14.42/13.92 bnd_image_1389863321_pname (F, A)));
% 14.42/13.92 ALL A B F X_2.
% 14.42/13.92 B = bnd_hAPP_p824302401iple_a (F, X_2) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, X_2), A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, B),
% 14.42/13.92 bnd_image_68284913iple_a (F, A)));
% 14.42/13.92 ALL A C B_1.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), A))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1)));
% 14.42/13.92 ALL A C B_1.
% 14.42/13.92 (~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 B_1)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 A))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1)));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_pname_bool (B_1, X_2)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (A, X_2))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (A, B_1), X_2));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 (~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (B_1, X_2)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (A, X_2))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (A, B_1), X_2));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_pname_bool (bnd_semila278973382e_bool (A, B_1), X_2)) -->
% 14.42/13.92 ~ bnd_hBOOL (bnd_hAPP_pname_bool (A, X_2)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_pname_bool (B_1, X_2));
% 14.42/13.92 ALL A B_1 X_2.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_semila1525949746a_bool (A, B_1), X_2)) -->
% 14.42/13.92 ~ bnd_hBOOL (bnd_hAPP_H1448631928a_bool (A, X_2)) -->
% 14.42/13.92 bnd_hBOOL (bnd_hAPP_H1448631928a_bool (B_1, X_2));
% 14.42/13.92 ALL C A B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C),
% 14.42/13.92 bnd_semila278973382e_bool (A, B_1))) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1664156314l_bool
% 14.42/13.92 (bnd_hAPP_p338031245l_bool (bnd_member_pname, C), B_1));
% 14.42/13.92 ALL C A B_1.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 bnd_semila1525949746a_bool (A, B_1))) -->
% 14.42/13.92 ~ bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C),
% 14.42/13.92 A)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, C), B_1));
% 14.42/13.92 ALL Ga Pa Qa Procsa.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (bnd_semila1525949746a_bool
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname
% 14.42/13.92 (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_body),
% 14.42/13.92 Qa),
% 14.42/13.92 Procsa)),
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_cOMBB_923936821_pname (bnd_the_com, bnd_body_1)),
% 14.42/13.92 Qa),
% 14.42/13.92 Procsa))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hoare_1617968510rivs_a
% 14.42/13.92 (Ga,
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname (bnd_hoare_1652181356iple_a, Pa),
% 14.42/13.92 bnd_body),
% 14.42/13.92 Qa),
% 14.42/13.92 Procsa)));
% 14.42/13.92 ALL Ga Ts.
% 14.42/13.92 bnd_hBOOL (bnd_hoare_1955801856lids_a (Ga, Ts)) =
% 14.42/13.92 (ALL N.
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 Ga)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a N, X))) -->
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 Ts)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a N, X))));
% 14.42/13.92 ALL Fun1_2 Com_2 Fun2_2 Fun1_1 Com_1 Fun2_1.
% 14.42/13.92 (bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a (bnd_hoare_1652181356iple_a, Fun1_2),
% 14.42/13.92 Com_2),
% 14.42/13.92 Fun2_2) =
% 14.42/13.92 bnd_hAPP_f711275241iple_a
% 14.42/13.92 (bnd_hAPP_c429049308iple_a
% 14.42/13.92 (bnd_hAPP_f185596029iple_a (bnd_hoare_1652181356iple_a, Fun1_1),
% 14.42/13.92 Com_1),
% 14.42/13.92 Fun2_1)) =
% 14.42/13.92 ((Fun1_2 = Fun1_1 & Com_2 = Com_1) & Fun2_2 = Fun2_1) |]
% 14.42/13.92 ==> (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_g)) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool
% 14.42/13.92 (bnd_hoare_1572001082alid_a bnd_n, X))) -->
% 14.42/13.92 (ALL X.
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_f1454306822l_bool
% 14.42/13.92 (bnd_hAPP_H694056973l_bool (bnd_member127332739iple_a, X),
% 14.42/13.92 bnd_image_68284913iple_a
% 14.42/13.92 (bnd_cOMBS_821474699iple_a
% 14.42/13.92 (bnd_cOMBS_1125763966iple_a
% 14.42/13.92 (bnd_cOMBB_1515136928_pname
% 14.42/13.92 (bnd_hoare_1652181356iple_a, bnd_p),
% 14.42/13.92 bnd_body),
% 14.42/13.92 bnd_q),
% 14.42/13.92 bnd_procs))) -->
% 14.42/13.92 bnd_hBOOL
% 14.42/13.92 (bnd_hAPP_H1448631928a_bool (bnd_hoare_1572001082alid_a bnd_n, X)))
% 14.42/13.92 Adding axioms...
% 14.42/13.93 Typedef.type_definition_def
% 14.62/14.11 Typedef.type_definition_def
% 14.83/14.32 Typedef.type_definition_def
% 14.92/14.49 Typedef.type_definition_def
% 15.12/14.66 Typedef.type_definition_def
% 15.32/14.89 Typedef.type_definition_def
% 15.72/15.21 Typedef.type_definition_def
% 15.83/15.39 Typedef.type_definition_def
% 16.13/15.60 Typedef.type_definition_def
% 16.23/15.78 Typedef.type_definition_def
% 16.42/15.99 Typedef.type_definition_def
% 16.62/16.16 Typedef.type_definition_def
% 16.83/16.39 Typedef.type_definition_def
% 17.73/17.23 Typedef.type_definition_def
% 17.92/17.41 Typedef.type_definition_def
% 18.22/17.79 Typedef.type_definition_def
% 18.43/17.97 Typedef.type_definition_def
% 18.73/18.27 Typedef.type_definition_def
% 19.03/18.58 Typedef.type_definition_def
% 19.33/18.88 Typedef.type_definition_def
% 20.43/19.91 Typedef.type_definition_def
% 20.63/20.12 Typedef.type_definition_def
% 21.03/20.51 Typedef.type_definition_def
% 21.45/20.96 Typedef.type_definition_def
% 21.63/21.19 Typedef.type_definition_def
% 21.84/21.39 Typedef.type_definition_def
% 22.44/21.97 Typedef.type_definition_def
% 23.43/22.99 Typedef.type_definition_def
% 23.84/23.33 Typedef.type_definition_def
% 24.14/23.67 Typedef.type_definition_def
% 24.94/24.48 Typedef.type_definition_def
% 25.75/25.23 Typedef.type_definition_def
% 31.54/31.08 Typedef.type_definition_def
% 91.74/91.19 ...done.
% 91.95/91.36 Ground types: ?'b, bnd_nat, bnd_hoare_1927711152iple_a, bnd_bool, bnd_fun_Ho1877127206a_bool, bnd_fun_fu832487784l_bool, bnd_fun_Ho525994229l_bool, bnd_fun_pname_bool, bnd_fun_pn708290217iple_a, bnd_fun_pn1683930517e_bool, bnd_fun_pn579076298iple_a, bnd_fun_pname_com, bnd_fun_pn308211645iple_a, bnd_fun_fu90068325iple_a, bnd_fun_pname_option_com, bnd_fun_option_com_com, bnd_pname, bnd_fun_co1155576772iple_a, bnd_fun_a_fun_state_bool, bnd_fun_fu1344872529iple_a, bnd_com, bnd_fun_Ho842746065_pname, bnd_fun_Ho843200573iple_a, bnd_fun_Ho440810351a_bool, bnd_fun_bo1549164019l_bool, bnd_fun_bool_bool, bnd_fun_Ho957066028l_bool, bnd_fun_pname_pname, bnd_fun_pn422929397l_bool, bnd_fun_fu1430349052l_bool, bnd_fun_pn250273176l_bool, bnd_option_com, bnd_fun_pn800050071e_bool, bnd_state
% 91.95/91.36 Translating term (sizes: 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) ...
% 128.13/127.50 Invoking SAT solver...
% 128.13/127.51 No model exists.
% 128.13/127.51 Translating term (sizes: 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) ...
% 189.13/188.22 Invoking SAT solver...
% 189.13/188.22 No model exists.
% 189.13/188.22 Translating term (sizes: 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) ...
% 226.67/225.69 Invoking SAT solver...
% 226.77/225.70 No model exists.
% 226.77/225.70 Translating term (sizes: 1, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) ...
% 278.03/276.75 Invoking SAT solver...
% 278.03/276.75 No model exists.
% 278.03/276.75 Translating term (sizes: 1, 1, 1, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1) ...
% 300.09/298.62 /export/starexec/sandbox/solver/lib/scripts/run-polyml-5.5.2: line 82: 3585 CPU time limit exceeded (core dumped) "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS
% 300.09/298.62 3586 (core dumped) | { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
% 300.09/298.63 /export/starexec/sandbox/solver/src/HOL/TPTP/lib/Tools/tptp_refute: line 26: 3531 Exit 152 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP
% 300.09/298.63 3532 CPU time limit exceeded (core dumped) | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
%------------------------------------------------------------------------------