************************************************** Claim { termination = Standard , system = (VAR x1) (RULES a -> , a b -> c , c c -> b c b a a) , deadline = Just (Time -2040347254) } is false because of looping forward closure of length 26 Derivation { lhs = [ c , c , b , c , b , c , b , c ] , rhs = [ b , c , b , b , c , b , b , c , b , c , c , b , c , b , c , b , c , a ] , hash_value = -1288689749 , strict = True , steps = [ Step { rule = 2 , position = 0 } , Step { rule = 1 , position = 4 } , Step { rule = 2 , position = 4 } , Step { rule = 1 , position = 3 } , Step { rule = 1 , position = 7 } , Step { rule = 2 , position = 3 } , Step { rule = 2 , position = 10 } , Step { rule = 1 , position = 9 } , Step { rule = 1 , position = 13 } , Step { rule = 1 , position = 7 } , Step { rule = 2 , position = 7 } , Step { rule = 1 , position = 6 } , Step { rule = 2 , position = 14 } , Step { rule = 1 , position = 13 } , Step { rule = 2 , position = 6 } , Step { rule = 1 , position = 10 } , Step { rule = 2 , position = 15 } , Step { rule = 0 , position = 18 } , Step { rule = 0 , position = 11 } , Step { rule = 0 , position = 19 } , Step { rule = 0 , position = 11 } , Step { rule = 2 , position = 10 } , Step { rule = 0 , position = 13 } , Step { rule = 1 , position = 9 } , Step { rule = 1 , position = 12 } , Step { rule = 1 , position = 16 } ] } this is closure number 5156 ************************************************** statistics: total atomic proof attempts number = 8, total = 6 maximal = [ Log { what = rfc match bounds (classical) , start = Time -2040353195 , end = Time -2040352692 , duration = 5 , success = False } ] successful atomic proof attempts number = 1, total = 0 maximal = [ Log { what = simplex , start = Time -2040353196 , end = Time -2040353196 , duration = 0 , success = True } ] failed atomic proof attempts number = 7, total = 6 maximal = [ Log { what = rfc match bounds (classical) , start = Time -2040353195 , end = Time -2040352692 , 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/tmpofj46w/matchbox-2007-06-01/minisat --timeout-command=/tmp/tmpofj46w/matchbox-2007-06-01/timeout --tmpdir=tmp --timeout=60 /tmp/tmp.bpEQ3JjzVe/a.srs started : Thu Jan 26 12:34:58 CET 2012 finished : Thu Jan 26 12:35:05 CET 2012 run system : Linux uc01-05 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