diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-07-31 12:17:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-31 12:17:29 -0500 |
| commit | 7537ff075dbb2d814d722d2d72586ce78235467c (patch) | |
| tree | 4adca4f03007da65ddfc2a313f6ecfaf9477626c /test/regress/regress1 | |
| parent | 79af28acb3bdd16d18f325c7a4fab36604232ab0 (diff) | |
Parsing THF and adding several regressions (#3131)
Diffstat (limited to 'test/regress/regress1')
19 files changed, 1269 insertions, 1146 deletions
diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2 new file mode 100644 index 000000000..bee17b21a --- /dev/null +++ b/test/regress/regress1/ho/NUM638^1.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --uf-ho --finite-model-find +; EXPECT: unsat + +(set-option :incremental false) +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort nat 0) +(declare-fun x () nat) +(declare-fun n_1 () nat) +(assert (not (= x n_1))) +(declare-fun suc (nat) nat) +(declare-fun some ((-> nat Bool)) Bool) +(assert (forall ((Xx nat) (Xy nat)) (=> (= (suc Xx) (suc Xy)) (= Xx Xy)) )) +(assert (forall ((Xx nat)) (=> (not (= Xx n_1)) (some (lambda ((Xu nat)) (= Xx (suc Xu))))) )) +(assert (not (not (=> (forall ((Xx_0 nat) (Xy nat)) (=> (= x (suc Xx_0)) (=> (= x (suc Xy)) (= Xx_0 Xy))) ) (not (some (lambda ((Xu nat)) (= x (suc Xu))))))))) +(meta-info :filename "NUM638^1") +(check-sat-assuming ( (not false) )) diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p new file mode 100644 index 000000000..d2977ddb8 --- /dev/null +++ b/test/regress/regress1/ho/NUM925^1.p @@ -0,0 +1,638 @@ +% COMMAND-LINE: --uf-ho +% EXPECT: % SZS status Theorem for NUM925^1 + +%------------------------------------------------------------------------------ +% File : NUM925^1 : TPTP v7.2.0. Released v5.3.0. +% Domain : Number Theory +% Problem : Sum of two squares line 192, 100 axioms selected +% Version : Especial. +% English : + +% Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day +% : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe +% Source : [Bla11] +% Names : s2s_100_thf_l192 [Bla11] + +% Status : Theorem +% Rating : 0.22 v7.2.0, 0.12 v7.1.0, 0.38 v7.0.0, 0.29 v6.4.0, 0.33 v6.3.0, 0.40 v6.2.0, 0.29 v6.1.0, 0.43 v5.5.0, 0.33 v5.4.0, 0.40 v5.3.0 +% Syntax : Number of formulae : 128 ( 0 unit; 21 type; 0 defn) +% Number of atoms : 868 ( 105 equality; 251 variable) +% Maximal formula depth : 11 ( 5 average) +% Number of connectives : 571 ( 20 ~; 4 |; 7 &; 495 @) +% ( 36 <=>; 9 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 18 ( 18 >; 0 *; 0 +; 0 <<) +% Number of symbols : 23 ( 21 :; 0 =) +% Number of variables : 118 ( 0 sgn; 118 !; 0 ?; 0 ^) +% ( 118 :; 0 !>; 0 ?*) +% ( 0 @-; 0 @+) +% SPC : TH0_THM_EQU_NAR + +% Comments : This file was generated by Isabelle (most likely Sledgehammer) +% 2011-08-09 19:10:38 +%------------------------------------------------------------------------------ +%----Should-be-implicit typings (2) +thf(ty_ty_tc__Int__Oint,type,( + int: $tType )). + +thf(ty_ty_tc__Nat__Onat,type,( + nat: $tType )). + +%----Explicit typings (19) +thf(sy_c_Groups_Oone__class_Oone_000tc__Int__Oint,type,( + one_one_int: int )). + +thf(sy_c_Groups_Oone__class_Oone_000tc__Nat__Onat,type,( + one_one_nat: nat )). + +thf(sy_c_Groups_Oplus__class_Oplus_000tc__Int__Oint,type,( + plus_plus_int: int > int > int )). + +thf(sy_c_Groups_Oplus__class_Oplus_000tc__Nat__Onat,type,( + plus_plus_nat: nat > nat > nat )). + +thf(sy_c_Groups_Ozero__class_Ozero_000tc__Int__Oint,type,( + zero_zero_int: int )). + +thf(sy_c_Groups_Ozero__class_Ozero_000tc__Nat__Onat,type,( + zero_zero_nat: nat )). + +thf(sy_c_Int_OBit0,type,( + bit0: int > int )). + +thf(sy_c_Int_OBit1,type,( + bit1: int > int )). + +thf(sy_c_Int_OPls,type,( + pls: int )). + +thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Int__Oint,type,( + number_number_of_int: int > int )). + +thf(sy_c_Int_Onumber__class_Onumber__of_000tc__Nat__Onat,type,( + number_number_of_nat: int > nat )). + +thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Int__Oint,type,( + semiri1621563631at_int: nat > int )). + +thf(sy_c_Nat_Osemiring__1__class_Oof__nat_000tc__Nat__Onat,type,( + semiri984289939at_nat: nat > nat )). + +thf(sy_c_Orderings_Oord__class_Oless_000tc__Int__Oint,type,( + ord_less_int: int > int > $o )). + +thf(sy_c_Orderings_Oord__class_Oless_000tc__Nat__Onat,type,( + ord_less_nat: nat > nat > $o )). + +thf(sy_c_Power_Opower__class_Opower_000tc__Int__Oint,type,( + power_power_int: int > nat > int )). + +thf(sy_c_Power_Opower__class_Opower_000tc__Nat__Onat,type,( + power_power_nat: nat > nat > nat )). + +thf(sy_v_n____,type,( + n: nat )). + +thf(sy_v_t____,type,( + t: int )). + +%----Relevant facts (106) +thf(fact_0_n1pos,axiom, + ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) )). + +thf(fact_1_t1,axiom, + ( ord_less_int @ one_one_int @ t )). + +thf(fact_2_sum__power2__eq__zero__iff,axiom,( + ! [X_3: int,Y_3: int] : + ( ( ( plus_plus_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) + = zero_zero_int ) + <=> ( ( X_3 = zero_zero_int ) + & ( Y_3 = zero_zero_int ) ) ) )). + +thf(fact_3_one__power2,axiom, + ( ( power_power_int @ one_one_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = one_one_int )). + +thf(fact_4_one__power2,axiom, + ( ( power_power_nat @ one_one_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = one_one_nat )). + +thf(fact_5_zero__power2,axiom, + ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_int )). + +thf(fact_6_zero__power2,axiom, + ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_nat )). + +thf(fact_7_zero__eq__power2,axiom,( + ! [A_7: int] : + ( ( ( power_power_int @ A_7 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = zero_zero_int ) + <=> ( A_7 = zero_zero_int ) ) )). + +thf(fact_8_add__special_I2_J,axiom,( + ! [W_7: int] : + ( ( plus_plus_int @ one_one_int @ ( number_number_of_int @ W_7 ) ) + = ( number_number_of_int @ ( plus_plus_int @ ( bit1 @ pls ) @ W_7 ) ) ) )). + +thf(fact_9_add__special_I3_J,axiom,( + ! [V_5: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_5 ) @ one_one_int ) + = ( number_number_of_int @ ( plus_plus_int @ V_5 @ ( bit1 @ pls ) ) ) ) )). + +thf(fact_10_one__add__one__is__two,axiom, + ( ( plus_plus_int @ one_one_int @ one_one_int ) + = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_11_semiring__one__add__one__is__two,axiom, + ( ( plus_plus_int @ one_one_int @ one_one_int ) + = ( number_number_of_int @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_12_semiring__one__add__one__is__two,axiom, + ( ( plus_plus_nat @ one_one_nat @ one_one_nat ) + = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_13_quartic__square__square,axiom,( + ! [X_3: int] : + ( ( power_power_int @ ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + = ( power_power_int @ X_3 @ ( number_number_of_nat @ ( bit0 @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) )). + +thf(fact_14_power__0__left__number__of,axiom,( + ! [W_6: int] : + ( ( ( ( number_number_of_nat @ W_6 ) + = zero_zero_nat ) + => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) ) + = one_one_int ) ) + & ( ( ( number_number_of_nat @ W_6 ) + != zero_zero_nat ) + => ( ( power_power_int @ zero_zero_int @ ( number_number_of_nat @ W_6 ) ) + = zero_zero_int ) ) ) )). + +thf(fact_15_power__0__left__number__of,axiom,( + ! [W_6: int] : + ( ( ( ( number_number_of_nat @ W_6 ) + = zero_zero_nat ) + => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) ) + = one_one_nat ) ) + & ( ( ( number_number_of_nat @ W_6 ) + != zero_zero_nat ) + => ( ( power_power_nat @ zero_zero_nat @ ( number_number_of_nat @ W_6 ) ) + = zero_zero_nat ) ) ) )). + +thf(fact_16_semiring__norm_I110_J,axiom, + ( one_one_int + = ( number_number_of_int @ ( bit1 @ pls ) ) )). + +thf(fact_17_numeral__1__eq__1,axiom, + ( ( number_number_of_int @ ( bit1 @ pls ) ) + = one_one_int )). + +thf(fact_18_n0,axiom, + ( ord_less_nat @ zero_zero_nat @ n )). + +thf(fact_19_zless__linear,axiom,( + ! [X_3: int,Y_3: int] : + ( ( ord_less_int @ X_3 @ Y_3 ) + | ( X_3 = Y_3 ) + | ( ord_less_int @ Y_3 @ X_3 ) ) )). + +thf(fact_20_less__number__of__int__code,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( number_number_of_int @ K ) @ ( number_number_of_int @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_21_plus__numeral__code_I9_J,axiom,( + ! [V_3: int,W_4: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_3 ) @ ( number_number_of_int @ W_4 ) ) + = ( number_number_of_int @ ( plus_plus_int @ V_3 @ W_4 ) ) ) )). + +thf(fact_22_less__number__of,axiom,( + ! [X_6: int,Y_5: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_6 ) @ ( number_number_of_int @ Y_5 ) ) + <=> ( ord_less_int @ X_6 @ Y_5 ) ) )). + +thf(fact_23_zero__is__num__zero,axiom, + ( zero_zero_int + = ( number_number_of_int @ pls ) )). + +thf(fact_24_zpower__int,axiom,( + ! [M: nat,N_1: nat] : + ( ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) + = ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) ) )). + +thf(fact_25_int__power,axiom,( + ! [M: nat,N_1: nat] : + ( ( semiri1621563631at_int @ ( power_power_nat @ M @ N_1 ) ) + = ( power_power_int @ ( semiri1621563631at_int @ M ) @ N_1 ) ) )). + +thf(fact_26_zadd__int__left,axiom,( + ! [M: nat,N_1: nat,Z: int] : + ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( plus_plus_int @ ( semiri1621563631at_int @ N_1 ) @ Z ) ) + = ( plus_plus_int @ ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) @ Z ) ) )). + +thf(fact_27_zadd__int,axiom,( + ! [M: nat,N_1: nat] : + ( ( plus_plus_int @ ( semiri1621563631at_int @ M ) @ ( semiri1621563631at_int @ N_1 ) ) + = ( semiri1621563631at_int @ ( plus_plus_nat @ M @ N_1 ) ) ) )). + +thf(fact_28_int__1,axiom, + ( ( semiri1621563631at_int @ one_one_nat ) + = one_one_int )). + +thf(fact_29_nat__number__of__Pls,axiom, + ( ( number_number_of_nat @ pls ) + = zero_zero_nat )). + +thf(fact_30_semiring__norm_I113_J,axiom, + ( zero_zero_nat + = ( number_number_of_nat @ pls ) )). + +thf(fact_31_int__eq__0__conv,axiom,( + ! [N_1: nat] : + ( ( ( semiri1621563631at_int @ N_1 ) + = zero_zero_int ) + <=> ( N_1 = zero_zero_nat ) ) )). + +thf(fact_32_int__0,axiom, + ( ( semiri1621563631at_int @ zero_zero_nat ) + = zero_zero_int )). + +thf(fact_33_nat__1__add__1,axiom, + ( ( plus_plus_nat @ one_one_nat @ one_one_nat ) + = ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) )). + +thf(fact_34_less__int__code_I16_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit1 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_35_rel__simps_I17_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ ( bit1 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_36_rel__simps_I2_J,axiom,( + ~ ( ord_less_int @ pls @ pls ) )). + +thf(fact_37_less__int__code_I13_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit0 @ K1 ) @ ( bit0 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_38_rel__simps_I14_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit0 @ K ) @ ( bit0 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_39_zadd__strict__right__mono,axiom,( + ! [K: int,I: int,J: int] : + ( ( ord_less_int @ I @ J ) + => ( ord_less_int @ ( plus_plus_int @ I @ K ) @ ( plus_plus_int @ J @ K ) ) ) )). + +thf(fact_40_add__nat__number__of,axiom,( + ! [V_4: int,V_3: int] : + ( ( ( ord_less_int @ V_3 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ V_4 ) ) ) + & ( ~ ( ord_less_int @ V_3 @ pls ) + => ( ( ( ord_less_int @ V_4 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ V_3 ) ) ) + & ( ~ ( ord_less_int @ V_4 @ pls ) + => ( ( plus_plus_nat @ ( number_number_of_nat @ V_3 ) @ ( number_number_of_nat @ V_4 ) ) + = ( number_number_of_nat @ ( plus_plus_int @ V_3 @ V_4 ) ) ) ) ) ) ) )). + +thf(fact_41_one__is__num__one,axiom, + ( one_one_int + = ( number_number_of_int @ ( bit1 @ pls ) ) )). + +thf(fact_42_nat__numeral__1__eq__1,axiom, + ( ( number_number_of_nat @ ( bit1 @ pls ) ) + = one_one_nat )). + +thf(fact_43_Numeral1__eq1__nat,axiom, + ( one_one_nat + = ( number_number_of_nat @ ( bit1 @ pls ) ) )). + +thf(fact_44_eq__number__of,axiom,( + ! [X_5: int,Y_4: int] : + ( ( ( number_number_of_int @ X_5 ) + = ( number_number_of_int @ Y_4 ) ) + <=> ( X_5 = Y_4 ) ) )). + +thf(fact_45_number__of__reorient,axiom,( + ! [W_5: int,X_4: nat] : + ( ( ( number_number_of_nat @ W_5 ) + = X_4 ) + <=> ( X_4 + = ( number_number_of_nat @ W_5 ) ) ) )). + +thf(fact_46_number__of__reorient,axiom,( + ! [W_5: int,X_4: int] : + ( ( ( number_number_of_int @ W_5 ) + = X_4 ) + <=> ( X_4 + = ( number_number_of_int @ W_5 ) ) ) )). + +thf(fact_47_rel__simps_I51_J,axiom,( + ! [K: int,L: int] : + ( ( ( bit1 @ K ) + = ( bit1 @ L ) ) + <=> ( K = L ) ) )). + +thf(fact_48_rel__simps_I48_J,axiom,( + ! [K: int,L: int] : + ( ( ( bit0 @ K ) + = ( bit0 @ L ) ) + <=> ( K = L ) ) )). + +thf(fact_49_even__less__0__iff,axiom,( + ! [A_6: int] : + ( ( ord_less_int @ ( plus_plus_int @ A_6 @ A_6 ) @ zero_zero_int ) + <=> ( ord_less_int @ A_6 @ zero_zero_int ) ) )). + +thf(fact_50_zadd__assoc,axiom,( + ! [Z1: int,Z2: int,Z3: int] : + ( ( plus_plus_int @ ( plus_plus_int @ Z1 @ Z2 ) @ Z3 ) + = ( plus_plus_int @ Z1 @ ( plus_plus_int @ Z2 @ Z3 ) ) ) )). + +thf(fact_51_zadd__left__commute,axiom,( + ! [X_3: int,Y_3: int,Z: int] : + ( ( plus_plus_int @ X_3 @ ( plus_plus_int @ Y_3 @ Z ) ) + = ( plus_plus_int @ Y_3 @ ( plus_plus_int @ X_3 @ Z ) ) ) )). + +thf(fact_52_zadd__commute,axiom,( + ! [Z: int,W_4: int] : + ( ( plus_plus_int @ Z @ W_4 ) + = ( plus_plus_int @ W_4 @ Z ) ) )). + +thf(fact_53_int__int__eq,axiom,( + ! [M: nat,N_1: nat] : + ( ( ( semiri1621563631at_int @ M ) + = ( semiri1621563631at_int @ N_1 ) ) + <=> ( M = N_1 ) ) )). + +thf(fact_54_less__special_I3_J,axiom,( + ! [X_2: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_2 ) @ zero_zero_int ) + <=> ( ord_less_int @ X_2 @ pls ) ) )). + +thf(fact_55_less__special_I1_J,axiom,( + ! [Y_2: int] : + ( ( ord_less_int @ zero_zero_int @ ( number_number_of_int @ Y_2 ) ) + <=> ( ord_less_int @ pls @ Y_2 ) ) )). + +thf(fact_56_rel__simps_I12_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ pls ) + <=> ( ord_less_int @ K @ pls ) ) )). + +thf(fact_57_less__int__code_I15_J,axiom,( + ! [K1: int,K2: int] : + ( ( ord_less_int @ ( bit1 @ K1 ) @ ( bit0 @ K2 ) ) + <=> ( ord_less_int @ K1 @ K2 ) ) )). + +thf(fact_58_rel__simps_I16_J,axiom,( + ! [K: int,L: int] : + ( ( ord_less_int @ ( bit1 @ K ) @ ( bit0 @ L ) ) + <=> ( ord_less_int @ K @ L ) ) )). + +thf(fact_59_rel__simps_I10_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ ( bit0 @ K ) @ pls ) + <=> ( ord_less_int @ K @ pls ) ) )). + +thf(fact_60_rel__simps_I4_J,axiom,( + ! [K: int] : + ( ( ord_less_int @ pls @ ( bit0 @ K ) ) + <=> ( ord_less_int @ pls @ K ) ) )). + +thf(fact_61_bin__less__0__simps_I4_J,axiom,( + ! [W_4: int] : + ( ( ord_less_int @ ( bit1 @ W_4 ) @ zero_zero_int ) + <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) )). + +thf(fact_62_bin__less__0__simps_I1_J,axiom,( + ~ ( ord_less_int @ pls @ zero_zero_int ) )). + +thf(fact_63_bin__less__0__simps_I3_J,axiom,( + ! [W_4: int] : + ( ( ord_less_int @ ( bit0 @ W_4 ) @ zero_zero_int ) + <=> ( ord_less_int @ W_4 @ zero_zero_int ) ) )). + +thf(fact_64_int__0__less__1,axiom, + ( ord_less_int @ zero_zero_int @ one_one_int )). + +thf(fact_65_zless__add1__eq,axiom,( + ! [W_4: int,Z: int] : + ( ( ord_less_int @ W_4 @ ( plus_plus_int @ Z @ one_one_int ) ) + <=> ( ( ord_less_int @ W_4 @ Z ) + | ( W_4 = Z ) ) ) )). + +thf(fact_66_int__less__0__conv,axiom,( + ! [K: nat] : + ~ ( ord_less_int @ ( semiri1621563631at_int @ K ) @ zero_zero_int ) )). + +thf(fact_67_less__special_I4_J,axiom,( + ! [X_1: int] : + ( ( ord_less_int @ ( number_number_of_int @ X_1 ) @ one_one_int ) + <=> ( ord_less_int @ X_1 @ ( bit1 @ pls ) ) ) )). + +thf(fact_68_less__special_I2_J,axiom,( + ! [Y_1: int] : + ( ( ord_less_int @ one_one_int @ ( number_number_of_int @ Y_1 ) ) + <=> ( ord_less_int @ ( bit1 @ pls ) @ Y_1 ) ) )). + +thf(fact_69_odd__less__0,axiom,( + ! [Z: int] : + ( ( ord_less_int @ ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) @ zero_zero_int ) + <=> ( ord_less_int @ Z @ zero_zero_int ) ) )). + +thf(fact_70_double__eq__0__iff,axiom,( + ! [A_5: int] : + ( ( ( plus_plus_int @ A_5 @ A_5 ) + = zero_zero_int ) + <=> ( A_5 = zero_zero_int ) ) )). + +thf(fact_71_rel__simps_I46_J,axiom,( + ! [K: int] : + ( ( bit1 @ K ) + != pls ) )). + +thf(fact_72_rel__simps_I39_J,axiom,( + ! [L: int] : + ( pls + != ( bit1 @ L ) ) )). + +thf(fact_73_rel__simps_I50_J,axiom,( + ! [K: int,L: int] : + ( ( bit1 @ K ) + != ( bit0 @ L ) ) )). + +thf(fact_74_rel__simps_I49_J,axiom,( + ! [K: int,L: int] : + ( ( bit0 @ K ) + != ( bit1 @ L ) ) )). + +thf(fact_75_rel__simps_I44_J,axiom,( + ! [K: int] : + ( ( ( bit0 @ K ) + = pls ) + <=> ( K = pls ) ) )). + +thf(fact_76_rel__simps_I38_J,axiom,( + ! [L: int] : + ( ( pls + = ( bit0 @ L ) ) + <=> ( pls = L ) ) )). + +thf(fact_77_Bit0__Pls,axiom, + ( ( bit0 @ pls ) + = pls )). + +thf(fact_78_Pls__def,axiom,( + pls = zero_zero_int )). + +thf(fact_79_int__0__neq__1,axiom,( + zero_zero_int != one_one_int )). + +thf(fact_80_add__Pls__right,axiom,( + ! [K: int] : + ( ( plus_plus_int @ K @ pls ) + = K ) )). + +thf(fact_81_add__Pls,axiom,( + ! [K: int] : + ( ( plus_plus_int @ pls @ K ) + = K ) )). + +thf(fact_82_add__Bit0__Bit0,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit0 @ L ) ) + = ( bit0 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_83_Bit0__def,axiom,( + ! [K: int] : + ( ( bit0 @ K ) + = ( plus_plus_int @ K @ K ) ) )). + +thf(fact_84_zadd__0__right,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ Z @ zero_zero_int ) + = Z ) )). + +thf(fact_85_zadd__0,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ zero_zero_int @ Z ) + = Z ) )). + +thf(fact_86_semiring__numeral__0__eq__0,axiom, + ( ( number_number_of_int @ pls ) + = zero_zero_int )). + +thf(fact_87_semiring__numeral__0__eq__0,axiom, + ( ( number_number_of_nat @ pls ) + = zero_zero_nat )). + +thf(fact_88_number__of__Pls,axiom, + ( ( number_number_of_int @ pls ) + = zero_zero_int )). + +thf(fact_89_semiring__norm_I112_J,axiom, + ( zero_zero_int + = ( number_number_of_int @ pls ) )). + +thf(fact_90_add__numeral__0,axiom,( + ! [A_4: int] : + ( ( plus_plus_int @ ( number_number_of_int @ pls ) @ A_4 ) + = A_4 ) )). + +thf(fact_91_add__numeral__0__right,axiom,( + ! [A_3: int] : + ( ( plus_plus_int @ A_3 @ ( number_number_of_int @ pls ) ) + = A_3 ) )). + +thf(fact_92_power__eq__0__iff__number__of,axiom,( + ! [A_2: int,W_3: int] : + ( ( ( power_power_int @ A_2 @ ( number_number_of_nat @ W_3 ) ) + = zero_zero_int ) + <=> ( ( A_2 = zero_zero_int ) + & ( ( number_number_of_nat @ W_3 ) + != zero_zero_nat ) ) ) )). + +thf(fact_93_power__eq__0__iff__number__of,axiom,( + ! [A_2: nat,W_3: int] : + ( ( ( power_power_nat @ A_2 @ ( number_number_of_nat @ W_3 ) ) + = zero_zero_nat ) + <=> ( ( A_2 = zero_zero_nat ) + & ( ( number_number_of_nat @ W_3 ) + != zero_zero_nat ) ) ) )). + +thf(fact_94_add__number__of__left,axiom,( + ! [V_2: int,W_2: int,Z_1: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_2 ) @ ( plus_plus_int @ ( number_number_of_int @ W_2 ) @ Z_1 ) ) + = ( plus_plus_int @ ( number_number_of_int @ ( plus_plus_int @ V_2 @ W_2 ) ) @ Z_1 ) ) )). + +thf(fact_95_add__number__of__eq,axiom,( + ! [V_1: int,W_1: int] : + ( ( plus_plus_int @ ( number_number_of_int @ V_1 ) @ ( number_number_of_int @ W_1 ) ) + = ( number_number_of_int @ ( plus_plus_int @ V_1 @ W_1 ) ) ) )). + +thf(fact_96_number__of__add,axiom,( + ! [V: int,W: int] : + ( ( number_number_of_int @ ( plus_plus_int @ V @ W ) ) + = ( plus_plus_int @ ( number_number_of_int @ V ) @ ( number_number_of_int @ W ) ) ) )). + +thf(fact_97_add__Bit1__Bit0,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit1 @ K ) @ ( bit0 @ L ) ) + = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_98_add__Bit0__Bit1,axiom,( + ! [K: int,L: int] : + ( ( plus_plus_int @ ( bit0 @ K ) @ ( bit1 @ L ) ) + = ( bit1 @ ( plus_plus_int @ K @ L ) ) ) )). + +thf(fact_99_Bit1__def,axiom,( + ! [K: int] : + ( ( bit1 @ K ) + = ( plus_plus_int @ ( plus_plus_int @ one_one_int @ K ) @ K ) ) )). + +thf(fact_100_odd__nonzero,axiom,( + ! [Z: int] : + ( ( plus_plus_int @ ( plus_plus_int @ one_one_int @ Z ) @ Z ) + != zero_zero_int ) )). + +thf(fact_101_number__of__int,axiom,( + ! [N: nat] : + ( ( number_number_of_nat @ ( semiri1621563631at_int @ N ) ) + = ( semiri984289939at_nat @ N ) ) )). + +thf(fact_102_number__of__int,axiom,( + ! [N: nat] : + ( ( number_number_of_int @ ( semiri1621563631at_int @ N ) ) + = ( semiri1621563631at_int @ N ) ) )). + +thf(fact_103_zero__less__power2,axiom,( + ! [A_1: int] : + ( ( ord_less_int @ zero_zero_int @ ( power_power_int @ A_1 @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) + <=> ( A_1 != zero_zero_int ) ) )). + +thf(fact_104_power2__less__0,axiom,( + ! [A: int] : + ~ ( ord_less_int @ ( power_power_int @ A @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ zero_zero_int ) )). + +thf(fact_105_sum__power2__gt__zero__iff,axiom,( + ! [X: int,Y: int] : + ( ( ord_less_int @ zero_zero_int @ ( plus_plus_int @ ( power_power_int @ X @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) @ ( power_power_int @ Y @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) ) ) + <=> ( ( X != zero_zero_int ) + | ( Y != zero_zero_int ) ) ) )). + +%----Conjectures (1) +thf(conj_0,conjecture,( + ( power_power_int @ ( plus_plus_int @ one_one_int @ ( semiri1621563631at_int @ n ) ) @ ( number_number_of_nat @ ( bit0 @ ( bit1 @ pls ) ) ) ) + != zero_zero_int )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p new file mode 100644 index 000000000..a8a6bafca --- /dev/null +++ b/test/regress/regress1/ho/SYO056^1.p @@ -0,0 +1,100 @@ +% COMMAND-LINE: --uf-ho --finite-model-find +% EXPECT: % SZS status CounterSatisfiable for SYO056^1 + +%------------------------------------------------------------------------------ +% File : SYO056^1 : TPTP v7.2.0. Released v4.0.0. +% Domain : Logic Calculi (Quantified multimodal logic) +% Problem : Simple textbook example 13 +% Version : [Ben09] axioms. +% English : + +% Refs : [Gol92] Goldblatt (1992), Logics of Time and Computation +% : [Ben09] Benzmueller (2009), Email to Geoff Sutcliffe +% Source : [Ben09] +% Names : ex13.p [Ben09] + +% Status : CounterSatisfiable +% Rating : 0.25 v7.2.0, 0.33 v6.4.0, 0.00 v6.3.0, 0.33 v5.4.0, 0.00 v5.0.0, 0.67 v4.1.0, 0.50 v4.0.0 +% Syntax : Number of formulae : 64 ( 0 unit; 32 type; 31 defn) +% Number of atoms : 238 ( 36 equality; 137 variable) +% Maximal formula depth : 12 ( 6 average) +% Number of connectives : 138 ( 4 ~; 4 |; 8 &; 114 @) +% ( 0 <=>; 8 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 172 ( 172 >; 0 *; 0 +; 0 <<) +% Number of symbols : 36 ( 32 :; 0 =) +% Number of variables : 87 ( 3 sgn; 30 !; 6 ?; 51 ^) +% ( 87 :; 0 !>; 0 ?*) +% ( 0 @-; 0 @+) +% SPC : TH0_CSA_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +%----Include embedding of quantified multimodal logic in simple type theory +%% include('Axioms/LCL013^0.ax'). +%------------------------------------------------------------------------------ +thf(mvalid_type,type,( + mvalid: ( $i > $o ) > $o )). + +thf(mvalid,definition, + ( mvalid + = ( ^ [Phi: $i > $o] : + ! [W: $i] : + ( Phi @ W ) ) )). + + +thf(mforall_prop_type,type,( + mforall_prop: ( ( $i > $o ) > $i > $o ) > $i > $o )). + +thf(mforall_prop,definition, + ( mforall_prop + = ( ^ [Phi: ( $i > $o ) > $i > $o,W: $i] : + ! [P: $i > $o] : + ( Phi @ P @ W ) ) )). + +thf(mnot_type,type,( + mnot: ( $i > $o ) > $i > $o )). + +thf(mnot,definition, + ( mnot + = ( ^ [Phi: $i > $o,W: $i] : + ~ ( Phi @ W ) ) )). + +thf(mor_type,type,( + mor: ( $i > $o ) > ( $i > $o ) > $i > $o )). + +thf(mor,definition, + ( mor + = ( ^ [Phi: $i > $o,Psi: $i > $o,W: $i] : + ( ( Phi @ W ) + | ( Psi @ W ) ) ) )). + +thf(mimplies_type,type,( + mimplies: ( $i > $o ) > ( $i > $o ) > $i > $o )). + +thf(mimplies,definition, + ( mimplies + = ( ^ [Phi: $i > $o,Psi: $i > $o] : + ( mor @ ( mnot @ Phi ) @ Psi ) ) )). + +thf(mbox_type,type,( + mbox: ( $i > $i > $o ) > ( $i > $o ) > $i > $o )). + +thf(mbox,definition, + ( mbox + = ( ^ [R: $i > $i > $o,Phi: $i > $o,W: $i] : + ! [V: $i] : + ( ~ ( R @ W @ V ) + | ( Phi @ V ) ) ) )). + + +thf(conj,conjecture,( + ! [R: $i > $i > $o] : + ( mvalid + @ ( mforall_prop + @ ^ [A: $i > $o] : + ( mforall_prop + @ ^ [B: $i > $o] : + ( mimplies @ ( mbox @ R @ ( mor @ A @ B ) ) @ ( mor @ ( mbox @ R @ A ) @ ( mbox @ R @ B ) ) ) ) ) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/auth0068.smt2 b/test/regress/regress1/ho/auth0068.smt2 deleted file mode 100644 index eb0bb5d36..000000000 --- a/test/regress/regress1/ho/auth0068.smt2 +++ /dev/null @@ -1,491 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) -(declare-sort Msg$ 0) -(declare-sort Nat$ 0) -(declare-sort Agent$ 0) -(declare-sort Event$ 0) -(declare-sort Msg_set$ 0) -(declare-sort Msg_list$ 0) -(declare-sort Agent_set$ 0) -(declare-sort Event_set$ 0) -(declare-sort Agent_list$ 0) -(declare-sort Event_list$ 0) -(declare-sort Event_option$ 0) -(declare-sort Msg_list_set$ 0) -(declare-sort Agent_list_set$ 0) -(declare-sort Event_list_set$ 0) -(declare-sort Event_list_list$ 0) -(declare-fun p$ () (-> Event$ Bool)) -(declare-fun uu$ ((-> Msg$ Bool) (-> Msg$ Bool) Msg$) Bool) -(declare-fun bad$ () Agent_set$) -(declare-fun nil$ () Event_list$) -(declare-fun set$ (Event_list$) Event_set$) -(declare-fun spy$ () Agent$) -(declare-fun uua$ (Event_set$ (-> Event$ Bool) Event$) Bool) -(declare-fun uub$ (Agent_set$ (-> Agent$ Bool) Agent$) Bool) -(declare-fun uuc$ (Msg_set$ (-> Msg$ Bool) Msg$) Bool) -(declare-fun uud$ (Event_set$ Event$) Bool) -(declare-fun uue$ (Agent_set$ Agent$) Bool) -(declare-fun uuf$ (Msg_set$ Msg$) Bool) -(declare-fun uug$ (Event$ Event_list$) Bool) -(declare-fun uuh$ (Event$ Event_list$) Bool) -(declare-fun uui$ ((-> Event$ Bool) Event$ Event$) Bool) -(declare-fun uuj$ (Event_list_set$ Event_list$ Event$) Bool) -(declare-fun uuk$ (Msg$ (-> Msg$ Bool) Msg$) Bool) -(declare-fun uul$ (Msg$ Msg_set$ Msg$) Bool) -(declare-fun uum$ (Event$ Event_set$ Event$) Bool) -(declare-fun uun$ (Agent$ Agent_set$ Agent$) Bool) -(declare-fun uuo$ (Event_list$ Agent$ Agent$ Msg$) Msg_set$) -(declare-fun uup$ (Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun uuq$ (Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun uur$ (Agent$ Event_list$ Agent$ Agent$ Msg$) Msg_set$) -(declare-fun uus$ (Agent$ Event_list$ Agent$ Msg$) Msg_set$) -(declare-fun bind$ (Event_list$ (-> Event$ Event_list$)) Event_list$) -(declare-fun cons$ (Event$ Event_list$) Event_list$) -(declare-fun gets$ (Agent$ Msg$) Event$) -(declare-fun maps$ ((-> Event$ Event_list$)) (-> Event_list$ Event_list$)) -(declare-fun nil$a () Event_list_list$) -(declare-fun nil$b () Msg_list$) -(declare-fun nil$c () Agent_list$) -(declare-fun null$ (Event_list$) Bool) -(declare-fun says$ (Agent$ Agent$ Msg$) Event$) -(declare-fun set$a (Msg_list$) Msg_set$) -(declare-fun set$b (Agent_list$) Agent_set$) -(declare-fun succ$ (Event_list_set$ Event_list$) Event_set$) -(declare-fun cons$a (Event_list$ Event_list_list$) Event_list_list$) -(declare-fun cons$b (Msg$ Msg_list$) Msg_list$) -(declare-fun cons$c (Agent$ Agent_list$) Agent_list$) -(declare-fun knows$ (Agent$ Event_list$) Msg_set$) -(declare-fun notes$ (Agent$ Msg$) Event$) -(declare-fun succ$a (Msg_list_set$ Msg_list$) Msg_set$) -(declare-fun succ$b (Agent_list_set$ Agent_list$) Agent_set$) -(declare-fun append$ (Event_list$ Event_list$) Event_list$) -(declare-fun insert$ (Msg$ Msg_set$) Msg_set$) -(declare-fun member$ (Agent$ Agent_set$) Bool) -(declare-fun splice$ (Event_list$) (-> Event_list$ Event_list$)) -(declare-fun append$a (Msg_list$ Msg_list$) Msg_list$) -(declare-fun append$b (Agent_list$ Agent_list$) Agent_list$) -(declare-fun collect$ ((-> Msg$ Bool)) Msg_set$) -(declare-fun insert$a (Event$) (-> Event_list$ Event_list$)) -(declare-fun insert$b (Event$ Event_set$) Event_set$) -(declare-fun insert$c (Agent$ Agent_set$) Agent_set$) -(declare-fun insert$d (Msg$ Msg_list$) Msg_list$) -(declare-fun insert$e (Agent$ Agent_list$) Agent_list$) -(declare-fun less_eq$ (Msg_set$ Msg_set$) Bool) -(declare-fun list_ex$ ((-> Event$ Bool)) (-> Event_list$ Bool)) -(declare-fun member$a (Msg$ Msg_set$) Bool) -(declare-fun member$b (Event$ Event_set$) Bool) -(declare-fun member$c (Event_list$ Event_list_set$) Bool) -(declare-fun member$d (Event_list$ Event$) Bool) -(declare-fun member$e (Msg_list$ Msg_list_set$) Bool) -(declare-fun member$f (Agent_list$ Agent_list_set$) Bool) -(declare-fun member$g (Msg_list$ Msg$) Bool) -(declare-fun member$h (Agent_list$ Agent$) Bool) -(declare-fun rotate1$ (Event_list$) Event_list$) -(declare-fun subseqs$ (Event_list$) Event_list_list$) -(declare-fun antimono$ ((-> Msg_set$ Msg_set$)) Bool) -(declare-fun collect$a ((-> Event$ Bool)) Event_set$) -(declare-fun collect$b ((-> Agent$ Bool)) Agent_set$) -(declare-fun greatest$ ((-> Msg_set$ Bool)) Msg_set$) -(declare-fun less_eq$a (Event_set$ Event_set$) Bool) -(declare-fun less_eq$b (Agent_set$ Agent_set$) Bool) -(declare-fun less_eq$c ((-> Event$ Bool) (-> Event$ Bool)) Bool) -(declare-fun less_eq$d ((-> Agent$ Bool) (-> Agent$ Bool)) Bool) -(declare-fun less_eq$e ((-> Msg$ Bool) (-> Msg$ Bool)) Bool) -(declare-fun less_eq$f ((-> Bool Msg_set$) (-> Bool Msg_set$)) Bool) -(declare-fun list_all$ ((-> Event$ Bool) Event_list$) Bool) -(declare-fun list_ex$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_ex$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun list_ex1$ ((-> Event$ Bool)) (-> Event_list$ Bool)) -(declare-fun case_list$ (Bool (-> Event$ (-> Event_list$ Bool)) Event_list$) Bool) -(declare-fun initState$ (Agent$) Msg_set$) -(declare-fun list_all$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_all$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun list_ex1$a ((-> Msg$ Bool) Msg_list$) Bool) -(declare-fun list_ex1$b ((-> Agent$ Bool) Agent_list$) Bool) -(declare-fun takeWhile$ ((-> Event$ Bool) Event_list$) Event_list$) -(declare-fun case_event$ ((-> Agent$ (-> Agent$ (-> Msg$ Msg_set$))) (-> Agent$ (-> Msg$ Msg_set$)) (-> Agent$ (-> Msg$ Msg_set$)) Event$) Msg_set$) -(declare-fun gen_length$ (Nat$) (-> Event_list$ Nat$)) -(declare-fun map_filter$ ((-> Event$ Event_option$)) (-> Event_list$ Event_list$)) -(declare-fun takeWhile$a ((-> Msg$ Bool) Msg_list$) Msg_list$) -(declare-fun takeWhile$b ((-> Agent$ Bool) Agent_list$) Agent_list$) -(declare-fun product_lists$ (Event_list_list$) Event_list_list$) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent$)) (! (= (uue$ ?v0 ?v1) (member$ ?v1 ?v0)) :pattern ((uue$ ?v0 ?v1)))) :named a0)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg$)) (! (= (uuf$ ?v0 ?v1) (member$a ?v1 ?v0)) :pattern ((uuf$ ?v0 ?v1)))) :named a1)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event$)) (! (= (uud$ ?v0 ?v1) (member$b ?v1 ?v0)) :pattern ((uud$ ?v0 ?v1)))) :named a2)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (! (= (uuq$ ?v0 ?v1 ?v2) (ite (member$ ?v1 bad$) (insert$ ?v2 (knows$ spy$ ?v0)) (knows$ spy$ ?v0))) :pattern ((uuq$ ?v0 ?v1 ?v2)))) :named a3)) -(assert (! (forall ((?v0 Event_list_set$) (?v1 Event_list$) (?v2 Event$)) (! (= (uuj$ ?v0 ?v1 ?v2) (member$c (append$ ?v1 (cons$ ?v2 nil$)) ?v0)) :pattern ((uuj$ ?v0 ?v1 ?v2)))) :named a4)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (! (= (uun$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$ ?v2 ?v1))) :pattern ((uun$ ?v0 ?v1 ?v2)))) :named a5)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (! (= (uul$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$a ?v2 ?v1))) :pattern ((uul$ ?v0 ?v1 ?v2)))) :named a6)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (! (= (uum$ ?v0 ?v1 ?v2) (or (= ?v2 ?v0) (member$b ?v2 ?v1))) :pattern ((uum$ ?v0 ?v1 ?v2)))) :named a7)) -(assert (! (forall ((?v0 Agent_set$) (?v1 (-> Agent$ Bool)) (?v2 Agent$)) (! (= (uub$ ?v0 ?v1 ?v2) (and (member$ ?v2 ?v0) (?v1 ?v2))) :pattern ((uub$ ?v0 ?v1 ?v2)))) :named a8)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uuc$ ?v0 ?v1 ?v2) (and (member$a ?v2 ?v0) (?v1 ?v2))) :pattern ((uuc$ ?v0 ?v1 ?v2)))) :named a9)) -(assert (! (forall ((?v0 Event_set$) (?v1 (-> Event$ Bool)) (?v2 Event$)) (! (= (uua$ ?v0 ?v1 ?v2) (and (member$b ?v2 ?v0) (?v1 ?v2))) :pattern ((uua$ ?v0 ?v1 ?v2)))) :named a10)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uu$ ?v0 ?v1 ?v2) (and (?v0 ?v2) (?v1 ?v2))) :pattern ((uu$ ?v0 ?v1 ?v2)))) :named a11)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool)) (?v2 Msg$)) (! (= (uuk$ ?v0 ?v1 ?v2) (=> (not (= ?v2 ?v0)) (?v1 ?v2))) :pattern ((uuk$ ?v0 ?v1 ?v2)))) :named a12)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event$)) (! (= (uui$ ?v0 ?v1 ?v2) (or (not (?v0 ?v2)) (= ?v1 ?v2))) :pattern ((uui$ ?v0 ?v1 ?v2)))) :named a13)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (! (= (uup$ ?v0 ?v1 ?v2) (knows$ spy$ ?v0)) :pattern ((uup$ ?v0 ?v1 ?v2)))) :named a14)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (! (= (uus$ ?v0 ?v1 ?v2 ?v3) (ite (= ?v2 ?v0) (insert$ ?v3 (knows$ ?v0 ?v1)) (knows$ ?v0 ?v1))) :pattern ((uus$ ?v0 ?v1 ?v2 ?v3)))) :named a15)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (! (= (uuo$ ?v0 ?v1 ?v2 ?v3) (insert$ ?v3 (knows$ spy$ ?v0))) :pattern ((uuo$ ?v0 ?v1 ?v2 ?v3)))) :named a16)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Agent$) (?v4 Msg$)) (! (= (uur$ ?v0 ?v1 ?v2 ?v3 ?v4) (ite (= ?v2 ?v0) (insert$ ?v4 (knows$ ?v0 ?v1)) (knows$ ?v0 ?v1))) :pattern ((uur$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a17)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (uug$ ?v0 ?v1) false) :pattern ((uug$ ?v0 ?v1)))) :named a18)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (uuh$ ?v0 ?v1) true) :pattern ((uuh$ ?v0 ?v1)))) :named a19)) -(assert (! (not (less_eq$ (knows$ spy$ (takeWhile$ p$ nil$)) (knows$ spy$ nil$))) :named a20)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (takeWhile$ ?v0 (takeWhile$ ?v0 ?v1)) (takeWhile$ ?v0 ?v1))) :named a21)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (=> (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))) (less_eq$a ?v0 ?v1))) :named a22)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (=> (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))) (less_eq$b ?v0 ?v1))) :named a23)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))) (less_eq$ ?v0 ?v1))) :named a24)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a25)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a26)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (takeWhile$ ?v0 nil$) nil$) :pattern ((takeWhile$ ?v0)))) :named a27)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool)) (?v2 (-> Msg$ Bool))) (= (less_eq$ ?v0 (collect$ (uu$ ?v1 ?v2))) (and (less_eq$ ?v0 (collect$ ?v1)) (less_eq$ ?v0 (collect$ ?v2))))) :named a28)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$) (?v3 (-> Event$ Bool))) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 (collect$a (uua$ ?v2 ?v3)))) (?v3 ?v0))) :named a29)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$) (?v3 (-> Agent$ Bool))) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 (collect$b (uub$ ?v2 ?v3)))) (?v3 ?v0))) :named a30)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$) (?v3 (-> Msg$ Bool))) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 (collect$ (uuc$ ?v2 ?v3)))) (?v3 ?v0))) :named a31)) -(assert (! (forall ((?v0 Event_set$) (?v1 (-> Event$ Bool))) (less_eq$a (collect$a (uua$ ?v0 ?v1)) ?v0)) :named a32)) -(assert (! (forall ((?v0 Agent_set$) (?v1 (-> Agent$ Bool))) (less_eq$b (collect$b (uub$ ?v0 ?v1)) ?v0)) :named a33)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg$ Bool))) (less_eq$ (collect$ (uuc$ ?v0 ?v1)) ?v0)) :named a34)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (less_eq$a ?v0 ?v1) (forall ((?v4 Event$)) (=> (and (member$b ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$a (collect$a (uua$ ?v0 ?v2)) (collect$a (uua$ ?v1 ?v3))))) :named a35)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (less_eq$b ?v0 ?v1) (forall ((?v4 Agent$)) (=> (and (member$ ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$b (collect$b (uub$ ?v0 ?v2)) (collect$b (uub$ ?v1 ?v3))))) :named a36)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (less_eq$ ?v0 ?v1) (forall ((?v4 Msg$)) (=> (and (member$a ?v4 ?v0) (?v2 ?v4)) (?v3 ?v4)))) (less_eq$ (collect$ (uuc$ ?v0 ?v2)) (collect$ (uuc$ ?v1 ?v3))))) :named a37)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 (-> Event$ Bool))) (=> (less_eq$a ?v0 ?v1) (= (less_eq$a ?v0 (collect$a (uua$ ?v1 ?v2))) (forall ((?v3 Event$)) (=> (member$b ?v3 ?v0) (?v2 ?v3)))))) :named a38)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 (-> Agent$ Bool))) (=> (less_eq$b ?v0 ?v1) (= (less_eq$b ?v0 (collect$b (uub$ ?v1 ?v2))) (forall ((?v3 Agent$)) (=> (member$ ?v3 ?v0) (?v2 ?v3)))))) :named a39)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg$ Bool))) (=> (less_eq$ ?v0 ?v1) (= (less_eq$ ?v0 (collect$ (uuc$ ?v1 ?v2))) (forall ((?v3 Msg$)) (=> (member$a ?v3 ?v0) (?v2 ?v3)))))) :named a40)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (=> (not (= ?v0 nil$)) false)) false)) :named a41)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a42)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a43)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a44)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (less_eq$c (uud$ ?v0) (uud$ ?v1)))) :named a45)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (less_eq$d (uue$ ?v0) (uue$ ?v1)))) :named a46)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (less_eq$e (uuf$ ?v0) (uuf$ ?v1)))) :named a47)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v1 ?v0))) :named a48)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v2 ?v0)) (less_eq$ ?v2 ?v1))) :named a49)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a50)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a51)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a52)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (= ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a53)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (= ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a54)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (! (=> (less_eq$ ?v0 ?v1) (= (less_eq$ ?v1 ?v0) (= ?v1 ?v0))) :pattern ((less_eq$ ?v1 ?v0)))) :named a55)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a56)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v0 ?v1))) :named a57)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) (= ?v0 ?v1))) :named a58)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (= ?v0 ?v1) (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)))) :named a59)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg_set$ Msg_set$)) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (and (= (?v2 ?v1) ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v2 ?v4) (?v2 ?v5)))))) (less_eq$ (?v2 ?v0) ?v3))) :named a60)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg_set$ Msg_set$)) (?v2 Msg_set$) (?v3 Msg_set$)) (=> (and (= ?v0 (?v1 ?v2)) (and (less_eq$ ?v2 ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v1 ?v4) (?v1 ?v5)))))) (less_eq$ ?v0 (?v1 ?v3)))) :named a61)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 (-> Msg_set$ Msg_set$)) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (and (less_eq$ (?v2 ?v1) ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v2 ?v4) (?v2 ?v5)))))) (less_eq$ (?v2 ?v0) ?v3))) :named a62)) -(assert (! (forall ((?v0 Msg_set$) (?v1 (-> Msg_set$ Msg_set$)) (?v2 Msg_set$) (?v3 Msg_set$)) (=> (and (less_eq$ ?v0 (?v1 ?v2)) (and (less_eq$ ?v2 ?v3) (forall ((?v4 Msg_set$) (?v5 Msg_set$)) (=> (less_eq$ ?v4 ?v5) (less_eq$ (?v1 ?v4) (?v1 ?v5)))))) (less_eq$ ?v0 (?v1 ?v3)))) :named a63)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool))) (= (less_eq$ (collect$ ?v0) (collect$ ?v1)) (forall ((?v2 Msg$)) (=> (?v0 ?v2) (?v1 ?v2))))) :named a64)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (not (member$b ?v2 ?v1))) (not (member$b ?v2 ?v0)))) :named a65)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (not (member$ ?v2 ?v1))) (not (member$ ?v2 ?v0)))) :named a66)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (not (member$a ?v2 ?v1))) (not (member$a ?v2 ?v0)))) :named a67)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (= ?v0 ?v1) (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)))) :named a68)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v2)) (less_eq$ ?v0 ?v2))) :named a69)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 (-> Msg$ Bool))) (=> (forall ((?v2 Msg$)) (=> (?v0 ?v2) (?v1 ?v2))) (less_eq$ (collect$ ?v0) (collect$ ?v1)))) :named a70)) -(assert (! (forall ((?v0 Msg_set$)) (less_eq$ ?v0 ?v0)) :named a71)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 ?v2)) (member$b ?v0 ?v2))) :named a72)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 ?v2)) (member$ ?v0 ?v2))) :named a73)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 ?v2)) (member$a ?v0 ?v2))) :named a74)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))))) :named a75)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))))) :named a76)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))))) :named a77)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool))) (= (member$a ?v0 (collect$ ?v1)) (?v1 ?v0))) :named a78)) -(assert (! (forall ((?v0 Event$) (?v1 (-> Event$ Bool))) (= (member$b ?v0 (collect$a ?v1)) (?v1 ?v0))) :named a79)) -(assert (! (forall ((?v0 Agent$) (?v1 (-> Agent$ Bool))) (= (member$ ?v0 (collect$b ?v1)) (?v1 ?v0))) :named a80)) -(assert (! (forall ((?v0 Msg_set$)) (= (collect$ (uuf$ ?v0)) ?v0)) :named a81)) -(assert (! (forall ((?v0 Event_set$)) (= (collect$a (uud$ ?v0)) ?v0)) :named a82)) -(assert (! (forall ((?v0 Agent_set$)) (= (collect$b (uue$ ?v0)) ?v0)) :named a83)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v1 ?v2)) (member$b ?v0 ?v2))) :named a84)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v1 ?v2)) (member$ ?v0 ?v2))) :named a85)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v1 ?v2)) (member$a ?v0 ?v2))) :named a86)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v1 ?v0))) :named a87)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (= ?v0 ?v1) (less_eq$ ?v0 ?v1))) :named a88)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$a ?v0 ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 ?v0) (member$b ?v2 ?v1))))) :named a89)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$b ?v0 ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 ?v0) (member$ ?v2 ?v1))))) :named a90)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$ ?v0 ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 ?v0) (member$a ?v2 ?v1))))) :named a91)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (=> (and (= ?v0 ?v1) (=> (and (less_eq$ ?v0 ?v1) (less_eq$ ?v1 ?v0)) false)) false)) :named a92)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (and (=> (not (member$b ?v2 ?v0)) false) (=> (member$b ?v2 ?v1) false))) false)) :named a93)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (and (=> (not (member$ ?v2 ?v0)) false) (=> (member$ ?v2 ?v1) false))) false)) :named a94)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (and (=> (not (member$a ?v2 ?v0)) false) (=> (member$a ?v2 ?v1) false))) false)) :named a95)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a96)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a97)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a98)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$) (?v2 Event$)) (=> (and (less_eq$a ?v0 ?v1) (member$b ?v2 ?v0)) (member$b ?v2 ?v1))) :named a99)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$) (?v2 Agent$)) (=> (and (less_eq$b ?v0 ?v1) (member$ ?v2 ?v0)) (member$ ?v2 ?v1))) :named a100)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (and (less_eq$ ?v0 ?v1) (member$a ?v2 ?v0)) (member$a ?v2 ?v1))) :named a101)) -(assert (! (forall ((?v0 Event_set$) (?v1 Event_set$)) (= (less_eq$c (uud$ ?v0) (uud$ ?v1)) (less_eq$a ?v0 ?v1))) :named a102)) -(assert (! (forall ((?v0 Agent_set$) (?v1 Agent_set$)) (= (less_eq$d (uue$ ?v0) (uue$ ?v1)) (less_eq$b ?v0 ?v1))) :named a103)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$)) (= (less_eq$e (uuf$ ?v0) (uuf$ ?v1)) (less_eq$ ?v0 ?v1))) :named a104)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_ex1$ ?v0 nil$) false) :pattern ((list_ex1$ ?v0)))) :named a105)) -(assert (! (forall ((?v0 (-> Event$ Event_list$))) (! (= (bind$ nil$ ?v0) nil$) :pattern ((bind$ nil$ ?v0)))) :named a106)) -(assert (! (forall ((?v0 (-> Msg_set$ Bool)) (?v1 Msg_set$)) (=> (and (?v0 ?v1) (forall ((?v2 Msg_set$)) (=> (?v0 ?v2) (less_eq$ ?v2 ?v1)))) (= (greatest$ ?v0) ?v1))) :named a107)) -(assert (! (forall ((?v0 (-> Msg_set$ Bool)) (?v1 Msg_set$) (?v2 (-> Msg_set$ Bool))) (=> (and (?v0 ?v1) (and (forall ((?v3 Msg_set$)) (=> (?v0 ?v3) (less_eq$ ?v3 ?v1))) (forall ((?v3 Msg_set$)) (=> (and (?v0 ?v3) (forall ((?v4 Msg_set$)) (=> (?v0 ?v4) (less_eq$ ?v4 ?v3)))) (?v2 ?v3))))) (?v2 (greatest$ ?v0)))) :named a108)) -(assert (! (forall ((?v0 Event$)) (! (= (member$d nil$ ?v0) false) :pattern ((member$d nil$ ?v0)))) :named a109)) -(assert (! (forall ((?v0 (-> Bool Msg_set$)) (?v1 (-> Bool Msg_set$))) (! (= (less_eq$f ?v0 ?v1) (and (less_eq$ (?v0 false) (?v1 false)) (less_eq$ (?v0 true) (?v1 true)))) :pattern ((less_eq$f ?v0 ?v1)))) :named a110)) -(assert (! (forall ((?v0 Nat$)) (! (= (gen_length$ ?v0 nil$) ?v0) :pattern ((gen_length$ ?v0)))) :named a111)) -(assert (! (forall ((?v0 (-> Event$ Event_list$))) (! (= (maps$ ?v0 nil$) nil$) :pattern ((maps$ ?v0)))) :named a112)) -(assert (! (forall ((?v0 Event_list$)) (= (= ?v0 nil$) (null$ ?v0))) :named a113)) -(assert (! (= (null$ nil$) true) :named a114)) -(assert (! (forall ((?v0 Event_list$)) (! (= (splice$ ?v0 nil$) ?v0) :pattern ((splice$ ?v0)))) :named a115)) -(assert (! (forall ((?v0 Event_list$)) (= (= (rotate1$ ?v0) nil$) (= ?v0 nil$))) :named a116)) -(assert (! (forall ((?v0 (-> Event$ Event_option$))) (! (= (map_filter$ ?v0 nil$) nil$) :pattern ((map_filter$ ?v0)))) :named a117)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$)) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (antimono$ ?v0) (less_eq$ ?v1 ?v2)) (less_eq$ (?v0 ?v2) (?v0 ?v1)))) :named a118)) -(assert (! (= (rotate1$ nil$) nil$) :named a119)) -(assert (! (forall ((?v0 Event_list$)) (! (= (splice$ nil$ ?v0) ?v0) :pattern ((splice$ nil$ ?v0)))) :named a120)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$))) (= (antimono$ ?v0) (forall ((?v1 Msg_set$) (?v2 Msg_set$)) (=> (less_eq$ ?v1 ?v2) (less_eq$ (?v0 ?v2) (?v0 ?v1)))))) :named a121)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$))) (=> (forall ((?v1 Msg_set$) (?v2 Msg_set$)) (=> (less_eq$ ?v1 ?v2) (less_eq$ (?v0 ?v2) (?v0 ?v1)))) (antimono$ ?v0))) :named a122)) -(assert (! (forall ((?v0 (-> Msg_set$ Msg_set$)) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (antimono$ ?v0) (and (less_eq$ ?v1 ?v2) (=> (less_eq$ (?v0 ?v2) (?v0 ?v1)) false))) false)) :named a123)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (=> (and (= (splice$ ?v0 ?v1) ?v2) (and (forall ((?v3 Event_list$)) (=> (and (= ?v0 nil$) (and (= ?v1 ?v3) (= ?v2 ?v3))) false)) (and (forall ((?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (cons$ ?v3 ?v4)) (and (= ?v1 nil$) (= ?v2 (cons$ ?v3 ?v4)))) false)) (forall ((?v3 Event$) (?v4 Event_list$) (?v5 Event$) (?v6 Event_list$)) (=> (and (= ?v0 (cons$ ?v3 ?v4)) (and (= ?v1 (cons$ ?v5 ?v6)) (= ?v2 (cons$ ?v3 (cons$ ?v5 (splice$ ?v4 ?v6)))))) false))))) false)) :named a124)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (splice$ (cons$ ?v0 ?v1) nil$) (cons$ ?v0 ?v1)) :pattern ((cons$ ?v0 ?v1)))) :named a125)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_ex$ ?v0 nil$) false) :pattern ((list_ex$ ?v0)))) :named a126)) -(assert (! (forall ((?v0 Event_list$)) (= (= ?v0 nil$) (case_list$ true uug$ ?v0))) :named a127)) -(assert (! (forall ((?v0 Event_list$)) (= (not (= ?v0 nil$)) (case_list$ false uuh$ ?v0))) :named a128)) -(assert (! (forall ((?v0 Agent$)) (! (= (knows$ ?v0 nil$) (initState$ ?v0)) :pattern ((knows$ ?v0)))) :named a129)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (= (= (cons$ ?v0 ?v1) (cons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a130)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_ex$ ?v0 (cons$ ?v1 ?v2)) (or (?v0 ?v1) (list_ex$ ?v0 ?v2))) :pattern ((list_ex$ ?v0 (cons$ ?v1 ?v2))))) :named a131)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (not (= (cons$ ?v0 ?v1) ?v1))) :named a132)) -(assert (! (forall ((?v0 Event_list_list$)) (=> (and (=> (= ?v0 nil$a) false) (and (forall ((?v1 Event_list_list$)) (=> (= ?v0 (cons$a nil$ ?v1)) false)) (forall ((?v1 Event$) (?v2 Event_list$) (?v3 Event_list_list$)) (=> (= ?v0 (cons$a (cons$ ?v1 ?v2) ?v3)) false)))) false)) :named a133)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (not (= nil$ (cons$ ?v0 ?v1)))) :named a134)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list$)) (=> (= ?v0 (cons$ ?v1 ?v2)) (not (= ?v0 nil$)))) :named a135)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (forall ((?v1 Event$) (?v2 Event_list$)) (=> (= ?v0 (cons$ ?v1 ?v2)) false))) false)) :named a136)) -(assert (! (forall ((?v0 Event_list$)) (= (not (= ?v0 nil$)) (exists ((?v1 Event$) (?v2 Event_list$)) (= ?v0 (cons$ ?v1 ?v2))))) :named a137)) -(assert (! (forall ((?v0 (-> Event_list$ (-> Event_list$ Bool))) (?v1 Event_list$) (?v2 Event_list$)) (=> (and (?v0 nil$ nil$) (and (forall ((?v3 Event$) (?v4 Event_list$)) (?v0 (cons$ ?v3 ?v4) nil$)) (and (forall ((?v3 Event$) (?v4 Event_list$)) (?v0 nil$ (cons$ ?v3 ?v4))) (forall ((?v3 Event$) (?v4 Event_list$) (?v5 Event$) (?v6 Event_list$)) (=> (?v0 ?v4 ?v6) (?v0 (cons$ ?v3 ?v4) (cons$ ?v5 ?v6))))))) (?v0 ?v1 ?v2))) :named a138)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (and (forall ((?v1 Event$)) (=> (= ?v0 (cons$ ?v1 nil$)) false)) (forall ((?v1 Event$) (?v2 Event$) (?v3 Event_list$)) (=> (= ?v0 (cons$ ?v1 (cons$ ?v2 ?v3))) false)))) false)) :named a139)) -(assert (! (forall ((?v0 (-> Event_list$ Bool)) (?v1 Event_list$)) (=> (and (?v0 nil$) (and (forall ((?v2 Event$)) (?v0 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event$) (?v4 Event_list$)) (=> (?v0 (cons$ ?v3 ?v4)) (?v0 (cons$ ?v2 (cons$ ?v3 ?v4))))))) (?v0 ?v1))) :named a140)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event_list$ Bool))) (=> (and (not (= ?v0 nil$)) (and (forall ((?v2 Event$)) (?v1 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (not (= ?v3 nil$)) (?v1 ?v3)) (?v1 (cons$ ?v2 ?v3)))))) (?v1 ?v0))) :named a141)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (! (= (splice$ (cons$ ?v0 ?v1) (cons$ ?v2 ?v3)) (cons$ ?v0 (cons$ ?v2 (splice$ ?v1 ?v3)))) :pattern ((splice$ (cons$ ?v0 ?v1) (cons$ ?v2 ?v3))))) :named a142)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Event$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ ?v2 ?v1)))) :named a143)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (null$ (cons$ ?v0 ?v1)) false) :pattern ((cons$ ?v0 ?v1)))) :named a144)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$)) (! (= (member$d (cons$ ?v0 ?v1) ?v2) (or (= ?v0 ?v2) (member$d ?v1 ?v2))) :pattern ((member$d (cons$ ?v0 ?v1) ?v2)))) :named a145)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$)) (less_eq$ (initState$ ?v0) (knows$ ?v0 ?v1))) :named a146)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (takeWhile$ ?v0 (cons$ ?v1 ?v2)) (ite (?v0 ?v1) (cons$ ?v1 (takeWhile$ ?v0 ?v2)) nil$)) :pattern ((takeWhile$ ?v0 (cons$ ?v1 ?v2))))) :named a147)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (gets$ ?v1 ?v2) ?v0)))) :named a148)) -(assert (! (forall ((?v0 Event$)) (! (= (insert$a ?v0 nil$) (cons$ ?v0 nil$)) :pattern ((insert$a ?v0)))) :named a149)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (! (= (knows$ spy$ (cons$ (gets$ ?v0 ?v1) ?v2)) (knows$ spy$ ?v2)) :pattern ((cons$ (gets$ ?v0 ?v1) ?v2)))) :named a150)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (notes$ ?v1 ?v2) ?v0)))) :named a151)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (= (list_ex1$ ?v0 (cons$ ?v1 ?v2)) (ite (?v0 ?v1) (list_all$ (uui$ ?v0 ?v1) ?v2) (list_ex1$ ?v0 ?v2)))) :named a152)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (= (= (notes$ ?v0 ?v1) (notes$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a153)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (= (= (gets$ ?v0 ?v1) (gets$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a154)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_all$ ?v0 (cons$ ?v1 ?v2)) (and (?v0 ?v1) (list_all$ ?v0 ?v2))) :pattern ((list_all$ ?v0 (cons$ ?v1 ?v2))))) :named a155)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$)) (! (= (list_all$ ?v0 (cons$ ?v1 ?v2)) (and (?v0 ?v1) (list_all$ ?v0 ?v2))) :pattern ((list_all$ ?v0 (cons$ ?v1 ?v2))))) :named a156)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (! (= (list_all$ ?v0 nil$) true) :pattern ((list_all$ ?v0)))) :named a157)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Agent$) (?v3 Msg$)) (not (= (gets$ ?v0 ?v1) (notes$ ?v2 ?v3)))) :named a158)) -(assert (! (forall ((?v0 (-> Event$ Bool))) (list_all$ ?v0 nil$)) :named a159)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (notes$ ?v2 ?v3) ?v1)))) :named a160)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (gets$ ?v2 ?v3) ?v1)))) :named a161)) -(assert (! (= (product_lists$ nil$a) (cons$a nil$ nil$a)) :named a162)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (gets$ ?v1 ?v2) nil$))) (knows$ spy$ ?v0))) :named a163)) -(assert (! (= (subseqs$ nil$) (cons$a nil$ nil$a)) :named a164)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (less_eq$ (knows$ spy$ ?v0) (knows$ spy$ (cons$ (says$ ?v1 ?v2 ?v3) ?v0)))) :named a165)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (append$ (append$ ?v0 ?v1) ?v2) (append$ ?v0 (append$ ?v1 ?v2)))) :named a166)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (append$ (append$ ?v0 ?v1) ?v2) (append$ ?v0 (append$ ?v1 ?v2)))) :named a167)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v2 ?v1)) (= ?v0 ?v2))) :named a168)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v0 ?v2)) (= ?v1 ?v2))) :named a169)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Agent$) (?v5 Msg$)) (= (= (says$ ?v0 ?v1 ?v2) (says$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a170)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ ?v0 nil$) ?v0) :pattern ((append$ ?v0)))) :named a171)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) ?v0) (= ?v1 nil$))) :named a172)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= ?v0 (append$ ?v0 ?v1)) (= ?v1 nil$))) :named a173)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) ?v1) (= ?v0 nil$))) :named a174)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= ?v0 (append$ ?v1 ?v0)) (= ?v1 nil$))) :named a175)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= nil$ (append$ ?v0 ?v1)) (and (= ?v0 nil$) (= ?v1 nil$)))) :named a176)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (= (= (append$ ?v0 ?v1) nil$) (and (= ?v0 nil$) (= ?v1 nil$)))) :named a177)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ ?v0 nil$) ?v0) :pattern ((append$ ?v0)))) :named a178)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 Event_list$)) (= (list_all$ ?v0 (append$ ?v1 ?v2)) (and (list_all$ ?v0 ?v1) (list_all$ ?v0 ?v2)))) :named a179)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 Event_list$)) (= (list_ex$ ?v0 (append$ ?v1 ?v2)) (or (list_ex$ ?v0 ?v1) (list_ex$ ?v0 ?v2)))) :named a180)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list$) (?v3 Event$)) (= (= (append$ ?v0 (cons$ ?v1 nil$)) (append$ ?v2 (cons$ ?v3 nil$))) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a181)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 (-> Event$ Event_list$))) (! (= (bind$ (cons$ ?v0 ?v1) ?v2) (append$ (?v2 ?v0) (bind$ ?v1 ?v2))) :pattern ((bind$ (cons$ ?v0 ?v1) ?v2)))) :named a182)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$)) (! (= (append$ (cons$ ?v0 ?v1) ?v2) (cons$ ?v0 (append$ ?v1 ?v2))) :pattern ((append$ (cons$ ?v0 ?v1) ?v2)))) :named a183)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (= (cons$ ?v0 ?v1) ?v2) (= ?v3 (append$ ?v1 ?v4))) (= (cons$ ?v0 ?v3) (append$ ?v2 ?v4)))) :named a184)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ nil$ ?v0) ?v0) :pattern ((append$ nil$ ?v0)))) :named a185)) -(assert (! (forall ((?v0 Event_list$)) (! (= (append$ nil$ ?v0) ?v0) :pattern ((append$ nil$ ?v0)))) :named a186)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$)) (=> (= ?v0 ?v1) (= ?v0 (append$ nil$ ?v1)))) :named a187)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (= (append$ ?v0 ?v1) ?v2) (= ?v3 (append$ ?v1 ?v4))) (= (append$ ?v0 ?v3) (append$ ?v2 ?v4)))) :named a188)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$)) (= (= (append$ ?v0 ?v1) (append$ ?v2 ?v3)) (exists ((?v4 Event_list$)) (or (and (= ?v0 (append$ ?v2 ?v4)) (= (append$ ?v4 ?v1) ?v3)) (and (= (append$ ?v0 ?v4) ?v2) (= ?v1 (append$ ?v4 ?v3))))))) :named a189)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Msg$)) (not (= (says$ ?v0 ?v1 ?v2) (notes$ ?v3 ?v4)))) :named a190)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Agent$) (?v4 Msg$)) (not (= (says$ ?v0 ?v1 ?v2) (gets$ ?v3 ?v4)))) :named a191)) -(assert (! (forall ((?v0 (-> Event_list$ Bool)) (?v1 Event_list$)) (=> (and (?v0 nil$) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (?v0 ?v3) (?v0 (append$ ?v3 (cons$ ?v2 nil$)))))) (?v0 ?v1))) :named a192)) -(assert (! (forall ((?v0 Event_list$)) (=> (and (=> (= ?v0 nil$) false) (forall ((?v1 Event_list$) (?v2 Event$)) (=> (= ?v0 (append$ ?v1 (cons$ ?v2 nil$))) false))) false)) :named a193)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$)) (= (= (cons$ ?v0 ?v1) (append$ ?v2 ?v3)) (or (and (= ?v2 nil$) (= (cons$ ?v0 ?v1) ?v3)) (exists ((?v4 Event_list$)) (and (= (cons$ ?v0 ?v4) ?v2) (= ?v1 (append$ ?v4 ?v3))))))) :named a194)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 Event$) (?v3 Event_list$)) (= (= (append$ ?v0 ?v1) (cons$ ?v2 ?v3)) (or (and (= ?v0 nil$) (= ?v1 (cons$ ?v2 ?v3))) (exists ((?v4 Event_list$)) (and (= ?v0 (cons$ ?v2 ?v4)) (= (append$ ?v4 ?v1) ?v3)))))) :named a195)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event_list$ Bool))) (=> (and (not (= ?v0 nil$)) (and (forall ((?v2 Event$)) (?v1 (cons$ ?v2 nil$))) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (not (= ?v3 nil$)) (?v1 ?v3)) (?v1 (append$ ?v3 (cons$ ?v2 nil$))))))) (?v1 ?v0))) :named a196)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event$) (?v2 Event_list$) (?v3 Event_list$)) (=> (not (?v0 ?v1)) (= (takeWhile$ ?v0 (append$ ?v2 (cons$ ?v1 ?v3))) (takeWhile$ ?v0 ?v2)))) :named a197)) -(assert (! (forall ((?v0 Event$)) (=> (and (forall ((?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (=> (= ?v0 (says$ ?v1 ?v2 ?v3)) false)) (and (forall ((?v1 Agent$) (?v2 Msg$)) (=> (= ?v0 (gets$ ?v1 ?v2)) false)) (forall ((?v1 Agent$) (?v2 Msg$)) (=> (= ?v0 (notes$ ?v1 ?v2)) false)))) false)) :named a198)) -(assert (! (forall ((?v0 (-> Event$ Event_list$)) (?v1 Event$) (?v2 Event_list$)) (! (= (maps$ ?v0 (cons$ ?v1 ?v2)) (append$ (?v0 ?v1) (maps$ ?v0 ?v2))) :pattern ((maps$ ?v0 (cons$ ?v1 ?v2))))) :named a199)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (rotate1$ (cons$ ?v0 ?v1)) (append$ ?v1 (cons$ ?v0 nil$)))) :named a200)) -(assert (! (forall ((?v0 Agent$) (?v1 Event_list$) (?v2 Agent$) (?v3 Agent$) (?v4 Msg$)) (less_eq$ (knows$ ?v0 ?v1) (knows$ ?v0 (cons$ (says$ ?v2 ?v3 ?v4) ?v1)))) :named a201)) -(assert (! (forall ((?v0 Event_list_set$) (?v1 Event_list$)) (= (succ$ ?v0 ?v1) (collect$a (uuj$ ?v0 ?v1)))) :named a202)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Agent$) (?v3 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (says$ ?v1 ?v2 ?v3) nil$))) (insert$ ?v3 (knows$ spy$ ?v0)))) :named a203)) -(assert (! (forall ((?v0 Msg$) (?v1 Agent$) (?v2 Event_list$)) (=> (and (member$a ?v0 (knows$ ?v1 ?v2)) (not (= ?v1 spy$))) (exists ((?v3 Agent$)) (or (member$b (says$ ?v1 ?v3 ?v0) (set$ ?v2)) (or (member$b (gets$ ?v1 ?v0) (set$ ?v2)) (or (member$b (notes$ ?v1 ?v0) (set$ ?v2)) (member$a ?v0 (initState$ ?v1)))))))) :named a204)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list_set$) (?v2 Msg_list$)) (=> (member$a ?v0 (succ$a ?v1 ?v2)) (member$e (append$a ?v2 (cons$b ?v0 nil$b)) ?v1))) :named a205)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list_set$) (?v2 Agent_list$)) (=> (member$ ?v0 (succ$b ?v1 ?v2)) (member$f (append$b ?v2 (cons$c ?v0 nil$c)) ?v1))) :named a206)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list_set$) (?v2 Event_list$)) (=> (member$b ?v0 (succ$ ?v1 ?v2)) (member$c (append$ ?v2 (cons$ ?v0 nil$)) ?v1))) :named a207)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (= (insert$ ?v0 (insert$ ?v0 ?v1)) (insert$ ?v0 ?v1))) :named a208)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (= (member$a ?v0 (insert$ ?v1 ?v2)) (or (= ?v0 ?v1) (member$a ?v0 ?v2)))) :named a209)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_set$)) (= (member$b ?v0 (insert$b ?v1 ?v2)) (or (= ?v0 ?v1) (member$b ?v0 ?v2)))) :named a210)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_set$)) (= (member$ ?v0 (insert$c ?v1 ?v2)) (or (= ?v0 ?v1) (member$ ?v0 ?v2)))) :named a211)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (=> (=> (not (member$a ?v0 ?v1)) (= ?v0 ?v2)) (member$a ?v0 (insert$ ?v2 ?v1)))) :named a212)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (=> (=> (not (member$b ?v0 ?v1)) (= ?v0 ?v2)) (member$b ?v0 (insert$b ?v2 ?v1)))) :named a213)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (=> (=> (not (member$ ?v0 ?v1)) (= ?v0 ?v2)) (member$ ?v0 (insert$c ?v2 ?v1)))) :named a214)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (= (less_eq$a (insert$b ?v0 ?v1) ?v2) (and (member$b ?v0 ?v2) (less_eq$a ?v1 ?v2)))) :named a215)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (= (less_eq$b (insert$c ?v0 ?v1) ?v2) (and (member$ ?v0 ?v2) (less_eq$b ?v1 ?v2)))) :named a216)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (= (less_eq$ (insert$ ?v0 ?v1) ?v2) (and (member$a ?v0 ?v2) (less_eq$ ?v1 ?v2)))) :named a217)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$)) (= (= (takeWhile$a ?v0 ?v1) ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 (set$a ?v1)) (?v0 ?v2))))) :named a218)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$)) (= (= (takeWhile$b ?v0 ?v1) ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 (set$b ?v1)) (?v0 ?v2))))) :named a219)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (= (takeWhile$ ?v0 ?v1) ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 (set$ ?v1)) (?v0 ?v2))))) :named a220)) -(assert (! (forall ((?v0 Event_list$)) (= (set$ (rotate1$ ?v0)) (set$ ?v0))) :named a221)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (=> (member$a ?v0 (set$a ?v1)) (= (insert$d ?v0 ?v1) ?v1)) :pattern ((insert$d ?v0 ?v1)))) :named a222)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (=> (member$ ?v0 (set$b ?v1)) (= (insert$e ?v0 ?v1) ?v1)) :pattern ((insert$e ?v0 ?v1)))) :named a223)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (=> (member$b ?v0 (set$ ?v1)) (= (insert$a ?v0 ?v1) ?v1)) :pattern ((insert$a ?v0 ?v1)))) :named a224)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (= (set$a (cons$b ?v0 ?v1)) (insert$ ?v0 (set$a ?v1))) :pattern ((cons$b ?v0 ?v1)))) :named a225)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (set$ (cons$ ?v0 ?v1)) (insert$b ?v0 (set$ ?v1))) :pattern ((cons$ ?v0 ?v1)))) :named a226)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool)) (?v2 Msg_list$)) (=> (forall ((?v3 Msg$)) (=> (member$a ?v3 (set$a ?v0)) (?v1 ?v3))) (= (takeWhile$a ?v1 (append$a ?v0 ?v2)) (append$a ?v0 (takeWhile$a ?v1 ?v2))))) :named a227)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool)) (?v2 Agent_list$)) (=> (forall ((?v3 Agent$)) (=> (member$ ?v3 (set$b ?v0)) (?v1 ?v3))) (= (takeWhile$b ?v1 (append$b ?v0 ?v2)) (append$b ?v0 (takeWhile$b ?v1 ?v2))))) :named a228)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool)) (?v2 Event_list$)) (=> (forall ((?v3 Event$)) (=> (member$b ?v3 (set$ ?v0)) (?v1 ?v3))) (= (takeWhile$ ?v1 (append$ ?v0 ?v2)) (append$ ?v0 (takeWhile$ ?v1 ?v2))))) :named a229)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 Msg_list$)) (=> (and (member$a ?v0 (set$a ?v1)) (not (?v2 ?v0))) (= (takeWhile$a ?v2 (append$a ?v1 ?v3)) (takeWhile$a ?v2 ?v1)))) :named a230)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 Agent_list$)) (=> (and (member$ ?v0 (set$b ?v1)) (not (?v2 ?v0))) (= (takeWhile$b ?v2 (append$b ?v1 ?v3)) (takeWhile$b ?v2 ?v1)))) :named a231)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 Event_list$)) (=> (and (member$b ?v0 (set$ ?v1)) (not (?v2 ?v0))) (= (takeWhile$ ?v2 (append$ ?v1 ?v3)) (takeWhile$ ?v2 ?v1)))) :named a232)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (set$a (insert$d ?v0 ?v1)) (insert$ ?v0 (set$a ?v1)))) :named a233)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (set$ (insert$a ?v0 ?v1)) (insert$b ?v0 (set$ ?v1)))) :named a234)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (=> (not (member$a ?v0 (set$a ?v1))) (= (insert$d ?v0 ?v1) (cons$b ?v0 ?v1))) :pattern ((insert$d ?v0 ?v1)))) :named a235)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (=> (not (member$ ?v0 (set$b ?v1))) (= (insert$e ?v0 ?v1) (cons$c ?v0 ?v1))) :pattern ((insert$e ?v0 ?v1)))) :named a236)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (=> (not (member$b ?v0 (set$ ?v1))) (= (insert$a ?v0 ?v1) (cons$ ?v0 ?v1))) :pattern ((insert$a ?v0 ?v1)))) :named a237)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (! (= (knows$ spy$ (cons$ (says$ ?v0 ?v1 ?v2) ?v3)) (insert$ ?v2 (knows$ spy$ ?v3))) :pattern ((cons$ (says$ ?v0 ?v1 ?v2) ?v3)))) :named a238)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_set$)) (= (less_eq$b (set$b ?v0) ?v1) (forall ((?v2 Agent$)) (=> (member$ ?v2 (set$b ?v0)) (member$ ?v2 ?v1))))) :named a239)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_set$)) (= (less_eq$a (set$ ?v0) ?v1) (forall ((?v2 Event$)) (=> (member$b ?v2 (set$ ?v0)) (member$b ?v2 ?v1))))) :named a240)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_set$)) (= (less_eq$ (set$a ?v0) ?v1) (forall ((?v2 Msg$)) (=> (member$a ?v2 (set$a ?v0)) (member$a ?v2 ?v1))))) :named a241)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (member$b ?v0 ?v1) (less_eq$a ?v2 ?v1)) (less_eq$a (insert$b ?v0 ?v2) ?v1))) :named a242)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (member$ ?v0 ?v1) (less_eq$b ?v2 ?v1)) (less_eq$b (insert$c ?v0 ?v2) ?v1))) :named a243)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (member$a ?v0 ?v1) (less_eq$ ?v2 ?v1)) (less_eq$ (insert$ ?v0 ?v2) ?v1))) :named a244)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (less_eq$ ?v0 ?v1) (less_eq$ ?v0 (insert$ ?v2 ?v1)))) :named a245)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg$)) (less_eq$ ?v0 (insert$ ?v1 ?v0))) :named a246)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (not (member$b ?v0 ?v1)) (= (less_eq$a ?v1 (insert$b ?v0 ?v2)) (less_eq$a ?v1 ?v2)))) :named a247)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (not (member$ ?v0 ?v1)) (= (less_eq$b ?v1 (insert$c ?v0 ?v2)) (less_eq$b ?v1 ?v2)))) :named a248)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (not (member$a ?v0 ?v1)) (= (less_eq$ ?v1 (insert$ ?v0 ?v2)) (less_eq$ ?v1 ?v2)))) :named a249)) -(assert (! (forall ((?v0 Msg_set$) (?v1 Msg_set$) (?v2 Msg$)) (=> (less_eq$ ?v0 ?v1) (less_eq$ (insert$ ?v2 ?v0) (insert$ ?v2 ?v1)))) :named a250)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$a ?v2 ?v0) (list_ex$a ?v3 ?v1)))) :named a251)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$b ?v2 ?v0) (list_ex$b ?v3 ?v1)))) :named a252)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_ex$ ?v2 ?v0) (list_ex$ ?v3 ?v1)))) :named a253)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool))) (= (insert$ ?v0 (collect$ ?v1)) (collect$ (uuk$ ?v0 ?v1)))) :named a254)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (= (insert$ ?v0 ?v1) (collect$ (uul$ ?v0 ?v1)))) :named a255)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (= (insert$b ?v0 ?v1) (collect$a (uum$ ?v0 ?v1)))) :named a256)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (= (insert$c ?v0 ?v1) (collect$b (uun$ ?v0 ?v1)))) :named a257)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (=> (member$a ?v0 ?v1) (exists ((?v2 Msg_set$)) (and (= ?v1 (insert$ ?v0 ?v2)) (not (member$a ?v0 ?v2)))))) :named a258)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (=> (member$b ?v0 ?v1) (exists ((?v2 Event_set$)) (and (= ?v1 (insert$b ?v0 ?v2)) (not (member$b ?v0 ?v2)))))) :named a259)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (=> (member$ ?v0 ?v1) (exists ((?v2 Agent_set$)) (and (= ?v1 (insert$c ?v0 ?v2)) (not (member$ ?v0 ?v2)))))) :named a260)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (= (insert$ ?v0 (insert$ ?v1 ?v2)) (insert$ ?v1 (insert$ ?v0 ?v2)))) :named a261)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$) (?v3 Msg_set$)) (=> (and (not (member$a ?v0 ?v1)) (not (member$a ?v2 ?v3))) (= (= (insert$ ?v0 ?v1) (insert$ ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Msg_set$)) (and (= ?v1 (insert$ ?v2 ?v4)) (and (not (member$a ?v2 ?v4)) (and (= ?v3 (insert$ ?v0 ?v4)) (not (member$a ?v0 ?v4)))))))))) :named a262)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$) (?v3 Event_set$)) (=> (and (not (member$b ?v0 ?v1)) (not (member$b ?v2 ?v3))) (= (= (insert$b ?v0 ?v1) (insert$b ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Event_set$)) (and (= ?v1 (insert$b ?v2 ?v4)) (and (not (member$b ?v2 ?v4)) (and (= ?v3 (insert$b ?v0 ?v4)) (not (member$b ?v0 ?v4)))))))))) :named a263)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$) (?v3 Agent_set$)) (=> (and (not (member$ ?v0 ?v1)) (not (member$ ?v2 ?v3))) (= (= (insert$c ?v0 ?v1) (insert$c ?v2 ?v3)) (ite (= ?v0 ?v2) (= ?v1 ?v3) (exists ((?v4 Agent_set$)) (and (= ?v1 (insert$c ?v2 ?v4)) (and (not (member$ ?v2 ?v4)) (and (= ?v3 (insert$c ?v0 ?v4)) (not (member$ ?v0 ?v4)))))))))) :named a264)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (! (=> (member$a ?v0 ?v1) (= (insert$ ?v0 ?v1) ?v1)) :pattern ((insert$ ?v0 ?v1)))) :named a265)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (! (=> (member$b ?v0 ?v1) (= (insert$b ?v0 ?v1) ?v1)) :pattern ((insert$b ?v0 ?v1)))) :named a266)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (! (=> (member$ ?v0 ?v1) (= (insert$c ?v0 ?v1) ?v1)) :pattern ((insert$c ?v0 ?v1)))) :named a267)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg_set$)) (=> (and (not (member$a ?v0 ?v1)) (not (member$a ?v0 ?v2))) (= (= (insert$ ?v0 ?v1) (insert$ ?v0 ?v2)) (= ?v1 ?v2)))) :named a268)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event_set$)) (=> (and (not (member$b ?v0 ?v1)) (not (member$b ?v0 ?v2))) (= (= (insert$b ?v0 ?v1) (insert$b ?v0 ?v2)) (= ?v1 ?v2)))) :named a269)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent_set$)) (=> (and (not (member$ ?v0 ?v1)) (not (member$ ?v0 ?v2))) (= (= (insert$c ?v0 ?v1) (insert$c ?v0 ?v2)) (= ?v1 ?v2)))) :named a270)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (=> (and (member$a ?v0 ?v1) (forall ((?v2 Msg_set$)) (=> (and (= ?v1 (insert$ ?v0 ?v2)) (not (member$a ?v0 ?v2))) false))) false)) :named a271)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (=> (and (member$b ?v0 ?v1) (forall ((?v2 Event_set$)) (=> (and (= ?v1 (insert$b ?v0 ?v2)) (not (member$b ?v0 ?v2))) false))) false)) :named a272)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (=> (and (member$ ?v0 ?v1) (forall ((?v2 Agent_set$)) (=> (and (= ?v1 (insert$c ?v0 ?v2)) (not (member$ ?v0 ?v2))) false))) false)) :named a273)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$) (?v2 Msg$)) (=> (member$a ?v0 ?v1) (member$a ?v0 (insert$ ?v2 ?v1)))) :named a274)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$) (?v2 Event$)) (=> (member$b ?v0 ?v1) (member$b ?v0 (insert$b ?v2 ?v1)))) :named a275)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$) (?v2 Agent$)) (=> (member$ ?v0 ?v1) (member$ ?v0 (insert$c ?v2 ?v1)))) :named a276)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_set$)) (member$a ?v0 (insert$ ?v0 ?v1))) :named a277)) -(assert (! (forall ((?v0 Event$) (?v1 Event_set$)) (member$b ?v0 (insert$b ?v0 ?v1))) :named a278)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_set$)) (member$ ?v0 (insert$c ?v0 ?v1))) :named a279)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_set$)) (=> (and (member$a ?v0 (insert$ ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$a ?v0 ?v2) false))) false)) :named a280)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_set$)) (=> (and (member$b ?v0 (insert$b ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$b ?v0 ?v2) false))) false)) :named a281)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_set$)) (=> (and (member$ ?v0 (insert$c ?v1 ?v2)) (and (=> (= ?v0 ?v1) false) (=> (member$ ?v0 ?v2) false))) false)) :named a282)) -(assert (! (forall ((?v0 Msg$) (?v1 (-> Msg$ Bool)) (?v2 Msg_list$)) (=> (member$a ?v0 (set$a (takeWhile$a ?v1 ?v2))) (and (member$a ?v0 (set$a ?v2)) (?v1 ?v0)))) :named a283)) -(assert (! (forall ((?v0 Agent$) (?v1 (-> Agent$ Bool)) (?v2 Agent_list$)) (=> (member$ ?v0 (set$b (takeWhile$b ?v1 ?v2))) (and (member$ ?v0 (set$b ?v2)) (?v1 ?v0)))) :named a284)) -(assert (! (forall ((?v0 Event$) (?v1 (-> Event$ Bool)) (?v2 Event_list$)) (=> (member$b ?v0 (set$ (takeWhile$ ?v1 ?v2))) (and (member$b ?v0 (set$ ?v2)) (?v1 ?v0)))) :named a285)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$a ?v2 ?v0) (takeWhile$a ?v3 ?v1)))) :named a286)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$b ?v2 ?v0) (takeWhile$b ?v3 ?v1)))) :named a287)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v0)) (= (?v2 ?v4) (?v3 ?v4))))) (= (takeWhile$ ?v2 ?v0) (takeWhile$ ?v3 ?v1)))) :named a288)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 Msg$)) (=> (member$a ?v0 (set$a ?v1)) (member$a ?v0 (set$a (cons$b ?v2 ?v1))))) :named a289)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 Agent$)) (=> (member$ ?v0 (set$b ?v1)) (member$ ?v0 (set$b (cons$c ?v2 ?v1))))) :named a290)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event$)) (=> (member$b ?v0 (set$ ?v1)) (member$b ?v0 (set$ (cons$ ?v2 ?v1))))) :named a291)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (member$a ?v0 (set$a (cons$b ?v0 ?v1)))) :named a292)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (member$ ?v0 (set$b (cons$c ?v0 ?v1)))) :named a293)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (member$b ?v0 (set$ (cons$ ?v0 ?v1)))) :named a294)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg$) (?v2 Msg_list$)) (=> (member$a ?v0 (set$a (cons$b ?v1 ?v2))) (or (= ?v0 ?v1) (member$a ?v0 (set$a ?v2))))) :named a295)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Agent_list$)) (=> (member$ ?v0 (set$b (cons$c ?v1 ?v2))) (or (= ?v0 ?v1) (member$ ?v0 (set$b ?v2))))) :named a296)) -(assert (! (forall ((?v0 Event$) (?v1 Event$) (?v2 Event_list$)) (=> (member$b ?v0 (set$ (cons$ ?v1 ?v2))) (or (= ?v0 ?v1) (member$b ?v0 (set$ ?v2))))) :named a297)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (and (member$a ?v0 (set$a ?v1)) (and (forall ((?v2 Msg_list$)) (=> (= ?v1 (cons$b ?v0 ?v2)) false)) (forall ((?v2 Msg$) (?v3 Msg_list$)) (=> (and (= ?v1 (cons$b ?v2 ?v3)) (member$a ?v0 (set$a ?v3))) false)))) false)) :named a298)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (and (member$ ?v0 (set$b ?v1)) (and (forall ((?v2 Agent_list$)) (=> (= ?v1 (cons$c ?v0 ?v2)) false)) (forall ((?v2 Agent$) (?v3 Agent_list$)) (=> (and (= ?v1 (cons$c ?v2 ?v3)) (member$ ?v0 (set$b ?v3))) false)))) false)) :named a299)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (and (member$b ?v0 (set$ ?v1)) (and (forall ((?v2 Event_list$)) (=> (= ?v1 (cons$ ?v0 ?v2)) false)) (forall ((?v2 Event$) (?v3 Event_list$)) (=> (and (= ?v1 (cons$ ?v2 ?v3)) (member$b ?v0 (set$ ?v3))) false)))) false)) :named a300)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg_list$) (?v2 (-> Msg$ Bool)) (?v3 (-> Msg$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Msg$)) (=> (member$a ?v4 (set$a ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$a ?v2 ?v0) (list_all$a ?v3 ?v1)))) :named a301)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent_list$) (?v2 (-> Agent$ Bool)) (?v3 (-> Agent$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Agent$)) (=> (member$ ?v4 (set$b ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$b ?v2 ?v0) (list_all$b ?v3 ?v1)))) :named a302)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event_list$) (?v2 (-> Event$ Bool)) (?v3 (-> Event$ Bool))) (=> (and (= ?v0 ?v1) (forall ((?v4 Event$)) (=> (member$b ?v4 (set$ ?v1)) (= (?v2 ?v4) (?v3 ?v4))))) (= (list_all$ ?v2 ?v0) (list_all$ ?v3 ?v1)))) :named a303)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$) (?v2 (-> Msg$ Bool))) (=> (and (list_all$a ?v0 ?v1) (forall ((?v3 Msg$)) (=> (and (member$a ?v3 (set$a ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$a ?v2 ?v1))) :named a304)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$) (?v2 (-> Agent$ Bool))) (=> (and (list_all$b ?v0 ?v1) (forall ((?v3 Agent$)) (=> (and (member$ ?v3 (set$b ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$b ?v2 ?v1))) :named a305)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$) (?v2 (-> Event$ Bool))) (=> (and (list_all$ ?v0 ?v1) (forall ((?v3 Event$)) (=> (and (member$b ?v3 (set$ ?v1)) (?v0 ?v3)) (?v2 ?v3)))) (list_all$ ?v2 ?v1))) :named a306)) -(assert (! (forall ((?v0 (-> Msg$ Bool)) (?v1 Msg_list$)) (= (list_ex1$a ?v0 ?v1) (exists ((?v2 Msg$)) (and (and (member$a ?v2 (set$a ?v1)) (?v0 ?v2)) (forall ((?v3 Msg$)) (=> (and (member$a ?v3 (set$a ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a307)) -(assert (! (forall ((?v0 (-> Agent$ Bool)) (?v1 Agent_list$)) (= (list_ex1$b ?v0 ?v1) (exists ((?v2 Agent$)) (and (and (member$ ?v2 (set$b ?v1)) (?v0 ?v2)) (forall ((?v3 Agent$)) (=> (and (member$ ?v3 (set$b ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a308)) -(assert (! (forall ((?v0 (-> Event$ Bool)) (?v1 Event_list$)) (= (list_ex1$ ?v0 ?v1) (exists ((?v2 Event$)) (and (and (member$b ?v2 (set$ ?v1)) (?v0 ?v2)) (forall ((?v3 Event$)) (=> (and (member$b ?v3 (set$ ?v1)) (?v0 ?v3)) (= ?v3 ?v2))))))) :named a309)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (member$g ?v1 ?v0))) :named a310)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (member$h ?v1 ?v0))) :named a311)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (member$d ?v1 ?v0))) :named a312)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$)) (less_eq$a (set$ ?v0) (set$ (cons$ ?v1 ?v0)))) :named a313)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg$)) (less_eq$ (set$a ?v0) (set$a (cons$b ?v1 ?v0)))) :named a314)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (= (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5))))))))) :named a315)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (= (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5))))))))) :named a316)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (= (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5))))))))) :named a317)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (= (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5))))))))) :named a318)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (= (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5))))))))) :named a319)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (= (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5))))))))) :named a320)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v2))))))) :named a321)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v2))))))) :named a322)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v2))))))) :named a323)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v3))))))) :named a324)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v3))))))) :named a325)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v3))))))) :named a326)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a327)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a328)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5)))))) false))) false)) :named a329)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a330)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a331)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5)))))) false))) false)) :named a332)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v2)) (not (?v1 ?v5))))))))) :named a333)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v2)) (not (?v1 ?v5))))))))) :named a334)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v2)) (not (?v1 ?v5))))))))) :named a335)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Msg$)) (=> (member$a ?v5 (set$a ?v4)) (not (?v1 ?v5))))))))) :named a336)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Agent$)) (=> (member$ ?v5 (set$b ?v4)) (not (?v1 ?v5))))))))) :named a337)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (and (?v1 ?v3) (forall ((?v5 Event$)) (=> (member$b ?v5 (set$ ?v4)) (not (?v1 ?v5))))))))) :named a338)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (= (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3)))))) :named a339)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (= (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3)))))) :named a340)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (= (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3)))))) :named a341)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$) (?v2 Msg_list$) (?v3 Msg_list$) (?v4 Msg_list$)) (=> (and (not (member$a ?v0 (set$a ?v1))) (not (member$a ?v0 (set$a ?v2)))) (= (= (append$a ?v1 (cons$b ?v0 ?v2)) (append$a ?v3 (cons$b ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a342)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$) (?v2 Agent_list$) (?v3 Agent_list$) (?v4 Agent_list$)) (=> (and (not (member$ ?v0 (set$b ?v1))) (not (member$ ?v0 (set$b ?v2)))) (= (= (append$b ?v1 (cons$c ?v0 ?v2)) (append$b ?v3 (cons$c ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a343)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$) (?v2 Event_list$) (?v3 Event_list$) (?v4 Event_list$)) (=> (and (not (member$b ?v0 (set$ ?v1))) (not (member$b ?v0 (set$ ?v2)))) (= (= (append$ ?v1 (cons$ ?v0 ?v2)) (append$ ?v3 (cons$ ?v0 ?v4))) (and (= ?v1 ?v3) (= ?v2 ?v4))))) :named a344)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (and (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (forall ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (=> (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a345)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (and (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (forall ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (=> (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a346)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (and (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (forall ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (=> (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (?v1 ?v3)) false))) false)) :named a347)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v2))))))) :named a348)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v2))))))) :named a349)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v2))))))) :named a350)) -(assert (! (forall ((?v0 Msg_list$) (?v1 (-> Msg$ Bool))) (=> (exists ((?v2 Msg$)) (and (member$a ?v2 (set$a ?v0)) (?v1 ?v2))) (exists ((?v2 Msg_list$) (?v3 Msg$) (?v4 Msg_list$)) (and (= ?v0 (append$a ?v2 (cons$b ?v3 ?v4))) (?v1 ?v3))))) :named a351)) -(assert (! (forall ((?v0 Agent_list$) (?v1 (-> Agent$ Bool))) (=> (exists ((?v2 Agent$)) (and (member$ ?v2 (set$b ?v0)) (?v1 ?v2))) (exists ((?v2 Agent_list$) (?v3 Agent$) (?v4 Agent_list$)) (and (= ?v0 (append$b ?v2 (cons$c ?v3 ?v4))) (?v1 ?v3))))) :named a352)) -(assert (! (forall ((?v0 Event_list$) (?v1 (-> Event$ Bool))) (=> (exists ((?v2 Event$)) (and (member$b ?v2 (set$ ?v0)) (?v1 ?v2))) (exists ((?v2 Event_list$) (?v3 Event$) (?v4 Event_list$)) (and (= ?v0 (append$ ?v2 (cons$ ?v3 ?v4))) (?v1 ?v3))))) :named a353)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (and (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3))) (not (member$a ?v0 (set$a ?v3))))))) :named a354)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (and (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3))) (not (member$ ?v0 (set$b ?v3))))))) :named a355)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (and (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3))) (not (member$b ?v0 (set$ ?v3))))))) :named a356)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (=> (member$a ?v0 (set$a ?v1)) (exists ((?v2 Msg_list$) (?v3 Msg_list$)) (= ?v1 (append$a ?v2 (cons$b ?v0 ?v3)))))) :named a357)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (=> (member$ ?v0 (set$b ?v1)) (exists ((?v2 Agent_list$) (?v3 Agent_list$)) (= ?v1 (append$b ?v2 (cons$c ?v0 ?v3)))))) :named a358)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (=> (member$b ?v0 (set$ ?v1)) (exists ((?v2 Event_list$) (?v3 Event_list$)) (= ?v1 (append$ ?v2 (cons$ ?v0 ?v3)))))) :named a359)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (=> (member$b (says$ ?v0 ?v1 ?v2) (set$ ?v3)) (member$a ?v2 (knows$ ?v0 ?v3)))) :named a360)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (member$b (notes$ ?v0 ?v1) (set$ ?v2)) (member$a ?v1 (knows$ ?v0 ?v2)))) :named a361)) -(assert (! (forall ((?v0 Msg$) (?v1 Msg_list$)) (! (= (insert$d ?v0 ?v1) (ite (member$a ?v0 (set$a ?v1)) ?v1 (cons$b ?v0 ?v1))) :pattern ((insert$d ?v0 ?v1)))) :named a362)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent_list$)) (! (= (insert$e ?v0 ?v1) (ite (member$ ?v0 (set$b ?v1)) ?v1 (cons$c ?v0 ?v1))) :pattern ((insert$e ?v0 ?v1)))) :named a363)) -(assert (! (forall ((?v0 Event$) (?v1 Event_list$)) (! (= (insert$a ?v0 ?v1) (ite (member$b ?v0 (set$ ?v1)) ?v1 (cons$ ?v0 ?v1))) :pattern ((insert$a ?v0 ?v1)))) :named a364)) -(assert (! (forall ((?v0 Agent$) (?v1 Agent$) (?v2 Msg$) (?v3 Event_list$)) (=> (member$b (says$ ?v0 ?v1 ?v2) (set$ ?v3)) (member$a ?v2 (knows$ spy$ ?v3)))) :named a365)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (and (not (= ?v0 spy$)) (member$b (gets$ ?v0 ?v1) (set$ ?v2))) (member$a ?v1 (knows$ ?v0 ?v2)))) :named a366)) -(assert (! (forall ((?v0 Msg$) (?v1 Event_list$)) (=> (member$a ?v0 (knows$ spy$ ?v1)) (exists ((?v2 Agent$) (?v3 Agent$)) (or (member$b (says$ ?v2 ?v3 ?v0) (set$ ?v1)) (or (member$b (notes$ ?v2 ?v0) (set$ ?v1)) (member$a ?v0 (initState$ spy$))))))) :named a367)) -(assert (! (forall ((?v0 Msg_list$) (?v1 Msg$) (?v2 Msg_list_set$)) (=> (member$e (append$a ?v0 (cons$b ?v1 nil$b)) ?v2) (member$a ?v1 (succ$a ?v2 ?v0)))) :named a368)) -(assert (! (forall ((?v0 Agent_list$) (?v1 Agent$) (?v2 Agent_list_set$)) (=> (member$f (append$b ?v0 (cons$c ?v1 nil$c)) ?v2) (member$ ?v1 (succ$b ?v2 ?v0)))) :named a369)) -(assert (! (forall ((?v0 Event_list$) (?v1 Event$) (?v2 Event_list_set$)) (=> (member$c (append$ ?v0 (cons$ ?v1 nil$)) ?v2) (member$b ?v1 (succ$ ?v2 ?v0)))) :named a370)) -(assert (! (forall ((?v0 Event_list$) (?v1 Agent$) (?v2 Msg$)) (= (knows$ spy$ (append$ ?v0 (cons$ (notes$ ?v1 ?v2) nil$))) (ite (member$ ?v1 bad$) (insert$ ?v2 (knows$ spy$ ?v0)) (knows$ spy$ ?v0)))) :named a371)) -(assert (! (member$ spy$ bad$) :named a372)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (! (= (knows$ spy$ (cons$ (notes$ ?v0 ?v1) ?v2)) (ite (member$ ?v0 bad$) (insert$ ?v1 (knows$ spy$ ?v2)) (knows$ spy$ ?v2))) :pattern ((cons$ (notes$ ?v0 ?v1) ?v2)))) :named a373)) -(assert (! (forall ((?v0 Agent$) (?v1 Msg$) (?v2 Event_list$)) (=> (and (member$b (notes$ ?v0 ?v1) (set$ ?v2)) (member$ ?v0 bad$)) (member$a ?v1 (knows$ spy$ ?v2)))) :named a374)) -(assert (! (forall ((?v0 Agent$) (?v1 Event$) (?v2 Event_list$)) (= (knows$ ?v0 (cons$ ?v1 ?v2)) (ite (= ?v0 spy$) (case_event$ (uuo$ ?v2) (uup$ ?v2) (uuq$ ?v2) ?v1) (case_event$ (uur$ ?v0 ?v2) (uus$ ?v0 ?v2) (uus$ ?v0 ?v2) ?v1)))) :named a375)) -(check-sat) diff --git a/test/regress/regress1/ho/bound_var_bug.p b/test/regress/regress1/ho/bound_var_bug.p new file mode 100644 index 000000000..0dc946d6a --- /dev/null +++ b/test/regress/regress1/ho/bound_var_bug.p @@ -0,0 +1,26 @@ +% COMMAND-LINE: --uf-ho +% EXPECT: % SZS status GaveUp for bound_var_bug + +% TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; } +% This file was generated by Isabelle (most likely Sledgehammer) +% 2017-07-27 17:26:12.634 + +% Could-be-implicit typings (91) + +thf(ty_n_t__Product____Type__Oprod_It__List__Olist_It__Product____Type__Oprod_It__Vars__Ovar_Mt__Terms__Oexp_J_J_Mt__Product____Type__Oprod_It__Terms__Oexp_Mt__List__Olist_It__SestoftConf__Ostack____elem_J_J_J, type, + produc1516857811k_elem : $tType). + + +thf(ty_n_t__Vars__Ovar, type, + var : $tType). + +thf(sy_c_Transitive__Closure_Ortranclp_001t__Product____Type__Oprod_It__List__Olist_It__Product____Type__Oprod_It__Vars__Ovar_Mt__Terms__Oexp_J_J_Mt__Product____Type__Oprod_It__Terms__Oexp_Mt__List__Olist_It__SestoftConf__Ostack____elem_J_J_J, type, + transi803447880k_elem : (produc1516857811k_elem > produc1516857811k_elem > $o) > produc1516857811k_elem > produc1516857811k_elem > $o). + +% Relevant facts (1094) + +thf(fact_233_rtranclp__idemp, axiom, + ((![R : produc1516857811k_elem > produc1516857811k_elem > $o]: ((transi803447880k_elem @ (transi803447880k_elem @ R)) = (transi803447880k_elem @ R))))). % rtranclp_idemp + +thf(fact_293_rtranclp_Osimps, axiom, + ((transi803447880k_elem = (^[R4 : produc1516857811k_elem > produc1516857811k_elem > $o]: (^[A12 : produc1516857811k_elem]: (^[A23 : produc1516857811k_elem]: (((?[A5 : produc1516857811k_elem]: (((A12 = A5)) & ((A23 = A5))))) | ((?[A5 : produc1516857811k_elem]: (?[B4 : produc1516857811k_elem]: (?[C5 : produc1516857811k_elem]: (((A12 = A5)) & ((((A23 = C5)) & ((((transi803447880k_elem @ R4 @ A5 @ B4)) & ((R4 @ B4 @ C5)))))))))))))))))). % rtranclp.simps diff --git a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p new file mode 100644 index 000000000..6c35270fd --- /dev/null +++ b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p @@ -0,0 +1,11 @@ +% COMMAND-LINE: --uf-ho --finite-model-find +% EXPECT: % SZS status Satisfiable for bug_freeVar_BDD_General_data_270 + +thf(ty_n_t__Nat__Onat, type, + nat : $tType). + +thf(sy_c_Orderings_Oord__class_Oless__eq_001t__Nat__Onat, type, + ord_less_eq_nat : nat > nat > $o). + +thf(fact_76_eq__iff, axiom, + (((^[Y3 : nat]: (^[Z2 : nat]: (Y3 = Z2))) = (^[X4 : nat]: (^[Y4 : nat]: (((ord_less_eq_nat @ X4 @ Y4)) & ((ord_less_eq_nat @ Y4 @ X4)))))))). % eq_iff diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 new file mode 100644 index 000000000..9dd95aeae --- /dev/null +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models +; EXPECT: sat + +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort qML_mu 0) +(declare-sort qML_i 0) +(declare-fun scott_G (qML_mu qML_i) Bool) +(declare-fun scott_P ((-> qML_mu qML_i Bool) qML_i) Bool) + +(assert + (= + scott_G + (lambda ((X qML_mu) (__flatten_var_0 qML_i)) + (forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool))) + (or + (not (scott_P BOUND_VARIABLE_292 __flatten_var_0)) + (BOUND_VARIABLE_292 X __flatten_var_0) + ) )))) + +(assert + (forall ((X_1 qML_i)) + (scott_P + (lambda ((X qML_mu) (__flatten_var_0 qML_i)) + (forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool))) + (or + (not (scott_P BOUND_VARIABLE_292 __flatten_var_0)) + (BOUND_VARIABLE_292 X __flatten_var_0)) )) + X_1 + ) + )) + + + +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/ho/fta0210.smt2 b/test/regress/regress1/ho/fta0210.smt2 deleted file mode 100644 index 9f0a39f25..000000000 --- a/test/regress/regress1/ho/fta0210.smt2 +++ /dev/null @@ -1,64 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(declare-sort A$ 0) -(declare-sort Nat$ 0) -(declare-sort A_poly$ 0) -(declare-sort Nat_poly$ 0) -(declare-sort A_poly_poly$ 0) -(declare-fun p$ () A_poly$) -(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$) -(declare-fun one$ () Nat$) -(declare-fun suc$ (Nat$) Nat$) -(declare-fun uua$ (A_poly$) A_poly$) -(declare-fun uub$ (A$ (-> A$ A$) A$) A$) -(declare-fun uuc$ (A$) A$) -(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$) -(declare-fun uue$ (Nat$) Nat$) -(declare-fun one$a () Nat_poly$) -(declare-fun one$b () A$) -(declare-fun one$c () A_poly$) -(declare-fun plus$ (A_poly$ A_poly$) A_poly$) -(declare-fun poly$ (A_poly$ A$) A$) -(declare-fun zero$ () A_poly$) -(declare-fun pCons$ (A$ A_poly$) A_poly$) -(declare-fun plus$a (Nat$ Nat$) Nat$) -(declare-fun plus$b (A$ A$) A$) -(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$) -(declare-fun poly$a (Nat_poly$ Nat$) Nat$) -(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$) -(declare-fun power$ (A$ Nat$) A$) -(declare-fun psize$ (A_poly$) Nat$) -(declare-fun times$ (A_poly$ A_poly$) A_poly$) -(declare-fun zero$a () Nat$) -(declare-fun zero$b () A$) -(declare-fun zero$c () Nat_poly$) -(declare-fun zero$d () A_poly_poly$) -(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$) -(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$) -(declare-fun power$a (A_poly$ Nat$) A_poly$) -(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) -(declare-fun power$c (Nat$ Nat$) Nat$) -(declare-fun psize$a (A_poly_poly$) Nat$) -(declare-fun times$a (Nat$ Nat$) Nat$) -(declare-fun times$b (A$ A$) A$) -(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$) -(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$) -(declare-fun uminus$ (A_poly$) A_poly$) -(declare-fun uminus$a (A$) A$) -(declare-fun constant$ ((-> A$ A$)) Bool) -(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$) -(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$) -(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$) -(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$) -(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$)) -(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$) -(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$)) -(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$)) - -(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14)) -(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69)) -(assert (! (not (constant$ (poly$ zero$))) :named a206)) - -(check-sat) -;(get-proof) diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p new file mode 100644 index 000000000..c33b43ca5 --- /dev/null +++ b/test/regress/regress1/ho/fta0328.lfho.p @@ -0,0 +1,200 @@ +% COMMAND-LINE: --uf-ho --uf-ho --finite-model-find +% EXPECT: % SZS status CounterSatisfiable for fta0328.lfho + +% TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; } +% This file was generated by Isabelle (most likely Sledgehammer) +% 2018-05-22 19:17:55.732 + +% Could-be-implicit typings (8) +thf(ty_n_t__Polynomial__Opoly_It__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J_J, type, + poly_p1267267526omplex : $tType). +thf(ty_n_t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, + poly_poly_complex : $tType). +thf(ty_n_t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, + poly_complex : $tType). +thf(ty_n_t__Polynomial__Opoly_It__Nat__Onat_J, type, + poly_nat : $tType). +thf(ty_n_t__Complex__Ocomplex, type, + complex : $tType). +thf(ty_n_t__Real__Oreal, type, + real : $tType). +thf(ty_n_t__HOL__Obool, type, + bool : $tType). +thf(ty_n_t__Nat__Onat, type, + nat : $tType). + +% Explicit typings (28) +thf(sy_c_Fundamental__Theorem__Algebra__Mirabelle__bptywjkimr_Oconstant_001t__Complex__Ocomplex_001t__Complex__Ocomplex, type, + fundam769667258omplex : (complex > complex) > $o). +thf(sy_c_Fundamental__Theorem__Algebra__Mirabelle__bptywjkimr_Opsize_001t__Complex__Ocomplex, type, + fundam835161864omplex : poly_complex > nat). +thf(sy_c_Groups_Oplus__class_Oplus_001t__Complex__Ocomplex, type, + plus_plus_complex : complex > complex > complex). +thf(sy_c_Groups_Oplus__class_Oplus_001t__Nat__Onat, type, + plus_plus_nat : nat > nat > nat). +thf(sy_c_Groups_Oplus__class_Oplus_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, + plus_p1547158847omplex : poly_complex > poly_complex > poly_complex). +thf(sy_c_Groups_Oplus__class_Oplus_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, + plus_p138939463omplex : poly_poly_complex > poly_poly_complex > poly_poly_complex). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Complex__Ocomplex, type, + zero_zero_complex : complex). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Nat__Onat, type, + zero_zero_nat : nat). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, + zero_z1746442943omplex : poly_complex). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Nat__Onat_J, type, + zero_zero_poly_nat : poly_nat). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, + zero_z1040703943omplex : poly_poly_complex). +thf(sy_c_Groups_Ozero__class_Ozero_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J_J, type, + zero_z1200043727omplex : poly_p1267267526omplex). +thf(sy_c_Orderings_Oord__class_Oless_001t__Nat__Onat, type, + ord_less_nat : nat > nat > $o). +thf(sy_c_Orderings_Oord__class_Oless__eq_001t__Nat__Onat, type, + ord_less_eq_nat : nat > nat > $o). +thf(sy_c_Orderings_Oord__class_Oless__eq_001t__Real__Oreal, type, + ord_less_eq_real : real > real > $o). +thf(sy_c_Polynomial_Opoly_001t__Complex__Ocomplex, type, + poly_complex2 : poly_complex > complex > complex). +thf(sy_c_Polynomial_Opoly_001t__Nat__Onat, type, + poly_nat2 : poly_nat > nat > nat). +thf(sy_c_Polynomial_Opoly_001t__Polynomial__Opoly_It__Complex__Ocomplex_J, type, + poly_poly_complex2 : poly_poly_complex > poly_complex > poly_complex). +thf(sy_c_Polynomial_Opoly_001t__Polynomial__Opoly_It__Polynomial__Opoly_It__Complex__Ocomplex_J_J, type, + poly_p282434315omplex : poly_p1267267526omplex > poly_poly_complex > poly_poly_complex). +thf(sy_c_Real__Vector__Spaces_Onorm__class_Onorm_001t__Complex__Ocomplex, type, + real_V638595069omplex : complex > real). +thf(sy_c_fFalse, type, + fFalse : bool). +thf(sy_c_fTrue, type, + fTrue : bool). +thf(sy_c_pp, type, + pp : bool > $o). +thf(sy_v_a____, type, + a : complex). +thf(sy_v_c____, type, + c : complex). +thf(sy_v_p, type, + p : poly_complex). +thf(sy_v_pa____, type, + pa : poly_complex). +thf(sy_v_q____, type, + q : poly_complex). + +% Relevant facts (53) +thf(fact_0_kas_I1_J, axiom, + ((~ ((a = zero_zero_complex))))). % kas(1) +thf(fact_1_q_I2_J, axiom, + ((![X : complex]: ((poly_complex2 @ q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))). % q(2) +thf(fact_2_nc, axiom, + ((~ ((fundam769667258omplex @ (poly_complex2 @ p)))))). % nc +thf(fact_3_False, axiom, + ((~ (((poly_complex2 @ pa @ c) = zero_zero_complex))))). % False +thf(fact_4_less_Oprems, axiom, + ((~ ((fundam769667258omplex @ (poly_complex2 @ pa)))))). % less.prems +thf(fact_5_a00, axiom, + ((~ (((poly_complex2 @ q @ zero_zero_complex) = zero_zero_complex))))). % a00 +thf(fact_6_pqc0, axiom, + (((poly_complex2 @ pa @ c) = (poly_complex2 @ q @ zero_zero_complex)))). % pqc0 +thf(fact_7_q_I1_J, axiom, + (((fundam835161864omplex @ q) = (fundam835161864omplex @ pa)))). % q(1) +thf(fact_8_poly__0, axiom, + ((![X2 : poly_poly_complex]: ((poly_p282434315omplex @ zero_z1200043727omplex @ X2) = zero_z1040703943omplex)))). % poly_0 +thf(fact_9_poly__0, axiom, + ((![X2 : nat]: ((poly_nat2 @ zero_zero_poly_nat @ X2) = zero_zero_nat)))). % poly_0 +thf(fact_10_poly__0, axiom, + ((![X2 : poly_complex]: ((poly_poly_complex2 @ zero_z1040703943omplex @ X2) = zero_z1746442943omplex)))). % poly_0 +thf(fact_11_poly__0, axiom, + ((![X2 : complex]: ((poly_complex2 @ zero_z1746442943omplex @ X2) = zero_zero_complex)))). % poly_0 +thf(fact_12_poly__all__0__iff__0, axiom, + ((![P : poly_p1267267526omplex]: ((![X3 : poly_poly_complex]: ((poly_p282434315omplex @ P @ X3) = zero_z1040703943omplex)) <=> (P = zero_z1200043727omplex))))). % poly_all_0_iff_0 +thf(fact_13_poly__all__0__iff__0, axiom, + ((![P : poly_complex]: ((![X3 : complex]: ((poly_complex2 @ P @ X3) = zero_zero_complex)) <=> (P = zero_z1746442943omplex))))). % poly_all_0_iff_0 +thf(fact_14_poly__all__0__iff__0, axiom, + ((![P : poly_poly_complex]: ((![X3 : poly_complex]: ((poly_poly_complex2 @ P @ X3) = zero_z1746442943omplex)) <=> (P = zero_z1040703943omplex))))). % poly_all_0_iff_0 +thf(fact_15__092_060open_062_092_060exists_062q_O_Apsize_Aq_A_061_Apsize_Ap_A_092_060and_062_A_I_092_060forall_062x_O_Apoly_Aq_Ax_A_061_Apoly_Ap_A_Ic_A_L_Ax_J_J_092_060close_062, axiom, + ((?[Q : poly_complex]: (((fundam835161864omplex @ Q) = (fundam835161864omplex @ pa)) & (![X : complex]: ((poly_complex2 @ Q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))))). % \<open>\<exists>q. psize q = psize p \<and> (\<forall>x. poly q x = poly p (c + x))\<close> +thf(fact_16__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062q_O_A_092_060lbrakk_062psize_Aq_A_061_Apsize_Ap_059_A_092_060forall_062x_O_Apoly_Aq_Ax_A_061_Apoly_Ap_A_Ic_A_L_Ax_J_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, axiom, + ((~ ((![Q : poly_complex]: (((fundam835161864omplex @ Q) = (fundam835161864omplex @ pa)) => (~ ((![X : complex]: ((poly_complex2 @ Q @ X) = (poly_complex2 @ pa @ (plus_plus_complex @ c @ X)))))))))))). % \<open>\<And>thesis. (\<And>q. \<lbrakk>psize q = psize p; \<forall>x. poly q x = poly p (c + x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> +thf(fact_17__092_060open_062constant_A_Ipoly_Aq_J_A_092_060Longrightarrow_062_AFalse_092_060close_062, axiom, + ((~ ((fundam769667258omplex @ (poly_complex2 @ q)))))). % \<open>constant (poly q) \<Longrightarrow> False\<close> +thf(fact_18_qnc, axiom, + ((~ ((fundam769667258omplex @ (poly_complex2 @ q)))))). % qnc +thf(fact_19_poly__eq__poly__eq__iff, axiom, + ((![P : poly_poly_complex, Q2 : poly_poly_complex]: (((poly_poly_complex2 @ P) = (poly_poly_complex2 @ Q2)) <=> (P = Q2))))). % poly_eq_poly_eq_iff +thf(fact_20_poly__eq__poly__eq__iff, axiom, + ((![P : poly_complex, Q2 : poly_complex]: (((poly_complex2 @ P) = (poly_complex2 @ Q2)) <=> (P = Q2))))). % poly_eq_poly_eq_iff +thf(fact_21_c, axiom, + ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ pa @ c)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W)))))). % c +thf(fact_22_zero__reorient, axiom, + ((![X2 : poly_poly_complex]: ((zero_z1040703943omplex = X2) <=> (X2 = zero_z1040703943omplex))))). % zero_reorient +thf(fact_23_zero__reorient, axiom, + ((![X2 : nat]: ((zero_zero_nat = X2) <=> (X2 = zero_zero_nat))))). % zero_reorient +thf(fact_24_zero__reorient, axiom, + ((![X2 : complex]: ((zero_zero_complex = X2) <=> (X2 = zero_zero_complex))))). % zero_reorient +thf(fact_25_zero__reorient, axiom, + ((![X2 : poly_complex]: ((zero_z1746442943omplex = X2) <=> (X2 = zero_z1746442943omplex))))). % zero_reorient +thf(fact_26_cq0, axiom, + ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ q @ zero_zero_complex)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W)))))). % cq0 +thf(fact_27_less_Ohyps, axiom, + ((![P : poly_complex]: ((ord_less_nat @ (fundam835161864omplex @ P) @ (fundam835161864omplex @ pa)) => ((~ ((fundam769667258omplex @ (poly_complex2 @ P)))) => (?[Z : complex]: ((poly_complex2 @ P @ Z) = zero_zero_complex))))))). % less.hyps +thf(fact_28_add__left__cancel, axiom, + ((![A : poly_complex, B : poly_complex, C : poly_complex]: (((plus_p1547158847omplex @ A @ B) = (plus_p1547158847omplex @ A @ C)) <=> (B = C))))). % add_left_cancel +thf(fact_29_add__left__cancel, axiom, + ((![A : complex, B : complex, C : complex]: (((plus_plus_complex @ A @ B) = (plus_plus_complex @ A @ C)) <=> (B = C))))). % add_left_cancel +thf(fact_30_add__right__cancel, axiom, + ((![B : poly_complex, A : poly_complex, C : poly_complex]: (((plus_p1547158847omplex @ B @ A) = (plus_p1547158847omplex @ C @ A)) <=> (B = C))))). % add_right_cancel +thf(fact_31_add__right__cancel, axiom, + ((![B : complex, A : complex, C : complex]: (((plus_plus_complex @ B @ A) = (plus_plus_complex @ C @ A)) <=> (B = C))))). % add_right_cancel +thf(fact_32__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062c_O_A_092_060forall_062w_O_Acmod_A_Ipoly_Ap_Ac_J_A_092_060le_062_Acmod_A_Ipoly_Ap_Aw_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, axiom, + ((~ ((![C2 : complex]: (~ ((![W : complex]: (ord_less_eq_real @ (real_V638595069omplex @ (poly_complex2 @ pa @ C2)) @ (real_V638595069omplex @ (poly_complex2 @ pa @ W))))))))))). % \<open>\<And>thesis. (\<And>c. \<forall>w. cmod (poly p c) \<le> cmod (poly p w) \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> +thf(fact_33_le__zero__eq, axiom, + ((![N : nat]: ((ord_less_eq_nat @ N @ zero_zero_nat) <=> (N = zero_zero_nat))))). % le_zero_eq +thf(fact_34_not__gr__zero, axiom, + ((![N : nat]: ((~ ((ord_less_nat @ zero_zero_nat @ N))) <=> (N = zero_zero_nat))))). % not_gr_zero +thf(fact_35_zero__eq__add__iff__both__eq__0, axiom, + ((![X2 : nat, Y : nat]: ((zero_zero_nat = (plus_plus_nat @ X2 @ Y)) <=> ((X2 = zero_zero_nat) & (Y = zero_zero_nat)))))). % zero_eq_add_iff_both_eq_0 +thf(fact_36_add__eq__0__iff__both__eq__0, axiom, + ((![X2 : nat, Y : nat]: (((plus_plus_nat @ X2 @ Y) = zero_zero_nat) <=> ((X2 = zero_zero_nat) & (Y = zero_zero_nat)))))). % add_eq_0_iff_both_eq_0 +thf(fact_37_add__cancel__right__right, axiom, + ((![A : poly_poly_complex, B : poly_poly_complex]: ((A = (plus_p138939463omplex @ A @ B)) <=> (B = zero_z1040703943omplex))))). % add_cancel_right_right +thf(fact_38_add__cancel__right__right, axiom, + ((![A : nat, B : nat]: ((A = (plus_plus_nat @ A @ B)) <=> (B = zero_zero_nat))))). % add_cancel_right_right +thf(fact_39_add__cancel__right__right, axiom, + ((![A : complex, B : complex]: ((A = (plus_plus_complex @ A @ B)) <=> (B = zero_zero_complex))))). % add_cancel_right_right +thf(fact_40_add__cancel__right__right, axiom, + ((![A : poly_complex, B : poly_complex]: ((A = (plus_p1547158847omplex @ A @ B)) <=> (B = zero_z1746442943omplex))))). % add_cancel_right_right +thf(fact_41_add__cancel__right__left, axiom, + ((![A : poly_poly_complex, B : poly_poly_complex]: ((A = (plus_p138939463omplex @ B @ A)) <=> (B = zero_z1040703943omplex))))). % add_cancel_right_left +thf(fact_42_add__cancel__right__left, axiom, + ((![A : nat, B : nat]: ((A = (plus_plus_nat @ B @ A)) <=> (B = zero_zero_nat))))). % add_cancel_right_left +thf(fact_43_add__cancel__right__left, axiom, + ((![A : complex, B : complex]: ((A = (plus_plus_complex @ B @ A)) <=> (B = zero_zero_complex))))). % add_cancel_right_left +thf(fact_44_add__cancel__right__left, axiom, + ((![A : poly_complex, B : poly_complex]: ((A = (plus_p1547158847omplex @ B @ A)) <=> (B = zero_z1746442943omplex))))). % add_cancel_right_left +thf(fact_45_add__cancel__left__right, axiom, + ((![A : poly_poly_complex, B : poly_poly_complex]: (((plus_p138939463omplex @ A @ B) = A) <=> (B = zero_z1040703943omplex))))). % add_cancel_left_right +thf(fact_46_add__cancel__left__right, axiom, + ((![A : nat, B : nat]: (((plus_plus_nat @ A @ B) = A) <=> (B = zero_zero_nat))))). % add_cancel_left_right +thf(fact_47_add__cancel__left__right, axiom, + ((![A : complex, B : complex]: (((plus_plus_complex @ A @ B) = A) <=> (B = zero_zero_complex))))). % add_cancel_left_right +thf(fact_48_add__cancel__left__right, axiom, + ((![A : poly_complex, B : poly_complex]: (((plus_p1547158847omplex @ A @ B) = A) <=> (B = zero_z1746442943omplex))))). % add_cancel_left_right +thf(fact_49_add__cancel__left__left, axiom, + ((![B : poly_poly_complex, A : poly_poly_complex]: (((plus_p138939463omplex @ B @ A) = A) <=> (B = zero_z1040703943omplex))))). % add_cancel_left_left +thf(fact_50_add__cancel__left__left, axiom, + ((![B : nat, A : nat]: (((plus_plus_nat @ B @ A) = A) <=> (B = zero_zero_nat))))). % add_cancel_left_left +thf(fact_51_add__cancel__left__left, axiom, + ((![B : complex, A : complex]: (((plus_plus_complex @ B @ A) = A) <=> (B = zero_zero_complex))))). % add_cancel_left_left +thf(fact_52_add__cancel__left__left, axiom, + ((![B : poly_complex, A : poly_complex]: (((plus_p1547158847omplex @ B @ A) = A) <=> (B = zero_z1746442943omplex))))). % add_cancel_left_left + +% Helper facts (2) +thf(help_pp_2_1_U, axiom, + ((pp @ fTrue))). +thf(help_pp_1_1_U, axiom, + ((~ ((pp @ fFalse))))). + +% Conjectures (1) +thf(conj_0, conjecture, + ((?[Z2 : complex]: ((poly_complex2 @ pa @ Z2) = zero_zero_complex)))). diff --git a/test/regress/regress1/ho/fta0409.smt2 b/test/regress/regress1/ho/fta0409.smt2 deleted file mode 100644 index 51ac5f2da..000000000 --- a/test/regress/regress1/ho/fta0409.smt2 +++ /dev/null @@ -1,427 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) -(declare-sort Nat$ 0) -(declare-sort Complex$ 0) -(declare-sort Nat_poly$ 0) -(declare-sort Complex_poly$ 0) -(declare-sort Complex_poly_poly$ 0) -(declare-fun n$ () Nat$) -(declare-fun q$ () Complex_poly$) -(declare-fun r$ () Complex_poly$) -(declare-fun dvd$ (Complex_poly$ Complex_poly$) Bool) -(declare-fun one$ () Nat$) -(declare-fun suc$ (Nat$) Nat$) -(declare-fun dvd$a (Complex$ Complex$) Bool) -(declare-fun dvd$b (Nat$ Nat$) Bool) -(declare-fun dvd$c (Complex_poly_poly$ Complex_poly_poly$) Bool) -(declare-fun dvd$d (Nat_poly$ Nat_poly$) Bool) -(declare-fun one$a () Complex_poly$) -(declare-fun one$b () Complex$) -(declare-fun one$c () Nat_poly$) -(declare-fun plus$ (Complex$ Complex$) Complex$) -(declare-fun poly$ (Complex_poly$) (-> Complex$ Complex$)) -(declare-fun zero$ () Complex$) -(declare-fun coeff$ (Complex_poly_poly$ Nat$) Complex_poly$) -(declare-fun monom$ (Complex$ Nat$) Complex_poly$) -(declare-fun order$ (Complex$ Complex_poly$) Nat$) -(declare-fun pCons$ (Complex$ Complex_poly$) Complex_poly$) -(declare-fun plus$a (Nat$ Nat$) Nat$) -(declare-fun plus$b (Nat_poly$ Nat_poly$) Nat_poly$) -(declare-fun plus$c (Complex_poly$ Complex_poly$) Complex_poly$) -(declare-fun poly$a (Complex_poly_poly$ Complex_poly$) Complex_poly$) -(declare-fun poly$b (Nat_poly$ Nat$) Nat$) -(declare-fun power$ (Complex_poly$ Nat$) Complex_poly$) -(declare-fun psize$ (Complex_poly$) Nat$) -(declare-fun times$ (Nat$ Nat$) Nat$) -(declare-fun zero$a () Nat$) -(declare-fun zero$b () Complex_poly_poly$) -(declare-fun zero$c () Complex_poly$) -(declare-fun zero$d () Nat_poly$) -(declare-fun coeff$a (Nat_poly$ Nat$) Nat$) -(declare-fun coeff$b (Complex_poly$ Nat$) Complex$) -(declare-fun degree$ (Complex_poly_poly$) Nat$) -(declare-fun monom$a (Complex_poly$ Nat$) Complex_poly_poly$) -(declare-fun monom$b (Nat$ Nat$) Nat_poly$) -(declare-fun order$a (Complex_poly$ Complex_poly_poly$) Nat$) -(declare-fun pCons$a (Complex_poly$ Complex_poly_poly$) Complex_poly_poly$) -(declare-fun pCons$b (Nat$ Nat_poly$) Nat_poly$) -(declare-fun power$a (Complex_poly_poly$ Nat$) Complex_poly_poly$) -(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) -(declare-fun power$c (Nat$ Nat$) Nat$) -(declare-fun power$d (Complex$ Nat$) Complex$) -(declare-fun degree$a (Nat_poly$) Nat$) -(declare-fun degree$b (Complex_poly$) Nat$) -(declare-fun is_zero$ (Complex_poly$) Bool) -(declare-fun less_eq$ (Nat$ Nat$) Bool) -(declare-fun of_bool$ (Bool) Complex$) -(declare-fun constant$ ((-> Complex$ Complex$)) Bool) -(declare-fun of_bool$a (Bool) Complex_poly$) -(declare-fun of_bool$b (Bool) Nat$) -(declare-fun pcompose$ (Complex_poly$ Complex_poly$) Complex_poly$) -(declare-fun pcompose$a (Complex_poly_poly$ Complex_poly_poly$) Complex_poly_poly$) -(declare-fun pcompose$b (Nat_poly$ Nat_poly$) Nat_poly$) -(declare-fun poly_shift$ (Nat$ Complex_poly$) Complex_poly$) -(declare-fun offset_poly$ (Complex_poly$ Complex$) Complex_poly$) -(declare-fun poly_cutoff$ (Nat$ Complex_poly$) Complex_poly$) -(declare-fun rsquarefree$ (Complex_poly$) Bool) -(declare-fun offset_poly$a (Nat_poly$ Nat$) Nat_poly$) -(declare-fun reflect_poly$ (Complex_poly$) Complex_poly$) -(declare-fun reflect_poly$a (Complex_poly_poly$) Complex_poly_poly$) -(declare-fun reflect_poly$b (Nat_poly$) Nat_poly$) -(declare-fun synthetic_div$ (Complex_poly$ Complex$) Complex_poly$) -(assert (! (not (= (poly$ (power$ q$ n$)) (poly$ r$))) :named a0)) -(assert (! (forall ((?v0 Complex$)) (= (poly$ (power$ q$ n$) ?v0) (poly$ r$ ?v0))) :named a1)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$) (?v2 Complex_poly$)) (= (poly$a (power$a ?v0 ?v1) ?v2) (power$ (poly$a ?v0 ?v2) ?v1))) :named a2)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$) (?v2 Nat$)) (= (poly$b (power$b ?v0 ?v1) ?v2) (power$c (poly$b ?v0 ?v2) ?v1))) :named a3)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex$)) (= (poly$ (power$ ?v0 ?v1) ?v2) (power$d (poly$ ?v0 ?v2) ?v1))) :named a4)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (poly$ ?v0) (poly$ ?v1)) (= ?v0 ?v1))) :named a5)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (constant$ (poly$ ?v0))) (exists ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)))) :named a6)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (reflect_poly$ (power$ ?v0 ?v1)) (power$ (reflect_poly$ ?v0) ?v1))) :named a7)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$)) (= (coeff$ (power$a ?v0 ?v1) zero$a) (power$ (coeff$ ?v0 zero$a) ?v1))) :named a8)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (= (coeff$a (power$b ?v0 ?v1) zero$a) (power$c (coeff$a ?v0 zero$a) ?v1))) :named a9)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (coeff$b (power$ ?v0 ?v1) zero$a) (power$d (coeff$b ?v0 zero$a) ?v1))) :named a10)) -(assert (! (forall ((?v0 (-> Complex$ Complex$))) (= (constant$ ?v0) (forall ((?v1 Complex$) (?v2 Complex$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a11)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (exists ((?v2 Complex_poly$)) (and (= (psize$ ?v2) (psize$ ?v0)) (forall ((?v3 Complex$)) (= (poly$ ?v2 ?v3) (poly$ ?v0 (plus$ ?v1 ?v3))))))) :named a12)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex$)) (= (poly$ (offset_poly$ ?v0 ?v1) ?v2) (poly$ ?v0 (plus$ ?v1 ?v2)))) :named a13)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$) (?v2 Nat$)) (= (poly$b (offset_poly$a ?v0 ?v1) ?v2) (poly$b ?v0 (plus$a ?v1 ?v2)))) :named a14)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex$)) (= (poly$ (pcompose$ ?v0 ?v1) ?v2) (poly$ ?v0 (poly$ ?v1 ?v2)))) :named a15)) -(assert (! (forall ((?v0 Complex_poly$)) (= (power$ ?v0 one$) ?v0)) :named a16)) -(assert (! (forall ((?v0 Nat$)) (= (power$c ?v0 one$) ?v0)) :named a17)) -(assert (! (forall ((?v0 Nat$)) (= (power$ one$a ?v0) one$a)) :named a18)) -(assert (! (forall ((?v0 Nat$)) (= (power$c one$ ?v0) one$)) :named a19)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$)) (= (coeff$ (power$a ?v0 ?v1) (degree$ (power$a ?v0 ?v1))) (power$ (coeff$ ?v0 (degree$ ?v0)) ?v1))) :named a20)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (= (coeff$a (power$b ?v0 ?v1) (degree$a (power$b ?v0 ?v1))) (power$c (coeff$a ?v0 (degree$a ?v0)) ?v1))) :named a21)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (coeff$b (power$ ?v0 ?v1) (degree$b (power$ ?v0 ?v1))) (power$d (coeff$b ?v0 (degree$b ?v0)) ?v1))) :named a22)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$ zero$b ?v0) zero$c)) :named a23)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$a zero$d ?v0) zero$a)) :named a24)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$b zero$c ?v0) zero$)) :named a25)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (coeff$a (plus$b ?v0 ?v1) ?v2) (plus$a (coeff$a ?v0 ?v2) (coeff$a ?v1 ?v2)))) :named a26)) -(assert (! (forall ((?v0 Complex_poly$)) (= (poly$a zero$b ?v0) zero$c)) :named a27)) -(assert (! (forall ((?v0 Nat$)) (= (poly$b zero$d ?v0) zero$a)) :named a28)) -(assert (! (forall ((?v0 Complex$)) (= (poly$ zero$c ?v0) zero$)) :named a29)) -(assert (! (= (degree$b one$a) zero$a) :named a30)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex$)) (= (poly$ (plus$c ?v0 ?v1) ?v2) (plus$ (poly$ ?v0 ?v2) (poly$ ?v1 ?v2)))) :named a31)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (poly$b (plus$b ?v0 ?v1) ?v2) (plus$a (poly$b ?v0 ?v2) (poly$b ?v1 ?v2)))) :named a32)) -(assert (! (forall ((?v0 Complex$)) (= (poly$ one$a ?v0) one$b)) :named a33)) -(assert (! (forall ((?v0 Nat$)) (= (poly$b one$c ?v0) one$)) :named a34)) -(assert (! (forall ((?v0 Complex_poly$)) (= (= (coeff$b ?v0 (degree$b ?v0)) zero$) (= ?v0 zero$c))) :named a35)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (coeff$ ?v0 (degree$ ?v0)) zero$c) (= ?v0 zero$b))) :named a36)) -(assert (! (forall ((?v0 Nat_poly$)) (= (= (coeff$a ?v0 (degree$a ?v0)) zero$a) (= ?v0 zero$d))) :named a37)) -(assert (! (= (coeff$b one$a (degree$b one$a)) one$b) :named a38)) -(assert (! (= (coeff$a one$c (degree$a one$c)) one$) :named a39)) -(assert (! (forall ((?v0 Complex_poly$)) (= (= (poly$ (reflect_poly$ ?v0) zero$) zero$) (= ?v0 zero$c))) :named a40)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (poly$a (reflect_poly$a ?v0) zero$c) zero$c) (= ?v0 zero$b))) :named a41)) -(assert (! (forall ((?v0 Nat_poly$)) (= (= (poly$b (reflect_poly$b ?v0) zero$a) zero$a) (= ?v0 zero$d))) :named a42)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= (coeff$b ?v0 zero$a) zero$)) (= (reflect_poly$ (reflect_poly$ ?v0)) ?v0))) :named a43)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= (coeff$ ?v0 zero$a) zero$c)) (= (reflect_poly$a (reflect_poly$a ?v0)) ?v0))) :named a44)) -(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= (coeff$a ?v0 zero$a) zero$a)) (= (reflect_poly$b (reflect_poly$b ?v0)) ?v0))) :named a45)) -(assert (! (forall ((?v0 Complex_poly$)) (= (= (coeff$b (reflect_poly$ ?v0) zero$a) zero$) (= ?v0 zero$c))) :named a46)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (coeff$ (reflect_poly$a ?v0) zero$a) zero$c) (= ?v0 zero$b))) :named a47)) -(assert (! (forall ((?v0 Nat_poly$)) (= (= (coeff$a (reflect_poly$b ?v0) zero$a) zero$a) (= ?v0 zero$d))) :named a48)) -(assert (! (forall ((?v0 Complex_poly$)) (= (coeff$b (reflect_poly$ ?v0) zero$a) (coeff$b ?v0 (degree$b ?v0)))) :named a49)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= (coeff$b ?v0 zero$a) zero$)) (= (degree$b (reflect_poly$ ?v0)) (degree$b ?v0)))) :named a50)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= (coeff$ ?v0 zero$a) zero$c)) (= (degree$ (reflect_poly$a ?v0)) (degree$ ?v0)))) :named a51)) -(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= (coeff$a ?v0 zero$a) zero$a)) (= (degree$a (reflect_poly$b ?v0)) (degree$a ?v0)))) :named a52)) -(assert (! (forall ((?v0 Complex_poly$)) (= (poly$ (reflect_poly$ ?v0) zero$) (coeff$b ?v0 (degree$b ?v0)))) :named a53)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (poly$a (reflect_poly$a ?v0) zero$c) (coeff$ ?v0 (degree$ ?v0)))) :named a54)) -(assert (! (forall ((?v0 Nat_poly$)) (= (poly$b (reflect_poly$b ?v0) zero$a) (coeff$a ?v0 (degree$a ?v0)))) :named a55)) -(assert (! (forall ((?v0 Complex_poly$)) (= (poly$ ?v0 zero$) (coeff$b ?v0 zero$a))) :named a56)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (poly$a ?v0 zero$c) (coeff$ ?v0 zero$a))) :named a57)) -(assert (! (forall ((?v0 Nat_poly$)) (= (poly$b ?v0 zero$a) (coeff$a ?v0 zero$a))) :named a58)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (coeff$a (plus$b ?v0 ?v1) ?v2) (plus$a (coeff$a ?v0 ?v2) (coeff$a ?v1 ?v2)))) :named a59)) -(assert (! (forall ((?v0 Complex_poly$)) (= (forall ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)) (= ?v0 zero$c))) :named a60)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (forall ((?v1 Complex_poly$)) (= (poly$a ?v0 ?v1) zero$c)) (= ?v0 zero$b))) :named a61)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$ zero$b ?v0) zero$c)) :named a62)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$a zero$d ?v0) zero$a)) :named a63)) -(assert (! (forall ((?v0 Nat$)) (= (coeff$b zero$c ?v0) zero$)) :named a64)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= ?v0 zero$b)) (not (= (coeff$ ?v0 (degree$ ?v0)) zero$c)))) :named a65)) -(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= ?v0 zero$d)) (not (= (coeff$a ?v0 (degree$a ?v0)) zero$a)))) :named a66)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= ?v0 zero$c)) (not (= (coeff$b ?v0 (degree$b ?v0)) zero$)))) :named a67)) -(assert (! (forall ((?v0 Complex_poly$)) (! (= (power$ ?v0 zero$a) one$a) :pattern ((power$ ?v0)))) :named a68)) -(assert (! (forall ((?v0 Nat$)) (! (= (power$c ?v0 zero$a) one$) :pattern ((power$c ?v0)))) :named a69)) -(assert (! (forall ((?v0 Nat$)) (= (power$d zero$ ?v0) (ite (= ?v0 zero$a) one$b zero$))) :named a70)) -(assert (! (forall ((?v0 Nat$)) (= (power$ zero$c ?v0) (ite (= ?v0 zero$a) one$a zero$c))) :named a71)) -(assert (! (forall ((?v0 Nat$)) (= (power$c zero$a ?v0) (ite (= ?v0 zero$a) one$ zero$a))) :named a72)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (degree$b (offset_poly$ ?v0 ?v1)) (degree$b ?v0))) :named a73)) -(assert (! (forall ((?v0 Complex_poly$)) (= (constant$ (poly$ ?v0)) (= (degree$b ?v0) zero$a))) :named a74)) -(assert (! (forall ((?v0 Complex$)) (= zero$ (poly$ zero$c ?v0))) :named a75)) -(assert (! (forall ((?v0 Complex_poly$)) (= zero$c (poly$a zero$b ?v0))) :named a76)) -(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex$)) (and (= (poly$ ?v0 ?v1) zero$) (not (= (poly$ zero$c ?v1) zero$)))) false)) :named a77)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (exists ((?v1 Complex_poly$)) (and (= (poly$a ?v0 ?v1) zero$c) (not (= (poly$a zero$b ?v1) zero$c)))) false)) :named a78)) -(assert (! (forall ((?v0 Nat_poly$)) (= (exists ((?v1 Nat$)) (and (= (poly$b ?v0 ?v1) zero$a) (not (= (poly$b zero$d ?v1) zero$a)))) false)) :named a79)) -(assert (! (= (exists ((?v0 Complex_poly$)) (not (= (poly$a zero$b ?v0) zero$c))) false) :named a80)) -(assert (! (= (exists ((?v0 Nat$)) (not (= (poly$b zero$d ?v0) zero$a))) false) :named a81)) -(assert (! (= (exists ((?v0 Complex$)) (not (= (poly$ zero$c ?v0) zero$))) false) :named a82)) -(assert (! (= (exists ((?v0 Complex_poly$)) (= (poly$a zero$b ?v0) zero$c)) true) :named a83)) -(assert (! (= (exists ((?v0 Nat$)) (= (poly$b zero$d ?v0) zero$a)) true) :named a84)) -(assert (! (= (exists ((?v0 Complex$)) (= (poly$ zero$c ?v0) zero$)) true) :named a85)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (not (= (power$d ?v0 ?v1) zero$)))) :named a86)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (not (= (power$ ?v0 ?v1) zero$c)))) :named a87)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (not (= ?v0 zero$a)) (not (= (power$c ?v0 ?v1) zero$a)))) :named a88)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a89)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a90)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a91)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a92)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a93)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a94)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= (plus$ ?v0 ?v1) ?v1) (= ?v0 zero$))) :named a95)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (plus$c ?v0 ?v1) ?v1) (= ?v0 zero$c))) :named a96)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) ?v1) (= ?v0 zero$a))) :named a97)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= (plus$ ?v0 ?v1) ?v0) (= ?v1 zero$))) :named a98)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (plus$c ?v0 ?v1) ?v0) (= ?v1 zero$c))) :named a99)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) ?v0) (= ?v1 zero$a))) :named a100)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v1 ?v0)) (= ?v1 zero$))) :named a101)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v1 ?v0)) (= ?v1 zero$c))) :named a102)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v1 ?v0)) (= ?v1 zero$a))) :named a103)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v0 ?v1)) (= ?v1 zero$))) :named a104)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v0 ?v1)) (= ?v1 zero$c))) :named a105)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v0 ?v1)) (= ?v1 zero$a))) :named a106)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) zero$a) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a107)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= zero$a (plus$a ?v0 ?v1)) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a108)) -(assert (! (forall ((?v0 Complex_poly$)) (! (= (power$ ?v0 zero$a) one$a) :pattern ((power$ ?v0)))) :named a109)) -(assert (! (forall ((?v0 Nat$)) (! (= (power$c ?v0 zero$a) one$) :pattern ((power$c ?v0)))) :named a110)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a111)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a112)) -(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ zero$c ?v0) zero$c)) :named a113)) -(assert (! (= (reflect_poly$ zero$c) zero$c) :named a114)) -(assert (! (= (degree$b zero$c) zero$a) :named a115)) -(assert (! (forall ((?v0 Complex_poly$)) (= (= (psize$ ?v0) zero$a) (= ?v0 zero$c))) :named a116)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (offset_poly$ ?v0 ?v1) zero$c) (= ?v0 zero$c))) :named a117)) -(assert (! (forall ((?v0 Complex$)) (= (offset_poly$ zero$c ?v0) zero$c)) :named a118)) -(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex$)) (not (= (poly$ ?v0 ?v1) zero$))) (not (= ?v0 zero$c)))) :named a119)) -(assert (! (forall ((?v0 Complex$)) (= (= zero$ ?v0) (= ?v0 zero$))) :named a120)) -(assert (! (forall ((?v0 Complex_poly$)) (= (= zero$c ?v0) (= ?v0 zero$c))) :named a121)) -(assert (! (forall ((?v0 Nat$)) (= (= zero$a ?v0) (= ?v0 zero$a))) :named a122)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a123)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a124)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a ?v1 (plus$a ?v0 ?v2)))) :named a125)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 ?v1) (plus$a ?v1 ?v0))) :named a126)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a127)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (= (plus$a (plus$a ?v0 ?v1) (plus$a ?v2 ?v3)) (plus$a (plus$a ?v0 ?v2) (plus$a ?v1 ?v3)))) :named a128)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a129)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a ?v1 (plus$a ?v0 ?v2)))) :named a130)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a (plus$a ?v0 ?v2) ?v1))) :named a131)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 ?v1) (plus$a ?v1 ?v0))) :named a132)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a (plus$a ?v0 ?v1) ?v2))) :named a133)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (=> (and (= ?v0 ?v1) (= ?v2 ?v3)) (= (plus$a ?v0 ?v2) (plus$a ?v1 ?v3)))) :named a134)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a135)) -(assert (! (forall ((?v0 Nat$)) (= (= one$ ?v0) (= ?v0 one$))) :named a136)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v0 ?v1)) (= ?v1 zero$))) :named a137)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v0 ?v1)) (= ?v1 zero$c))) :named a138)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v0 ?v1)) (= ?v1 zero$a))) :named a139)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a140)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a141)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a142)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a143)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a144)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a145)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a146)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a147)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a148)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a149)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a150)) -(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a151)) -(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a152)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a153)) -(assert (! (forall ((?v0 Complex_poly$)) (= (power$ ?v0 one$) ?v0)) :named a154)) -(assert (! (forall ((?v0 Nat$)) (= (power$c ?v0 one$) ?v0)) :named a155)) -(assert (! (forall ((?v0 Nat$)) (= (poly_cutoff$ ?v0 one$a) (ite (= ?v0 zero$a) zero$c one$a))) :named a156)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a157)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) zero$a) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a158)) -(assert (! (forall ((?v0 Nat$)) (= (poly_shift$ ?v0 one$a) (ite (= ?v0 zero$a) one$a zero$c))) :named a159)) -(assert (! (not (= zero$ one$b)) :named a160)) -(assert (! (not (= zero$c one$a)) :named a161)) -(assert (! (not (= zero$a one$)) :named a162)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (synthetic_div$ ?v0 ?v1) zero$c) (= (degree$b ?v0) zero$a))) :named a163)) -(assert (! (= (of_bool$ false) zero$) :named a164)) -(assert (! (= (of_bool$a false) zero$c) :named a165)) -(assert (! (= (of_bool$b false) zero$a) :named a166)) -(assert (! (= (of_bool$b true) one$) :named a167)) -(assert (! (forall ((?v0 Complex$)) (= (synthetic_div$ zero$c ?v0) zero$c)) :named a168)) -(assert (! (forall ((?v0 Nat$)) (= (poly_shift$ ?v0 zero$c) zero$c)) :named a169)) -(assert (! (forall ((?v0 Nat$)) (= (poly_cutoff$ ?v0 zero$c) zero$c)) :named a170)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a171)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a172)) -(assert (! (forall ((?v0 Bool)) (! (= (of_bool$ ?v0) (ite ?v0 one$b zero$)) :pattern ((of_bool$ ?v0)))) :named a173)) -(assert (! (forall ((?v0 Bool)) (! (= (of_bool$a ?v0) (ite ?v0 one$a zero$c)) :pattern ((of_bool$a ?v0)))) :named a174)) -(assert (! (forall ((?v0 Bool)) (! (= (of_bool$b ?v0) (ite ?v0 one$ zero$a)) :pattern ((of_bool$b ?v0)))) :named a175)) -(assert (! (forall ((?v0 (-> Complex$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$ ?v1)) (and (=> ?v1 (?v0 one$b)) (=> (not ?v1) (?v0 zero$))))) :named a176)) -(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$a ?v1)) (and (=> ?v1 (?v0 one$a)) (=> (not ?v1) (?v0 zero$c))))) :named a177)) -(assert (! (forall ((?v0 (-> Nat$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$b ?v1)) (and (=> ?v1 (?v0 one$)) (=> (not ?v1) (?v0 zero$a))))) :named a178)) -(assert (! (forall ((?v0 (-> Complex$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$ ?v1)) (not (or (and ?v1 (not (?v0 one$b))) (and (not ?v1) (not (?v0 zero$))))))) :named a179)) -(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$a ?v1)) (not (or (and ?v1 (not (?v0 one$a))) (and (not ?v1) (not (?v0 zero$c))))))) :named a180)) -(assert (! (forall ((?v0 (-> Nat$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$b ?v1)) (not (or (and ?v1 (not (?v0 one$))) (and (not ?v1) (not (?v0 zero$a))))))) :named a181)) -(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a182)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (= (plus$a ?v0 ?v1) ?v0) (= ?v1 zero$a))) :named a183)) -(assert (! (forall ((?v0 Nat$)) (=> (and (=> (= ?v0 zero$a) false) (=> (not (= ?v0 zero$a)) false)) false)) :named a184)) -(assert (! (forall ((?v0 (-> Nat$ (-> Nat$ Bool))) (?v1 Nat$) (?v2 Nat$)) (=> (and (forall ((?v3 Nat$) (?v4 Nat$)) (= (?v0 ?v3 ?v4) (?v0 ?v4 ?v3))) (and (forall ((?v3 Nat$)) (?v0 ?v3 zero$a)) (forall ((?v3 Nat$) (?v4 Nat$)) (=> (?v0 ?v3 ?v4) (?v0 ?v3 (plus$a ?v3 ?v4)))))) (?v0 ?v1 ?v2))) :named a185)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (forall ((?v2 Complex$)) (=> (= (poly$ ?v0 ?v2) zero$) (= (poly$ ?v1 ?v2) zero$))) (or (dvd$ ?v0 (power$ ?v1 (degree$b ?v0))) (and (= ?v0 zero$c) (= ?v1 zero$c))))) :named a186)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Nat$)) (=> (and (forall ((?v3 Complex$)) (=> (= (poly$ ?v0 ?v3) zero$) (= (poly$ ?v1 ?v3) zero$))) (and (= (degree$b ?v0) ?v2) (not (= ?v2 zero$a)))) (dvd$ ?v0 (power$ ?v1 ?v2)))) :named a187)) -(assert (! (forall ((?v0 Complex_poly$)) (! (= (is_zero$ ?v0) (= ?v0 zero$c)) :pattern ((is_zero$ ?v0)))) :named a188)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (poly$ ?v0 ?v1) zero$) (or (= ?v0 zero$c) (not (= (order$ ?v1 ?v0) zero$a))))) :named a189)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (= (= (poly$a ?v0 ?v1) zero$c) (or (= ?v0 zero$b) (not (= (order$a ?v1 ?v0) zero$a))))) :named a190)) -(assert (! (forall ((?v0 Complex$)) (dvd$a ?v0 zero$)) :named a191)) -(assert (! (forall ((?v0 Complex_poly$)) (dvd$ ?v0 zero$c)) :named a192)) -(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 zero$a)) :named a193)) -(assert (! (forall ((?v0 Complex$)) (= (dvd$a zero$ ?v0) (= ?v0 zero$))) :named a194)) -(assert (! (forall ((?v0 Complex_poly$)) (= (dvd$ zero$c ?v0) (= ?v0 zero$c))) :named a195)) -(assert (! (forall ((?v0 Nat$)) (= (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a196)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$ ?v0 (plus$c ?v0 ?v1)) (dvd$ ?v0 ?v1))) :named a197)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b ?v0 (plus$a ?v0 ?v1)) (dvd$b ?v0 ?v1))) :named a198)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$ ?v0 (plus$c ?v1 ?v0)) (dvd$ ?v0 ?v1))) :named a199)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b ?v0 (plus$a ?v1 ?v0)) (dvd$b ?v0 ?v1))) :named a200)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (not (= ?v0 zero$a)) (= (dvd$b (power$c ?v1 ?v0) (power$c ?v2 ?v0)) (dvd$b ?v1 ?v2)))) :named a201)) -(assert (! (forall ((?v0 Complex$)) (=> (dvd$a zero$ ?v0) (= ?v0 zero$))) :named a202)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (dvd$ zero$c ?v0) (= ?v0 zero$c))) :named a203)) -(assert (! (forall ((?v0 Nat$)) (=> (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a204)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (= (dvd$ ?v0 (plus$c ?v1 ?v2)) (dvd$ ?v0 ?v2)))) :named a205)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (= (dvd$b ?v0 (plus$a ?v1 ?v2)) (dvd$b ?v0 ?v2)))) :named a206)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (= (dvd$ ?v0 (plus$c ?v2 ?v1)) (dvd$ ?v0 ?v2)))) :named a207)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (= (dvd$b ?v0 (plus$a ?v2 ?v1)) (dvd$b ?v0 ?v2)))) :named a208)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v0 ?v2)) (dvd$ ?v0 (plus$c ?v1 ?v2)))) :named a209)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v0 ?v2)) (dvd$b ?v0 (plus$a ?v1 ?v2)))) :named a210)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v1 one$a)) (dvd$ ?v0 one$a))) :named a211)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v1 one$)) (dvd$b ?v0 one$))) :named a212)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (dvd$ ?v0 one$a) (dvd$ ?v0 ?v1))) :named a213)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (dvd$b ?v0 one$) (dvd$b ?v0 ?v1))) :named a214)) -(assert (! (forall ((?v0 Complex_poly$)) (dvd$ one$a ?v0)) :named a215)) -(assert (! (forall ((?v0 Nat$)) (dvd$b one$ ?v0)) :named a216)) -(assert (! (forall ((?v0 Complex_poly$)) (dvd$ ?v0 ?v0)) :named a217)) -(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 ?v0)) :named a218)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v1 ?v2)) (dvd$ ?v0 ?v2))) :named a219)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v1 ?v2)) (dvd$b ?v0 ?v2))) :named a220)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Nat$)) (=> (dvd$ ?v0 ?v1) (dvd$ (power$ ?v0 ?v2) (power$ ?v1 ?v2)))) :named a221)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (dvd$b (power$c ?v0 ?v2) (power$c ?v1 ?v2)))) :named a222)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b (power$c ?v0 ?v1) (power$c ?v2 ?v1)) (not (= ?v1 zero$a))) (dvd$b ?v0 ?v2))) :named a223)) -(assert (! (not (dvd$ zero$c one$a)) :named a224)) -(assert (! (not (dvd$b zero$a one$)) :named a225)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (dvd$ (power$ ?v0 ?v1) one$a) (or (dvd$ ?v0 one$a) (= ?v1 zero$a)))) :named a226)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b (power$c ?v0 ?v1) one$) (or (dvd$b ?v0 one$) (= ?v1 zero$a)))) :named a227)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (! (=> (not (= (poly$ ?v0 ?v1) zero$)) (= (order$ ?v1 ?v0) zero$a)) :pattern ((order$ ?v1 ?v0)))) :named a228)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (! (=> (not (= (poly$a ?v0 ?v1) zero$c)) (= (order$a ?v1 ?v0) zero$a)) :pattern ((order$a ?v1 ?v0)))) :named a229)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= ?v0 zero$c)) (= (dvd$ ?v0 one$a) (= (degree$b ?v0) zero$a)))) :named a230)) -(assert (! (forall ((?v0 Complex_poly$)) (= (rsquarefree$ ?v0) (and (not (= ?v0 zero$c)) (forall ((?v1 Complex$)) (or (= (order$ ?v1 ?v0) zero$a) (= (order$ ?v1 ?v0) one$)))))) :named a231)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex_poly$)) (=> (not (= ?v0 zero$c)) (= (exists ((?v3 Complex$)) (and (= (poly$ (pCons$ ?v1 ?v0) ?v3) zero$) (not (= (poly$ ?v2 ?v3) zero$)))) (not (dvd$ (pCons$ ?v1 ?v0) (power$ ?v2 (psize$ ?v0))))))) :named a232)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (! (= (dvd$a ?v0 ?v1) (=> (= ?v0 zero$) (= ?v1 zero$))) :pattern ((dvd$a ?v0 ?v1)))) :named a233)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (dvd$ ?v0 one$a) (= (monom$ (coeff$b ?v0 (degree$b ?v0)) zero$a) ?v0))) :named a234)) -(assert (! (forall ((?v0 Nat$)) (= (dvd$b ?v0 one$) (= ?v0 one$))) :named a235)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$) (?v3 Complex_poly$)) (= (= (pCons$ ?v0 ?v1) (pCons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a236)) -(assert (! (= (pCons$ zero$ zero$c) zero$c) :named a237)) -(assert (! (= (pCons$a zero$c zero$b) zero$b) :named a238)) -(assert (! (= (pCons$b zero$a zero$d) zero$d) :named a239)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly_poly$)) (= (= (pCons$a ?v0 ?v1) zero$b) (and (= ?v0 zero$c) (= ?v1 zero$b)))) :named a240)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$)) (= (= (pCons$b ?v0 ?v1) zero$d) (and (= ?v0 zero$a) (= ?v1 zero$d)))) :named a241)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (= (pCons$ ?v0 ?v1) zero$c) (and (= ?v0 zero$) (= ?v1 zero$c)))) :named a242)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (coeff$b (pCons$ ?v0 ?v1) zero$a) ?v0)) :named a243)) -(assert (! (forall ((?v0 Nat$)) (= (monom$ zero$ ?v0) zero$c)) :named a244)) -(assert (! (forall ((?v0 Nat$)) (= (monom$a zero$c ?v0) zero$b)) :named a245)) -(assert (! (forall ((?v0 Nat$)) (= (monom$b zero$a ?v0) zero$d)) :named a246)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (= (monom$a ?v0 ?v1) zero$b) (= ?v0 zero$c))) :named a247)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (monom$b ?v0 ?v1) zero$d) (= ?v0 zero$a))) :named a248)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (= (monom$ ?v0 ?v1) zero$c) (= ?v0 zero$))) :named a249)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$))) :named a250)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$ (monom$a ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$c))) :named a251)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$a (monom$b ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$a))) :named a252)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$) (?v3 Complex_poly$)) (= (plus$c (pCons$ ?v0 ?v1) (pCons$ ?v2 ?v3)) (pCons$ (plus$ ?v0 ?v2) (plus$c ?v1 ?v3)))) :named a253)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$) (?v2 Nat$) (?v3 Nat_poly$)) (= (plus$b (pCons$b ?v0 ?v1) (pCons$b ?v2 ?v3)) (pCons$b (plus$a ?v0 ?v2) (plus$b ?v1 ?v3)))) :named a254)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) (degree$b (monom$ ?v0 ?v1))) ?v0)) :named a255)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (= (order$ zero$ (monom$ ?v0 ?v1)) ?v1))) :named a256)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (= (order$a zero$c (monom$a ?v0 ?v1)) ?v1))) :named a257)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (pcompose$ (pCons$ ?v0 zero$c) ?v1) (pCons$ ?v0 zero$c))) :named a258)) -(assert (! (forall ((?v0 Complex$)) (= (reflect_poly$ (pCons$ ?v0 zero$c)) (pCons$ ?v0 zero$c))) :named a259)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$)) (= (synthetic_div$ (pCons$ ?v0 ?v1) ?v2) (pCons$ (poly$ ?v1 ?v2) (synthetic_div$ ?v1 ?v2)))) :named a260)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (= ?v0 zero$c) (= (coeff$b (pCons$ ?v1 ?v0) (degree$b (pCons$ ?v1 ?v0))) ?v1))) :named a261)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (not (= ?v0 zero$c)) (= (coeff$b (pCons$ ?v1 ?v0) (degree$b (pCons$ ?v1 ?v0))) (coeff$b ?v0 (degree$b ?v0))))) :named a262)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$c (pCons$a ?v0 zero$b) (pCons$a ?v1 zero$b)) (dvd$ ?v0 ?v1))) :named a263)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$d (pCons$b ?v0 zero$d) (pCons$b ?v1 zero$d)) (dvd$b ?v0 ?v1))) :named a264)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (dvd$ (pCons$ ?v0 zero$c) (pCons$ ?v1 zero$c)) (dvd$a ?v0 ?v1))) :named a265)) -(assert (! (= (= (pCons$b one$ zero$d) one$c) true) :named a266)) -(assert (! (= (= (pCons$ one$b zero$c) one$a) true) :named a267)) -(assert (! (= (= one$c (pCons$b one$ zero$d)) true) :named a268)) -(assert (! (= (= one$a (pCons$ one$b zero$c)) true) :named a269)) -(assert (! (= (monom$b one$ zero$a) one$c) :named a270)) -(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ ?v0 (pCons$ zero$ (pCons$ one$b zero$c))) ?v0)) :named a271)) -(assert (! (forall ((?v0 Complex_poly_poly$)) (= (pcompose$a ?v0 (pCons$a zero$c (pCons$a one$a zero$b))) ?v0)) :named a272)) -(assert (! (forall ((?v0 Nat_poly$)) (= (pcompose$b ?v0 (pCons$b zero$a (pCons$b one$ zero$d))) ?v0)) :named a273)) -(assert (! (forall ((?v0 Nat$)) (=> (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a274)) -(assert (! (forall ((?v0 Nat$)) (= (not (= ?v0 zero$a)) (and (dvd$b ?v0 zero$a) (not (= ?v0 zero$a))))) :named a275)) -(assert (! (forall ((?v0 Nat$)) (! (= (dvd$b zero$a ?v0) (= ?v0 zero$a)) :pattern ((dvd$b zero$a ?v0)))) :named a276)) -(assert (! (forall ((?v0 Nat$)) (not (and (dvd$b zero$a ?v0) (not (= zero$a ?v0))))) :named a277)) -(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 zero$a)) :named a278)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex_poly$)) (= (= (monom$a ?v0 ?v1) (pCons$a ?v2 zero$b)) (and (= ?v0 ?v2) (or (= ?v0 zero$c) (= ?v1 zero$a))))) :named a279)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (monom$b ?v0 ?v1) (pCons$b ?v2 zero$d)) (and (= ?v0 ?v2) (or (= ?v0 zero$a) (= ?v1 zero$a))))) :named a280)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Complex$)) (= (= (monom$ ?v0 ?v1) (pCons$ ?v2 zero$c)) (and (= ?v0 ?v2) (or (= ?v0 zero$) (= ?v1 zero$a))))) :named a281)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (forall ((?v1 Complex$) (?v2 Complex_poly$)) (=> (= ?v0 (pCons$ ?v1 ?v2)) false)) false)) :named a282)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (forall ((?v1 Complex$) (?v2 Complex_poly$)) (=> (= ?v0 (pCons$ ?v1 ?v2)) false)) false)) :named a283)) -(assert (! (forall ((?v0 (-> Complex_poly$ (-> Complex_poly$ Bool))) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (?v0 zero$c zero$c) (forall ((?v3 Complex$) (?v4 Complex_poly$) (?v5 Complex$) (?v6 Complex_poly$)) (=> (?v0 ?v4 ?v6) (?v0 (pCons$ ?v3 ?v4) (pCons$ ?v5 ?v6))))) (?v0 ?v1 ?v2))) :named a284)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Complex$) (?v3 Nat$)) (= (= (monom$ ?v0 ?v1) (monom$ ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$) (= ?v1 ?v3))))) :named a285)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex_poly$) (?v3 Nat$)) (= (= (monom$a ?v0 ?v1) (monom$a ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$c) (= ?v1 ?v3))))) :named a286)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (= (= (monom$b ?v0 ?v1) (monom$b ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$a) (= ?v1 ?v3))))) :named a287)) -(assert (! (forall ((?v0 Complex$)) (! (= (monom$ ?v0 zero$a) (pCons$ ?v0 zero$c)) :pattern ((monom$ ?v0)))) :named a288)) -(assert (! (forall ((?v0 (-> Complex_poly_poly$ Bool)) (?v1 Complex_poly_poly$)) (=> (and (?v0 zero$b) (forall ((?v2 Complex_poly$) (?v3 Complex_poly_poly$)) (=> (and (or (not (= ?v2 zero$c)) (not (= ?v3 zero$b))) (?v0 ?v3)) (?v0 (pCons$a ?v2 ?v3))))) (?v0 ?v1))) :named a289)) -(assert (! (forall ((?v0 (-> Nat_poly$ Bool)) (?v1 Nat_poly$)) (=> (and (?v0 zero$d) (forall ((?v2 Nat$) (?v3 Nat_poly$)) (=> (and (or (not (= ?v2 zero$a)) (not (= ?v3 zero$d))) (?v0 ?v3)) (?v0 (pCons$b ?v2 ?v3))))) (?v0 ?v1))) :named a290)) -(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Complex_poly$)) (=> (and (?v0 zero$c) (forall ((?v2 Complex$) (?v3 Complex_poly$)) (=> (and (or (not (= ?v2 zero$)) (not (= ?v3 zero$c))) (?v0 ?v3)) (?v0 (pCons$ ?v2 ?v3))))) (?v0 ?v1))) :named a291)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (= (poly$ ?v0 ?v1) zero$) (= (poly$ (pCons$ zero$ ?v0) ?v1) zero$))) :named a292)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (=> (= (poly$a ?v0 ?v1) zero$c) (= (poly$a (pCons$a zero$c ?v0) ?v1) zero$c))) :named a293)) -(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (=> (= (poly$b ?v0 ?v1) zero$a) (= (poly$b (pCons$b zero$a ?v0) ?v1) zero$a))) :named a294)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (= (degree$b (monom$ ?v0 ?v1)) ?v1))) :named a295)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (= (degree$ (monom$a ?v0 ?v1)) ?v1))) :named a296)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (not (= ?v0 zero$a)) (= (degree$a (monom$b ?v0 ?v1)) ?v1))) :named a297)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$))) :named a298)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$ (monom$a ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$c))) :named a299)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$a (monom$b ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$a))) :named a300)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (dvd$ ?v0 (pCons$ zero$ ?v1)))) :named a301)) -(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly_poly$)) (=> (dvd$c ?v0 ?v1) (dvd$c ?v0 (pCons$a zero$c ?v1)))) :named a302)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (poly$ (pCons$ (poly$ zero$c ?v0) zero$c) ?v1) (poly$ zero$c ?v1))) :named a303)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= ?v0 (poly$ (pCons$ ?v0 zero$c) ?v1))) :named a304)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$b (monom$b ?v0 ?v1) (monom$b ?v2 ?v1)) (monom$b (plus$a ?v0 ?v2) ?v1))) :named a305)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (offset_poly$ (pCons$ ?v0 zero$c) ?v1) (pCons$ ?v0 zero$c))) :named a306)) -(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex_poly$)) (= (poly$a (pCons$a ?v0 zero$b) ?v1) zero$c)) (= ?v0 zero$c))) :named a307)) -(assert (! (forall ((?v0 Nat$)) (= (exists ((?v1 Nat$)) (= (poly$b (pCons$b ?v0 zero$d) ?v1) zero$a)) (= ?v0 zero$a))) :named a308)) -(assert (! (forall ((?v0 Complex$)) (= (exists ((?v1 Complex$)) (= (poly$ (pCons$ ?v0 zero$c) ?v1) zero$)) (= ?v0 zero$))) :named a309)) -(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex_poly$)) (not (= (poly$a (pCons$a ?v0 zero$b) ?v1) zero$c))) (not (= ?v0 zero$c)))) :named a310)) -(assert (! (forall ((?v0 Nat$)) (= (exists ((?v1 Nat$)) (not (= (poly$b (pCons$b ?v0 zero$d) ?v1) zero$a))) (not (= ?v0 zero$a)))) :named a311)) -(assert (! (forall ((?v0 Complex$)) (= (exists ((?v1 Complex$)) (not (= (poly$ (pCons$ ?v0 zero$c) ?v1) zero$))) (not (= ?v0 zero$)))) :named a312)) -(assert (! (forall ((?v0 Complex$)) (= (poly$ (pCons$ zero$ zero$c) ?v0) (poly$ zero$c ?v0))) :named a313)) -(assert (! (forall ((?v0 Complex_poly$)) (= (poly$a (pCons$a zero$c zero$b) ?v0) (poly$a zero$b ?v0))) :named a314)) -(assert (! (forall ((?v0 Complex$)) (= (degree$b (pCons$ ?v0 zero$c)) zero$a)) :named a315)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (and (= (degree$b ?v0) zero$a) (forall ((?v1 Complex$)) (=> (= ?v0 (pCons$ ?v1 zero$c)) false))) false)) :named a316)) -(assert (! (= (pCons$b one$ zero$d) one$c) :named a317)) -(assert (! (= (pCons$ one$b zero$c) one$a) :named a318)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (monom$b ?v0 ?v1) one$c) (and (= ?v0 one$) (= ?v1 zero$a)))) :named a319)) -(assert (! (forall ((?v0 Complex$)) (= ?v0 (poly$ (pCons$ zero$ (pCons$ one$b zero$c)) ?v0))) :named a320)) -(assert (! (forall ((?v0 Complex_poly$)) (= ?v0 (poly$a (pCons$a zero$c (pCons$a one$a zero$b)) ?v0))) :named a321)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (not (exists ((?v1 Complex$) (?v2 Complex_poly$)) (and (not (= ?v1 zero$)) (and (= ?v2 zero$c) (= ?v0 (pCons$ ?v1 ?v2)))))) (exists ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)))) :named a322)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex$)) (=> (not (= ?v0 zero$c)) (exists ((?v3 Complex$)) (= (poly$ (pCons$ ?v1 (pCons$ ?v2 ?v0)) ?v3) zero$)))) :named a323)) -(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly_poly$)) (= (dvd$c (pCons$a ?v0 zero$b) ?v1) (forall ((?v2 Nat$)) (dvd$ ?v0 (coeff$ ?v1 ?v2))))) :named a324)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$)) (= (dvd$d (pCons$b ?v0 zero$d) ?v1) (forall ((?v2 Nat$)) (dvd$b ?v0 (coeff$a ?v1 ?v2))))) :named a325)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (dvd$ (pCons$ ?v0 zero$c) ?v1) (forall ((?v2 Nat$)) (dvd$a ?v0 (coeff$b ?v1 ?v2))))) :named a326)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (degree$a (power$b (pCons$b ?v0 (pCons$b one$ zero$d)) ?v1)) ?v1)) :named a327)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (degree$b (power$ (pCons$ ?v0 (pCons$ one$b zero$c)) ?v1)) ?v1)) :named a328)) -(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ ?v0 zero$c) (pCons$ (coeff$b ?v0 zero$a) zero$c))) :named a329)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (coeff$a (power$b (pCons$b ?v0 (pCons$b one$ zero$d)) ?v1) ?v1) one$)) :named a330)) -(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (coeff$b (power$ (pCons$ ?v0 (pCons$ one$b zero$c)) ?v1) ?v1) one$b)) :named a331)) -(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (dvd$ (pCons$ ?v0 ?v1) one$a) (and (= ?v1 zero$c) (not (= ?v0 zero$))))) :named a332)) -(assert (! (forall ((?v0 Complex$)) (=> (not (= ?v0 zero$)) (dvd$ (pCons$ ?v0 zero$c) one$a))) :named a333)) -(assert (! (forall ((?v0 Complex_poly$)) (=> (and (dvd$ ?v0 one$a) (forall ((?v1 Complex$)) (=> (and (= ?v0 (monom$ ?v1 zero$a)) (not (= ?v1 zero$))) false))) false)) :named a334)) -(assert (! (forall ((?v0 Complex$)) (=> (not (= ?v0 zero$)) (dvd$ (monom$ ?v0 zero$a) one$a))) :named a335)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (times$ ?v0 ?v1) (times$ ?v2 ?v1)) (or (= ?v0 ?v2) (= ?v1 zero$a)))) :named a336)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (times$ ?v0 ?v1) (times$ ?v0 ?v2)) (or (= ?v1 ?v2) (= ?v0 zero$a)))) :named a337)) -(assert (! (forall ((?v0 Nat$)) (! (= (times$ ?v0 zero$a) zero$a) :pattern ((times$ ?v0)))) :named a338)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) zero$a) (or (= ?v0 zero$a) (= ?v1 zero$a)))) :named a339)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ ?v0) (suc$ ?v1)) (= ?v0 ?v1))) :named a340)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ ?v0) (suc$ ?v1)) (= ?v0 ?v1))) :named a341)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) one$) (and (= ?v0 one$) (= ?v1 one$)))) :named a342)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= one$ (times$ ?v0 ?v1)) (and (= ?v0 one$) (= ?v1 one$)))) :named a343)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) (suc$ zero$a)) (and (= ?v0 (suc$ zero$a)) (= ?v1 (suc$ zero$a))))) :named a344)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ zero$a) (times$ ?v0 ?v1)) (and (= ?v0 (suc$ zero$a)) (= ?v1 (suc$ zero$a))))) :named a345)) -(assert (! (forall ((?v0 Nat$)) (! (= (power$c (suc$ zero$a) ?v0) (suc$ zero$a)) :pattern ((power$c (suc$ zero$a) ?v0)))) :named a346)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (power$c ?v0 ?v1) (suc$ zero$a)) (or (= ?v1 zero$a) (= ?v0 (suc$ zero$a))))) :named a347)) -(assert (! (forall ((?v0 Nat$)) (less_eq$ zero$a ?v0)) :named a348)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (less_eq$ (suc$ ?v0) (suc$ ?v1)) (less_eq$ ?v0 ?v1))) :named a349)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 (suc$ ?v1)) (suc$ (plus$a ?v0 ?v1)))) :named a350)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (! (= (times$ ?v0 (suc$ ?v1)) (plus$a ?v0 (times$ ?v0 ?v1))) :pattern ((times$ ?v0 (suc$ ?v1))))) :named a351)) -(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (less_eq$ (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (less_eq$ ?v1 ?v2))) :named a352)) -(check-sat) diff --git a/test/regress/regress1/ho/ho-exponential-model.smt2 b/test/regress/regress1/ho/ho-exponential-model.smt2 deleted file mode 100644 index 3f0011828..000000000 --- a/test/regress/regress1/ho/ho-exponential-model.smt2 +++ /dev/null @@ -1,40 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: sat -(set-logic UFLIA) -(set-info :status sat) -(declare-fun f1 (Int Int Int Int) Int) -(declare-fun f2 (Int Int Int) Int) -(declare-fun f3 (Int Int) Int) -(declare-fun f4 (Int) Int) -(declare-fun f5 (Int Int Int) Int) -(declare-fun f6 (Int Int) Int) -(declare-fun f7 (Int) Int) - - -(assert (= (f1 0) (f1 1))) -(assert (= (f1 1) f2)) - -(assert (= (f2 0) (f2 1))) -(assert (= (f2 1) f3)) - -(assert (= (f3 0) (f3 1))) -(assert (= (f3 1) f4)) - -(assert (= (f4 0) (f4 1))) -(assert (= (f4 1) 2)) - - -(assert (= (f1 3) (f1 4))) -(assert (= (f1 4) f5)) - -(assert (= (f5 3) (f5 4))) -(assert (= (f5 4) f6)) - -(assert (= (f6 3) (f6 4))) -(assert (= (f6 4) f7)) - -(assert (= (f7 3) (f7 4))) -(assert (= (f7 4) 5)) - -; this benchmark has a concise model representation for f1 if we use curried (tree-like) models for UF -(check-sat) diff --git a/test/regress/regress1/ho/ho-matching-enum-2.smt2 b/test/regress/regress1/ho/ho-matching-enum-2.smt2 deleted file mode 100644 index 9581e4c4f..000000000 --- a/test/regress/regress1/ho/ho-matching-enum-2.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) - -(declare-sort U 0) - -(declare-fun p (Int) Bool) -(declare-fun q (Int) Bool) -(declare-fun k (Int Int) Int) - -(assert (q (k 0 1))) -(assert (not (p (k 0 0)))) - -(assert (forall ((f (-> Int Int Int)) (y Int) (z Int)) (or (p (f y z)) (not (q (f z y)))))) - -(check-sat) -(exit) diff --git a/test/regress/regress1/ho/ho-std-fmf.smt2 b/test/regress/regress1/ho/ho-std-fmf.smt2 deleted file mode 100644 index 61d82d00c..000000000 --- a/test/regress/regress1/ho/ho-std-fmf.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -; EXPECT: sat -(set-logic UF) -(set-info :status sat) -(declare-sort U 0) -(declare-fun P (U U) Bool) -(declare-fun Q (U U) Bool) -(declare-fun R (U U) Bool) -(declare-fun a () U) -(declare-fun b () U) - -; can solve this using standard MBQI model for P = \ xy true -(assert (forall ((x U) (y U)) (or (P x y) (Q x y)))) -(assert (forall ((x U) (y U)) (or (P x y) (R x y)))) - -(assert (not (= a b))) -(assert (= (Q a) (R b))) -(check-sat) diff --git a/test/regress/regress1/ho/hoa0008.smt2 b/test/regress/regress1/ho/hoa0008.smt2 deleted file mode 100644 index f4833aadf..000000000 --- a/test/regress/regress1/ho/hoa0008.smt2 +++ /dev/null @@ -1,68 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic ALL) -(declare-sort A$ 0) -(declare-sort Com$ 0) -(declare-sort Loc$ 0) -(declare-sort Nat$ 0) -(declare-sort Pname$ 0) -(declare-sort State$ 0) -(declare-sort Vname$ 0) -(declare-sort Literal$ 0) -(declare-sort Natural$ 0) -(declare-sort Typerep$ 0) -(declare-sort A_triple$ 0) -(declare-sort Com_option$ 0) -(declare-fun p$ () (-> A$ (-> State$ Bool))) -(declare-fun q$ () (-> A$ (-> State$ Bool))) -(declare-fun pn$ () Pname$) -(declare-fun wt$ (Com$) Bool) -(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$) -(declare-fun suc$ (Nat$) Nat$) -(declare-fun the$ (Com_option$) Com$) -(declare-fun body$ (Pname$) Com$) -(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$) -(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$) -(declare-fun none$ () Com_option$) -(declare-fun plus$ (Nat$ Nat$) Nat$) -(declare-fun semi$ (Com$ Com$) Com$) -(declare-fun size$ (A_triple$) Nat$) -(declare-fun skip$ () Com$) -(declare-fun some$ (Com$) Com_option$) -(declare-fun suc$a (Natural$) Natural$) -(declare-fun zero$ () Nat$) -(declare-fun body$a (Pname$) Com_option$) -(declare-fun evalc$ (Com$ State$ State$) Bool) -(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool) -(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$) -(declare-fun plus$a (Natural$ Natural$) Natural$) -(declare-fun size$a (Com$) Nat$) -(declare-fun size$b (Natural$) Nat$) -(declare-fun size$c (Bool) Nat$) -(declare-fun size$d (Com_option$) Nat$) -(declare-fun size$e (Typerep$) Nat$) -(declare-fun size$f (Literal$) Nat$) -(declare-fun while$ ((-> State$ Bool) Com$) Com$) -(declare-fun zero$a () Natural$) -(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$) -(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$)) -(declare-fun size_com$ (Com$) Nat$) -(declare-fun size_bool$ (Bool) Nat$) -(declare-fun wT_bodies$ () Bool) -(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$)) -(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$) -(declare-fun size_natural$ (Natural$) Nat$) -(declare-fun triple_valid$ (Nat$ A_triple$) Bool) -(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0)) - -(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6)) - -(assert (! (= (size_bool$ true) zero$) :named a13)) -(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14)) - -(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37)) - -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204)) - -(check-sat) -;(get-proof) diff --git a/test/regress/regress1/ho/match-middle.smt2 b/test/regress/regress1/ho/match-middle.smt2 deleted file mode 100644 index 0485f9a6f..000000000 --- a/test/regress/regress1/ho/match-middle.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -; COMMAND-LINE: --uf-ho -; EXPECT: unsat -(set-logic UFLIA) -(set-info :status unsat) -(declare-fun f (Int Int Int) Int) -(declare-fun h (Int Int Int) Int) -(declare-fun g (Int Int) Int) -(declare-fun a () Int) -(declare-fun b () Int) -(declare-fun c () Int) -(declare-fun d () Int) - -(assert (or (= (f a) g) (= (h a) g))) - -(assert (= (f a b d) c)) -(assert (= (h a b d) c)) - -(assert (forall ((x Int) (y Int)) (not (= (g x y) c)))) - -(check-sat) diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 new file mode 100644 index 000000000..1670e0711 --- /dev/null +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -0,0 +1,101 @@ +; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat + +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort mu 0) +(declare-fun meq_ind (mu mu $$unsorted) Bool) +(assert (= meq_ind (lambda ((X mu) (Y mu) (W $$unsorted)) (= X Y)))) +(declare-fun meq_prop ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= meq_prop (lambda ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (W $$unsorted)) (= (X W) (Y W))))) +(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W))))) +(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (Phi W) (Psi W))))) +(declare-fun mand ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mand (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mor (mnot Phi) (mnot Psi)) __flatten_var_0)))) +(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0)))) +(declare-fun mimplied ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplied (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Psi) Phi __flatten_var_0)))) +(declare-fun mequiv ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mequiv (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mand (mimplies Phi Psi) (mimplies Psi Phi) __flatten_var_0)))) +(declare-fun mxor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mxor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mequiv Phi Psi) __flatten_var_0)))) +(declare-fun mforall_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_ind (lambda ((Phi (-> mu $$unsorted Bool)) (W $$unsorted)) (forall ((X mu)) (Phi X W) )))) +(declare-fun mforall_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_prop (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) (forall ((P (-> $$unsorted Bool))) (Phi P W) )))) +(declare-fun mexists_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mexists_ind (lambda ((Phi (-> mu $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mnot (Phi X) __flatten_var_0))) __flatten_var_0)))) +(declare-fun mexists_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool) +(assert (= mexists_prop (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mforall_prop (lambda ((P (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (Phi P) __flatten_var_0))) __flatten_var_0)))) +(declare-fun mtrue ($$unsorted) Bool) +(assert (= mtrue (lambda ((W $$unsorted)) true))) +(declare-fun mfalse ($$unsorted) Bool) +(assert (= mfalse (mnot mtrue))) +(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) +(declare-fun mdia ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mdia (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mbox R (mnot Phi)) __flatten_var_0)))) +(declare-fun mreflexive ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mreflexive (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (R S S) )))) +(declare-fun msymmetric ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= msymmetric (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted)) (=> (R S T) (R T S)) )))) +(declare-fun mserial ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mserial (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (exists ((T $$unsorted)) (R S T) ) )))) +(declare-fun mtransitive ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mtransitive (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R T U)) (R S U)) )))) +(declare-fun meuclidean ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= meuclidean (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (R T U)) )))) +(declare-fun mpartially_functional ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mpartially_functional (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (= T U)) )))) +(declare-fun mfunctional ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mfunctional (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (exists ((T $$unsorted)) (and (R S T) (forall ((U $$unsorted)) (=> (R S U) (= T U)) )) ) )))) +(declare-fun mweakly_dense ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_dense (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (R S T) (exists ((U $$unsorted)) (and (R S U) (R U T)) )) )))) +(declare-fun mweakly_connected ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_connected (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (or (R T U) (= T U) (R U T))) )))) +(declare-fun mweakly_directed ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_directed (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (exists ((V $$unsorted)) (and (R T V) (R U V)) )) )))) +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) +(declare-fun minvalid ((-> $$unsorted Bool)) Bool) +(assert (= minvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (not (Phi W)) )))) +(declare-fun msatisfiable ((-> $$unsorted Bool)) Bool) +(assert (= msatisfiable (lambda ((Phi (-> $$unsorted Bool))) (exists ((W $$unsorted)) (Phi W) )))) +(declare-fun mcountersatisfiable ((-> $$unsorted Bool)) Bool) +(assert (= mcountersatisfiable (lambda ((Phi (-> $$unsorted Bool))) (exists ((W $$unsorted)) (not (Phi W)) )))) +(declare-fun a1 ($$unsorted $$unsorted) Bool) +(declare-fun a2 ($$unsorted $$unsorted) Bool) +(declare-fun a3 ($$unsorted $$unsorted) Bool) +(declare-fun jan () mu) +(declare-fun piotr () mu) +(declare-fun cola () mu) +(declare-fun pepsi () mu) +(declare-fun beer () mu) +(declare-fun likes (mu mu $$unsorted) Bool) +(declare-fun very_much_likes (mu mu $$unsorted) Bool) +(declare-fun possibly_likes (mu mu $$unsorted) Bool) +(assert (mvalid (mbox a1 (likes jan cola)))) +(assert (mvalid (mbox a1 (likes piotr pepsi)))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a1 (mimplies (mdia a1 (likes X pepsi)) (likes X cola)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a1 (mimplies (mdia a1 (likes X cola)) (likes X pepsi)) __flatten_var_0))))) +(assert (mvalid (mbox a2 (likes jan pepsi)))) +(assert (mvalid (mbox a1 (likes piotr cola)))) +(assert (mvalid (mbox a1 (likes piotr beer)))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a2 (mimplies (likes X pepsi) (likes X cola)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a2 (mimplies (likes X cola) (likes X pepsi)) __flatten_var_0))))) +(assert (mvalid (mbox a3 (likes jan cola)))) +(assert (mvalid (mdia a3 (likes piotr pepsi)))) +(assert (mvalid (mdia a1 (likes piotr beer)))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mbox a3 (mimplies (mand (likes X Y) (mand (mbox a1 (likes X Y)) (mbox a2 (likes X Y)))) (very_much_likes X Y)) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mbox a3 (very_much_likes X Y)) (very_much_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a3 (very_much_likes X Y)) (likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a1 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a2 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a3 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (not (mvalid (very_much_likes jan cola)))) +(meta-info :filename "AGT034^2") + +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 new file mode 100644 index 000000000..9211adfb5 --- /dev/null +++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 @@ -0,0 +1,50 @@ +; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models +; EXPECT: sat + + +(set-logic ALL) +(declare-sort $$unsorted 0) + +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) + +(declare-fun mforall_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_prop + (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) + (forall ((P (-> $$unsorted Bool))) (Phi P W) )))) + +(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W))))) + +(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mor + (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) + (or (Phi W) (Psi W))))) + +(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplies + (lambda ( + (Phi (-> $$unsorted Bool)) + (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) + (mor (mnot Phi) Psi __flatten_var_0)))) + +(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mbox + (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) + (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) + +(assert (not (forall ((R (-> $$unsorted $$unsorted Bool))) + (mvalid + (mforall_prop + (lambda ((A (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) + (mforall_prop + (lambda ((B (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) + (mimplies + (mbox R (mor A B)) + (mor + (mbox R A) + (mbox R B)) + __flatten_var_0)) + __flatten_var_0)))) ))) + +(check-sat) diff --git a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p new file mode 100644 index 000000000..baabd675a --- /dev/null +++ b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -0,0 +1,63 @@ +% COMMAND-LINE: --uf-ho --finite-model-find +% EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta + +%------------------------------------------------------------------------------ +% File : SYO362^5 : TPTP v7.2.0. Released v4.0.0. +% Domain : Syntactic +% Problem : TPS problem THM631A +% Version : Especial. +% English : If a set function preserves unions, then it is monotone. + +% Refs : [Bro09] Brown (2009), Email to Geoff Sutcliffe +% Source : [Bro09] +% Names : tps_0419 [Bro09] +% : THM631 [TPS] +% : THM631A [TPS] + +% Status : Theorem +% Rating : 0.22 v7.2.0, 0.12 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.20 v6.2.0, 0.29 v6.1.0, 0.14 v6.0.0, 0.29 v5.5.0, 0.50 v5.4.0, 0.60 v5.3.0, 0.80 v4.1.0, 1.00 v4.0.0 +% Syntax : Number of formulae : 2 ( 0 unit; 1 type; 0 defn) +% Number of atoms : 22 ( 1 equality; 16 variable) +% Maximal formula depth : 9 ( 6 average) +% Number of connectives : 19 ( 0 ~; 2 |; 0 &; 13 @) +% ( 0 <=>; 4 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 7 ( 7 >; 0 *; 0 +; 0 <<) +% Number of symbols : 3 ( 1 :; 0 =) +% Number of variables : 8 ( 0 sgn; 6 !; 0 ?; 2 ^) +% ( 8 :; 0 !>; 0 ?*) +% ( 0 @-; 0 @+) +% SPC : TH0_THM_EQU_NAR + +% Comments : This problem is from the TPS library. Copyright (c) 2009 The TPS +% project in the Department of Mathematical Sciences at Carnegie +% Mellon University. Distributed under the Creative Commons copyleft +% license: http://creativecommons.org/licenses/by-sa/3.0/ +% : Polymorphic definitions expanded. +% : +%------------------------------------------------------------------------------ +thf(cK,type,( + cK: ( $i > $o ) > $i > $o )). + +thf(cTHM631A_pme,conjecture, + ( ! [X: $i > $o,Y: $i > $o] : + ( ( cK + @ ^ [Xz: $i] : + ( ( X @ Xz ) + | ( Y @ Xz ) ) ) + = ( ^ [Xw: $i] : + ( ( cK @ X @ Xw ) + | ( cK @ Y @ Xw ) ) ) ) + => ! [X: $i > $o,Y: $i > $o] : + ( ! [Xx: $i] : + ( ( X @ Xx ) + => ( Y @ Xx ) ) + => ! [Xx: $i] : + ( ( cK @ X @ Xx ) + => ( cK @ Y @ Xx ) ) ) )). + +%------------------------------------------------------------------------------ + +%% soundness issue (since resolved) was due to wrong lambda +%% lifting. Free variables in lambda body not being carried out to +%% quantified formula standing for lambda lifting diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p new file mode 100644 index 000000000..d67eb8dad --- /dev/null +++ b/test/regress/regress1/ho/store-ax-min.p @@ -0,0 +1,28 @@ +% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim-store-ax +% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% EXPECT: % SZS status Theorem for store-ax-min + +thf(a, type, (a: $i)). +thf(b, type, (b: $i)). + +%% thf(blah1, axiom, ( ! [X: $i, Y: $i] : (X = Y))). + +thf(blah2, axiom, ( ~ (a = b))). + +%% thf(storeax, axiom, ( +%% ! [F : $i > $i, D : $i, R : $i] : +%% ( +%% ? [G : $i > $i] : +%% ( +%% ! [X : $i] : +%% ( +%% (G @ X) = $ite( X = D, R, F @ X) +%% ) +%% ) +%% ) + + +%% (~ (X = Y))) +%% ). + +thf(blah, conjecture, ( ? [F : $i > $i, G : $i > $i] : (~ (F = G)))). |