|
1 #2 := false |
|
2 decl uf_6 :: (-> T4 T2) |
|
3 decl uf_10 :: T4 |
|
4 #39 := uf_10 |
|
5 #44 := (uf_6 uf_10) |
|
6 decl uf_2 :: (-> T1 T2) |
|
7 decl uf_7 :: T1 |
|
8 #34 := uf_7 |
|
9 #43 := (uf_2 uf_7) |
|
10 #45 := (= #43 #44) |
|
11 decl uf_4 :: (-> T3 T2 T4) |
|
12 decl uf_8 :: T2 |
|
13 #35 := uf_8 |
|
14 decl uf_9 :: T3 |
|
15 #36 := uf_9 |
|
16 #40 := (uf_4 uf_9 uf_8) |
|
17 #204 := (uf_6 #40) |
|
18 #598 := (= #204 #44) |
|
19 #595 := (= #44 #204) |
|
20 #41 := (= uf_10 #40) |
|
21 decl uf_1 :: (-> T2 T3 T1) |
|
22 #37 := (uf_1 uf_8 uf_9) |
|
23 #38 := (= uf_7 #37) |
|
24 #42 := (and #38 #41) |
|
25 #109 := [asserted]: #42 |
|
26 #114 := [and-elim #109]: #41 |
|
27 #256 := [monotonicity #114]: #595 |
|
28 #599 := [symm #256]: #598 |
|
29 #596 := (= #43 #204) |
|
30 #269 := (= uf_8 #204) |
|
31 #23 := (:var 0 T2) |
|
32 #22 := (:var 1 T3) |
|
33 #24 := (uf_4 #22 #23) |
|
34 #643 := (pattern #24) |
|
35 #25 := (uf_6 #24) |
|
36 #86 := (= #23 #25) |
|
37 #644 := (forall (vars (?x5 T3) (?x6 T2)) (:pat #643) #86) |
|
38 #90 := (forall (vars (?x5 T3) (?x6 T2)) #86) |
|
39 #647 := (iff #90 #644) |
|
40 #645 := (iff #86 #86) |
|
41 #646 := [refl]: #645 |
|
42 #648 := [quant-intro #646]: #647 |
|
43 #119 := (~ #90 #90) |
|
44 #144 := (~ #86 #86) |
|
45 #145 := [refl]: #144 |
|
46 #120 := [nnf-pos #145]: #119 |
|
47 #26 := (= #25 #23) |
|
48 #27 := (forall (vars (?x5 T3) (?x6 T2)) #26) |
|
49 #91 := (iff #27 #90) |
|
50 #88 := (iff #26 #86) |
|
51 #89 := [rewrite]: #88 |
|
52 #92 := [quant-intro #89]: #91 |
|
53 #85 := [asserted]: #27 |
|
54 #95 := [mp #85 #92]: #90 |
|
55 #146 := [mp~ #95 #120]: #90 |
|
56 #649 := [mp #146 #648]: #644 |
|
57 #613 := (not #644) |
|
58 #619 := (or #613 #269) |
|
59 #609 := [quant-inst]: #619 |
|
60 #267 := [unit-resolution #609 #649]: #269 |
|
61 #600 := (= #43 uf_8) |
|
62 #289 := (uf_2 #37) |
|
63 #259 := (= #289 uf_8) |
|
64 #296 := (= uf_8 #289) |
|
65 #17 := (:var 0 T3) |
|
66 #16 := (:var 1 T2) |
|
67 #18 := (uf_1 #16 #17) |
|
68 #636 := (pattern #18) |
|
69 #28 := (uf_2 #18) |
|
70 #94 := (= #16 #28) |
|
71 #650 := (forall (vars (?x7 T2) (?x8 T3)) (:pat #636) #94) |
|
72 #98 := (forall (vars (?x7 T2) (?x8 T3)) #94) |
|
73 #653 := (iff #98 #650) |
|
74 #651 := (iff #94 #94) |
|
75 #652 := [refl]: #651 |
|
76 #654 := [quant-intro #652]: #653 |
|
77 #121 := (~ #98 #98) |
|
78 #147 := (~ #94 #94) |
|
79 #148 := [refl]: #147 |
|
80 #122 := [nnf-pos #148]: #121 |
|
81 #29 := (= #28 #16) |
|
82 #30 := (forall (vars (?x7 T2) (?x8 T3)) #29) |
|
83 #99 := (iff #30 #98) |
|
84 #96 := (iff #29 #94) |
|
85 #97 := [rewrite]: #96 |
|
86 #100 := [quant-intro #97]: #99 |
|
87 #93 := [asserted]: #30 |
|
88 #103 := [mp #93 #100]: #98 |
|
89 #149 := [mp~ #103 #122]: #98 |
|
90 #655 := [mp #149 #654]: #650 |
|
91 #615 := (not #650) |
|
92 #616 := (or #615 #296) |
|
93 #617 := [quant-inst]: #616 |
|
94 #618 := [unit-resolution #617 #655]: #296 |
|
95 #597 := [symm #618]: #259 |
|
96 #611 := (= #43 #289) |
|
97 #113 := [and-elim #109]: #38 |
|
98 #252 := [monotonicity #113]: #611 |
|
99 #601 := [trans #252 #597]: #600 |
|
100 #602 := [trans #601 #267]: #596 |
|
101 #238 := [trans #602 #599]: #45 |
|
102 #46 := (not #45) |
|
103 #110 := [asserted]: #46 |
|
104 [unit-resolution #110 #238]: false |
|
105 unsat |