COPPER version 2.0 ...
Command Line: copper --default --specification abs_1 philosopher.pp philosopher.spec 
Simplify process started ...
parsing preprocessed C file philosopher.pp ...
parsing specification file philosopher.spec ...
control locations created ...
skip locations eliminated ...
useless branch locations eliminated ...
procedures inlined ...
number of locations before parallelization = 10 ...
number of locations after parallelization = 9 ...
proc manager for philosopher created ...
component for philosopher created ...
relevant propositions computed ...
inputs processed ...
checking PhilSpec1 {simul} temp_var_8
starting iteration number 1 ...
model extracted in 0.4 milliseconds ...
implementation machine extracted in 0.8 milliseconds ...
global states : ( 1048576 ) = 1048576
simulation checked in 3.5 milliseconds ...
conformance relation exists !!
specification abs_1 is valid ...
total global time = 45.3 milliseconds
total cpu time = 10.0 milliseconds
total input processing time = 36.0 milliseconds
total Buchi automaton construction time = 0.0 milliseconds
total implementation machine extraction time = 0.8 milliseconds
total verification time = 3.5 milliseconds
total proof generation time = 0.0 milliseconds
total abstraction refinement time = 0.0 milliseconds
total CE generation time = 0.0 milliseconds
total CE verification time = 0.0 milliseconds
total predicate abstraction refinement time = 0.0 milliseconds
total LTS abstraction refinement time = 0.0 milliseconds
total number of eliminating combinations = 0
max number of eliminating combinations for a CE = 0
max size of eliminating combination = 0
max size of tried combination = 0
number of iterations = 1
number of predicate iterations = 1
number of lts iterations = 0
number of seed branches : 0
specification details : 2 states 2 transitions
number of explored states : 1048576
number of theorem prover calls = 2
number of formulas found in cache = 0
number of formulas stored in cache = 2
number of membership calls to MAT = 0
number of MAT membership cache misses = 0
number of candidate calls to MAT = 0
assumption alphabet size = 0
optimal assumption alphabet size = 0
assumption alphabet ratio = 0.000000
total certificate CNF size = 0
total certificate resolution file size = 0
total certificate packed resolution file size = 0
total certificate zipped resolution file size = 0
total witness file size = 0
total witness zipped file size = 0
total certificate zipped file size = 0
Simplify process destroyed ...
terminating normally ...