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/manquinho/logic-synthesis/normalized-f51m.b.opb
MD5SUM	4fc22abde8250807abd95442a25fac44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	18
Optimality of the best value was proved	NO
Number of terms in the objective function	407
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	407
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	407
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	406
Total number of constraints	538
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	18
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 5422

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 23:51:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3829 boxname=wulflinc12 idbench=69 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4fc22abde8250807abd95442a25fac44  /oldhome/oroussel/tmp/wulflinc12/normalized-f51m.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-f51m.b.opb /oldhome/oroussel/tmp/wulflinc12/normalized-f51m.b.opb
IDLAUNCH: 3829
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915464 kB
Buffers:         34872 kB
Cached:          65208 kB
SwapCached:         16 kB
Active:          60504 kB
Inactive:        42392 kB
HighTotal:      131008 kB
HighFree:        61936 kB
LowTotal:       903652 kB
LowFree:        853528 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10772 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:11:11 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3829 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 498 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     470    12717 |     140       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  288/288          
c |         0 |     421    11795 |      --       0       --      -- |     --   | -49/-922
c |         0 |     421    11795 |     168       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.151976 s)
c ==============================================================================
c [1mFound solution: 26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:14920     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   16527    49348 |    4958       1       18    18.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10906          
c   -- var.elim.:  2000/10906          
c   -- var.elim.:  3000/10906          
c   -- var.elim.:  4000/10906          
c   -- var.elim.:  5000/10906          
c   -- var.elim.:  6000/10906          
c   -- var.elim.:  7000/10906          
c   -- var.elim.:  8000/10906          
c   -- var.elim.:  9000/10906          
c   -- var.elim.:  10000/10906          
c   -- var.elim.:  10906/10906          
c   -- var.elim.:  1000/5419          
c   -- var.elim.:  2000/5419          
c   -- var.elim.:  3000/5419          
c   -- var.elim.:  4000/5419          
c   -- var.elim.:  5000/5419          
c   -- var.elim.:  5419/5419          
c   -- subsuming                       
c   -- var.elim.:  1000/4320          
c   -- var.elim.:  2000/4320          
c   -- var.elim.:  3000/4320          
c   -- var.elim.:  4000/4320          
c   -- var.elim.:  4320/4320          
c   -- var.elim.:  24/24          
c |         1 |   11238    77026 |      --       1       --      -- |     --   | -5289/27679
c |         1 |   11238    77026 |    4495       1       18    18.0 |  0.000 % |
c |       101 |   11238    77026 |    4944     101     3915    38.8 |  0.111 % |
c |       251 |   11238    77026 |    5439     251    11297    45.0 |  0.111 % |
c ==============================================================================
c (current CPU-time: 6.06808 s)
c ==============================================================================
c [1mFound solution: 23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       266 |   11420    77523 |    3425     266    11739    44.1 |  0.111 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3742          
c   -- var.elim.:  2000/3742          
c   -- var.elim.:  3000/3742          
c   -- var.elim.:  3742/3742          
c   -- var.elim.:  1000/3598          
c   -- var.elim.:  2000/3598          
c   -- var.elim.:  3000/3598          
c   -- var.elim.:  3598/3598          
c   -- var.elim.:  1000/1227          
c   -- var.elim.:  1227/1227          
c   -- var.elim.:  1000/1346          
c   -- var.elim.:  1346/1346          
c   -- var.elim.:  659/659          
c   -- var.elim.:  111/111          
c   -- subsuming                       
c   -- var.elim.:  1000/1476          
c   -- var.elim.:  1476/1476          
c |       266 |    9601    61967 |      --     266       --      -- |     --   | -972/1347
c |       266 |    9601    61967 |    3840      97     2429    25.0 |  0.111 % |
c |       366 |    9601    61967 |    4224     197     7085    36.0 |  4.043 % |
c |       516 |    9595    61941 |    4643     345    18384    53.3 |  4.085 % |
c ==============================================================================
c (current CPU-time: 8.28374 s)
c ==============================================================================
c [1mFound solution: 22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       619 |   13164    71777 |    3949     448    24533    54.8 |  4.085 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5500          
c   -- var.elim.:  2000/5500          
c   -- var.elim.:  3000/5500          
c   -- var.elim.:  4000/5500          
c   -- var.elim.:  5000/5500          
c   -- var.elim.:  5500/5500          
c   -- var.elim.:  1000/2861          
c   -- var.elim.:  2000/2861          
c   -- var.elim.:  2861/2861          
c   -- var.elim.:  1000/2490          
c   -- var.elim.:  2000/2490          
c   -- var.elim.:  2490/2490          
c   -- var.elim.:  845/845          
c   -- var.elim.:  290/290          
c   -- subsuming                       
c   -- var.elim.:  36/36          
c |       619 |    9637    62229 |      --     448       --      -- |     --   | -3527/-9547
c |       619 |    9637    62229 |    3854     448    24533    54.8 |  4.085 % |
c ==============================================================================
c (current CPU-time: 10.3784 s)
c ==============================================================================
c [1mFound solution: 21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       652 |    9644    62246 |    2893     481    26028    54.1 |  4.085 % |
c   -- subsuming                       
c   -- var.elim.:  50/50          
c   -- var.elim.:  96/96          
c |       652 |    9628    62185 |      --     481       --      -- |     --   | -3/17
c |       652 |    9628    62185 |    3851     442    23561    53.3 |  4.085 % |
c |       754 |    9628    62185 |    4236     544    28817    53.0 |  4.155 % |
c |       905 |    9628    62185 |    4659     695    38728    55.7 |  4.155 % |
c |      1130 |    9628    62185 |    5125     920    67838    73.7 |  4.155 % |
c |      1470 |    9628    62185 |    5638    1260    99491    79.0 |  4.155 % |
c |      1977 |    9628    62185 |    6202    1767   155378    87.9 |  4.155 % |
c |      2736 |    9628    62185 |    6822    2526   238503    94.4 |  4.155 % |
c |      3876 |    9628    62185 |    7504    3666   314518    85.8 |  4.155 % |
c |      5585 |    9628    62185 |    8255    5375   494538    92.0 |  4.155 % |
c |      8147 |    9628    62185 |    9080    7937   751282    94.7 |  4.155 % |
c ==============================================================================
c (current CPU-time: 23.6064 s)
c ==============================================================================
c [1mFound solution: 20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11288 |   15117    77334 |    4535    7798   723535    92.8 |  4.155 % |
c   -- subsuming                       
c   -- var.elim.:  1000/8508          
c   -- var.elim.:  2000/8508          
c   -- var.elim.:  3000/8508          
c   -- var.elim.:  4000/8508          
c   -- var.elim.:  5000/8508          
c   -- var.elim.:  6000/8508          
c   -- var.elim.:  7000/8508          
c   -- var.elim.:  8000/8508          
c   -- var.elim.:  8508/8508          
c   -- var.elim.:  1000/4383          
c   -- var.elim.:  2000/4383          
c   -- var.elim.:  3000/4383          
c   -- var.elim.:  4000/4383          
c   -- var.elim.:  4383/4383          
c   -- var.elim.:  1000/3735          
c   -- var.elim.:  2000/3735          
c   -- var.elim.:  3000/3735          
c   -- var.elim.:  3735/3735          
c   -- var.elim.:  1000/1572          
c   -- var.elim.:  1572/1572          
c   -- var.elim.:  200/200          
c   -- subsuming                       
c   -- var.elim.:  27/27          
c |     11288 |    9659    62332 |      --    7798       --      -- |     --   | -5458/-15001
c |     11288 |    9659    62332 |    3863    7798   723535    92.8 |  4.155 % |
c |     11388 |    9659    62332 |    4249    3566   288122    80.8 |  4.168 % |
c |     11541 |    9659    62332 |    4674    3719   296448    79.7 |  4.168 % |
c |     11766 |    9659    62332 |    5142    3944   311018    78.9 |  4.168 % |
c |     12103 |    9659    62332 |    5656    4281   327911    76.6 |  4.168 % |
c |     12610 |    9659    62332 |    6222    4788   398332    83.2 |  4.168 % |
c |     13373 |    9659    62332 |    6844    5551   457120    82.3 |  4.168 % |
c |     14512 |    9659    62332 |    7529    6690   582304    87.0 |  4.168 % |
c |     16223 |    9659    62332 |    8281    8401   745672    88.8 |  4.168 % |
c |     18785 |    9659    62332 |    9110    7833   704061    89.9 |  4.168 % |
c |     22629 |    9659    62332 |   10021    8062   667544    82.8 |  4.168 % |
c |     28395 |    9659    62332 |   11023   10213   824119    80.7 |  4.168 % |
c |     37044 |    9659    62332 |   12125   11069   977361    88.3 |  4.168 % |
c |     50018 |    9659    62332 |   13338   11240  1148416   102.2 |  4.168 % |
c |     69480 |    9659    62332 |   14672   11699  1145779    97.9 |  4.168 % |
c ==============================================================================
c (current CPU-time: 172.946 s)
c ==============================================================================
c [1mFound solution: 19[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     84321 |    9669    62357 |    2900   11119   945400    85.0 |  4.168 % |
c   -- subsuming                       
c   -- var.elim.:  328/328          
c   -- var.elim.:  208/208          
c   -- var.elim.:  57/57          
c   -- var.elim.:  19/19          
c |     84321 |    9533    61347 |      --   11119       --      -- |     --   | -21/38
c |     84321 |    9533    61347 |    3813    5439   350572    64.5 |  4.168 % |
c |     84423 |    9533    61347 |    4194    3728   218719    58.7 |  4.643 % |
c |     84573 |    9533    61347 |    4613    3878   230216    59.4 |  4.643 % |
c |     84800 |    9533    61347 |    5075    4105   243512    59.3 |  4.643 % |
c |     85140 |    9533    61347 |    5582    4445   267231    60.1 |  4.643 % |
c |     85649 |    9533    61347 |    6141    4954   304228    61.4 |  4.643 % |
c |     86408 |    9533    61347 |    6755    5713   343371    60.1 |  4.643 % |
c |     87547 |    9533    61347 |    7430    6852   421272    61.5 |  4.643 % |
c |     89257 |    9533    61347 |    8173    5805   367718    63.3 |  4.643 % |
c |     91820 |    9533    61347 |    8991    8368   545186    65.2 |  4.643 % |
c |     95664 |    9533    61347 |    9890    8952   578524    64.6 |  4.643 % |
c |    101431 |    9533    61347 |   10879   10766   814943    75.7 |  4.643 % |
c |    110080 |    9533    61347 |   11967   11734   892373    76.1 |  4.643 % |
c |    123056 |    9533    61347 |   13164   12013   750923    62.5 |  4.643 % |
c |    142519 |    9522    61283 |   14463   12327   828550    67.2 |  4.706 % |
c ==============================================================================
c (current CPU-time: 298.499 s)
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    152948 |   12935    70731 |    3880   12234  1068889    87.4 |  4.706 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5402          
c   -- var.elim.:  2000/5402          
c   -- var.elim.:  3000/5402          
c   -- var.elim.:  4000/5402          
c   -- var.elim.:  5000/5402          
c   -- var.elim.:  5402/5402          
c   -- var.elim.:  1000/2770          
c   -- var.elim.:  2000/2770          
c   -- var.elim.:  2770/2770          
c   -- var.elim.:  1000/2486          
c   -- var.elim.:  2000/2486          
c   -- var.elim.:  2486/2486          
c   -- var.elim.:  844/844          
c   -- var.elim.:  67/67          
c   -- subsuming                       
c   -- var.elim.:  47/47          
c |    152948 |    9547    61462 |      --   12234       --      -- |     --   | -3388/-9268
c |    152948 |    9547    61462 |    3818   12196  1064752    87.3 |  4.706 % |
c |    153048 |    9547    61462 |    4200    3714   256587    69.1 |  4.738 % |
c |    153198 |    9547    61462 |    4620    3864   265202    68.6 |  4.737 % |
c |    153427 |    9547    61462 |    5082    4093   280729    68.6 |  4.737 % |
c |    153767 |    9547    61462 |    5591    4433   296098    66.8 |  4.737 % |
c |    154273 |    9547    61462 |    6150    4939   315836    63.9 |  4.737 % |
c |    155032 |    9547    61462 |    6765    5698   354169    62.2 |  4.737 % |
c |    156172 |    9547    61462 |    7441    6838   437616    64.0 |  4.737 % |
c |    157880 |    9547    61462 |    8185    5812   315712    54.3 |  4.737 % |
c |    160442 |    9547    61462 |    9004    8374   474816    56.7 |  4.737 % |
c |    164286 |    9547    61462 |    9904    8990   523700    58.3 |  4.737 % |
c |    170053 |    9547    61462 |   10895   11123   593938    53.4 |  4.738 % |
c |    178702 | #### 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.85 0.95 0.90 2/54 29363
Raw data (stat): 29363 (runsolver) R 29362 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421824145 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 2592 0 0 0 987 11 0 0 25 0 1 0 421824145 10661888 2098 4294967295 134512640 134672761 3221224576 3221223024 134643518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2603 2098 603 41 0 2562 0
vsize: 10412
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 3641 0 0 0 1982 16 0 0 25 0 1 0 421824145 13717504 2845 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3349 2845 603 41 0 3308 0
vsize: 13396
[startup+30.001 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4229 0 0 0 2978 20 0 0 25 0 1 0 421824145 15953920 3265 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3265 603 41 0 3854 0
vsize: 15580
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4229 0 0 0 3978 20 0 0 25 0 1 0 421824145 15953920 3265 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3895 3265 603 41 0 3854 0
vsize: 15580
[startup+50.002 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4337 0 0 0 4978 20 0 0 25 0 1 0 421824145 16347136 3373 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3373 603 41 0 3950 0
vsize: 15964
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4338 0 0 0 5978 20 0 0 25 0 1 0 421824145 16347136 3374 4294967295 134512640 134672761 3221224576 3221223760 134615563 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3991 3374 603 41 0 3950 0
vsize: 15964
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4419 0 0 0 6978 20 0 0 25 0 1 0 421824145 16740352 3455 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4087 3455 603 41 0 4046 0
vsize: 16348
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4588 0 0 0 7978 21 0 0 25 0 1 0 421824145 17399808 3624 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4248 3624 603 41 0 4207 0
vsize: 16992
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4750 0 0 0 8978 21 0 0 25 0 1 0 421824145 18063360 3786 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4410 3786 603 41 0 4369 0
vsize: 17640
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4775 0 0 0 9978 22 0 0 25 0 1 0 421824145 18194432 3811 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4442 3811 603 41 0 4401 0
vsize: 17768
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4825 0 0 0 10978 22 0 0 25 0 1 0 421824145 18325504 3861 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4474 3861 603 41 0 4433 0
vsize: 17896
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4825 0 0 0 11978 22 0 0 25 0 1 0 421824145 18325504 3861 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4474 3861 603 41 0 4433 0
vsize: 17896
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4826 0 0 0 12978 22 0 0 25 0 1 0 421824145 18325504 3862 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4474 3862 603 41 0 4433 0
vsize: 17896
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 4934 0 0 0 13978 22 0 0 25 0 1 0 421824145 18862080 3970 4294967295 134512640 134672761 3221224576 3221223616 134612927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4605 3970 603 41 0 4564 0
vsize: 18420
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5157 0 0 0 14977 23 0 0 25 0 1 0 421824145 19734528 4193 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4818 4193 603 41 0 4777 0
vsize: 19272
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5164 0 0 0 15977 23 0 0 25 0 1 0 421824145 19734528 4200 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4818 4200 603 41 0 4777 0
vsize: 19272
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5164 0 0 0 16978 23 0 0 25 0 1 0 421824145 19734528 4200 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4818 4200 603 41 0 4777 0
vsize: 19272
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 17974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223776 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 18974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 19973 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 20974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 21974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 22974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 23974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 24974 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 25975 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223616 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 26975 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 27975 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 5785 0 0 0 28975 26 0 0 25 0 1 0 421824145 20578304 4414 4294967295 134512640 134672761 3221224576 3221223616 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5024 4414 603 41 0 4983 0
vsize: 20096
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 29972 29 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223024 134643963 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 30972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 31972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223616 134613818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 32972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223712 134614656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 33972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 34971 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 35972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 36972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 37972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 38972 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 39973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 40973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 41973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223712 134614812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 42973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 43973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223616 134612471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 44973 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 45974 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6244 0 0 0 46974 30 0 0 25 0 1 0 421824145 19832832 4274 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4842 4274 603 41 0 4801 0
vsize: 19368
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6261 0 0 0 47974 30 0 0 25 0 1 0 421824145 19963904 4291 4294967295 134512640 134672761 3221224576 3221223728 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4291 603 41 0 4833 0
vsize: 19496
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6261 0 0 0 48974 30 0 0 25 0 1 0 421824145 19963904 4291 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4291 603 41 0 4833 0
vsize: 19496
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6261 0 0 0 49975 30 0 0 25 0 1 0 421824145 19963904 4291 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4291 603 41 0 4833 0
vsize: 19496
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6261 0 0 0 50975 30 0 0 25 0 1 0 421824145 19963904 4291 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4291 603 41 0 4833 0
vsize: 19496
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6261 0 0 0 51975 30 0 0 25 0 1 0 421824145 19963904 4291 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4291 603 41 0 4833 0
vsize: 19496
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29363
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6262 0 0 0 52975 30 0 0 25 0 1 0 421824145 19963904 4292 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4292 603 41 0 4833 0
vsize: 19496
[startup+540.021 s]
Raw data (loadavg): 1.07 0.99 0.91 3/59 29415
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6262 0 0 0 53975 30 0 0 25 0 1 0 421824145 19963904 4292 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4292 603 41 0 4833 0
vsize: 19496
[startup+550.022 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6262 0 0 0 54975 30 0 0 25 0 1 0 421824145 19963904 4292 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4292 603 41 0 4833 0
vsize: 19496
[startup+560.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6262 0 0 0 55976 30 0 0 25 0 1 0 421824145 19963904 4292 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4292 603 41 0 4833 0
vsize: 19496
[startup+570.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6263 0 0 0 56976 30 0 0 25 0 1 0 421824145 19963904 4293 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4293 603 41 0 4833 0
vsize: 19496
[startup+580.023 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6263 0 0 0 57976 30 0 0 25 0 1 0 421824145 19963904 4293 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4293 603 41 0 4833 0
vsize: 19496
[startup+590.023 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6263 0 0 0 58976 30 0 0 25 0 1 0 421824145 19963904 4293 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4293 603 41 0 4833 0
vsize: 19496
[startup+600.023 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6263 0 0 0 59976 30 0 0 25 0 1 0 421824145 19963904 4293 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4293 603 41 0 4833 0
vsize: 19496
[startup+610.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29416
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6273 0 0 0 60977 30 0 0 25 0 1 0 421824145 19996672 4302 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4882 4302 603 41 0 4841 0
vsize: 19528
[startup+620.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6273 0 0 0 61977 30 0 0 25 0 1 0 421824145 19996672 4302 4294967295 134512640 134672761 3221224576 3221223672 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4882 4302 603 41 0 4841 0
vsize: 19528
[startup+630.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6273 0 0 0 62977 30 0 0 25 0 1 0 421824145 19996672 4302 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4882 4302 603 41 0 4841 0
vsize: 19528
[startup+640.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6289 0 0 0 63977 30 0 0 25 0 1 0 421824145 20062208 4317 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+650.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6289 0 0 0 64977 30 0 0 25 0 1 0 421824145 20062208 4317 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4898 4317 603 41 0 4857 0
vsize: 19592
[startup+660.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6298 0 0 0 65978 30 0 0 25 0 1 0 421824145 20094976 4325 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4325 603 41 0 4865 0
vsize: 19624
[startup+670.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6299 0 0 0 66978 30 0 0 25 0 1 0 421824145 20094976 4326 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4326 603 41 0 4865 0
vsize: 19624
[startup+680.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6299 0 0 0 67978 30 0 0 25 0 1 0 421824145 20094976 4326 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4326 603 41 0 4865 0
vsize: 19624
[startup+690.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6299 0 0 0 68978 30 0 0 25 0 1 0 421824145 20094976 4326 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4326 603 41 0 4865 0
vsize: 19624
[startup+700.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6299 0 0 0 69978 30 0 0 25 0 1 0 421824145 20094976 4326 4294967295 134512640 134672761 3221224576 3221223776 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4326 603 41 0 4865 0
vsize: 19624
[startup+710.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6299 0 0 0 70979 30 0 0 25 0 1 0 421824145 20094976 4326 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4906 4326 603 41 0 4865 0
vsize: 19624
[startup+720.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6314 0 0 0 71979 30 0 0 25 0 1 0 421824145 20160512 4340 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4340 603 41 0 4881 0
vsize: 19688
[startup+730.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6315 0 0 0 72979 30 0 0 25 0 1 0 421824145 20160512 4341 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4341 603 41 0 4881 0
vsize: 19688
[startup+740.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6315 0 0 0 73979 30 0 0 25 0 1 0 421824145 20160512 4341 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4341 603 41 0 4881 0
vsize: 19688
[startup+750.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6330 0 0 0 74979 30 0 0 25 0 1 0 421824145 20205568 4355 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4933 4355 603 41 0 4892 0
vsize: 19732
[startup+760.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6330 0 0 0 75979 30 0 0 25 0 1 0 421824145 20205568 4355 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4933 4355 603 41 0 4892 0
vsize: 19732
[startup+770.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6358 0 0 0 76979 30 0 0 25 0 1 0 421824145 20328448 4383 4294967295 134512640 134672761 3221224576 3221223760 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4963 4383 603 41 0 4922 0
vsize: 19852
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6358 0 0 0 77980 30 0 0 25 0 1 0 421824145 20328448 4383 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4963 4383 603 41 0 4922 0
vsize: 19852
[startup+790.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6362 0 0 0 78980 30 0 0 25 0 1 0 421824145 20336640 4386 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4965 4386 603 41 0 4924 0
vsize: 19860
[startup+800.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6362 0 0 0 79980 30 0 0 25 0 1 0 421824145 20336640 4386 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4965 4386 603 41 0 4924 0
vsize: 19860
[startup+810.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6372 0 0 0 80980 30 0 0 25 0 1 0 421824145 20369408 4395 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4973 4395 603 41 0 4932 0
vsize: 19892
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6372 0 0 0 81980 30 0 0 25 0 1 0 421824145 20369408 4395 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4973 4395 603 41 0 4932 0
vsize: 19892
[startup+830.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6372 0 0 0 82980 30 0 0 25 0 1 0 421824145 20369408 4395 4294967295 134512640 134672761 3221224576 3221223760 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4973 4395 603 41 0 4932 0
vsize: 19892
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6476 0 0 0 83980 31 0 0 25 0 1 0 421824145 20795392 4498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5077 4498 603 41 0 5036 0
vsize: 20308
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6476 0 0 0 84980 31 0 0 25 0 1 0 421824145 20795392 4498 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5077 4498 603 41 0 5036 0
vsize: 20308
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6553 0 0 0 85980 31 0 0 25 0 1 0 421824145 21106688 4574 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5153 4574 603 41 0 5112 0
vsize: 20612
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29418
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6553 0 0 0 86980 31 0 0 25 0 1 0 421824145 21106688 4574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5153 4574 603 41 0 5112 0
vsize: 20612
[startup+880.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6597 0 0 0 87981 31 0 0 25 0 1 0 421824145 21282816 4617 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5196 4617 603 41 0 5155 0
vsize: 20784
[startup+890.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6597 0 0 0 88981 31 0 0 25 0 1 0 421824145 21282816 4617 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5196 4617 603 41 0 5155 0
vsize: 20784
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6597 0 0 0 89981 31 0 0 25 0 1 0 421824145 21282816 4617 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5196 4617 603 41 0 5155 0
vsize: 20784
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6597 0 0 0 90981 31 0 0 25 0 1 0 421824145 21270528 4616 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5193 4616 603 41 0 5152 0
vsize: 20772
[startup+920.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6597 0 0 0 91981 31 0 0 25 0 1 0 421824145 21270528 4616 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5193 4616 603 41 0 5152 0
vsize: 20772
[startup+930.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6598 0 0 0 92981 31 0 0 25 0 1 0 421824145 21270528 4617 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5193 4617 603 41 0 5152 0
vsize: 20772
[startup+940.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6598 0 0 0 93982 31 0 0 25 0 1 0 421824145 21270528 4617 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5193 4617 603 41 0 5152 0
vsize: 20772
[startup+950.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6598 0 0 0 94982 31 0 0 25 0 1 0 421824145 21270528 4617 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5193 4617 603 41 0 5152 0
vsize: 20772
[startup+960.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6598 0 0 0 95982 31 0 0 25 0 1 0 421824145 21262336 4616 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5191 4616 603 41 0 5150 0
vsize: 20764
[startup+970.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6598 0 0 0 96982 31 0 0 25 0 1 0 421824145 21262336 4616 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5191 4616 603 41 0 5150 0
vsize: 20764
[startup+980.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6599 0 0 0 97982 31 0 0 25 0 1 0 421824145 21262336 4617 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5191 4617 603 41 0 5150 0
vsize: 20764
[startup+990.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6599 0 0 0 98982 31 0 0 25 0 1 0 421824145 21262336 4617 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5191 4617 603 41 0 5150 0
vsize: 20764
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6608 0 0 0 99983 31 0 0 25 0 1 0 421824145 21393408 4626 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5223 4626 603 41 0 5182 0
vsize: 20892
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6635 0 0 0 100983 31 0 0 25 0 1 0 421824145 21422080 4652 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4652 603 41 0 5189 0
vsize: 20920
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6645 0 0 0 101983 31 0 0 25 0 1 0 421824145 21422080 4662 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5230 4662 603 41 0 5189 0
vsize: 20920
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6768 0 0 0 102982 31 0 0 25 0 1 0 421824145 21962752 4784 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5362 4784 603 41 0 5321 0
vsize: 21448
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6768 0 0 0 103983 31 0 0 25 0 1 0 421824145 21962752 4784 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5362 4784 603 41 0 5321 0
vsize: 21448
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6781 0 0 0 104983 31 0 0 25 0 1 0 421824145 22011904 4796 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5374 4796 603 41 0 5333 0
vsize: 21496
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6782 0 0 0 105983 31 0 0 25 0 1 0 421824145 22011904 4797 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5374 4797 603 41 0 5333 0
vsize: 21496
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 106983 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 107983 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 108984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 109984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223832 134618007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 110984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 111984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223776 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 112984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 113984 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 114985 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6803 0 0 0 115985 31 0 0 25 0 1 0 421824145 22110208 4818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4818 603 41 0 5357 0
vsize: 21592
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6852 0 0 0 116985 32 0 0 25 0 1 0 421824145 22306816 4866 4294967295 134512640 134672761 3221224576 3221223712 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5446 4866 603 41 0 5405 0
vsize: 21784
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6852 0 0 0 117985 32 0 0 25 0 1 0 421824145 22306816 4866 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5446 4866 603 41 0 5405 0
vsize: 21784
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 6991 0 0 0 118985 32 0 0 25 0 1 0 421824145 22962176 5005 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5606 5005 603 41 0 5565 0
vsize: 22424
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29420
Raw data (stat): 29363 (minisat+) R 29362 25285 25284 0 -1 0 7154 0 0 0 119985 32 0 0 25 0 1 0 421824145 23535616 5167 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5746 5167 603 41 0 5705 0
vsize: 22984
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29420
Raw data (stat): 29363 (minisat+) Z 29362 25285 25284 0 -1 12 7155 0 0 0 119985 34 0 0 25 0 1 0 421824145 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: 10
Real time (s): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1199.85
CPU system time (s): 0.342947
CPU usage (%): 100.012
Max. virtual memory (Kb): 22984
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####