**************************************************
Claim
{ termination = Standard
, system = (VAR x1)
(RULES a a b -> a c c a a a ,
a c -> b)
, deadline = Just
(Time
-2040257482)
}
is false because of
mirror image
R' = { reverse(l) -> reverse(r) | (l -> r) in R }
(VAR x1)
(RULES b a a -> a a a c c a ,
c a -> b)
looping forward closure
of length 116
Derivation
{ lhs = [ b , a , a , a , a , a , a , a , a ]
, rhs = [ a , a , a , a , a , a , a , a , a , a , a , a , a , a , a
, a , a , a , b , a , a , a , a , a , a , a , a , c , c , a , c , b
, a , c , b , c , c , a , c , c , a , c , b , a , c , b , c , b , c
, b , c , b , a , c , b , c , b , c , b , c , b , a , c , c , a , c
, b , c , b , c , b , a , c , b , c , b , c , b , c , b , a , c , b
, c , b
]
, hash_value = -1614321005 , strict = True
, steps = [ Step
{ rule = 0 , position = 0 }
, Step
{ rule = 1 , position = 4 }
, Step
{ rule = 0 , position = 4 }
, Step
{ rule = 1 , position = 3 }
, Step
{ rule = 0 , position = 3 }
, Step
{ rule = 1 , position = 10 }
, Step
{ rule = 1 , position = 7 }
, Step
{ rule = 0 , position = 9 }
, Step
{ rule = 1 , position = 8 }
, Step
{ rule = 0 , position = 8 }
, Step
{ rule = 0 , position = 7 }
, Step
{ rule = 1 , position = 6 }
, Step
{ rule = 1 , position = 17 }
, Step
{ rule = 0 , position = 6 }
, Step
{ rule = 0 , position = 20 }
, Step
{ rule = 1 , position = 19 }
, Step
{ rule = 1 , position = 10 }
, Step
{ rule = 1 , position = 16 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 0 , position = 17 }
, Step
{ rule = 0 , position = 16 }
, Step
{ rule = 1 , position = 15 }
, Step
{ rule = 0 , position = 15 }
, Step
{ rule = 1 , position = 12 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 1 , position = 18 }
, Step
{ rule = 0 , position = 12 }
, Step
{ rule = 1 , position = 16 }
, Step
{ rule = 0 , position = 16 }
, Step
{ rule = 1 , position = 20 }
, Step
{ rule = 1 , position = 11 }
, Step
{ rule = 0 , position = 11 }
, Step
{ rule = 0 , position = 10 }
, Step
{ rule = 1 , position = 20 }
, Step
{ rule = 0 , position = 20 }
, Step
{ rule = 1 , position = 9 }
, Step
{ rule = 1 , position = 13 }
, Step
{ rule = 1 , position = 16 }
, Step
{ rule = 0 , position = 16 }
, Step
{ rule = 1 , position = 24 }
, Step
{ rule = 1 , position = 15 }
, Step
{ rule = 0 , position = 15 }
, Step
{ rule = 1 , position = 22 }
, Step
{ rule = 0 , position = 13 }
, Step
{ rule = 1 , position = 12 }
, Step
{ rule = 0 , position = 12 }
, Step
{ rule = 1 , position = 19 }
, Step
{ rule = 0 , position = 9 }
, Step
{ rule = 1 , position = 19 }
, Step
{ rule = 1 , position = 13 }
, Step
{ rule = 0 , position = 20 }
, Step
{ rule = 0 , position = 13 }
, Step
{ rule = 1 , position = 17 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 0 , position = 21 }
, Step
{ rule = 1 , position = 12 }
, Step
{ rule = 1 , position = 45 }
, Step
{ rule = 0 , position = 19 }
, Step
{ rule = 1 , position = 23 }
, Step
{ rule = 1 , position = 18 }
, Step
{ rule = 0 , position = 18 }
, Step
{ rule = 1 , position = 31 }
, Step
{ rule = 0 , position = 12 }
, Step
{ rule = 1 , position = 16 }
, Step
{ rule = 0 , position = 18 }
, Step
{ rule = 1 , position = 38 }
, Step
{ rule = 1 , position = 22 }
, Step
{ rule = 0 , position = 22 }
, Step
{ rule = 1 , position = 17 }
, Step
{ rule = 0 , position = 17 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 0 , position = 16 }
, Step
{ rule = 1 , position = 15 }
, Step
{ rule = 0 , position = 15 }
, Step
{ rule = 1 , position = 19 }
, Step
{ rule = 1 , position = 26 }
, Step
{ rule = 0 , position = 26 }
, Step
{ rule = 0 , position = 25 }
, Step
{ rule = 1 , position = 24 }
, Step
{ rule = 0 , position = 24 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 0 , position = 21 }
, Step
{ rule = 1 , position = 33 }
, Step
{ rule = 1 , position = 20 }
, Step
{ rule = 1 , position = 24 }
, Step
{ rule = 1 , position = 34 }
, Step
{ rule = 0 , position = 24 }
, Step
{ rule = 0 , position = 20 }
, Step
{ rule = 1 , position = 26 }
, Step
{ rule = 1 , position = 30 }
, Step
{ rule = 1 , position = 24 }
, Step
{ rule = 0 , position = 25 }
, Step
{ rule = 0 , position = 24 }
, Step
{ rule = 0 , position = 19 }
, Step
{ rule = 1 , position = 23 }
, Step
{ rule = 1 , position = 25 }
, Step
{ rule = 1 , position = 18 }
, Step
{ rule = 0 , position = 24 }
, Step
{ rule = 1 , position = 48 }
, Step
{ rule = 1 , position = 40 }
, Step
{ rule = 1 , position = 35 }
, Step
{ rule = 0 , position = 22 }
, Step
{ rule = 1 , position = 51 }
, Step
{ rule = 1 , position = 26 }
, Step
{ rule = 1 , position = 21 }
, Step
{ rule = 0 , position = 21 }
, Step
{ rule = 0 , position = 28 }
, Step
{ rule = 1 , position = 27 }
, Step
{ rule = 0 , position = 27 }
, Step
{ rule = 1 , position = 25 }
, Step
{ rule = 0 , position = 25 }
, Step
{ rule = 1 , position = 33 }
, Step
{ rule = 1 , position = 24 }
, Step
{ rule = 1 , position = 40 }
, Step
{ rule = 1 , position = 28 }
, Step
{ rule = 0 , position = 24 }
]
}
this is closure number 1677
**************************************************
statistics:
total atomic proof attempts
number = 7, total = 6
maximal = [ Log
{ what = rfc match bounds (classical)
, start = Time
-2040263406
, end = Time
-2040262902
, duration = 5 , success = False
}
]
successful atomic proof attempts
number = 0, total = 0
maximal = [ ]
failed atomic proof attempts
number = 7, total = 6
maximal = [ Log
{ what = rfc match bounds (classical)
, start = Time
-2040263406
, end = Time
-2040262902
, duration = 5 , success = False
}
]
**************************************************
matchbox general information (including details on proof methods):
http://dfa.imn.htwk-leipzig.de/matchbox/
this matchbox implementation uses the SAT solver
MiniSat by Niklas Een and Niklas Sörensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
matchbox process information
arguments : --solver=/tmp/tmp2xV4B8/matchbox-2007-06-01/minisat --timeout-command=/tmp/tmp2xV4B8/matchbox-2007-06-01/timeout --tmpdir=tmp --timeout=60 /tmp/tmp.wCPpTSz8zf/a.srs
started : Thu Jan 26 12:50:02 CET 2012
finished : Thu Jan 26 12:50:09 CET 2012
run system : Linux uc01-11 2.6.32-5-amd64 #1 SMP Wed Jan 12 03:40:32 UTC 2011 x86_64
release date : Fri Jun 1 17:36:44 CEST 2007
build date : Fri Jun 1 17:36:44 CEST 2007
build system : Linux dfa 2.6.8-2-k7 #1 Tue Aug 16 14:00:15 UTC 2005 i686 GNU/Linux
used clock time: 7 secs