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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 6039

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 03:13:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4502 boxname=wulflinc10 idbench=366 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc10/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-10:10:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc10/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 4502
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        863164 kB
Buffers:         35384 kB
Cached:         116500 kB
SwapCached:        164 kB
Active:          54592 kB
Inactive:       100340 kB
HighTotal:      131008 kB
HighFree:        10892 kB
LowTotal:       903652 kB
LowFree:        852272 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10916 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:33:48 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4502 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4084    11649 |    1361       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 355[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:20800     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39610    94771 |   13203       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        52 |   40635    97290 |   13545      47      509    10.8 |  0.000 % |
c |       153 |   40635    97290 |   14899     148     2006    13.6 |  0.807 % |
c |       303 |   40635    97290 |   16389     298     3680    12.3 |  0.807 % |
c ==============================================================================
c [1mFound solution: 93[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       335 |   40816    97778 |   13605     330     3969    12.0 |  0.807 % |
c ==============================================================================
c [1mFound solution: 74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       381 |   40957    98168 |   13652     376     4254    11.3 |  0.807 % |
c |       482 |   40957    98168 |   15017     477     6680    14.0 |  0.809 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |   41021    98358 |   13673     538     7309    13.6 |  0.809 % |
c |       643 |   41007    98330 |   15040     637     8156    12.8 |  0.847 % |
c ==============================================================================
c [1mFound solution: 39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       741 |   41137    98688 |   13712     735    12723    17.3 |  0.847 % |
c |       841 |   41137    98688 |   15083     835    14812    17.7 |  0.858 % |
c |       991 |   41137    98688 |   16591     985    15900    16.1 |  0.858 % |
c |      1216 |   41137    98688 |   18250    1210    24830    20.5 |  0.858 % |
c ==============================================================================
c [1mFound solution: 32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1549 |   40826    98032 |   13608    1526    31796    20.8 |  0.858 % |
c |      1649 |   40807    97993 |   14968    1625    32748    20.2 |  1.610 % |
c |      1799 |   40807    97993 |   16465    1775    35020    19.7 |  1.610 % |
c |      2024 |   40807    97993 |   18112    2000    57066    28.5 |  1.610 % |
c |      2361 |   40157    96519 |   19923    2253    61245    27.2 |  2.962 % |
c |      2870 |   40157    96519 |   21915    2762    71091    25.7 |  2.962 % |
c |      3629 |   40157    96519 |   24107    3521    86728    24.6 |  2.962 % |
c |      4768 |   40069    96331 |   26518    4641   109000    23.5 |  3.209 % |
c |      6476 |   39881    95923 |   29169    6320   241528    38.2 |  3.710 % |
c |      9040 |   39881    95923 |   32086    8884   558335    62.8 |  3.710 % |
c |     12886 |   39881    95923 |   35295   12730   837536    65.8 |  3.710 % |
c |     18654 |   39881    95923 |   38825   18498  1338946    72.4 |  3.710 % |
c |     27303 |   39881    95923 |   42707   27147  2479319    91.3 |  3.710 % |
c ==============================================================================
c [1mFound solution: 31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30230 |   39885    95933 |   13295   30074  2833854    94.2 |  3.710 % |
c |     30330 |   39885    95933 |   14624   13138  1476713   112.4 |  3.714 % |
c |     30481 |   39885    95933 |   16086   13289  1480028   111.4 |  3.714 % |
c |     30709 |   39885    95933 |   17695   13517  1485023   109.9 |  3.714 % |
c |     31046 |   39885    95933 |   19465   13854  1491450   107.7 |  3.714 % |
c |     31552 |   39885    95933 |   21411   14360  1526895   106.3 |  3.714 % |
c |     32311 |   39885    95933 |   23552   15119  1570893   103.9 |  3.714 % |
c |     33452 |   39885    95933 |   25908   16260  1620404    99.7 |  3.714 % |
c |     35160 |   39871    95901 |   28499   17966  1667556    92.8 |  3.734 % |
c |     37722 |   39871    95901 |   31348   20528  1922784    93.7 |  3.734 % |
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37876 |   39892    95963 |   13297   20682  1934151    93.5 |  3.734 % |
c |     37977 |   39838    95840 |   14626   10433   624856    59.9 |  3.810 % |
c |     38128 |   39838    95840 |   16089   10584   628193    59.4 |  3.810 % |
c |     38354 |   39838    95840 |   17698   10810   630346    58.3 |  3.810 % |
c |     38692 |   39838    95840 |   19468   11148   638017    57.2 |  3.810 % |
c |     39198 |   39838    95840 |   21414   11654   656390    56.3 |  3.810 % |
c |     39957 |   39820    95799 |   23556   12406   664944    53.6 |  3.835 % |
c ==============================================================================
c [1mFound solution: 25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40470 |   39846    95875 |   13282   12919   696562    53.9 |  3.835 % |
c |     40570 |   39846    95875 |   14610   13019   698367    53.6 |  3.837 % |
c |     40720 |   39846    95875 |   16071   13169   700531    53.2 |  3.837 % |
c |     40945 |   39846    95875 |   17678   13394   705284    52.7 |  3.837 % |
c |     41282 |   39739    95631 |   19446   13723   724893    52.8 |  4.074 % |
c |     41789 |   39739    95631 |   21390   14230   774776    54.4 |  4.074 % |
c |     42549 |   39721    95589 |   23529   14989   793085    52.9 |  4.129 % |
c |     43688 |   39721    95589 |   25882   16128   862249    53.5 |  4.129 % |
c |     45397 |   39721    95589 |   28471   17837   943295    52.9 |  4.129 % |
c |     47959 |   39721    95589 |   31318   20399  1340906    65.7 |  4.129 % |
c |     51803 |   39721    95589 |   34450   24243  1730566    71.4 |  4.129 % |
c ==============================================================================
c [1mFound solution: 18[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53697 |   39759    95694 |   13253   26132  1833701    70.2 |  4.129 % |
c |     53798 |   39759    95694 |   14578   13167   983300    74.7 |  4.137 % |
c |     53948 |   39721    95606 |   16036   13310   984452    74.0 |  4.197 % |
c |     54173 |   39721    95606 |   17639   13535   995185    73.5 |  4.197 % |
c |     54510 |   39721    95606 |   19403   13872  1004647    72.4 |  4.197 % |
c ==============================================================================
c [1mFound solution: 9[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54616 |   39766    95725 |   13255   13978  1006538    72.0 |  4.197 % |
c |     54716 |   39748    95684 |   14580   14071  1007232    71.6 |  4.220 % |
c |     54866 |   39748    95684 |   16038   14221  1012093    71.2 |  4.220 % |
c |     55091 |   39742    95670 |   17642   14443  1014604    70.2 |  4.230 % |
c |     55428 |   39738    95661 |   19406   14779  1023087    69.2 |  4.235 % |
c |     55934 |   39738    95661 |   21347   15285  1037095    67.9 |  4.235 % |
c |     56693 |   39738    95661 |   23482   16044  1092277    68.1 |  4.235 % |
c |     57832 |   39738    95661 |   25830   17183  1134775    66.0 |  4.235 % |
c |     59541 |   39738    95661 |   28413   18892  1247008    66.0 |  4.235 % |
c |     62103 |   39738    95661 |   31254   21454  1403165    65.4 |  4.235 % |
c |     65947 |   39738    95661 |   34380   25298  2020808    79.9 |  4.235 % |
c |     71714 |   39738    95661 |   37818   31065  2590932    83.4 |  4.235 % |
c |     80363 |   39738    95661 |   41599   39714  3547339    89.3 |  4.235 % |
c |     93337 |   39738    95661 |   45759   19456  2317262   119.1 |  4.235 % |
c |    112798 |   39738    95661 |   50335   38917  5379251   138.2 |  4.235 % |
c |    141992 |   39716    95612 |   55369   26150  3557617   136.0 |  4.270 % |
c |    185781 |   39640    95444 |   60906   27874  1990715    71.4 |  4.457 % |
c |    251466 |   39640    95444 |   66997   44447  9458461   212.8 |  4.457 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 31907
Raw data (stat): 31907 (runsolver) R 31906 25347 25346 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 423050006 1052672 97 4294967295 134512640 135381576 3221224432 3221219872 134514522 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 2211 0 0 0 994 4 0 0 25 0 1 0 423050006 11268096 2135 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2135 603 41 0 2710 0
vsize: 11004
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 2688 0 0 0 1992 7 0 0 25 0 1 0 423050006 13283328 2612 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3243 2612 603 41 0 3202 0
vsize: 12972
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 3107 0 0 0 2990 8 0 0 25 0 1 0 423050006 15020032 3031 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3667 3031 603 41 0 3626 0
vsize: 14668
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 3519 0 0 0 3989 9 0 0 25 0 1 0 423050006 16646144 3443 4294967295 134512640 134672761 3221224544 3221223728 134559367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4064 3443 603 41 0 4023 0
vsize: 16256
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 3909 0 0 0 4988 10 0 0 25 0 1 0 423050006 18255872 3833 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4457 3833 603 41 0 4416 0
vsize: 17828
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 4301 0 0 0 5986 12 0 0 25 0 1 0 423050006 19861504 4225 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4849 4225 603 41 0 4808 0
vsize: 19396
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 4683 0 0 0 6985 13 0 0 25 0 1 0 423050006 21471232 4607 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5242 4607 603 41 0 5201 0
vsize: 20968
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 7983 15 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+90.004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 8983 15 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 9983 15 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+110.006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 10982 16 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 11982 16 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+130.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 12982 16 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 13981 16 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+150.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 14981 16 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5061 0 0 0 15981 17 0 0 25 0 1 0 423050006 22929408 4985 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5598 4985 603 41 0 5557 0
vsize: 22392
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5062 0 0 0 16981 17 0 0 25 0 1 0 423050006 22929408 4986 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5598 4986 603 41 0 5557 0
vsize: 22392
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5358 0 0 0 17981 18 0 0 25 0 1 0 423050006 24264704 5282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5924 5282 603 41 0 5883 0
vsize: 23696
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 5768 0 0 0 18980 18 0 0 25 0 1 0 423050006 26005504 5692 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6349 5692 603 41 0 6308 0
vsize: 25396
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 6113 0 0 0 19979 20 0 0 25 0 1 0 423050006 27344896 6037 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6676 6037 603 41 0 6635 0
vsize: 26704
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 6516 0 0 0 20978 21 0 0 25 0 1 0 423050006 29069312 6440 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7097 6440 603 41 0 7056 0
vsize: 28388
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 6951 0 0 0 21977 22 0 0 25 0 1 0 423050006 30826496 6875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7526 6875 603 41 0 7485 0
vsize: 30104
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 22976 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 23976 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 24976 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 25977 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 26977 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 27977 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 28977 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7388 0 0 0 29977 23 0 0 25 0 1 0 423050006 32575488 7312 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7953 7312 603 41 0 7912 0
vsize: 31812
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 7694 0 0 0 30977 24 0 0 25 0 1 0 423050006 33783808 7618 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8248 7618 603 41 0 8207 0
vsize: 32992
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 8105 0 0 0 31976 25 0 0 25 0 1 0 423050006 35524608 8029 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8673 8029 603 41 0 8632 0
vsize: 34692
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 8452 0 0 0 32975 26 0 0 25 0 1 0 423050006 36868096 8376 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9001 8376 603 41 0 8960 0
vsize: 36004
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 8838 0 0 0 33974 27 0 0 25 0 1 0 423050006 38481920 8762 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9395 8762 603 41 0 9354 0
vsize: 37580
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 9244 0 0 0 34974 28 0 0 25 0 1 0 423050006 40202240 9168 4294967295 134512640 134672761 3221224544 3221223648 134559814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9815 9168 603 41 0 9774 0
vsize: 39260
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 9629 0 0 0 35973 29 0 0 25 0 1 0 423050006 41799680 9553 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10205 9553 603 41 0 10164 0
vsize: 40820
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 10059 0 0 0 36972 31 0 0 25 0 1 0 423050006 43532288 9983 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10628 9983 603 41 0 10587 0
vsize: 42512
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 10515 0 0 0 37971 32 0 0 25 0 1 0 423050006 45400064 10439 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11084 10439 603 41 0 11043 0
vsize: 44336
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 10965 0 0 0 38970 33 0 0 25 0 1 0 423050006 47140864 10889 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11509 10889 603 41 0 11468 0
vsize: 46036
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 39969 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 40970 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 41970 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 42970 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 43970 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 44970 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223728 134558382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 45971 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 46971 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 47971 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 48971 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 49972 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 50972 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 51972 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 52972 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 53972 33 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 54972 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 55972 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 56972 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 57972 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 58973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 59973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 60973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 61973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 62973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 63973 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+650.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 64974 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 65974 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 66974 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11144 0 0 0 67974 34 0 0 25 0 1 0 423050006 47951872 11068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11068 603 41 0 11666 0
vsize: 46828
[startup+690.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11267 0 0 0 68974 34 0 0 25 0 1 0 423050006 48476160 11191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11835 11191 603 41 0 11794 0
vsize: 47340
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 11632 0 0 0 69973 35 0 0 25 0 1 0 423050006 49958912 11556 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12197 11556 603 41 0 12156 0
vsize: 48788
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 12009 0 0 0 70972 36 0 0 25 0 1 0 423050006 51417088 11933 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12553 11933 603 41 0 12512 0
vsize: 50212
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 12359 0 0 0 71971 37 0 0 25 0 1 0 423050006 52891648 12283 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12913 12283 603 41 0 12872 0
vsize: 51652
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 12678 0 0 0 72970 39 0 0 25 0 1 0 423050006 54226944 12602 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13239 12602 603 41 0 13198 0
vsize: 52956
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13012 0 0 0 73969 40 0 0 25 0 1 0 423050006 55558144 12936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13564 12936 603 41 0 13523 0
vsize: 54256
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13312 0 0 0 74969 41 0 0 25 0 1 0 423050006 57020416 13236 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13921 13236 603 41 0 13880 0
vsize: 55684
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13605 0 0 0 75968 42 0 0 25 0 1 0 423050006 58339328 13529 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14243 13529 603 41 0 14202 0
vsize: 56972
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13769 0 0 0 76967 43 0 0 25 0 1 0 423050006 58998784 13693 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13693 603 41 0 14363 0
vsize: 57616
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13769 0 0 0 77967 43 0 0 25 0 1 0 423050006 58998784 13693 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13693 603 41 0 14363 0
vsize: 57616
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 78967 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 79967 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 80968 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 81968 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 82968 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 83968 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 84968 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 85969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 86969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 87969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 88969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 89969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 90969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 91970 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 92969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 93969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 94969 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 13770 0 0 0 95970 43 0 0 25 0 1 0 423050006 58998784 13694 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13694 603 41 0 14363 0
vsize: 57616
[startup+970.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 14015 0 0 0 96969 44 0 0 25 0 1 0 423050006 59936768 13939 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14633 13939 603 41 0 14592 0
vsize: 58532
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 14357 0 0 0 97968 45 0 0 25 0 1 0 423050006 61403136 14281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14991 14281 603 41 0 14950 0
vsize: 59964
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 14747 0 0 0 98967 46 0 0 25 0 1 0 423050006 63012864 14671 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15384 14671 603 41 0 15343 0
vsize: 61536
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15202 0 0 0 99966 47 0 0 25 0 1 0 423050006 64753664 15126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15809 15126 603 41 0 15768 0
vsize: 63236
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15580 0 0 0 100965 49 0 0 25 0 1 0 423050006 66363392 15504 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16202 15504 603 41 0 16161 0
vsize: 64808
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 101964 49 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 102965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 103965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 104965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 105965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 106965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 107965 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 108966 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 109966 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 110966 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 111966 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15755 0 0 0 112967 50 0 0 25 0 1 0 423050006 67039232 15679 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15679 603 41 0 16326 0
vsize: 65468
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 113967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 114967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 115967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 116967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 117967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 118967 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31907
Raw data (stat): 31907 (minisat+) R 31906 25347 25346 0 -1 0 15756 0 0 0 119968 50 0 0 25 0 1 0 423050006 67039232 15680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15680 603 41 0 16326 0
vsize: 65468
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31907
Raw data (stat): 31907 (minisat+) Z 31906 25347 25346 0 -1 12 15759 0 0 0 119968 53 0 0 25 0 1 0 423050006 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.04
CPU time (s): 1200.21
CPU user time (s): 1199.68
CPU system time (s): 0.531919
CPU usage (%): 100.014
Max. virtual memory (Kb): 65468
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####