## Bug #14

Bug #13: Wrong CL result

### Strange CL result

Status:
Closed
Priority:
Normal
Assignee:
-
Start date:
05/09/2014
Due date:
% Done:

0%

Description

What would tatl do?

### History

#### #1 Updated by Thorsten Wißmannabout 5 years ago

Tatl claims the solution to be satisfiable:

```         ----------------------------------------------
|           TATL : Tableaux for ATL          |
|          Amelie David - Lab. IBISC         |
|     23 bd de France -  91037 Evry Cedex    |
----------------------------------------------

*
* The formula is satisfiable.
*

*
* Pre-tableau
**************

P0: ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p)
Succ: S1
P1: ~~c
Succ: S6
P2: ~~~c
Succ: S5
P3: T
Succ: S4
P4: p\/~p
Succ: S2 ; S3
S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
Succ: (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->P1 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->P2 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->P3 ; (0,0,0,0,0)->P4
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->P3
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->P3
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->P3
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->P3
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->P3
*
* Tableau
**********

S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
Succ: (0,0,0,0,0)->S2 ; (0,0,0,0,0)->S3 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->S4 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->S5 ; (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->S6
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->S4
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->S4
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->S4
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->S4
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
Succ: (0,0,0,0,0)->S4
```

#### #2 Updated by Thorsten Wißmannabout 5 years ago

• Status changed from New to Closed

Also available in: Atom PDF