#!/usr/bin/perl -w

# Copyright Gaal Yahas <gaal@forum2.org>

use strict; # ("how can you expect a program to run without strictures?")

our(                                                                       $A,$
N,$C                                                                       ,$D,
$I);$A=qr/[p-u]/;$N=qr/[~]/;$C=qr/[\^]/;$D=qr/[v]/;$I=qr/[>]/;sub e{my($c,$e,$f
)=@_;$e||=[];$f||=[];return if f([@$e,$c]);my@g=my@h=$c;while(my$i=shift@g){($_
,my($x,$y))=c($i);/A/?do{return if f([@$e,@g,$x])}:/a/?do{push@g,$x;return if f
([@$e,@g]);push@g,$y;return if f([@$e,@g]);push@h,$x,$y;}:/b/?do{push@$f,{1,$x,
2,$y}}:die}return\@h unless@$f;my$j=shift@$f;my$k=e($j->{1},[@$e,@h],\@$f);if (
$k){return[@h,@$k]}$k=e($j->{2},[@$e,@h],\@$f);return[@h,@$k]if$k;return}sub f{
my$c=shift or die;my$p=d($$c[-1]);for(@$c){return 1if$_ eq $p}return}my($l,$p,$
e);$e=shift or do{print"Enter a formula: ";chomp($e=<>)};if($e!~/^($A|$N|$C|$D|
$I|[()])+$/x){print"unknown character\n";exit 1}sub c{my($x,$y);my@a=a(shift);@
                                 a==1?(                          "A",$
                               a[0]):                              @a==2
                             ?do{($                                  _,$x,
                            $y)=a(                                    $a[1])
                           ;/$N/?                                      ("a1",
                          $x):/${                                      A}/?("".
                         "AA","~"                                      .$_):/$C
                         /x?("b1"                                      ,d($x),d
                         ($y)):/$D                                    /x?("a2",
                         d($x),d($y)                                ):/$I/?("".
                         "a3",$x,d($y))                          :die}:@a==3?do
                          {($_,$x,$y)=@a;                      /$C/?("a4",$x,$
                           y):/($D)/x?("b2",$x            ,$y):/$I/?("b3",d($
                            x),$y):die}:die}sub a{$_=shift or die;/^($A)$/?$
                             1:/^($N)(.*)$/?($1,$2):b($_)}sub d{$_="~".$_[0
                              ]||die;s/^$N$N//;$_}sub b{my$c=shift or die;
                                my$x='';my$d=0;$c=~s/^\((.*)\)$/$1/ or 1
                                  && die;while($c=~s/(.)//){$_=$1;(($_
                                    =~/($C|$D|$I)/)&&($d eq 0))&&do{
                                       return($1,$x,$c)};/\(/&&$d








 ++;/\)/&&$d--;             $x.=$_}die}if(!($p=e(d($e)))){print"tautology [$e]"
."\n";exit 0}if             (!($l=e($e))){print"contradiction [$e]\n";exit 0}$e
=$e;print"cont"             ."ingency [$e]\n";print"true path:\n\t",(join"\n\t"
 ,@$l),"\n";$e=             $e;print"false path:\n\t",(join"\n\t",@$p),"\n";$e;