blob: 4fe5926381b733edc66f8bfc2660092c6e336c30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
; COMMAND-LINE: --finite-model-find --mbqi=gen-ev
; EXPECT: sat
(benchmark Isabelle
:status sat
:logic AUFLIA
:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18)
:extrafuns (
(f1 S1)
(f2 S1)
(f3 S2 S3 S4)
(f4 S2)
(f5 S3)
(f6 S4)
(f7 S3 S5 S1)
(f8 S6 S5)
(f9 S6)
(f10 S7 S6 S6)
(f11 S7)
(f12 S8 S4 S4)
(f13 S8)
(f14 S10 S3 S3)
(f15 S11 S9 S10)
(f16 S12 S4 S11)
(f17 S12)
(f18 S4 S13 S1)
(f19 S13)
(f20 S4 S1)
(f21 S2)
(f22 S10)
(f23 S3 S9 S1)
(f24 S14 S9 S9)
(f25 S15 S4 S14)
(f26 S15)
(f27 S13)
(f28 S8)
(f29 S16 S9 S3)
(f30 S17 S4 S16)
(f31 S18 S4 S17)
(f32 S18)
(f33 S18)
(f34 S4 S4 S1)
)
:assumption (not (= f1 f2))
:assumption (not (not (= (f3 f4 f5) f6)))
:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) )
:assumption (= (f7 f5 (f8 (f10 f11 f9))) f1)
:assumption (forall (?v0 S4) (iff (= f6 ?v0) (= ?v0 f6)) )
:assumption (= (f12 f13 f6) f6)
:assumption (forall (?v0 S4) (iff (= f6 (f12 f13 ?v0)) (= ?v0 f6)) )
:assumption (forall (?v0 S4) (iff (= (f12 f13 ?v0) f6) (= ?v0 f6)) )
:assumption (forall (?v0 S4) (?v1 S9) (?v2 S3) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) )
:assumption (= (f18 f6 f19) f1)
:assumption (= (f20 f6) f1)
:assumption (forall (?v0 S4) (iff (= (f20 ?v0) f1) (= ?v0 f6)) )
:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) )
:assumption (forall (?v0 S3) (implies (not (not (= (f3 f21 ?v0) f6))) (implies (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) )
:assumption (forall (?v0 S4) (?v1 S4) (iff (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) )
:assumption (forall (?v0 S6) (?v1 S9) (implies (forall (?v2 S3) (implies (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6)))) (iff (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))) (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))))) )
:assumption (forall (?v0 S4) (= (f18 (f12 f13 ?v0) f27) f1) )
:assumption (= (f12 f28 f6) f6)
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) )
:assumption (= (f18 f6 f27) f1)
:assumption (forall (?v0 S3) (?v1 S4) (?v2 S9) (implies (not (not (= (f3 f21 ?v0) f6))) (iff (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) )
:assumption (forall (?v0 S4) (iff (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) )
:assumption (forall (?v0 S4) (iff (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5))) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5))) )
:assumption (forall (?v0 S4) (= (f34 ?v0 ?v0) f1) )
:assumption (forall (?v0 S4) (?v1 S4) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )
:assumption (forall (?v0 S4) (?v1 S4) (?v2 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) )
:assumption (forall (?v0 S4) (?v1 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) )
:formula true)
; solver: z3
; timeout: 1.897
; random seed: 1
; arguments:
; DISPLAY_PROOF=true
; PROOF_MODE=2
; -rs:1
; MODEL=true
; -smt
|
