equal
deleted
inserted
replaced
1 #2 := false |
|
2 decl uf_6 :: T2 |
|
3 #23 := uf_6 |
|
4 decl uf_4 :: T2 |
|
5 #19 := uf_4 |
|
6 #25 := (= uf_4 uf_6) |
|
7 decl uf_2 :: (-> T1 T2) |
|
8 decl uf_1 :: (-> T2 T3 T1) |
|
9 decl uf_5 :: T3 |
|
10 #20 := uf_5 |
|
11 #21 := (uf_1 uf_4 uf_5) |
|
12 #22 := (uf_2 #21) |
|
13 #24 := (= #22 uf_6) |
|
14 #65 := [asserted]: #24 |
|
15 #143 := (= uf_4 #22) |
|
16 #11 := (:var 0 T3) |
|
17 #10 := (:var 1 T2) |
|
18 #12 := (uf_1 #10 #11) |
|
19 #567 := (pattern #12) |
|
20 #16 := (uf_2 #12) |
|
21 #58 := (= #10 #16) |
|
22 #574 := (forall (vars (?x4 T2) (?x5 T3)) (:pat #567) #58) |
|
23 #62 := (forall (vars (?x4 T2) (?x5 T3)) #58) |
|
24 #577 := (iff #62 #574) |
|
25 #575 := (iff #58 #58) |
|
26 #576 := [refl]: #575 |
|
27 #578 := [quant-intro #576]: #577 |
|
28 #71 := (~ #62 #62) |
|
29 #87 := (~ #58 #58) |
|
30 #88 := [refl]: #87 |
|
31 #72 := [nnf-pos #88]: #71 |
|
32 #17 := (= #16 #10) |
|
33 #18 := (forall (vars (?x4 T2) (?x5 T3)) #17) |
|
34 #63 := (iff #18 #62) |
|
35 #60 := (iff #17 #58) |
|
36 #61 := [rewrite]: #60 |
|
37 #64 := [quant-intro #61]: #63 |
|
38 #57 := [asserted]: #18 |
|
39 #67 := [mp #57 #64]: #62 |
|
40 #89 := [mp~ #67 #72]: #62 |
|
41 #579 := [mp #89 #578]: #574 |
|
42 #214 := (not #574) |
|
43 #551 := (or #214 #143) |
|
44 #553 := [quant-inst]: #551 |
|
45 #233 := [unit-resolution #553 #579]: #143 |
|
46 #235 := [trans #233 #65]: #25 |
|
47 #26 := (not #25) |
|
48 #66 := [asserted]: #26 |
|
49 [unit-resolution #66 #235]: false |
|
50 unsat |
|