PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_51_pb.cnf.cr.opb
MD5SUM	00bdc6bb9bafd4b1100d8bfa4f886626
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	52
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.156976
Number of variables	5100
Total number of constraints	202
Number of constraints which are clauses	102
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	51
Trace number 5353

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-13 23:35:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3780 boxname=wulflinc25 idbench=20 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00bdc6bb9bafd4b1100d8bfa4f886626  /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_51_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_51_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_51_pb.cnf.cr.opb
IDLAUNCH: 3780
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898668 kB
Buffers:         33640 kB
Cached:          67780 kB
SwapCached:         36 kB
Active:          46644 kB
Inactive:        57668 kB
HighTotal:      131008 kB
HighFree:        59528 kB
LowTotal:       903652 kB
LowFree:        839140 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26088 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:55:48 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 3780 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 202 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................
c ---[  99]---> BDD-cost:   99
c ---[  98]---> BDD-cost:   99
c ---[  97]---> BDD-cost:   99
c ---[  96]---> BDD-cost:   99
c ---[  95]---> BDD-cost:   99
c ---[  94]---> BDD-cost:   99
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:   99
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:   99
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:   99
c ---[  87]---> BDD-cost:   99
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   99
c ---[  83]---> BDD-cost:   99
c ---[  82]---> BDD-cost:   99
c ---[  81]---> BDD-cost:   99
c ---[  80]---> BDD-cost:   99
c ---[  79]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   99
c ---[  77]---> BDD-cost:   99
c ---[  76]---> BDD-cost:   99
c ---[  75]---> BDD-cost:   99
c ---[  74]---> BDD-cost:   99
c ---[  73]---> BDD-cost:   99
c ---[  72]---> BDD-cost:   99
c ---[  71]---> BDD-cost:   99
c ---[  70]---> BDD-cost:   99
c ---[  69]---> BDD-cost:   99
c ---[  68]---> BDD-cost:   99
c ---[  67]---> BDD-cost:   99
c ---[  66]---> BDD-cost:   99
c ---[  65]---> BDD-cost:   99
c ---[  64]---> BDD-cost:   99
c ---[  63]---> BDD-cost:   99
c ---[  62]---> BDD-cost:   99
c ---[  61]---> BDD-cost:   99
c ---[  60]---> BDD-cost:   99
c ---[  59]---> BDD-cost:   99
c ---[  58]---> BDD-cost:   99
c ---[  57]---> BDD-cost:   99
c ---[  56]---> BDD-cost:   99
c ---[  55]---> BDD-cost:   99
c ---[  54]---> BDD-cost:   99
c ---[  53]---> BDD-cost:   99
c ---[  52]---> BDD-cost:   99
c ---[  51]---> BDD-cost:   99
c ---[  50]---> BDD-cost:   99
c ---[  49]---> BDD-cost:   99
c ---[  48]---> BDD-cost:   99
c ---[  47]---> BDD-cost:   99
c ---[  46]---> BDD-cost:   99
c ---[  45]---> BDD-cost:   99
c ---[  44]---> BDD-cost:   99
c ---[  43]---> BDD-cost:   99
c ---[  42]---> BDD-cost:   99
c ---[  41]---> BDD-cost:   99
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:   99
c ---[  36]---> BDD-cost:   99
c ---[  35]---> BDD-cost:   99
c ---[  34]---> BDD-cost:   99
c ---[  33]---> BDD-cost:   99
c ---[  32]---> BDD-cost:   99
c ---[  31]---> BDD-cost:   99
c ---[  30]---> BDD-cost:   99
c ---[  29]---> BDD-cost:   99
c ---[  28]---> BDD-cost:   99
c ---[  27]---> BDD-cost:   99
c ---[  26]---> BDD-cost:   99
c ---[  25]---> BDD-cost:   99
c ---[  24]---> BDD-cost:   99
c ---[  23]---> BDD-cost:   99
c ---[  22]---> BDD-cost:   99
c ---[  21]---> BDD-cost:   99
c ---[  20]---> BDD-cost:   99
c ---[  19]---> BDD-cost:   99
c ---[  18]---> BDD-cost:   99
c ---[  17]---> BDD-cost:   99
c ---[  16]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   99
c ---[  14]---> BDD-cost:   99
c ---[  13]---> BDD-cost:   99
c ---[  12]---> BDD-cost:   99
c ---[  11]---> BDD-cost:   99
c ---[  10]---> BDD-cost:   99
c ---[   9]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   99
c ---[   7]---> BDD-cost:   99
c ---[   6]---> BDD-cost:   99
c ---[   5]---> BDD-cost:   99
c ---[   4]---> BDD-cost:   99
c ---[   3]---> BDD-cost:   99
c ---[   2]---> BDD-cost:   99
c ---[   1]---> BDD-cost:   99
c ---[   0]---> BDD-cost:   99
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   24702    69100 |    7410       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/14900          
c   -- var.elim.:  2000/14900          
c   -- var.elim.:  3000/14900          
c   -- var.elim.:  4000/14900          
c   -- var.elim.:  5000/14900          
c   -- var.elim.:  6000/14900          
c   -- var.elim.:  7000/14900          
c   -- var.elim.:  8000/14900          
c   -- var.elim.:  9000/14900          
c   -- var.elim.:  10000/14900          
c   -- var.elim.:  11000/14900          
c   -- var.elim.:  12000/14900          
c   -- var.elim.:  13000/14900          
c   -- var.elim.:  14000/14900          
c   -- var.elim.:  14900/14900          
c   -- var.elim.:  1000/5526          
c   -- var.elim.:  2000/5526          
c   -- var.elim.:  3000/5526          
c   -- var.elim.:  4000/5526          
c   -- var.elim.:  5000/5526          
c   -- var.elim.:  5526/5526          
c   -- var.elim.:  206/206          
c   -- subsuming                       
c   -- var.elim.:  1000/3080          
c   -- var.elim.:  2000/3080          
c   -- var.elim.:  3000/3080          
c   -- var.elim.:  3080/3080          
c   -- var.elim.:  982/982          
c   -- var.elim.:  124/124          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  122/122          
c   -- var.elim.:  124/124          
c   -- var.elim.:  126/126          
c   -- var.elim.:  128/128          
c   -- var.elim.:  130/130          
c   -- var.elim.:  132/132          
c   -- var.elim.:  134/134          
c   -- var.elim.:  136/136          
c   -- var.elim.:  138/138          
c   -- var.elim.:  140/140          
c   -- var.elim.:  142/142          
c   -- var.elim.:  144/144          
c   -- var.elim.:  146/146          
c   -- var.elim.:  148/148          
c   -- var.elim.:  150/150          
c   -- var.elim.:  152/152          
c   -- var.elim.:  154/154          
c   -- var.elim.:  156/156          
c   -- var.elim.:  158/158          
c   -- var.elim.:  160/160          
c   -- var.elim.:  162/162          
c   -- var.elim.:  164/164          
c   -- var.elim.:  166/166          
c   -- var.elim.:  168/168          
c   -- var.elim.:  170/170          
c   -- var.elim.:  172/172          
c   -- var.elim.:  174/174          
c   -- var.elim.:  176/176          
c   -- var.elim.:  178/178          
c   -- var.elim.:  180/180          
c   -- var.elim.:  182/182          
c   -- var.elim.:  184/184          
c   -- var.elim.:  186/186          
c   -- var.elim.:  188/188          
c   -- var.elim.:  190/190          
c   -- var.elim.:  192/192          
c   -- var.elim.:  194/194          
c   -- var.elim.:  196/196          
c   -- var.elim.:  198/198          
c   -- var.elim.:  200/200          
c   -- var.elim.:  486/486          
c   -- subsuming                       
c   -- var.elim.:  1000/5416          
c   -- var.elim.:  2000/5416          
c   -- var.elim.:  3000/5416          
c   -- var.elim.:  4000/5416          
c   -- var.elim.:  5000/5416          
c   -- var.elim.:  5416/5416          
c   -- var.elim.:  1000/5178          
c   -- var.elim.:  2000/5178          
c   -- var.elim.:  3000/5178          
c   -- var.elim.:  4000/5178          
c   -- var.elim.:  5000/5178          
c   -- var.elim.:  5178/5178          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  574/574          
c |         0 |   23510    85574 |      --       0       --      -- |     --   | -1192/16774
c |         0 |   23510    85574 |    9404       0        0     nan |  0.000 % |
c |       100 |   23510    85574 |   10344     100    18104   181.0 |  0.709 % |
c |       250 |   23510    85574 |   11378     250    48874   195.5 |  0.709 % |
c |       477 |   23510    85574 |   12516     477   105407   221.0 |  0.709 % |
c |       814 |   23510    85574 |   13768     814   185530   227.9 |  0.709 % |
c |      1322 |   23510    85574 |   15145    1322   307757   232.8 |  0.709 % |
c |      2085 |   23510    85574 |   16659    2085   520341   249.6 |  0.709 % |
c |      3224 |   23510    85574 |   18325    3224   898478   278.7 |  0.709 % |
c |      4936 |   23510    85574 |   20158    4936  1456229   295.0 |  0.709 % |
c |      7498 |   23510    85574 |   22174    7498  2346227   312.9 |  0.709 % |
c |     11342 |   23510    85574 |   24391   11342  3916#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 31156
Raw data (stat): 31156 (runsolver) R 31155 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479965803 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 4287 0 0 0 988 10 0 0 25 0 1 0 479965803 19034112 4164 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4164 603 41 0 4606 0
vsize: 18588
[startup+19.9997 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 6076 0 0 0 1983 15 0 0 25 0 1 0 479965803 26296320 5953 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6420 5953 603 41 0 6379 0
vsize: 25680
[startup+30.0001 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 8154 0 0 0 2977 20 0 0 25 0 1 0 479965803 34865152 8031 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8512 8031 603 41 0 8471 0
vsize: 34048
[startup+40 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 10293 0 0 0 3972 25 0 0 25 0 1 0 479965803 43696128 10170 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10668 10170 603 41 0 10627 0
vsize: 42672
[startup+50.0006 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 11193 0 0 0 4970 28 0 0 25 0 1 0 479965803 47271936 11070 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11541 11070 603 41 0 11500 0
vsize: 46164
[startup+59.9999 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 12492 0 0 0 5966 32 0 0 25 0 1 0 479965803 52699136 12369 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12866 12369 603 41 0 12825 0
vsize: 51464
[startup+69.9998 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 13846 0 0 0 6963 35 0 0 25 0 1 0 479965803 58126336 13723 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14191 13723 603 41 0 14150 0
vsize: 56764
[startup+80.0004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 15874 0 0 0 7959 39 0 0 25 0 1 0 479965803 66531328 15751 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16243 15751 603 41 0 16202 0
vsize: 64972
[startup+89.9997 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 17032 0 0 0 8956 42 0 0 25 0 1 0 479965803 71262208 16909 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17398 16909 603 41 0 17357 0
vsize: 69592
[startup+99.9996 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 17771 0 0 0 9955 44 0 0 25 0 1 0 479965803 74297344 17648 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18139 17648 603 41 0 18098 0
vsize: 72556
[startup+110 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 18540 0 0 0 10953 46 0 0 25 0 1 0 479965803 77590528 18417 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18943 18417 603 41 0 18902 0
vsize: 75772
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 19328 0 0 0 11951 48 0 0 25 0 1 0 479965803 80752640 19205 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19715 19205 603 41 0 19674 0
vsize: 78860
[startup+129.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20067 0 0 0 12949 50 0 0 25 0 1 0 479965803 83603456 19908 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19908 603 41 0 20370 0
vsize: 81644
[startup+139.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20068 0 0 0 13950 50 0 0 25 0 1 0 479965803 83603456 19909 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19909 603 41 0 20370 0
vsize: 81644
[startup+149.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 14950 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+159.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 15950 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+169.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 16950 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+179.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 17950 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+189.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 18950 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+199.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 19951 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+209.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20069 0 0 0 20951 50 0 0 25 0 1 0 479965803 83603456 19910 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19910 603 41 0 20370 0
vsize: 81644
[startup+219.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 20459 0 0 0 21950 51 0 0 25 0 1 0 479965803 85323776 20300 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20831 20300 603 41 0 20790 0
vsize: 83324
[startup+229.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 21002 0 0 0 22949 52 0 0 25 0 1 0 479965803 87568384 20843 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21379 20843 603 41 0 21338 0
vsize: 85516
[startup+239.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 21576 0 0 0 23948 53 0 0 25 0 1 0 479965803 89948160 21417 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21960 21417 603 41 0 21919 0
vsize: 87840
[startup+249.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 22249 0 0 0 24947 54 0 0 25 0 1 0 479965803 92725248 22090 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22638 22090 603 41 0 22597 0
vsize: 90552
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 23681 0 0 0 25944 57 0 0 25 0 1 0 479965803 98529280 23522 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24055 23522 603 41 0 24014 0
vsize: 96220
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 24851 0 0 0 26942 60 0 0 25 0 1 0 479965803 103280640 24692 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25215 24692 603 41 0 25174 0
vsize: 100860
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 25942 0 0 0 27939 63 0 0 25 0 1 0 479965803 107761664 25783 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26309 25783 603 41 0 26268 0
vsize: 105236
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 26643 0 0 0 28938 64 0 0 25 0 1 0 479965803 110653440 26484 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27015 26484 603 41 0 26974 0
vsize: 108060
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27404 0 0 0 29937 65 0 0 25 0 1 0 479965803 113803264 27245 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27784 27245 603 41 0 27743 0
vsize: 111136
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27709 0 0 0 30937 65 0 0 25 0 1 0 479965803 114802688 27508 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27508 603 41 0 27987 0
vsize: 112112
[startup+319.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27709 0 0 0 31937 65 0 0 25 0 1 0 479965803 114802688 27508 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27508 603 41 0 27987 0
vsize: 112112
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27709 0 0 0 32937 65 0 0 25 0 1 0 479965803 114802688 27508 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27508 603 41 0 27987 0
vsize: 112112
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 33938 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 34938 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 35938 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 36938 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 37939 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 38939 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 39939 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 40939 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 41939 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 42940 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 43940 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 27710 0 0 0 44940 65 0 0 25 0 1 0 479965803 114802688 27509 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28028 27509 603 41 0 27987 0
vsize: 112112
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 28691 0 0 0 45938 67 0 0 25 0 1 0 479965803 118886400 28490 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29025 28490 603 41 0 28984 0
vsize: 116100
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 29932 0 0 0 46935 70 0 0 25 0 1 0 479965803 123899904 29731 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30249 29731 603 41 0 30208 0
vsize: 120996
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 47933 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 48933 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 49933 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 50933 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 51934 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 52934 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 53934 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 54934 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 55934 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 56935 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 57935 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+590.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 58935 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+600.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 59935 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+610.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 60935 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+620.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 61936 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+630.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 62936 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+640.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 63936 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+650.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 64936 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+660.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 65936 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+670.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 66937 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+680.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 67937 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+690.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 68937 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+700.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 69937 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+710.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 70938 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+720.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30840 0 0 0 71938 73 0 0 25 0 1 0 479965803 127414272 30593 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30593 603 41 0 31066 0
vsize: 124428
[startup+730.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30841 0 0 0 72938 73 0 0 25 0 1 0 479965803 127414272 30594 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30594 603 41 0 31066 0
vsize: 124428
[startup+740.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30844 0 0 0 73938 73 0 0 25 0 1 0 479965803 127414272 30597 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31107 30597 603 41 0 31066 0
vsize: 124428
[startup+750.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 74938 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+760.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 75939 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+770.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 76939 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+780.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 77939 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+790.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 78939 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+800.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 79939 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+810.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 80940 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+820.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 81940 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+830.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 82940 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+840.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 83940 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+850.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 84940 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+860.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 85941 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+870.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 86941 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+880.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 87941 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+890.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 88941 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+900.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 89941 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+910.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 90942 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+920.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 91942 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+930.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 92942 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+940.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 93942 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+950.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 94942 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+960.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 95943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+970.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 96943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+980.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 97943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+990.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 98943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 99943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 100943 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30845 0 0 0 101944 73 0 0 25 0 1 0 479965803 127406080 30596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30596 603 41 0 31064 0
vsize: 124420
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30846 0 0 0 102944 73 0 0 25 0 1 0 479965803 127406080 30597 4294967295 134512640 134672761 3221224544 3221223640 134616312 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30597 603 41 0 31064 0
vsize: 124420
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30846 0 0 0 103944 73 0 0 25 0 1 0 479965803 127406080 30597 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30597 603 41 0 31064 0
vsize: 124420
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30846 0 0 0 104944 73 0 0 25 0 1 0 479965803 127406080 30597 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30597 603 41 0 31064 0
vsize: 124420
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30846 0 0 0 105944 73 0 0 25 0 1 0 479965803 127406080 30597 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30597 603 41 0 31064 0
vsize: 124420
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 106944 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 107945 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 108945 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 109945 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 110945 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 111945 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 112946 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 113946 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30848 0 0 0 114946 73 0 0 25 0 1 0 479965803 127406080 30599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30599 603 41 0 31064 0
vsize: 124420
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30849 0 0 0 115946 73 0 0 25 0 1 0 479965803 127406080 30600 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30600 603 41 0 31064 0
vsize: 124420
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30849 0 0 0 116946 73 0 0 25 0 1 0 479965803 127406080 30600 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30600 603 41 0 31064 0
vsize: 124420
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30849 0 0 0 117947 73 0 0 25 0 1 0 479965803 127406080 30600 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30600 603 41 0 31064 0
vsize: 124420
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30849 0 0 0 118947 73 0 0 25 0 1 0 479965803 127406080 30600 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30600 603 41 0 31064 0
vsize: 124420
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31156
Raw data (stat): 31156 (minisat+) R 31155 28099 28098 0 -1 0 30849 0 0 0 119947 73 0 0 25 0 1 0 479965803 127406080 30600 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31105 30600 603 41 0 31064 0
vsize: 124420
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31156
Raw data (stat): 31156 (minisat+) Z 31155 28099 28098 0 -1 12 30849 0 0 0 119947 79 0 0 25 0 1 0 479965803 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.27
CPU user time (s): 1199.47
CPU system time (s): 0.798878
CPU usage (%): 100.017
Max. virtual memory (Kb): 124428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####