1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003-2005, Renate Schmidt,  University of Manchester
    4%           2009-2010, Ullrich Hustadt, University of Liverpool
    5%
    6%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    7
    8%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    9%
   10% problems(+ProblemClassId, +ProblemList)
   11%
   12%     Classification of problems
   13
   14
   15problems(routine, [
   16    1, 2, 3, 4, 5, 6, 7, 8, 9, 
   17    14, 15, 16, 17, 18, 19, 
   18    20, 22, 23, 24, 25, 26, 28, 29, 
   19    30, 31, 33, 34, 35, 36, 37, 38, 39,
   20    40, 41, 42, 44, 45, 46, 47, 48, 49,
   21    51, 52, 53, 54, 55, 56, 57, 58, 59,
   22    60, 61, 63, 64, 65, 66, 67, 68, 69,
   23    70, 71, 72, 73, 74, 75, 76, 77, 78, 79,
   24    80, 81, 82, 83, 84, 85, 88, 89, 
   25    90, 91, 92, 93, 94, 95, 96, 97, 98, 99,
   26   100, 101, 102, 103, 104, 105, 106, 107
   27]).
   28
   29% remove problems difficult for complement splitting rules:
   30problems(routine_cs, Set) :-
   31    problems(routine, Routine),
   32    list_difference(Routine, [
   33        41, 
   34        60, 61, 62, 63, 64
   35], Set).
   36
   37% remove problems difficult for 3 way complement splitting rules:
   38problems(routine_cs3, Set) :-
   39    problems(routine_cs, Routine),
   40    list_difference(Routine, [
   41        21, 22, 51,
   42        67
   43], Set).
   44
   45problems(routine_w_test, [
   46    43,
   47    50,
   48    71
   49]).
   50
   51problems(difficult, [
   52    12, 
   53    27,
   54    32,
   55    62,
   56    86, 87
   57]).
   58
   59problems(very_difficult, [
   60    10, 11, 13,
   61    21
   62]).
   63
   64%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   65%
   66% problem(+ProblemId, +ExpectedResult, -Result)
   67%
   68%     Collection of problems together with ExpectedResult (satisfiable,
   69%     unsatisfiable or unknown)
   70
   71% unsatisfiable
   72problem(1, unsatisfiable, Result) :- 
   73    satisfiable(
   74        not(
   75            equiv(box(comp(a,b),p), box(a,box(b,p)))
   76    ), Result).
   77
   78% unsatisfiable
   79problem(2, unsatisfiable, Result) :- 
   80    satisfiable(
   81        not(
   82            implies(box(or(a,b),p), and(box(a,p), box(b,p)))
   83    ), Result).
   84
   85% unsatisfiable
   86problem(3, unsatisfiable, Result) :- 
   87    satisfiable(not(
   88        implies(box(star(a),p), and(p, box(star(a),p)))
   89    ), Result).
   90
   91% De Giacomo, Massacci (2000), p. 127, Fig. 6
   92% unsatisfiable
   93problem(4, unsatisfiable, Result) :- 
   94    satisfiable(and(dia(comp(b,star(a)),p),
   95            box(comp(star(b),star(a)), not(p))
   96    ), Result).
   97
   98% De Giacomo, Massacci (2000), p. 127, Fig. 7
   99% satisfiable
  100problem(5, satisfiable, Result) :- 
  101    satisfiable(and(not(p), and(
  102            box(star(b),dia(b,not(p))),
  103    box(star(b),dia(star(a),p))
  104    )), Result).
  105
  106problem(6, satisfiable, Result) :- 
  107    satisfiable(and(not(p), and(
  108            box(star(b),dia(b,not(p))),
  109    box(star(b),dia(star(a),not(p)))
  110    )), Result).
  111
  112% Dima's example
  113problem(7, satisfiable, Result) :- 
  114    satisfiable(
  115        and(dia(star(comp(star(a),b)),p),
  116            box(star(comp(a,comp(star(a), b))), not(p)))
  117    , Result).
  118
  119% Dima's example
  120problem(8, satisfiable, Result) :- 
  121    satisfiable(
  122        and(dia(star(comp(star(a),b)),p),
  123            box(star(comp(b,comp(star(b), star(a)))), not(p)))
  124    , Result).
  125
  126problem(9, satisfiable, Result) :- 
  127    satisfiable(and(
  128        dia(b,dia(b,not(p))),dia(c,p)
  129    ), Result).
  130
  131% Ullrich's example
  132problem(10, satisfiable, Result) :- 
  133    satisfiable(
  134        and(p2,
  135        and( or(or(p5, p3), p4),
  136        and( or(or(p5, not(p2)), not(p3)),  
  137        and( or(or(p1, p3), p4),
  138        and( or(or(not(p4), not(p5)), p3),  
  139        and( or(or(not(p3), not(p4)), not(p5)),  
  140        and( or(or(p3, p2), not(p1)),
  141        and( or(or(p2, not(p5)), not(p3)),  
  142        and( or(or(not(p1), p3), p4),
  143        and( or(or(not(p4), p2), not(p5)),  
  144        and( or(or(not(p2), not(p1)), not(p5)),
  145        and( or(or(not(p5), not(p1)), not(p2)),  
  146        and( or(or(not(p4), not(p2)), not(p3)),  
  147        and( or(or(not(p2), not(p3)), p4),
  148        and( or(or(not(p3), not(p5)), p1),
  149             or(or(not(p2), not(p1)), p4)
  150        ))))))))))))))), 
  151    Result).
  152        
  153% Ullrich's example
  154% note the close relationship to problem 10: problem 11 is a modalized
  155% version of problem 10 (except for the first conjunct of problem 10).
  156% unsatisfiable?
  157% Dima: unknown result; algorithm interrupted after 21 million proof steps
  158problem(11, unknown, Result) :- 
  159    satisfiable(
  160        and( box(star(r1), dia(r1, or(p0, not(p0)))),
  161        and( box(star(r1), or(or(box(r1,p5), box(r1,p3)), box(r1,p4))),
  162        and( box(star(r1), or(or(box(r1,p5), box(r1,not(p2))), box(r1,not(p3)))),  
  163        and( box(star(r1), or(or(box(r1,p1), box(r1,p3)), box(r1,p4))),
  164        and( box(star(r1), or(or(box(r1,not(p4)), box(r1,not(p5))), box(r1,p3))),  
  165        and( box(star(r1), or(or(box(r1,not(p3)), box(r1,not(p4))), box(r1,not(p5)))),  
  166        and( box(star(r1), or(or(box(r1,p3), box(r1,p2)), box(r1,(not(p1))))), 
  167        and( box(star(r1), or(or(box(r1,p2), box(r1,not(p5))), box(r1,not(p3)))),  
  168        and( box(star(r1), or(or(box(r1,not(p1)), box(r1,p3)), box(r1,p4))),
  169        and( box(star(r1), or(or(box(r1,not(p4)), box(r1,p2)), box(r1,not(p5)))),  
  170        and( box(star(r1), or(or(box(r1,not(p2)), box(r1,not(p1))), box(r1,not(p5)))),
  171        and( box(star(r1), or(or(box(r1,not(p5)), box(r1,not(p1))), box(r1,not(p2)))),  
  172        and( box(star(r1), or(or(box(r1,not(p4)), box(r1,not(p2))), box(r1,not(p3)))),  
  173        and( box(star(r1), or(or(box(r1,not(p2)), box(r1,not(p3))), box(r1,p4))),
  174        and( box(star(r1), or(or(box(r1,not(p3)), box(r1,not(p5))), box(r1,p1))),
  175        and( box(star(r1), or(or(box(r1,not(p2)), box(r1,not(p1))), box(r1,p4))),
  176        and( box(star(r1), or(not(p1), dia(star(r1),p2))),
  177        and( box(star(r1), or(not(p2), dia(star(r1),p3))),
  178        and( box(star(r1), or(not(p3), dia(star(r1),p4))),
  179        and( box(star(r1), or(not(p4), dia(star(r1),p5))),
  180             box(star(r1), or(not(p5), dia(star(r1),p1)))
  181        )))))))))))))))))))),
  182     Result).
  183
  184% Dima's example
  185problem(12, unsatisfiable, Result) :- 
  186    satisfiable(
  187        and(box(star(star(comp(a,star(b)))),p),
  188                dia(star(comp(comp(star(a),a),star(b))),not(p))), 
  189    Result).
  190
  191problem(13, unsatisfiable, Result) :- 
  192    satisfiable(
  193        and(box(star(star(comp(star(a),star(star(b))))),p),
  194            dia(star(comp(comp(star(star(a)),star(a)),star(star(b)))),not(p))
  195    ), Result).
  196
  197% From Baader (1990), Example 3.6, p. 16.
  198% An example of a `good cycle'
  199problem(14, satisfiable, Result) :- 
  200    satisfiable(
  201        and(p, and(dia(a,p),
  202               box(plus(a), dia(a,p))))
  203    , Result).
  204
  205% Another example of a `good cycle'
  206problem(15, satisfiable, Result) :- 
  207    satisfiable(
  208        and(p, and(dia(a,p),
  209               box(star(a), dia(a,p))))
  210    , Result).
  211
  212% From Baader (1990), Example 3.8, p. 17.
  213% An example of a `bad cycle'
  214problem(16, unsatisfiable, Result) :- 
  215    satisfiable(
  216        and(not(p), and(dia(plus(a),p),
  217               box(plus(a), not(p))))
  218    , Result).
  219
  220% A smaller example of a `bad cycle'
  221problem(17, unsatisfiable, Result) :- 
  222    satisfiable(
  223        and(dia(star(a),p),
  224            box(star(a),not(p)))
  225    , Result).
  226
  227problem(18, satisfiable, Result) :- 
  228    satisfiable(
  229        and(dia(star(or(a,b)),p),
  230            box(star(a),not(p))
  231        )
  232    , Result).
  233
  234problem(19, unsatisfiable, Result) :- 
  235    satisfiable(
  236        and(dia(star(b),p),
  237            box(star(or(a,b)),not(p))
  238    )
  239    , Result).
  240
  241problem(20, unsatisfiable, Result) :- 
  242    satisfiable(
  243        and(dia(star(or(a,b)),p),
  244            box(star(b),and(dia(star(a),p),
  245                            box(star(a),not(p))))
  246    )
  247    , Result).
  248
  249% Dima's example
  250% unsatisfiable
  251% test_free_pdl.pl: 7,378,999 inferences in 31.60 seconds (233513 Lips) (NNF version)
  252% pdl.pl:          13,387,034 inferences in 35.47 seconds (377418 Lips) (NNF version)
  253% dGM still working
  254problem(21, unsatisfiable, Result) :- 
  255    satisfiable(
  256        and(box(star(star(comp(star(or(star(or(a,c)),c)),star(b)))),p),
  257            dia(star(comp(comp(star(or(star(or(a,c)),c)),
  258                                       star(or(star(or(a,c)),c))),star(b))),
  259                not(p))), Result).
  260
  261problem(22, unsatisfiable, Result) :- 
  262    satisfiable(
  263        and(box(star(or(star(or(a,c)),c)),p),
  264            dia(star(or(a,c)),not(p))
  265        ), Result).
  266
  267problem(23, satisfiable, Result) :- 
  268    satisfiable(not(
  269            implies( 
  270                implies(dia(comp(x,y),p), dia(y,p)),
  271                implies(dia(comp(star(x),y),p), dia(y,p))
  272        ))
  273    , Result).
  274
  275problem(24, satisfiable, Result) :- 
  276    satisfiable(not(
  277        implies( 
  278            equiv(dia(or(comp(x,y),y),p), dia(y,p)),
  279            equiv(dia(or(comp(star(x),y),y),q), dia(y,q))
  280        ))
  281    , Result).
  282
  283% satisfiable
  284problem(25, satisfiable, Result) :- 
  285    satisfiable(not(
  286        implies( 
  287            equiv(box(or(comp(x,y),y),p), box(y,p)),
  288            equiv(box(or(comp(star(x),y),y),q), box(y,q))
  289        ))
  290    , Result).
  291
  292problem(26, satisfiable, Result) :- 
  293    satisfiable([],not(
  294        equiv( 
  295            box(or(comp(x,y),y),p), 
  296            box(or(comp(star(x),y),y),p)
  297        ))
  298    , Result).
  299
  300problem(27, satisfiable, Result) :- 
  301    satisfiable(
  302        [implies(dia(u,true), dia(x,true)),
  303         implies(dia(v,true), dia(y,true))],
  304        not(
  305            implies(dia(comp(u,v),true), dia(comp(x,y),true))
  306        )
  307, Result).
  308
  309problem(28, satisfiable, Result) :- 
  310    satisfiable(
  311        [implies(dia(u,p1), dia(x,p1)),
  312         implies(dia(v,p2), dia(y,p2))],
  313        not(
  314            implies(dia(comp(u,v),q), dia(comp(x,y),q))
  315        )
  316, Result).
  317
  318problem(29, satisfiable, Result) :- 
  319    satisfiable([],
  320        not(
  321        implies(and(
  322         implies(dia(u,p1), dia(x,p1)),
  323         implies(dia(v,p2), dia(y,p2))),
  324            implies(dia(comp(u,v),q), dia(comp(x,y),q))
  325        ))
  326, Result).
  327
  328problem(30, satisfiable, Result) :- 
  329    satisfiable([],
  330        not(
  331        implies(and(
  332         equiv(dia(or(u,x),p1), dia(x,p1)),
  333         equiv(dia(or(v,y),p2), dia(y,p2))),
  334            equiv(dia(or(comp(u,v),comp(x,y)),q), dia(comp(x,y),q))
  335        ))
  336, Result).
  337
  338problem(31, satisfiable, Result) :- 
  339    satisfiable(
  340        [equiv(dia(or(u,x),p1), dia(x,p1)),
  341         equiv(dia(or(v,y),p2), dia(y,p2))],
  342        not(
  343            equiv(dia(or(comp(u,v),comp(x,y)),q), dia(comp(x,y),q))
  344        )
  345    , Result).
  346
  347problem(32, satisfiable, Result) :- 
  348    satisfiable(
  349        [implies(dia(u,true), dia(x,true)),
  350         implies(dia(v,true), dia(y,true))],
  351        not(
  352            implies(dia(comp(u,v),true), dia(comp(x,y),true))
  353        )
  354, Result).
  355
  356problem(33, satisfiable, Result) :- 
  357    satisfiable(not(
  358        implies( and(
  359            implies(dia(u,p), dia(x,p)),
  360            implies(dia(v,p), dia(x,p))),
  361            implies(dia(comp(u,v),p), dia(comp(x,x),p))
  362        ))
  363, Result).
  364
  365problem(34, unsatisfiable, Result) :- 
  366    satisfiable(
  367        [ implies(dia(u,p), p) ],
  368        not(
  369            implies(dia(u,p), dia(star(x),p))
  370        )
  371    , Result).
  372
  373problem(35, unsatisfiable, Result) :- 
  374    satisfiable(
  375        [ implies(dia(u,p), dia(x,p)) ],
  376        not(
  377           implies(dia(u,p), dia(star(x),p))
  378        )
  379    , Result).
  380
  381problem(36, unsatisfiable, Result) :- 
  382    satisfiable(
  383       [ implies(dia(u,true), dia(star(x),true)),
  384         implies(dia(v,true), dia(star(x),true))],
  385       not(
  386           implies(dia(comp(u,v),true), dia(star(x),true))
  387       )
  388, Result).
  389
  390problem(37, unsatisfiable, Result) :- 
  391    satisfiable(
  392        [ implies(dia(u,p), dia(y,p)),
  393          implies(dia(comp(x,y),p), dia(y,p))],
  394        not(
  395            implies(dia(comp(star(x),u),p), dia(y,p))
  396        )
  397, Result).
  398
  399problem(38, satisfiable, Result) :- 
  400    satisfiable([],
  401        not(
  402        implies(and(
  403          equiv(dia(or(u,y),p1), dia(y,p1)),
  404          equiv(dia(or(comp(x,y),y),p2), dia(y,p2))),
  405            equiv(dia(or(comp(star(x),y),u),q), dia(y,q))
  406        ))
  407, Result).
  408
  409problem(39, unsatisfiable, Result) :- 
  410    satisfiable(
  411        [ implies(dia(u,true), dia(y,true)),
  412           implies(dia(comp(y,x),true), dia(y,true))],
  413        not(
  414           implies(dia(comp(u,star(x)),true), dia(y,true))
  415        )
  416, Result).
  417
  418problem(40, unsatisfiable, Result) :- 
  419    satisfiable(
  420        [ implies(dia(x,true), dia(u,true)),
  421          implies(dia(u,true), dia(y,true))],
  422        not(
  423           implies(dia(x,true), dia(y,true))
  424        )
  425, Result).
  426
  427% (a + b)* = (a*;b*)*, Kracht
  428% Jan 2006: equivalent reduction
  429problem(41, unsatisfiable, Result) :- 
  430    satisfiable([],
  431        not(
  432        equiv(
  433            dia(star(or(a,b)),p),
  434            dia(star(comp(star(a),star(b))),p)
  435        ))
  436, Result).
  437
  438% (a;b)* = skip + a;(b;a)*;b
  439% Jan 2006: equivalent reduction
  440problem(42, unsatisfiable, Result) :- 
  441    satisfiable([],
  442        not(
  443        equiv(
  444            dia(star(comp(a,b)),p),
  445            or(p,
  446               dia(comp(a,comp(star(comp(b,a)),b)),p)
  447            )
  448        ))
  449, Result).
  450
  451% (p?)* = skip
  452% Jan 2006: equivalent reduction
  453problem(43, unsatisfiable, Result) :- 
  454    satisfiable([],
  455        not(
  456        equiv(
  457            q,
  458            dia(star(test(p)),q)
  459        ))
  460, Result).
  461
  462% [(a^2)+]p & [(a^3)+]-p . -> -<a^6>T
  463problem(44, unsatisfiable, Result) :- 
  464    satisfiable([],
  465        not(
  466        implies(
  467            and(
  468                box(plus(comp(a,a)),p),
  469                box(plus(comp(a,comp(a,a))),not(p))
  470            ),
  471            not( dia(comp(a,comp(a,comp(a,comp(a,comp(a,a))))),true) )
  472        ))
  473, Result).
  474
  475% <(a + b)*>p & [a*]-p
  476problem(45, satisfiable, Result) :- 
  477    satisfiable([],
  478        and(
  479            dia(star(or(a,b)),p),
  480            box(star(a),not(p))
  481        )
  482, Result).
  483
  484problem(45, satisfiable, Result) :- 
  485    satisfiable([],
  486        and(
  487            dia(star(or(b,a)),p),
  488            box(star(a),not(p))
  489        )
  490, Result).
  491
  492% <(a*;b*)*>p & [a*]-p
  493problem(46, satisfiable, Result) :- 
  494    satisfiable([],
  495        and(
  496            dia(star(comp(star(a),star(b))),p),
  497            box(star(a),not(p))
  498        )
  499, Result).
  500
  501% <(a*;b*)*>p & [a*]-p
  502problem('46a', satisfiable, Result) :- 
  503    satisfiable([],
  504        and(
  505            dia(star(comp(star(b),star(a))),p),
  506            box(star(a),not(p))
  507        )
  508, Result).
  509
  510problem(47, satisfiable, Result) :- 
  511    satisfiable([],
  512        and(
  513            dia(star(comp(star(b),star(a))),p),
  514            box(star(a),not(p))
  515        )
  516, Result).
  517
  518problem(48, satisfiable, Result) :- 
  519    satisfiable([],
  520        and(
  521            or(dia(star(a),p),
  522               dia(star(b),p)),
  523            box(star(a),not(p))
  524        )
  525, Result).
  526
  527% Dima/Ullrich's example
  528problem(49, satisfiable, Result) :- 
  529    satisfiable([],
  530        and(
  531            box(star(or(a,b)), dia(plus(comp(a,b)),p)),
  532            box(star(or(a,b)), dia(plus(comp(b,a)),not(p)))
  533        )
  534, Result).
  535
  536problem(50, unsatisfiable, Result) :- 
  537    satisfiable([],
  538        and(not(p),
  539            dia(star(or(test(p),test(not(p)))),p)
  540        )
  541    , Result).
  542
  543problem(51, satisfiable, Result) :- 
  544    satisfiable(
  545        and(and(
  546            dia(star(or(star(a),star(b))),p),
  547            box(star(a),not(p))),
  548            box(star(b),not(p)))
  549    , Result).
  550
  551problem(52, satisfiable, Result) :- 
  552    satisfiable(
  553        and(and(
  554            dia(star(or(a,b)),p),
  555            box(star(a),not(p))),
  556            box(star(b),not(p)))
  557    , Result).
  558
  559problem(53, satisfiable, Result) :- 
  560    satisfiable(
  561        and(and(
  562            dia(star(comp(star(a),star(b))),p),
  563            box(star(a),not(p))),
  564            box(star(b),not(p)))
  565    , Result).
  566
  567problem(54, satisfiable, Result) :- 
  568    satisfiable(
  569        and(dia(star(or(a,b)),p),
  570            box(star(a),
  571               or(and(dia(star(a),p), 
  572                      box(star(a),not(p))), 
  573                  not(p)))
  574        )
  575    , Result).
  576
  577problem(55, satisfiable, Result) :- 
  578    satisfiable(
  579        and(dia(star(or(a,b)),p),
  580            box(star(a),
  581               or(not(p),
  582                  and(dia(star(a),p), 
  583                      box(star(a),not(p)))
  584               ))
  585        )
  586    , Result).
  587
  588problem(56, satisfiable, Result) :- 
  589    satisfiable(
  590        and(dia(star(or(a,b)),p),
  591            box(star(a),
  592               or(and(dia(star(c),p), 
  593                      box(star(c),not(p))), 
  594                  not(p)))
  595        )
  596    , Result).
  597
  598problem(57, satisfiable, Result) :- 
  599    satisfiable(
  600        and(dia(star(or(a,b)),p),
  601            box(star(a),
  602               or(and(p, 
  603                      not(p)), 
  604                  not(p)))
  605        )
  606    , Result).
  607
  608% a+ = a;a*
  609% Jan 2006: equivalent reduction
  610problem(58, unsatisfiable, Result) :- 
  611    satisfiable([],
  612        not(
  613        equiv(
  614            dia(plus(a),p),
  615            dia(comp(a,star(a)),p)
  616        ))
  617, Result).
  618
  619% a* = id + a+
  620% Jan 2006: equivalent reduction
  621problem(59, unsatisfiable, Result) :- 
  622    satisfiable([],
  623        not(
  624        equiv(
  625            dia(star(a),p),
  626            dia(or(id,star(a)),p)
  627        ))
  628, Result).
  629
  630% (a + b)* = a*;(b;a*)*
  631% Jan 2006: equivalent reduction
  632problem(60, unsatisfiable, Result) :- 
  633    satisfiable([],
  634        not(
  635        equiv(
  636            dia(star(or(a,b)),p),
  637            dia(comp(star(a),star(comp(b,star(a)))),p)
  638        ))
  639, Result).
  640
  641% (a + b)* = (a*;b)*;a*
  642% Jan 2006: equivalent reduction
  643problem(61, unsatisfiable, Result) :- 
  644    satisfiable([],
  645        not(
  646        equiv(
  647            dia(star(or(a,b)),p),
  648            dia(comp(star(comp(star(a),b)),star(a)),p)
  649        ))
  650, Result).
  651
  652% a + b;(a + b)*;a = (b+;a*)*;a
  653% From Dima: R+(Q;(R+Q)*;R) is equivalent to (Q+;R*)*;R
  654% The proof has length 4831 (NNF version), 3632/3885 (new dGM_nd/dGM version)
  655% Jan 2006: equivalent reduction
  656problem(62, unsatisfiable, Result) :- 
  657    satisfiable([],
  658        not(
  659        equiv(
  660            dia(or(a,comp(comp(b,star(or(a,b))),a)),p),
  661            dia(comp(star(comp(plus(b),star(a))),a),p)
  662        ))
  663, Result).
  664
  665% S;(S+;R)+ = S;S+;R + S;S+;R;(S+;R)+
  666% Jan 2006: equivalent reduction
  667problem(63, unsatisfiable, Result) :- 
  668    satisfiable([],
  669        not(
  670        equiv(
  671            dia(comp(s,plus(comp(plus(s),r))),p),
  672            dia(or(comp(comp(s,plus(s)),r),
  673                   comp(comp(comp(s,plus(s)),r),plus(comp(plus(s),r)))),p)
  674        ))
  675, Result).
  676
  677% (S;R+)+;R = S;R+;R + (S;R+)+;S;R+;R
  678% Jan 2006: equivalent reduction
  679problem(64, unsatisfiable, Result) :- 
  680    satisfiable([],
  681        not(
  682        equiv(
  683            dia(comp(plus(comp(s,plus(r))),r),p),
  684            dia(or(comp(comp(s,plus(r)),r),
  685                   comp(comp(comp(plus(comp(s,plus(r))),s),plus(r)),r)),p)
  686        ))
  687, Result).
  688
  689% R+;R+ = R;R*;R
  690% Jan 2006: equivalent reduction
  691problem(65, unsatisfiable, Result) :- 
  692    satisfiable([],
  693        not(
  694        implies(
  695            dia(comp(plus(r),plus(r)), p),
  696            dia(comp(comp(r,star(r)),r), p)
  697        ))
  698, Result).
  699
  700% Dima's example
  701problem(66, satisfiable, Result) :- 
  702    satisfiable([],
  703        and(dia(star(comp(star(a),b)), p),
  704            not(dia(star(comp(comp(b,star(b)),star(a))), p))
  705        )
  706, Result).
  707
  708% Transscribed example from Alberucci & Jaeger
  709problem(67, unsatisfiable, Result) :- 
  710    satisfiable([],
  711        not(
  712        implies(
  713            and(box(a,and(p,box(plus(or(a,b)),q))), 
  714                box(b,and(q,box(plus(or(a,b)),p)))), 
  715            box(plus(or(a,b)),or(p,q))
  716        ))
  717, Result).
  718
  719% Negation of 67
  720problem(68, satisfiable, Result) :- 
  721    satisfiable([],
  722        implies(
  723            and(box(a,and(p,box(plus(or(a,b)),q))), 
  724                box(b,and(q,box(plus(or(a,b)),p)))), 
  725            box(plus(or(a,b)),or(p,q))
  726        )
  727, Result).
  728
  729% From Alberucci, PhD, p. 96
  730problem(69, satisfiable, Result) :- 
  731    satisfiable([],
  732        not(
  733        implies(
  734            box(a,and(p,box(plus(or(a,b)),q))), 
  735            box(or(a,b), box(a,and(p,box(plus(or(a,b)),q))))
  736        ))
  737, Result).
  738
  739problem(70, unsatisfiable, Result) :- 
  740    satisfiable([],
  741        not(
  742        equiv(q,
  743            dia(star(id),q)
  744        ))
  745    , Result).
  746
  747problem(71, unsatisfiable, Result) :- 
  748    satisfiable([],
  749        not(
  750        implies(q,
  751            dia(test(true),q)
  752        ))
  753    , Result).
  754
  755% S;(S+;R)+ = S;S+;R + S;S+;R;T
  756problem(72, satisfiable, Result) :- 
  757    satisfiable([],
  758        not(
  759        equiv(
  760            dia(comp(s,plus(comp(plus(s),r))),p),
  761            dia(or(comp(comp(s,plus(s)),r),
  762                   comp(comp(comp(s,plus(s)),r),t)),p)
  763        ))
  764, Result).
  765
  766% (S;R+)+;R = S;R+;R + T;S;R+;R
  767problem(73, satisfiable, Result) :- 	% check !!
  768    satisfiable([],
  769        not(
  770        equiv(
  771            dia(comp(plus(comp(s,plus(r))),r),p),
  772            dia(or(comp(comp(s,plus(r)),r),
  773                   comp(comp(comp(t,s),plus(r)),r)),p)
  774        ))
  775, Result).
  776
  777% 1+a;a* <= a*
  778% Jan 2006: equivalent reduction
  779problem(74, unsatisfiable, Result) :-
  780    satisfiable([],
  781        not(
  782            implies(
  783                dia(or(test(true),comp(a,star(a))), p),
  784                dia(star(a),p))
  785        )
  786, Result).
  787
  788% 1+a*;a <= a*
  789% Jan 2006: equivalent reduction
  790problem(75, unsatisfiable, Result) :-
  791    satisfiable([],
  792        not(
  793            implies(
  794                dia(or(test(true),comp(star(a),a)), p),
  795                dia(star(a),p))
  796        )
  797, Result).
  798
  799% a;c+b <= c implies a*;b <= c
  800% equivalent to problem 37
  801problem(76, unsatisfiable, Result) :- 
  802    satisfiable([
  803            implies(
  804                dia(or(comp(a,c),b), true),
  805                dia(c,true))
  806        ],
  807        not(
  808            implies(
  809                dia(comp(star(a),b), true),
  810                dia(c,true))
  811        )
  812, Result).
  813
  814% c;a+b <= c implies b;a* <= c
  815% equivalent to problem 39
  816% Jan 2006: not equivalent
  817problem(77, unsatisfiable, Result) :-
  818    satisfiable([
  819            implies(
  820                dia(or(comp(c,a),b), true),
  821                dia(c,true))
  822        ],
  823        not(
  824            implies(
  825                dia(comp(b,star(a)), true),
  826                dia(c,true))
  827        )
  828, Result).
  829
  830problem(78, satisfiable, Result) :-
  831    satisfiable([
  832            implies(
  833                dia(or(comp(c,a),b), p),
  834                dia(c,p))
  835        ],
  836        not(
  837            implies(
  838                dia(comp(b,star(a)), p),
  839                dia(c,p))
  840        )
  841, Result).
  842
  843% p;q = 0 implies (p + q)*;1 <= q*;p*
  844% Jan 2006: equivalent reduction
  845problem(79, unsatisfiable, Result) :-
  846    satisfiable([
  847            not(
  848                dia(comp(p,q),true))
  849        ],
  850        not(
  851            implies(
  852                dia(comp(star(or(p,q)),test(true)), y),
  853                dia(comp(star(q),star(p)),y))
  854        )
  855, Result).
  856
  857% p;(q;p)* = (p;q)*;p
  858% Jan 2006: equivalent reduction
  859problem(80, unsatisfiable, Result) :-
  860    satisfiable([],
  861        not(
  862            equiv(
  863                dia(comp(p,star(comp(q,p))),x),
  864                dia(comp(star(comp(p,q)),p),x))
  865        )
  866, Result).
  867
  868% s + uru = t + uru  implies  s* + uru = t* + uru  
  869% Jan 2006: not equivalent
  870problem(81, unsatisfiable, Result) :-
  871    satisfiable([
  872            equiv(
  873                dia(or(s,comp(u,comp(r,u))),true),
  874                dia(or(t,comp(u,comp(r,u))),true)
  875            )
  876        ],
  877        not(
  878            equiv(
  879                dia(or(star(s),comp(u,comp(r,u))),true),
  880                dia(or(star(t),comp(u,comp(r,u))),true))
  881        )
  882, Result).
  883
  884% b(d*ca*b)*d*ca* <= (a*bd*c)*a*
  885problem(82, unsatisfiable, Result) :-
  886    satisfiable([],
  887        not(
  888            implies(
  889                dia(comp(b,comp(star(comp(star(d),comp(c,comp(star(a),b)))),comp(star(d),comp(c,star(a))))),true),
  890                dia(comp(star(comp(star(a),comp(b,comp(star(d),c)))),star(a)),true))
  891        )
  892, Result).
  893
  894% b(d*ca*b)*d*ca* <= (a*bd*c)*a*
  895% equivalent variation of problem 82
  896problem(83, unsatisfiable, Result) :-
  897    satisfiable([],
  898        not(
  899            implies(
  900                dia(comp(b,comp(star(comp(star(d),comp(c,comp(star(a),b)))),comp(star(d),comp(c,star(a))))),p),
  901                dia(comp(star(comp(star(a),comp(b,comp(star(d),c)))),star(a)),p))
  902        )
  903, Result).
  904
  905% b(d*ca*b)*d* <= (a*bd*c)*a*bd*
  906problem(84, unsatisfiable, Result) :-
  907    satisfiable([],
  908        not(
  909            implies(
  910                dia(comp(b,comp(star(comp(star(d),comp(c,comp(star(a),b)))),star(d))),true),
  911                dia(comp(star(comp(star(a),comp(b,comp(star(d),c)))),comp(star(a),comp(b,star(d)))),true))
  912        )
  913, Result).
  914
  915% b(d*ca*b)*d* <= (a*bd*c)*a*bd*
  916% equivalent variation of problem 84
  917problem(85, unsatisfiable, Result) :-
  918    satisfiable([],
  919        not(
  920            implies(
  921                dia(comp(b,comp(star(comp(star(d),comp(c,comp(star(a),b)))),star(d))),p),
  922                dia(comp(star(comp(star(a),comp(b,comp(star(d),c)))),comp(star(a),comp(b,star(d)))),p))
  923        )
  924, Result).
  925
  926% ax + by <= x and cx + dy <= y  implies  (a + bd*c)*x + (a + bd*c)*bd*y <= x
  927problem(86, unsatisfiable, Result) :-
  928    satisfiable([
  929            implies(
  930                dia(or(comp(a,x),comp(b,y)),true),
  931                dia(x,true)),
  932            implies(
  933                dia(or(comp(c,x),comp(d,y)),true),
  934                dia(y,true))
  935        ],
  936        not(
  937            implies(
  938                dia(or(
  939                    comp(star(or(a,comp(b,comp(star(d),c)))),x),
  940                    comp(star(or(a,comp(b,comp(star(d),c)))),comp(b,comp(star(d),y)))), true),
  941                dia(x,true))
  942        )
  943, Result).
  944
  945% ax + by <= x and cx + dy <= y  implies  (d + ca*b)*y + (d + ca*b)*ca*x <= y
  946% check equivalence
  947problem(87, unsatisfiable, Result) :-
  948    satisfiable([
  949            implies(
  950                dia(or(comp(a,x),comp(b,y)),true),
  951                dia(x,true)),
  952            implies(
  953                dia(or(comp(c,x),comp(d,y)),true),
  954                dia(y,true))
  955        ],
  956        not(
  957            implies(
  958                dia(or(
  959                    comp(star(or(d,comp(c,comp(star(a),b)))),y),
  960                    comp(star(or(d,comp(c,comp(star(a),b)))),comp(c,comp(star(a),x)))), true),
  961                dia(y,true))
  962        )
  963, Result).
  964
  965problem(88, unsatisfiable, Result) :-
  966    satisfiable([],
  967        and(
  968            dia(star(a),and(not(p),and(not(q),or(p,q)))),
  969        and(dia(a,dia(star(a),and(not(p),and(not(q),or(p,q))))), 
  970            box(star(a),dia(a,dia(star(a),and(not(p),and(not(q),or(p,q))))))))
  971, Result).
  972
  973problem(89, satisfiable, Result) :-
  974    satisfiable([],
  975        and(
  976            dia(star(star(a)),p),
  977            not(p)
  978        )
  979, Result).
  980
  981
  982problem(90, unsatisfiable, Result) :-
  983    satisfiable([],
  984        and(
  985            dia(star(star(a)),dia(star(a),p)),
  986            not(dia(star(a),p))
  987        )
  988, Result).
  989
  990problem(91, satisfiable, Result) :-
  991    satisfiable([],
  992        and(
  993            dia(star(star(a)),and(p,q)),
  994            not(and(p,q))
  995        )
  996, Result).
  997
  998problem(92, satisfiable, Result) :-
  999    satisfiable([],
 1000        dia(a,and(
 1001            dia(star(star(a)),p),
 1002            not(p)
 1003        ))
 1004, Result).
 1005
 1006problem(93, unsatisfiable, Result) :-
 1007    satisfiable([],
 1008        and(
 1009            dia(star(star(a)),dia(star(a),dia(a,p))),
 1010            not(dia(star(a),p))
 1011        )
 1012, Result).
 1013
 1014
 1015problem(94, unsatisfiable, Result) :-
 1016    satisfiable([],
 1017        and(
 1018            dia(star(a),dia(a,p)),
 1019            not(dia(a,dia(star(a),p)))
 1020        )
 1021, Result).
 1022
 1023problem(95, unsatisfiable, Result) :-
 1024    satisfiable([],
 1025        and(
 1026            dia(star(a),dia(a,p)),
 1027            not(dia(a,dia(star(star(a)),p)))
 1028        )
 1029, Result).
 1030
 1031
 1032problem(96, unsatisfiable, Result) :-
 1033    satisfiable([],
 1034        and(and(
 1035	    q,
 1036            not(dia(star(a),q))),
 1037            dia(star(star(a)),or(dia(star(a),q),not(q)))
 1038        )
 1039, Result).
 1040
 1041% Variations of 41
 1042problem(97, unsatisfiable, Result) :-
 1043    satisfiable([],
 1044        and(
 1045            dia(star(comp(star(a),star(b))), p),
 1046            not(dia(star(or(a,b)),dia(star(a),p)))
 1047        )
 1048, Result).
 1049
 1050
 1051problem(98, satisfiable, Result) :-
 1052    satisfiable([],
 1053        and(
 1054            dia(star(comp(star(a),star(b))), p),
 1055            not(dia(star(or(a,b)),dia(a,p)))
 1056        )
 1057, Result).
 1058
 1059
 1060problem(99, satisfiable, Result) :-
 1061    satisfiable([],
 1062        and(
 1063            dia(star(comp(star(a),star(b))), p),
 1064            not(dia(star(or(a,comp(b,a))),p))
 1065        )
 1066, Result).
 1067
 1068
 1069problem(100, satisfiable, Result) :-
 1070    satisfiable([],
 1071        and(
 1072            dia(star(comp(star(a),star(b))), p),
 1073            not(dia(star(or(a,comp(comp(star(b),b),comp(star(a),a)))),p))
 1074        )
 1075, Result).
 1076
 1077% same as 100, but a and b switched in 1st conjunct -> many more steps
 1078problem(101, satisfiable, Result) :-
 1079    satisfiable([],
 1080        and(
 1081            dia(star(comp(star(b),star(a))), p),
 1082            not(dia(star(or(a,comp(comp(star(b),b),comp(star(a),a)))),p))
 1083        )
 1084, Result).
 1085
 1086problem(102, unsatisfiable, Result) :-
 1087    satisfiable([],
 1088        and(
 1089            not(dia(star(or(a,b)),dia(star(a),p))),
 1090            dia(star(a),dia(star(a), p))
 1091        )
 1092, Result).
 1093
 1094
 1095problem(103, unsatisfiable, Result) :-
 1096    satisfiable([],
 1097        and(and(
 1098            dia(star(a),p),
 1099            not(p)),
 1100            box(a,not(dia(star(a),p)))
 1101        )
 1102, Result).
 1103
 1104problem(104, satisfiable, Result) :-
 1105    satisfiable([],
 1106        dia(a,or(
 1107                 dia(b,and(and(and(or(p,q),or(not(p),q)),
 1108                               or(p,not(q))),or(not(p),not(q)))),
 1109	         dia(c,and(and(and(or(p,q),or(not(p),q)),
 1110                               or(p,not(q))),or(not(p), or(not(q), r)))))),
 1111          Result).
 1112
 1113% Problem 105 is due to Florian Widmann
 1114% ignorability and the formation of inconsistent sets
 1115problem(105, satisfiable, Result):-
 1116    satisfiable([],
 1117      and(box(star(a),dia(a,box(c,not(p)))),
 1118          and(box(c,not(p)),box(star(a),dia(star(b),dia(c,p))))), Result).
 1119
 1120% Problem 106 is due to Florian Widmann
 1121% problems with the definition of 'fulfilled'
 1122problem(106, unsatisfiable, Result) :-
 1123    satisfiable(and(dia(star(comp(a,a)),p),
 1124                and(dia(a,dia(star(comp(a,a)),p)),
 1125                    box(a,box(star(comp(a,a)),and(not(p),q))))), Result).
 1126
 1127% Problem 107 is due to Florian Widmann
 1128% caching of consistent sets is unsound
 1129problem(107, unsatisfiable, Result) :-
 1130    satisfiable(or(dia(a,box(star(comp(b,b)),and(p,and(dia(c,and(p,and(q,not(p)))),dia(b,dia(b,p)))))),
 1131                   and(dia(a,dia(b,p)),
 1132                       box(a,box(b,box(star(comp(b,b)),and(p,and(dia(c,and(p,and(q,not(p)))),dia(b,dia(b,p))))))))), Result)