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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb
MD5SUM	375b355299c9fbf8170e172bcbc73eb2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16728
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	242
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	122
Trace number 14174

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-20 23:08:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19492 boxname=wulflinc19 idbench=1500 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  375b355299c9fbf8170e172bcbc73eb2  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-markshare2_1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-markshare2_1.opb
IDLAUNCH: 19492
/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:        624488 kB
Buffers:         34528 kB
Cached:         341804 kB
SwapCached:        660 kB
Active:          93192 kB
Inactive:       285280 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        624236 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            26036 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:28:44 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19492 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  12]---> Adder-cost: 590   maxlim: 469334   bits: 20/19
c ---[  10]---> Adder-cost: 648   maxlim: 507792   bits: 20/19
c ---[   8]---> Adder-cost: 604   maxlim: 482140   bits: 20/19
c ---[   6]---> Adder-cost: 572   maxlim: 518845   bits: 20/19
c ---[   4]---> Adder-cost: 688   maxlim: 476350   bits: 20/19
c ---[   2]---> Adder-cost: 646   maxlim: 516106   bits: 20/19
c ---[   0]---> Adder-cost: 598   maxlim: 472356   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29589   105189 |    9863       0        0     nan |  0.000 % |
c |       100 |   29589   105189 |   10849     100      294     2.9 |  6.191 % |
c |       250 |   29589   105189 |   11934     250     1546     6.2 |  6.191 % |
c ==============================================================================
c [1mFound solution: 895884[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1831     Base: 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 |       420 |   34259   116094 |   11419     420     3527     8.4 |  6.191 % |
c ==============================================================================
c [1mFound solution: 277009[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 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 |       442 |   34312   116266 |   11437     442     3696     8.4 |  6.191 % |
c |       542 |   34312   116266 |   12580     542    19307    35.6 |  4.622 % |
c |       692 |   34312   116266 |   13838     692    20278    29.3 |  4.622 % |
c |       919 |   34304   116240 |   15222     918    23363    25.4 |  4.638 % |
c |      1256 |   34296   116214 |   16744    1254    26303    21.0 |  4.654 % |
c |      1762 |   34282   116183 |   18419    1758    31387    17.9 |  4.716 % |
c |      2523 |   34274   116157 |   20261    2518    52135    20.7 |  4.732 % |
c |      3663 |   34266   116131 |   22287    3657    86430    23.6 |  4.748 % |
c |      5371 |   34258   116105 |   24516    5364   157198    29.3 |  4.763 % |
c |      7933 |   34250   116079 |   26967    7925   283775    35.8 |  4.779 % |
c |     11777 |   34232   116039 |   29664   11766   467502    39.7 |  4.857 % |
c |     17545 |   34232   116039 |   32631   17534   744678    42.5 |  4.857 % |
c |     26194 |   34232   116039 |   35894   26183  1229982    47.0 |  4.857 % |
c |     39168 |   34232   116039 |   39483   16577   675473    40.7 |  4.857 % |
c |     58629 |   34224   116013 |   43431   36037  1748106    48.5 |  4.873 % |
c |     87821 |   34216   115987 |   47775   35097  1973601    56.2 |  4.889 % |
c |    131610 |   34216   115987 |   52552   44264  2632869    59.5 |  4.889 % |
c |    197294 |   34208   115965 |   57807   34890  2157751    61.8 |  4.920 % |
c |    295820 |   34194   115921 |   63588   47108  2866807    60.9 |  4.951 % |
c |    443610 |   34185   115894 |   69947   48453  3071079    63.4 |  4.983 % |
#### 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): 1.05 0.99 0.91 2/55 16320
Raw data (stat): 16320 (runsolver) R 16319 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540276869 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99994 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 1738 0 0 0 993 5 0 0 25 0 1 0 540276869 8744960 1711 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2135 1711 603 41 0 2094 0
vsize: 8540
[startup+20.0008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 2372 0 0 0 1992 7 0 0 25 0 1 0 540276869 11419648 2345 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2788 2345 603 41 0 2747 0
vsize: 11152
[startup+30.0005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 2904 0 0 0 2990 9 0 0 25 0 1 0 540276869 13565952 2877 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3312 2877 603 41 0 3271 0
vsize: 13248
[startup+40.0013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3162 0 0 0 3989 10 0 0 25 0 1 0 540276869 14770176 3135 4294967295 134512640 134672761 3221224624 3221223728 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3606 3135 603 41 0 3565 0
vsize: 14424
[startup+50.0021 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3162 0 0 0 4989 10 0 0 25 0 1 0 540276869 14770176 3135 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3606 3135 603 41 0 3565 0
vsize: 14424
[startup+60.0019 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3162 0 0 0 5989 10 0 0 25 0 1 0 540276869 14770176 3135 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3606 3135 603 41 0 3565 0
vsize: 14424
[startup+70.0027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16320
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3557 0 0 0 6988 12 0 0 25 0 1 0 540276869 16384000 3530 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4000 3530 603 41 0 3959 0
vsize: 16000
[startup+80.0026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3866 0 0 0 7986 14 0 0 25 0 1 0 540276869 17596416 3839 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4296 3839 603 41 0 4255 0
vsize: 17184
[startup+90.0038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3866 0 0 0 8986 14 0 0 25 0 1 0 540276869 17596416 3839 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4296 3839 603 41 0 4255 0
vsize: 17184
[startup+100.004 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 3868 0 0 0 9986 14 0 0 25 0 1 0 540276869 17596416 3841 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4296 3841 603 41 0 4255 0
vsize: 17184
[startup+110.004 s]
Raw data (loadavg): 1.15 1.02 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4007 0 0 0 10985 15 0 0 25 0 1 0 540276869 18137088 3980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4428 3980 603 41 0 4387 0
vsize: 17712
[startup+120.005 s]
Raw data (loadavg): 1.12 1.02 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4401 0 0 0 11984 16 0 0 25 0 1 0 540276869 19742720 4374 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4820 4374 603 41 0 4779 0
vsize: 19280
[startup+130.005 s]
Raw data (loadavg): 1.10 1.02 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4459 0 0 0 12983 17 0 0 25 0 1 0 540276869 20013056 4432 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4432 603 41 0 4845 0
vsize: 19544
[startup+140.005 s]
Raw data (loadavg): 1.09 1.02 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4459 0 0 0 13983 17 0 0 25 0 1 0 540276869 20013056 4432 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4432 603 41 0 4845 0
vsize: 19544
[startup+150.007 s]
Raw data (loadavg): 1.07 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4459 0 0 0 14984 17 0 0 25 0 1 0 540276869 20013056 4432 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4432 603 41 0 4845 0
vsize: 19544
[startup+160.006 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4459 0 0 0 15983 18 0 0 25 0 1 0 540276869 20013056 4432 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4432 603 41 0 4845 0
vsize: 19544
[startup+170.006 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4459 0 0 0 16983 18 0 0 25 0 1 0 540276869 20013056 4432 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4886 4432 603 41 0 4845 0
vsize: 19544
[startup+180.006 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 4837 0 0 0 17982 19 0 0 25 0 1 0 540276869 21483520 4810 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5245 4810 603 41 0 5204 0
vsize: 20980
[startup+190.006 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5066 0 0 0 18982 20 0 0 25 0 1 0 540276869 22417408 5039 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5473 5039 603 41 0 5432 0
vsize: 21892
[startup+200.006 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5066 0 0 0 19982 20 0 0 25 0 1 0 540276869 22417408 5039 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5473 5039 603 41 0 5432 0
vsize: 21892
[startup+210.006 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5066 0 0 0 20981 20 0 0 25 0 1 0 540276869 22417408 5039 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5473 5039 603 41 0 5432 0
vsize: 21892
[startup+220.007 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5066 0 0 0 21981 20 0 0 25 0 1 0 540276869 22417408 5039 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5473 5039 603 41 0 5432 0
vsize: 21892
[startup+230.007 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5092 0 0 0 22980 21 0 0 25 0 1 0 540276869 22560768 5065 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5508 5065 603 41 0 5467 0
vsize: 22032
[startup+240.014 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5102 0 0 0 23981 21 0 0 25 0 1 0 540276869 22560768 5075 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5508 5075 603 41 0 5467 0
vsize: 22032
[startup+250.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5145 0 0 0 24980 22 0 0 25 0 1 0 540276869 22827008 5118 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5573 5118 603 41 0 5532 0
vsize: 22292
[startup+260.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5145 0 0 0 25980 22 0 0 25 0 1 0 540276869 22827008 5118 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5573 5118 603 41 0 5532 0
vsize: 22292
[startup+270.016 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5145 0 0 0 26980 22 0 0 25 0 1 0 540276869 22827008 5118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5573 5118 603 41 0 5532 0
vsize: 22292
[startup+280.017 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5148 0 0 0 27979 22 0 0 25 0 1 0 540276869 22827008 5121 4294967295 134512640 134672761 3221224624 3221223872 134562614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5573 5121 603 41 0 5532 0
vsize: 22292
[startup+290.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5246 0 0 0 28978 23 0 0 25 0 1 0 540276869 23232512 5219 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5672 5219 603 41 0 5631 0
vsize: 22688
[startup+300.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5676 0 0 0 29977 24 0 0 25 0 1 0 540276869 24985600 5649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6100 5649 603 41 0 6059 0
vsize: 24400
[startup+310.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 30977 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+320.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 31978 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+330.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 32979 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+340.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 33979 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+350.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 34979 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223760 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+360.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 5710 0 0 0 35979 24 0 0 25 0 1 0 540276869 25120768 5683 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6133 5683 603 41 0 6092 0
vsize: 24532
[startup+370.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16322
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6015 0 0 0 36979 25 0 0 25 0 1 0 540276869 26324992 5988 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6427 5988 603 41 0 6386 0
vsize: 25708
[startup+380.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 37979 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+390.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 38979 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+400.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 39979 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+410.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 40979 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223728 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+420.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 41977 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+430.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6241 0 0 0 42977 26 0 0 25 0 1 0 540276869 27267072 6214 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6214 603 41 0 6616 0
vsize: 26628
[startup+440.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6246 0 0 0 43977 26 0 0 25 0 1 0 540276869 27267072 6219 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6219 603 41 0 6616 0
vsize: 26628
[startup+450.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 44977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 45977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+470.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 46977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+480.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 47977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+490.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 48977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+500.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 49977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+510.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 50977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223808 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+520.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 51977 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+530.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 52978 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+540.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 53978 27 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+550.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6350 0 0 0 54978 28 0 0 25 0 1 0 540276869 27664384 6323 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6754 6323 603 41 0 6713 0
vsize: 27016
[startup+560.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6365 0 0 0 55978 28 0 0 25 0 1 0 540276869 27799552 6338 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6787 6338 603 41 0 6746 0
vsize: 27148
[startup+570.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6574 0 0 0 56977 28 0 0 25 0 1 0 540276869 28733440 6547 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7015 6547 603 41 0 6974 0
vsize: 28060
[startup+580.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6576 0 0 0 57977 28 0 0 25 0 1 0 540276869 28733440 6549 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7015 6549 603 41 0 6974 0
vsize: 28060
[startup+590.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6584 0 0 0 58978 28 0 0 25 0 1 0 540276869 28733440 6557 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7015 6557 603 41 0 6974 0
vsize: 28060
[startup+600.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6597 0 0 0 59978 29 0 0 25 0 1 0 540276869 28876800 6570 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6570 603 41 0 7009 0
vsize: 28200
[startup+610.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6599 0 0 0 60979 29 0 0 25 0 1 0 540276869 28876800 6572 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6572 603 41 0 7009 0
vsize: 28200
[startup+620.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6616 0 0 0 61979 29 0 0 25 0 1 0 540276869 28876800 6589 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6589 603 41 0 7009 0
vsize: 28200
[startup+630.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6616 0 0 0 62979 29 0 0 25 0 1 0 540276869 28876800 6589 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6589 603 41 0 7009 0
vsize: 28200
[startup+640.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6622 0 0 0 63979 29 0 0 25 0 1 0 540276869 28876800 6595 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6595 603 41 0 7009 0
vsize: 28200
[startup+650.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6629 0 0 0 64979 29 0 0 25 0 1 0 540276869 29040640 6602 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7090 6602 603 41 0 7049 0
vsize: 28360
[startup+660.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6630 0 0 0 65979 29 0 0 25 0 1 0 540276869 29040640 6603 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7090 6603 603 41 0 7049 0
vsize: 28360
[startup+670.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16324
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6630 0 0 0 66979 29 0 0 25 0 1 0 540276869 29040640 6603 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7090 6603 603 41 0 7049 0
vsize: 28360
[startup+680.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6665 0 0 0 67979 29 0 0 25 0 1 0 540276869 29237248 6638 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6638 603 41 0 7097 0
vsize: 28552
[startup+690.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6712 0 0 0 68979 29 0 0 25 0 1 0 540276869 29499392 6685 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7202 6685 603 41 0 7161 0
vsize: 28808
[startup+700.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6919 0 0 0 69979 30 0 0 25 0 1 0 540276869 30302208 6892 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7398 6892 603 41 0 7357 0
vsize: 29592
[startup+710.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6974 0 0 0 70979 31 0 0 25 0 1 0 540276869 30437376 6947 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7431 6947 603 41 0 7390 0
vsize: 29724
[startup+720.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6974 0 0 0 71979 31 0 0 25 0 1 0 540276869 30437376 6947 4294967295 134512640 134672761 3221224624 3221223808 134559379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7431 6947 603 41 0 7390 0
vsize: 29724
[startup+730.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6974 0 0 0 72979 31 0 0 25 0 1 0 540276869 30437376 6947 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7431 6947 603 41 0 7390 0
vsize: 29724
[startup+740.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6974 0 0 0 73979 31 0 0 25 0 1 0 540276869 30437376 6947 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7431 6947 603 41 0 7390 0
vsize: 29724
[startup+750.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6981 0 0 0 74979 31 0 0 25 0 1 0 540276869 30601216 6954 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6954 603 41 0 7430 0
vsize: 29884
[startup+760.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6982 0 0 0 75979 31 0 0 25 0 1 0 540276869 30601216 6955 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6955 603 41 0 7430 0
vsize: 29884
[startup+770.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6988 0 0 0 76979 31 0 0 25 0 1 0 540276869 30601216 6961 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6961 603 41 0 7430 0
vsize: 29884
[startup+780.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 6995 0 0 0 77979 31 0 0 25 0 1 0 540276869 30601216 6968 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7471 6968 603 41 0 7430 0
vsize: 29884
[startup+790.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7005 0 0 0 78978 31 0 0 25 0 1 0 540276869 30601216 6978 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7471 6978 603 41 0 7430 0
vsize: 29884
[startup+800.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7016 0 0 0 79978 32 0 0 25 0 1 0 540276869 30797824 6989 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7519 6989 603 41 0 7478 0
vsize: 30076
[startup+810.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7016 0 0 0 80978 32 0 0 25 0 1 0 540276869 30797824 6989 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7519 6989 603 41 0 7478 0
vsize: 30076
[startup+820.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7093 0 0 0 81978 32 0 0 25 0 1 0 540276869 31330304 7066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7649 7066 603 41 0 7608 0
vsize: 30596
[startup+830.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7347 0 0 0 82977 33 0 0 25 0 1 0 540276869 32395264 7320 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7909 7320 603 41 0 7868 0
vsize: 31636
[startup+840.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7508 0 0 0 83976 34 0 0 25 0 1 0 540276869 33079296 7481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7481 603 41 0 8035 0
vsize: 32304
[startup+850.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7509 0 0 0 84977 34 0 0 25 0 1 0 540276869 33079296 7482 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7482 603 41 0 8035 0
vsize: 32304
[startup+860.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7510 0 0 0 85977 34 0 0 25 0 1 0 540276869 33079296 7483 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7483 603 41 0 8035 0
vsize: 32304
[startup+870.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7512 0 0 0 86977 34 0 0 25 0 1 0 540276869 33079296 7485 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7485 603 41 0 8035 0
vsize: 32304
[startup+880.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7524 0 0 0 87977 34 0 0 25 0 1 0 540276869 33079296 7497 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7497 603 41 0 8035 0
vsize: 32304
[startup+890.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7525 0 0 0 88977 34 0 0 25 0 1 0 540276869 33079296 7498 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7498 603 41 0 8035 0
vsize: 32304
[startup+900.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7525 0 0 0 89977 34 0 0 25 0 1 0 540276869 33079296 7498 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7498 603 41 0 8035 0
vsize: 32304
[startup+910.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7525 0 0 0 90977 34 0 0 25 0 1 0 540276869 33079296 7498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8076 7498 603 41 0 8035 0
vsize: 32304
[startup+920.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7539 0 0 0 91978 34 0 0 25 0 1 0 540276869 33218560 7512 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8110 7512 603 41 0 8069 0
vsize: 32440
[startup+930.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7542 0 0 0 92978 34 0 0 25 0 1 0 540276869 33218560 7515 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8110 7515 603 41 0 8069 0
vsize: 32440
[startup+940.054 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7556 0 0 0 93978 34 0 0 25 0 1 0 540276869 33218560 7529 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8110 7529 603 41 0 8069 0
vsize: 32440
[startup+950.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7673 0 0 0 94988 34 0 0 25 0 1 0 540276869 33751040 7646 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8240 7646 603 41 0 8199 0
vsize: 32960
[startup+960.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 7939 0 0 0 95987 35 0 0 25 0 1 0 540276869 34811904 7912 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7912 603 41 0 8458 0
vsize: 33996
[startup+970.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16326
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 96987 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+980.157 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 97987 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+990.158 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 98987 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1000.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 99987 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 100987 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1020.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 101988 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1030.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 102988 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1040.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 103988 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1050.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 104988 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8100 0 0 0 105988 36 0 0 25 0 1 0 540276869 35471360 8073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8073 603 41 0 8619 0
vsize: 34640
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8109 0 0 0 106988 36 0 0 25 0 1 0 540276869 35627008 8082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8082 603 41 0 8657 0
vsize: 34792
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8109 0 0 0 107988 36 0 0 25 0 1 0 540276869 35627008 8082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8082 603 41 0 8657 0
vsize: 34792
[startup+1090.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8109 0 0 0 108988 37 0 0 25 0 1 0 540276869 35627008 8082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8082 603 41 0 8657 0
vsize: 34792
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8118 0 0 0 109988 37 0 0 25 0 1 0 540276869 35627008 8091 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8091 603 41 0 8657 0
vsize: 34792
[startup+1110.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8127 0 0 0 110989 37 0 0 25 0 1 0 540276869 35627008 8100 4294967295 134512640 134672761 3221224624 3221223720 1075347133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8100 603 41 0 8657 0
vsize: 34792
[startup+1120.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8127 0 0 0 111989 37 0 0 25 0 1 0 540276869 35627008 8100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8100 603 41 0 8657 0
vsize: 34792
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8127 0 0 0 112989 37 0 0 25 0 1 0 540276869 35627008 8100 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8100 603 41 0 8657 0
vsize: 34792
[startup+1140.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8127 0 0 0 113989 37 0 0 25 0 1 0 540276869 35627008 8100 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8100 603 41 0 8657 0
vsize: 34792
[startup+1150.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8132 0 0 0 114989 37 0 0 25 0 1 0 540276869 35627008 8105 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8105 603 41 0 8657 0
vsize: 34792
[startup+1160.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8132 0 0 0 115989 37 0 0 25 0 1 0 540276869 35627008 8105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8105 603 41 0 8657 0
vsize: 34792
[startup+1170.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8132 0 0 0 116989 37 0 0 25 0 1 0 540276869 35627008 8105 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8105 603 41 0 8657 0
vsize: 34792
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8132 0 0 0 117990 37 0 0 25 0 1 0 540276869 35627008 8105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8698 8105 603 41 0 8657 0
vsize: 34792
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8141 0 0 0 118990 37 0 0 25 0 1 0 540276869 35790848 8114 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8738 8114 603 41 0 8697 0
vsize: 34952
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 16328
Raw data (stat): 16320 (minisat+) R 16319 22929 22928 0 -1 0 8142 0 0 0 119990 37 0 0 25 0 1 0 540276869 35790848 8115 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8738 8115 603 41 0 8697 0
vsize: 34952
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 16328
Raw data (stat): 16320 (minisat+) Z 16319 22929 22928 0 -1 12 8145 0 0 0 119990 39 0 0 25 0 1 0 540276869 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.18
CPU time (s): 1200.3
CPU user time (s): 1199.9
CPU system time (s): 0.39094
CPU usage (%): 100.01
Max. virtual memory (Kb): 34952
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####