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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc03.opb
MD5SUM	0a25291690224f6f7c8a4bead47a7b72
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1478528
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11386239
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.20881
Number of variables	180
Total number of constraints	255
Number of constraints which are clauses	31
Number of constraints which are cardinality constraints (but not clauses)	170
Number of constraints which are nor clauses,nor cardinality constraints	54
Minimum length of a constraint	1
Maximum length of a constraint	159
Trace number 19160

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 18:05:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16964 boxname=wulflinc23 idbench=1305 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0a25291690224f6f7c8a4bead47a7b72  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-misc03.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-misc03.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-misc03.opb
IDLAUNCH: 16964
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        632704 kB
Buffers:         27492 kB
Cached:         348828 kB
SwapCached:        536 kB
Active:          38804 kB
Inactive:       339612 kB
HighTotal:      131008 kB
HighFree:         9184 kB
LowTotal:       903652 kB
LowFree:        623520 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            17996 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:25:49 (client local time) WITH STATUS 10 IN 1200.29 SECONDS
stats: 16964 7 1200.29 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 123 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################
c   -- Clauses(.)/Splits(s): ...............................
c ---[ 121]---> BDD-cost:531660
c ---[ 119]---> BDD-cost:   39
c ---[ 117]---> BDD-cost:   39
c ---[ 115]---> BDD-cost:   39
c ---[ 113]---> BDD-cost:   39
c ---[ 111]---> BDD-cost:   39
c ---[ 110]---> BDD-cost:   98
c ---[ 109]---> BDD-cost:   98
c ---[ 108]---> BDD-cost:   98
c ---[  75]---> BDD-cost:   46
c ---[  73]---> BDD-cost:   46
c ---[  71]---> BDD-cost:   46
c ---[  69]---> BDD-cost:   46
c ---[  67]---> BDD-cost:   46
c ---[  65]---> BDD-cost:   46
c ---[  63]---> BDD-cost:   46
c ---[  61]---> BDD-cost:   46
c ---[  59]---> BDD-cost:   46
c ---[  57]---> BDD-cost:   46
c ---[  55]---> BDD-cost:   46
c ---[  53]---> BDD-cost:   46
c ---[  51]---> BDD-cost:   46
c ---[  49]---> BDD-cost:   46
c ---[  47]---> BDD-cost:   46
c ---[  45]---> BDD-cost:   46
c ---[  43]---> BDD-cost:   46
c ---[  41]---> BDD-cost:   46
c ---[  39]---> BDD-cost:   46
c ---[  37]---> BDD-cost:   46
c ---[  35]---> BDD-cost:   46
c ---[  34]---> BDD-cost:   17
c ---[  33]---> BDD-cost:   17
c ---[  32]---> BDD-cost:   17
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   21
c ---[  28]---> BDD-cost:   21
c ---[  27]---> BDD-cost:   21
c ---[  26]---> BDD-cost:   21
c ---[  25]---> BDD-cost:   21
c ---[  24]---> BDD-cost:   21
c ---[  23]---> BDD-cost:   38
c ---[  22]---> BDD-cost:   38
c ---[  21]---> BDD-cost:   38
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   38
c ---[  16]---> BDD-cost:   38
c ---[  15]---> BDD-cost:   38
c ---[  14]---> BDD-cost:   21
c ---[  13]---> BDD-cost:   21
c ---[  12]---> BDD-cost:   21
c ---[  11]---> BDD-cost:   38
c ---[  10]---> BDD-cost:   38
c ---[   9]---> BDD-cost:   38
c ---[   8]---> BDD-cost:   21
c ---[   7]---> BDD-cost:   21
c ---[   6]---> BDD-cost:   21
c ---[   5]---> BDD-cost:   38
c ---[   4]---> BDD-cost:   38
c ---[   3]---> BDD-cost:   38
c ---[   2]---> BDD-cost:   21
c ---[   1]---> BDD-cost:   21
c ---[   0]---> BDD-cost:   21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1546605  4535117 |  515535       0        0     nan |  0.000 % |
c |       100 | 1546605  4535117 |  567088     100     4043    40.4 |  0.012 % |
c ==============================================================================
c [1mFound solution: 1663488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  127     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       108 | 1546874  4535748 |  515624     108     4305    39.9 |  0.012 % |
c ==============================================================================
c [1mFound solution: 1548288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   34     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 | 1546930  4535883 |  515643     118     4741    40.2 |  0.012 % |
c |       219 | 1546930  4535883 |  567207     219     9401    42.9 |  0.013 % |
c ==============================================================================
c [1mFound solution: 1527168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       325 | 1547063  4536197 |  515687     325    14186    43.6 |  0.013 % |
c |       425 | 1547063  4536197 |  567255     425    18126    42.6 |  0.013 % |
c ==============================================================================
c [1mFound solution: 1478528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       501 | 1547168  4536446 |  515722     501    21377    42.7 |  0.013 % |
c |       601 | 1547168  4536446 |  567294     601    27500    45.8 |  0.013 % |
c |       756 | 1547168  4536446 |  624023     756    49317    65.2 |  0.013 % |
c |       984 | 1547168  4536446 |  686425     984    62896    63.9 |  0.013 % |
c |      1323 | 1547168  4536446 |  755068    1323    78224    59.1 |  0.013 % |
c |      1829 | 1547168  4536446 |  830575    1829   103047    56.3 |  0.013 % |
c |      2589 | 1547168  4536446 |  913632    2589   141039    54.5 |  0.013 % |
c |      3728 | 1547168  4536446 | 1004996    3728   189767    50.9 |  0.013 % |
c |      5437 | 1547168  4536446 | 1105495    5437   264426    48.6 |  0.013 % |
#### 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.82 0.94 0.90 2/54 9850
Raw data (stat): 9850 (runsolver) R 9849 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547104868 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.85 0.94 0.91 2/54 9850
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 48775 0 0 0 885 114 0 0 25 0 1 0 547104868 231997440 44812 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56640 44812 603 41 0 56599 0
vsize: 226560
[startup+20.0019 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 9850
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49056 0 0 0 1884 115 0 0 25 0 1 0 547104868 232808448 45093 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56838 45093 603 41 0 56797 0
vsize: 227352
[startup+30.002 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 9850
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49807 0 0 0 2883 117 0 0 25 0 1 0 547104868 237387776 45844 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57956 45844 603 41 0 57915 0
vsize: 231824
[startup+40.0032 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49818 0 0 0 3882 117 0 0 25 0 1 0 547104868 237387776 45855 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57956 45855 603 41 0 57915 0
vsize: 231824
[startup+50.0038 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49823 0 0 0 4882 118 0 0 25 0 1 0 547104868 237518848 45860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45860 603 41 0 57947 0
vsize: 231952
[startup+60.0032 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49830 0 0 0 5881 118 0 0 25 0 1 0 547104868 237518848 45867 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45867 603 41 0 57947 0
vsize: 231952
[startup+70.0044 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49838 0 0 0 6881 119 0 0 25 0 1 0 547104868 237518848 45875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45875 603 41 0 57947 0
vsize: 231952
[startup+80.0048 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49849 0 0 0 7881 119 0 0 25 0 1 0 547104868 237518848 45886 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57988 45886 603 41 0 57947 0
vsize: 231952
[startup+90.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 8881 119 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+100.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 9880 120 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 10880 120 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+120.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 11880 120 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 12880 120 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 13880 121 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+150.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 14880 121 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+160.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49989 0 0 0 15880 121 0 0 25 0 1 0 547104868 238166016 46026 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58146 46026 603 41 0 58105 0
vsize: 232584
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49995 0 0 0 16880 121 0 0 25 0 1 0 547104868 238170112 46031 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58147 46031 603 41 0 58106 0
vsize: 232588
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49995 0 0 0 17880 121 0 0 25 0 1 0 547104868 238170112 46031 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58147 46031 603 41 0 58106 0
vsize: 232588
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49997 0 0 0 18881 121 0 0 25 0 1 0 547104868 238170112 46033 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58147 46033 603 41 0 58106 0
vsize: 232588
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 49997 0 0 0 19881 121 0 0 25 0 1 0 547104868 238170112 46033 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58147 46033 603 41 0 58106 0
vsize: 232588
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50001 0 0 0 20881 121 0 0 25 0 1 0 547104868 238170112 46037 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58147 46037 603 41 0 58106 0
vsize: 232588
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50015 0 0 0 21881 121 0 0 25 0 1 0 547104868 238256128 46051 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50015 0 0 0 22881 121 0 0 25 0 1 0 547104868 238256128 46051 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50015 0 0 0 23881 121 0 0 25 0 1 0 547104868 238256128 46051 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58168 46051 603 41 0 58127 0
vsize: 232672
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50017 0 0 0 24881 121 0 0 25 0 1 0 547104868 238256128 46053 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58168 46053 603 41 0 58127 0
vsize: 232672
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50025 0 0 0 25882 121 0 0 25 0 1 0 547104868 238415872 46061 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46061 603 41 0 58166 0
vsize: 232828
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50036 0 0 0 26882 121 0 0 25 0 1 0 547104868 238415872 46072 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46072 603 41 0 58166 0
vsize: 232828
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50036 0 0 0 27882 121 0 0 25 0 1 0 547104868 238415872 46072 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46072 603 41 0 58166 0
vsize: 232828
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50038 0 0 0 28881 121 0 0 25 0 1 0 547104868 238415872 46074 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46074 603 41 0 58166 0
vsize: 232828
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50038 0 0 0 29882 121 0 0 25 0 1 0 547104868 238415872 46074 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46074 603 41 0 58166 0
vsize: 232828
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50038 0 0 0 30882 122 0 0 25 0 1 0 547104868 238415872 46074 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46074 603 41 0 58166 0
vsize: 232828
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50052 0 0 0 31882 122 0 0 25 0 1 0 547104868 238415872 46088 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46088 603 41 0 58166 0
vsize: 232828
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50053 0 0 0 32882 122 0 0 25 0 1 0 547104868 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50053 0 0 0 33882 122 0 0 25 0 1 0 547104868 238415872 46089 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50053 0 0 0 34882 122 0 0 25 0 1 0 547104868 238415872 46089 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46089 603 41 0 58166 0
vsize: 232828
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50054 0 0 0 35883 122 0 0 25 0 1 0 547104868 238415872 46090 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46090 603 41 0 58166 0
vsize: 232828
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50054 0 0 0 36883 122 0 0 25 0 1 0 547104868 238415872 46090 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46090 603 41 0 58166 0
vsize: 232828
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50066 0 0 0 37883 122 0 0 25 0 1 0 547104868 238415872 46102 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46102 603 41 0 58166 0
vsize: 232828
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50066 0 0 0 38883 122 0 0 25 0 1 0 547104868 238415872 46102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46102 603 41 0 58166 0
vsize: 232828
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50067 0 0 0 39883 122 0 0 25 0 1 0 547104868 238415872 46103 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58207 46103 603 41 0 58166 0
vsize: 232828
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50068 0 0 0 40883 122 0 0 25 0 1 0 547104868 238415872 46104 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58207 46104 603 41 0 58166 0
vsize: 232828
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50086 0 0 0 41883 122 0 0 25 0 1 0 547104868 238551040 46122 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58240 46122 603 41 0 58199 0
vsize: 232960
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50088 0 0 0 42883 122 0 0 25 0 1 0 547104868 238551040 46124 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58240 46124 603 41 0 58199 0
vsize: 232960
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50088 0 0 0 43883 122 0 0 25 0 1 0 547104868 238551040 46124 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58240 46124 603 41 0 58199 0
vsize: 232960
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50097 0 0 0 44883 123 0 0 25 0 1 0 547104868 238551040 46133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58240 46133 603 41 0 58199 0
vsize: 232960
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50105 0 0 0 45883 123 0 0 25 0 1 0 547104868 238637056 46141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46141 603 41 0 58220 0
vsize: 233044
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50106 0 0 0 46883 123 0 0 25 0 1 0 547104868 238637056 46142 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46142 603 41 0 58220 0
vsize: 233044
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50108 0 0 0 47883 123 0 0 25 0 1 0 547104868 238637056 46144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46144 603 41 0 58220 0
vsize: 233044
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50108 0 0 0 48883 123 0 0 25 0 1 0 547104868 238637056 46144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46144 603 41 0 58220 0
vsize: 233044
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50112 0 0 0 49884 123 0 0 25 0 1 0 547104868 238637056 46148 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46148 603 41 0 58220 0
vsize: 233044
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50112 0 0 0 50884 123 0 0 25 0 1 0 547104868 238637056 46148 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58261 46148 603 41 0 58220 0
vsize: 233044
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50125 0 0 0 51884 123 0 0 25 0 1 0 547104868 238731264 46161 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46161 603 41 0 58243 0
vsize: 233136
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50134 0 0 0 52884 123 0 0 25 0 1 0 547104868 238731264 46170 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46170 603 41 0 58243 0
vsize: 233136
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50134 0 0 0 53884 123 0 0 25 0 1 0 547104868 238731264 46170 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46170 603 41 0 58243 0
vsize: 233136
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50136 0 0 0 54884 123 0 0 25 0 1 0 547104868 238731264 46172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46172 603 41 0 58243 0
vsize: 233136
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50136 0 0 0 55885 123 0 0 25 0 1 0 547104868 238731264 46172 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46172 603 41 0 58243 0
vsize: 233136
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50141 0 0 0 56885 123 0 0 25 0 1 0 547104868 238731264 46177 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46177 603 41 0 58243 0
vsize: 233136
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50141 0 0 0 57884 123 0 0 25 0 1 0 547104868 238731264 46177 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46177 603 41 0 58243 0
vsize: 233136
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50141 0 0 0 58884 123 0 0 25 0 1 0 547104868 238731264 46177 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58284 46177 603 41 0 58243 0
vsize: 233136
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50147 0 0 0 59885 123 0 0 25 0 1 0 547104868 238800896 46183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46183 603 41 0 58260 0
vsize: 233204
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50152 0 0 0 60885 123 0 0 25 0 1 0 547104868 238800896 46188 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50152 0 0 0 61885 123 0 0 25 0 1 0 547104868 238800896 46188 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50152 0 0 0 62885 123 0 0 25 0 1 0 547104868 238800896 46188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58301 46188 603 41 0 58260 0
vsize: 233204
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50167 0 0 0 63885 123 0 0 25 0 1 0 547104868 238878720 46203 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58320 46203 603 41 0 58279 0
vsize: 233280
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50186 0 0 0 64885 124 0 0 25 0 1 0 547104868 238944256 46221 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46221 603 41 0 58295 0
vsize: 233344
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 65885 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 66885 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 67886 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 68886 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 69886 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 70886 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50188 0 0 0 71886 124 0 0 25 0 1 0 547104868 238944256 46223 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46223 603 41 0 58295 0
vsize: 233344
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50190 0 0 0 72886 124 0 0 25 0 1 0 547104868 238944256 46225 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58336 46225 603 41 0 58295 0
vsize: 233344
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50205 0 0 0 73887 124 0 0 25 0 1 0 547104868 239046656 46240 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50205 0 0 0 74887 124 0 0 25 0 1 0 547104868 239046656 46240 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50205 0 0 0 75887 124 0 0 25 0 1 0 547104868 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50205 0 0 0 76887 124 0 0 25 0 1 0 547104868 239046656 46240 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46240 603 41 0 58320 0
vsize: 233444
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50206 0 0 0 77887 124 0 0 25 0 1 0 547104868 239046656 46241 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46241 603 41 0 58320 0
vsize: 233444
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50222 0 0 0 78888 124 0 0 25 0 1 0 547104868 239046656 46257 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46257 603 41 0 58320 0
vsize: 233444
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50222 0 0 0 79888 124 0 0 25 0 1 0 547104868 239046656 46257 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46257 603 41 0 58320 0
vsize: 233444
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50222 0 0 0 80888 124 0 0 25 0 1 0 547104868 239046656 46257 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46257 603 41 0 58320 0
vsize: 233444
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50224 0 0 0 81888 124 0 0 25 0 1 0 547104868 239046656 46259 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58361 46259 603 41 0 58320 0
vsize: 233444
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50228 0 0 0 82888 124 0 0 25 0 1 0 547104868 239153152 46263 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46263 603 41 0 58346 0
vsize: 233548
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50237 0 0 0 83888 124 0 0 25 0 1 0 547104868 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50237 0 0 0 84888 124 0 0 25 0 1 0 547104868 239153152 46272 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50237 0 0 0 85888 125 0 0 25 0 1 0 547104868 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50237 0 0 0 86888 125 0 0 25 0 1 0 547104868 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+880.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50237 0 0 0 87888 125 0 0 25 0 1 0 547104868 239153152 46272 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58387 46272 603 41 0 58346 0
vsize: 233548
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50254 0 0 0 88888 125 0 0 25 0 1 0 547104868 239210496 46288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50254 0 0 0 89889 125 0 0 25 0 1 0 547104868 239210496 46288 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50254 0 0 0 90889 125 0 0 25 0 1 0 547104868 239210496 46288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46288 603 41 0 58360 0
vsize: 233604
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50255 0 0 0 91889 125 0 0 25 0 1 0 547104868 239210496 46289 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46289 603 41 0 58360 0
vsize: 233604
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50256 0 0 0 92889 125 0 0 25 0 1 0 547104868 239210496 46290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46290 603 41 0 58360 0
vsize: 233604
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50258 0 0 0 93889 125 0 0 25 0 1 0 547104868 239210496 46292 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46292 603 41 0 58360 0
vsize: 233604
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50265 0 0 0 94889 125 0 0 25 0 1 0 547104868 239210496 46299 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+960.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50265 0 0 0 95890 125 0 0 25 0 1 0 547104868 239210496 46299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50265 0 0 0 96890 125 0 0 25 0 1 0 547104868 239210496 46299 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46299 603 41 0 58360 0
vsize: 233604
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50266 0 0 0 97890 125 0 0 25 0 1 0 547104868 239210496 46300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46300 603 41 0 58360 0
vsize: 233604
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50266 0 0 0 98890 125 0 0 25 0 1 0 547104868 239210496 46300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58401 46300 603 41 0 58360 0
vsize: 233604
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50271 0 0 0 99890 125 0 0 25 0 1 0 547104868 239304704 46305 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58424 46305 603 41 0 58383 0
vsize: 233696
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50286 0 0 0 100890 125 0 0 25 0 1 0 547104868 239325184 46319 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46319 603 41 0 58388 0
vsize: 233716
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50287 0 0 0 101891 125 0 0 25 0 1 0 547104868 239325184 46320 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46320 603 41 0 58388 0
vsize: 233716
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50287 0 0 0 102890 126 0 0 25 0 1 0 547104868 239325184 46320 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46320 603 41 0 58388 0
vsize: 233716
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50287 0 0 0 103890 126 0 0 25 0 1 0 547104868 239325184 46320 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46320 603 41 0 58388 0
vsize: 233716
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50288 0 0 0 104890 126 0 0 25 0 1 0 547104868 239325184 46321 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50288 0 0 0 105891 126 0 0 25 0 1 0 547104868 239325184 46321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50288 0 0 0 106891 126 0 0 25 0 1 0 547104868 239325184 46321 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46321 603 41 0 58388 0
vsize: 233716
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50289 0 0 0 107891 126 0 0 25 0 1 0 547104868 239325184 46322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46322 603 41 0 58388 0
vsize: 233716
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50291 0 0 0 108891 126 0 0 25 0 1 0 547104868 239325184 46324 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46324 603 41 0 58388 0
vsize: 233716
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50295 0 0 0 109891 126 0 0 25 0 1 0 547104868 239325184 46328 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58429 46328 603 41 0 58388 0
vsize: 233716
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50299 0 0 0 110891 126 0 0 25 0 1 0 547104868 239427584 46332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46332 603 41 0 58413 0
vsize: 233816
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50304 0 0 0 111891 126 0 0 25 0 1 0 547104868 239427584 46337 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46337 603 41 0 58413 0
vsize: 233816
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50305 0 0 0 112891 126 0 0 25 0 1 0 547104868 239427584 46338 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46338 603 41 0 58413 0
vsize: 233816
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50312 0 0 0 113892 126 0 0 25 0 1 0 547104868 239427584 46345 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46345 603 41 0 58413 0
vsize: 233816
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50312 0 0 0 114892 127 0 0 25 0 1 0 547104868 239427584 46345 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58454 46345 603 41 0 58413 0
vsize: 233816
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50312 0 0 0 115891 127 0 0 25 0 1 0 547104868 239427584 46345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46345 603 41 0 58413 0
vsize: 233816
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50315 0 0 0 116892 127 0 0 25 0 1 0 547104868 239427584 46348 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46348 603 41 0 58413 0
vsize: 233816
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50322 0 0 0 117892 127 0 0 25 0 1 0 547104868 239427584 46355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46355 603 41 0 58413 0
vsize: 233816
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50323 0 0 0 118892 127 0 0 25 0 1 0 547104868 239427584 46356 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58454 46356 603 41 0 58413 0
vsize: 233816
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9852
Raw data (stat): 9850 (minisat+) R 9849 3260 3259 0 -1 0 50331 0 0 0 119892 127 0 0 25 0 1 0 547104868 239554560 46364 4294967295 134512640 134672761 3221224544 3221223696 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58485 46364 603 41 0 58444 0
vsize: 233940
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 9852
Raw data (stat): 9850 (minisat+) Z 9849 3260 3259 0 -1 12 50334 0 0 0 119892 136 0 0 25 0 1 0 547104868 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.12
CPU time (s): 1200.29
CPU user time (s): 1198.93
CPU system time (s): 1.36479
CPU usage (%): 100.014
Max. virtual memory (Kb): 233940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####