**************************************************
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 1 -> 0 1 q0 ,
1 q0 0 -> 0 0 q1 ,
1 q0 1 -> 0 1 q1 ,
1 q1 0 -> 1 0 q1 ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 1 -> 0 1 q1 ,
0 q5 -> q6 0 ,
1 q6 -> q6 1 ,
1 q7 0 -> 0 0 q8 ,
1 q7 1 -> 0 1 q8 ,
0 q8 -> 0 q0 ,
1 q8 0 -> 1 0 q8 ,
1 q8 1 -> 1 1 q8 ,
0 q6 -> q9 0 ,
0 q9 0 -> 1 0 q7 ,
0 q9 1 -> 1 1 q7 ,
1 q9 -> q9 1 ,
h q0 -> h 0 q0 ,
q0 h -> q0 0 h ,
h q1 -> h 0 q1 ,
q1 h -> q1 0 h ,
h q2 -> h 0 q2 ,
q2 h -> q2 0 h ,
h q3 -> h 0 q3 ,
q3 h -> q3 0 h ,
h q4 -> h 0 q4 ,
q4 h -> q4 0 h ,
h q5 -> h 0 q5 ,
q5 h -> q5 0 h ,
h q6 -> h 0 q6 ,
q6 h -> q6 0 h)
, deadline = Just
(Time
-2040392993)
}
is false because of
mirror image
R' = { reverse(l) -> reverse(r) | (l -> r) in R }
(VAR x1)
(RULES 0 q0 0 -> q0 0 0 ,
1 q0 0 -> q0 1 0 ,
0 q0 1 -> q1 0 0 ,
1 q0 1 -> q1 1 0 ,
0 q1 1 -> q1 0 1 ,
1 q1 1 -> q1 1 1 ,
0 q1 0 -> q2 0 0 ,
1 q1 0 -> q2 1 0 ,
0 q2 1 -> q2 0 1 ,
1 q2 1 -> q2 1 1 ,
q2 0 -> 1 q3 ,
q3 1 -> 1 q3 ,
q3 0 -> 0 q4 ,
q4 1 -> 1 q4 ,
0 q4 0 -> q5 0 1 ,
1 q4 0 -> q5 1 1 ,
0 q5 1 -> q1 0 0 ,
1 q5 1 -> q1 1 0 ,
q5 0 -> 0 q6 ,
q6 1 -> 1 q6 ,
0 q7 1 -> q8 0 0 ,
1 q7 1 -> q8 1 0 ,
q8 0 -> q0 0 ,
0 q8 1 -> q8 0 1 ,
1 q8 1 -> q8 1 1 ,
q6 0 -> 0 q9 ,
0 q9 0 -> q7 0 1 ,
1 q9 0 -> q7 1 1 ,
q9 1 -> 1 q9 ,
q0 h -> q0 0 h ,
h q0 -> h 0 q0 ,
q1 h -> q1 0 h ,
h q1 -> h 0 q1 ,
q2 h -> q2 0 h ,
h q2 -> h 0 q2 ,
q3 h -> q3 0 h ,
h q3 -> h 0 q3 ,
q4 h -> q4 0 h ,
h q4 -> h 0 q4 ,
q5 h -> q5 0 h ,
h q5 -> h 0 q5 ,
q6 h -> q6 0 h ,
h q6 -> h 0 q6)
plain loop
Derivation
{ lhs = [ h , q0 , 0 ] , rhs = [ h , q0 , 0 , 0 ]
, hash_value = -1037175702 , strict = True
, steps = [ Step
{ rule = 30 , position = 0 }
, Step
{ rule = 0 , position = 1 }
]
}
**************************************************
statistics:
total atomic proof attempts
number = 23, total = 21
maximal = [ Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040398986
, end = Time
-2040398024
, duration = 9 , success = False
}
]
successful atomic proof attempts
number = 16, total = 4
maximal = [ Log
{ what = simplex
, start = Time
-2040397946
, end = Time
-2040397707
, duration = 2 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397994
, end = Time
-2040397870
, duration = 1 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397706
, end = Time
-2040397583
, duration = 1 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397528
, end = Time
-2040397472
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397828
, end = Time
-2040397804
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397702
, end = Time
-2040397636
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397868
, end = Time
-2040397860
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397581
, end = Time
-2040397577
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397842
, end = Time
-2040397840
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040398020
, end = Time
-2040397959
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397576
, end = Time
-2040397530
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397838
, end = Time
-2040397829
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397740
, end = Time
-2040397704
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397858
, end = Time
-2040397849
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040397802
, end = Time
-2040397742
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040398016
, end = Time
-2040397996
, duration = 0 , success = True
}
]
failed atomic proof attempts
number = 7, total = 17
maximal = [ Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040398986
, end = Time
-2040398024
, duration = 9 , 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/tmppwwZvJ/matchbox-2007-06-01/minisat --timeout-command=/tmp/tmppwwZvJ/matchbox-2007-06-01/timeout --tmpdir=tmp --timeout=60 /tmp/tmp.gtkt4DajhC/a.srs
started : Thu Jan 26 12:27:59 CET 2012
finished : Thu Jan 26 12:28:19 CET 2012
run system : Linux uc01-09 2.6.32-5-amd64 #1 SMP Mon Mar 7 21:35:22 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: 20 secs