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 14691

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 00:48:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19497 boxname=wulflinc10 idbench=1500 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  375b355299c9fbf8170e172bcbc73eb2  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-markshare2_1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-markshare2_1.opb
IDLAUNCH: 19497
/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:        694208 kB
Buffers:         27656 kB
Cached:         290652 kB
SwapCached:          0 kB
Active:          50916 kB
Inactive:       269936 kB
HighTotal:      131008 kB
HighFree:        61180 kB
LowTotal:       903652 kB
LowFree:        633028 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13984 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:08:45 (client local time) WITH STATUS 10 IN 1200.53 SECONDS
stats: 19497 7 1200.53 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]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  18]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  17]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  16]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  14]---> Adder-cost: 14   maxlim: 126   bits: 8/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 |   30099   107163 |   10033       0        0     nan |  0.000 % |
c |       100 |   30099   107163 |   11036     100      297     3.0 |  6.788 % |
c |       250 |   30091   107137 |   12139     249     1082     4.3 |  6.808 % |
c |       475 |   30091   107137 |   13353     474     2996     6.3 |  6.808 % |
c ==============================================================================
c [1mFound solution: 440239[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 216   maxlim: 1394762   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       648 |   31537   112344 |   10512     647     4567     7.1 |  6.808 % |
c |       748 |   31529   112318 |   11563     746     5777     7.7 |  6.705 % |
c |       898 |   31521   112292 |   12719     895     6720     7.5 |  6.725 % |
c |      1123 |   31506   112243 |   13991    1118    15244    13.6 |  6.764 % |
c |      1460 |   31506   112243 |   15390    1455    31241    21.5 |  6.764 % |
c |      1966 |   31498   112217 |   16929    1960    45448    23.2 |  6.784 % |
c ==============================================================================
c [1mFound solution: 356273[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1478728   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2059 |   31518   112342 |   10506    2053    46402    22.6 |  6.784 % |
c |      2161 |   31518   112342 |   11556    2155    52252    24.2 |  6.891 % |
c |      2311 |   31510   112316 |   12712    2304    53894    23.4 |  6.911 % |
c |      2536 |   31510   112316 |   13983    2529    58862    23.3 |  6.911 % |
c |      2873 |   31502   112290 |   15381    2865    65703    22.9 |  6.931 % |
c |      3379 |   31497   112274 |   16920    3369    76934    22.8 |  6.950 % |
c |      4138 |   31497   112274 |   18612    4128   102452    24.8 |  6.950 % |
c ==============================================================================
c [1mFound solution: 258866[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1576135   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4299 |   31459   112077 |   10486    4283   104168    24.3 |  6.950 % |
c |      4399 |   31450   112048 |   11534    4380   107201    24.5 |  7.273 % |
c |      4550 |   31450   112048 |   12688    4531   108203    23.9 |  7.273 % |
c |      4775 |   31450   112048 |   13956    4756   110092    23.1 |  7.273 % |
c |      5113 |   31450   112048 |   15352    5094   172346    33.8 |  7.273 % |
c |      5619 |   31442   112022 |   16887    5599   183034    32.7 |  7.293 % |
c |      6378 |   31434   111996 |   18576    6357   199888    31.4 |  7.313 % |
c |      7517 |   31434   111996 |   20434    7496   258434    34.5 |  7.313 % |
c |      9227 |   31426   111970 |   22477    9205   356224    38.7 |  7.332 % |
c |     11790 |   31426   111970 |   24725   11768   527866    44.9 |  7.332 % |
c |     15635 |   31404   111900 |   27197   15610   768131    49.2 |  7.391 % |
c |     21401 |   31404   111900 |   29917   21376  1117998    52.3 |  7.391 % |
c |     30050 |   31404   111900 |   32909   30025  1734106    57.8 |  7.391 % |
c ==============================================================================
c [1mFound solution: 201389[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1633612   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30844 |   31426   112048 |   10475   30819  1799076    58.4 |  7.391 % |
c |     30945 |   31426   112048 |   11522    7245   393124    54.3 |  7.570 % |
c |     31095 |   31426   112048 |   12674    7395   396379    53.6 |  7.570 % |
c |     31321 |   31426   112048 |   13942    7621   399195    52.4 |  7.570 % |
c |     31659 |   31426   112048 |   15336    7959   402644    50.6 |  7.570 % |
c |     32165 |   31426   112048 |   16870    8465   415315    49.1 |  7.570 % |
c |     32924 |   31426   112048 |   18557    9224   446102    48.4 |  7.570 % |
c |     34064 |   31426   112048 |   20412   10364   496195    47.9 |  7.570 % |
c |     35772 |   31426   112048 |   22454   12072   578340    47.9 |  7.570 % |
c |     38334 |   31426   112048 |   24699   14634   679495    46.4 |  7.570 % |
c |     42178 |   31426   112048 |   27169   18478   836570    45.3 |  7.570 % |
c |     47945 |   31426   112048 |   29886   24245  1197829    49.4 |  7.570 % |
c |     56596 |   31402   111970 |   32875   15176   787321    51.9 |  7.629 % |
c ==============================================================================
c [1mFound solution: 145600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1689401   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57759 |   31425   112125 |   10475   16339   827376    50.6 |  7.629 % |
c |     57860 |   31425   112125 |   11522    8271   418922    50.6 |  7.808 % |
c |     58010 |   31425   112125 |   12674    8421   419964    49.9 |  7.808 % |
c |     58237 |   31425   112125 |   13942    8648   423715    49.0 |  7.808 % |
c |     58574 |   31417   112099 |   15336    8984   428929    47.7 |  7.828 % |
c |     59080 |   31417   112099 |   16870    9490   435981    45.9 |  7.828 % |
c |     59839 |   31417   112099 |   18557   10249   470304    45.9 |  7.828 % |
c |     60978 |   31417   112099 |   20412   11388   522592    45.9 |  7.828 % |
c |     62686 |   31417   112099 |   22454   13096   598887    45.7 |  7.828 % |
c |     65249 |   31417   112099 |   24699   15659   677422    43.3 |  7.828 % |
c |     69097 |   31417   112099 |   27169   19507   983109    50.4 |  7.828 % |
c |     74863 |   31417   112099 |   29886   25273  1446561    57.2 |  7.828 % |
c |     83512 |   31417   112099 |   32875   16447   950052    57.8 |  7.828 % |
c |     96488 |   31417   112099 |   36162   29423  1733033    58.9 |  7.828 % |
c |    115949 |   31417   112099 |   39778   25972  1766969    68.0 |  7.828 % |
c |    145141 |   31409   112073 |   43756   26850  1552284    57.8 |  7.847 % |
c |    188930 |   31409   112073 |   48132   39076  4227641   108.2 |  7.847 % |
c |    254614 |   31409   112073 |   52945   33251  2081466    62.6 |  7.847 % |
c ==============================================================================
c [1mFound solution: 135406[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 1699595   bits: 21/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    276924 |   31407   112116 |   10469   16043   850883    53.0 |  7.847 % |
c |    277024 |   31407   112116 |   11515    8122   487282    60.0 |  8.023 % |
c |    277175 |   31398   112089 |   12667    8272   488995    59.1 |  8.062 % |
c |    277400 |   31398   112089 |   13934    8497   492685    58.0 |  8.062 % |
c |    277739 |   31398   112089 |   15327    8836   516956    58.5 |  8.062 % |
c |    278245 |   31398   112089 |   16860    9342   527457    56.5 |  8.062 % |
c |    279004 |   31398   112089 |   18546   10101   547907    54.2 |  8.062 % |
c |    280144 |   31398   112089 |   20401   11241   598133    53.2 |  8.062 % |
c |    281852 |   31398   112089 |   22441   12949   656767    50.7 |  8.062 % |
c |    284414 |   31398   112089 |   24685   15511   756431    48.8 |  8.062 % |
c |    288258 |   31398   112089 |   27153   19355   929635    48.0 |  8.062 % |
c |    294024 |   31398   112089 |   29869   25121  1228918    48.9 |  8.062 % |
c |    302674 |   31398   112089 |   32856   17310   714327    41.3 |  8.062 % |
c |    315649 |   31398   112089 |   36141   30285  1291782    42.7 |  8.062 % |
c |    335110 |   31398   112089 |   39756   26688  1324563    49.6 |  8.062 % |
c |    364302 |   31398   112089 |   43731   26413  2280791    86.4 |  8.062 % |
c |    408092 |   31398   112089 |   48104   39866  2503650    62.8 |  8.062 % |
c |    473776 |   31398   112089 |   52915   37642  2882037    76.6 |  8.062 % |
c |    572302 |   31398   112089 |   58206   18203  1345340    73.9 |  8.062 % |
c ==============================================================================
c [1mFound solution: 130978[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8   maxlim: 786519   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    645127 |   31363   111985 |   10454   44633  4900732   109.8 |  8.062 % |
c |    645230 |   31363   111985 |   11499    7935   563771    71.0 |  8.333 % |
c |    645380 |   31363   111985 |   12649    8085   566026    70.0 |  8.333 % |
c |    645605 |   31363   111985 |   13914    8310   569655    68.6 |  8.333 % |
c |    645943 |   31363   111985 |   15305    8648   578138    66.9 |  8.333 % |
c |    646449 |   31363   111985 |   16836    9154   584506    63.9 |  8.333 % |
c |    647208 |   31363   111985 |   18519    9913   611053    61.6 |  8.333 % |
c |    648347 |   31363   111985 |   20371   11052   658505    59.6 |  8.333 % |
c |    650055 |   31351   111943 |   22409   12758   717621    56.2 |  8.353 % |
c |    652617 |   31351   111943 |   24649   15320   840535    54.9 |  8.353 % |
c ==============================================================================
c [1mFound solution: 85805[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 831692   bits: 20/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    653534 |   31364   112043 |   10454   16237   861496    53.1 |  8.353 % |
c |    653634 |   31364   112043 |   11499    8219   265812    32.3 |  8.487 % |
c |    653784 |   31364   112043 |   12649    8369   266973    31.9 |  8.487 % |
c |    654010 |   31364   112043 |   13914    8595   270823    31.5 |  8.487 % |
c |    654348 |   31364   112043 |   15305    8933   278822    31.2 |  8.487 % |
c |    654855 |   31257   111446 |   16836    9424   294391    31.2 |  8.778 % |
c |    655616 |   31257   111446 |   18519   10185   317629    31.2 |  8.778 % |
c |    656756 |   31257   111446 |   20371   11325   354698    31.3 |  8.778 % |
c |    658464 |   31257   111446 |   22409   13033   418708    32.1 |  8.778 % |
c |    661027 |   31257   111446 |   24649   15596   574943    36.9 |  8.778 % |
c |    664872 |   31257   111446 |   27114   19441   943554    48.5 |  8.778 % |
c |    670638 |   31257   111446 |   29826   25207  1234922    49.0 |  8.778 % |
c |    679288 |   31257   111446 |   32809   15826   839590    53.1 |  8.778 % |
c |    692264 |   31257   111446 |   36090   28802  1630050    56.6 |  8.778 % |
c |    711725 |   31257   111446 |   39699   25577  1379054    53.9 |  8.778 % |
#### 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.92 0.93 2/54 21313
Raw data (stat): 21313 (runsolver) R 21312 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482668746 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.92 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 1556 0 0 0 994 5 0 0 25 0 1 0 482668746 8126464 1533 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1984 1533 603 41 0 1943 0
vsize: 7936
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2340 0 0 0 1991 8 0 0 25 0 1 0 482668746 11341824 2317 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2769 2317 603 41 0 2728 0
vsize: 11076
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2992 0 0 0 2988 10 0 0 25 0 1 0 482668746 13901824 2969 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2969 603 41 0 3353 0
vsize: 13576
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2992 0 0 0 3989 10 0 0 25 0 1 0 482668746 13901824 2969 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2969 603 41 0 3353 0
vsize: 13576
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2992 0 0 0 4988 11 0 0 25 0 1 0 482668746 13901824 2969 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2969 603 41 0 3353 0
vsize: 13576
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2994 0 0 0 5988 11 0 0 25 0 1 0 482668746 13901824 2971 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2971 603 41 0 3353 0
vsize: 13576
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.93 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 2994 0 0 0 6988 11 0 0 25 0 1 0 482668746 13901824 2971 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2971 603 41 0 3353 0
vsize: 13576
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3150 0 0 0 7987 12 0 0 25 0 1 0 482668746 14573568 3127 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3127 603 41 0 3517 0
vsize: 14232
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3150 0 0 0 8987 13 0 0 25 0 1 0 482668746 14573568 3127 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3127 603 41 0 3517 0
vsize: 14232
[startup+100.004 s]
Raw data (loadavg): 0.97 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3452 0 0 0 9986 14 0 0 25 0 1 0 482668746 15912960 3429 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3885 3429 603 41 0 3844 0
vsize: 15540
[startup+110.005 s]
Raw data (loadavg): 0.97 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3762 0 0 0 10985 16 0 0 25 0 1 0 482668746 17252352 3739 4294967295 134512640 134672761 3221224528 3221223712 134558697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4212 3739 603 41 0 4171 0
vsize: 16848
[startup+120.006 s]
Raw data (loadavg): 0.98 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3762 0 0 0 11984 16 0 0 25 0 1 0 482668746 17252352 3739 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4212 3739 603 41 0 4171 0
vsize: 16848
[startup+130.006 s]
Raw data (loadavg): 0.98 0.94 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3762 0 0 0 12984 16 0 0 25 0 1 0 482668746 17252352 3739 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4212 3739 603 41 0 4171 0
vsize: 16848
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 3984 0 0 0 13983 17 0 0 25 0 1 0 482668746 18063360 3961 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 3961 603 41 0 4369 0
vsize: 17640
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4223 0 0 0 14983 18 0 0 25 0 1 0 482668746 19132416 4200 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4671 4200 603 41 0 4630 0
vsize: 18684
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4223 0 0 0 15982 18 0 0 25 0 1 0 482668746 19132416 4200 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4671 4200 603 41 0 4630 0
vsize: 18684
[startup+170.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4223 0 0 0 16982 19 0 0 25 0 1 0 482668746 19132416 4200 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4671 4200 603 41 0 4630 0
vsize: 18684
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4223 0 0 0 17981 20 0 0 25 0 1 0 482668746 19132416 4200 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4671 4200 603 41 0 4630 0
vsize: 18684
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4739 0 0 0 18979 22 0 0 25 0 1 0 482668746 21143552 4716 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5162 4716 603 41 0 5121 0
vsize: 20648
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4859 0 0 0 19979 22 0 0 25 0 1 0 482668746 21684224 4836 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5294 4836 603 41 0 5253 0
vsize: 21176
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4859 0 0 0 20980 22 0 0 25 0 1 0 482668746 21684224 4836 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5294 4836 603 41 0 5253 0
vsize: 21176
[startup+220.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4859 0 0 0 21980 22 0 0 25 0 1 0 482668746 21684224 4836 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5294 4836 603 41 0 5253 0
vsize: 21176
[startup+230.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 4905 0 0 0 22980 22 0 0 25 0 1 0 482668746 21819392 4882 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5327 4882 603 41 0 5286 0
vsize: 21308
[startup+240.007 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 5385 0 0 0 23978 24 0 0 25 0 1 0 482668746 23830528 5362 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5818 5362 603 41 0 5777 0
vsize: 23272
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 5827 0 0 0 24977 25 0 0 25 0 1 0 482668746 25694208 5804 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6273 5804 603 41 0 6232 0
vsize: 25092
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 6216 0 0 0 25976 27 0 0 25 0 1 0 482668746 27303936 6193 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6666 6193 603 41 0 6625 0
vsize: 26664
[startup+270.008 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 6661 0 0 0 26973 29 0 0 25 0 1 0 482668746 29061120 6638 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7095 6638 603 41 0 7054 0
vsize: 28380
[startup+280.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7107 0 0 0 27972 30 0 0 25 0 1 0 482668746 30937088 7084 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7553 7084 603 41 0 7512 0
vsize: 30212
[startup+290.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 28972 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+300.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 29972 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+310.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 30972 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+320.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 31972 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 32972 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+340.012 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 33973 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 34973 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 35973 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 36973 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7453 0 0 0 37973 31 0 0 25 0 1 0 482668746 32276480 7430 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7430 603 41 0 7839 0
vsize: 31520
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7456 0 0 0 38973 31 0 0 25 0 1 0 482668746 32276480 7433 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7433 603 41 0 7839 0
vsize: 31520
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 39974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 40974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223584 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 41974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 42974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 43974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 44974 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 45975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 46975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 47975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 48975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 49975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 50975 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 51976 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 52976 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223712 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 53976 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 54976 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 55976 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223624 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 56977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 57977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 58977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 59977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 60977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 61977 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 62978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 63978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 64978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223664 134565078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 65978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 66978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21313
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 67978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+690.011 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 68978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+700.01 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 69978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+710.011 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7459 0 0 0 70978 31 0 0 25 0 1 0 482668746 32276480 7436 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7436 603 41 0 7839 0
vsize: 31520
[startup+720.011 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 71978 31 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+730.011 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 72977 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+740.012 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 73977 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+750.012 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21366
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 74978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+760.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 75978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+770.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 76978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+780.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 77978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+790.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 78978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+800.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 79978 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+810.011 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 80979 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+820.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 81979 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+830.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 82979 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+840.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 83979 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+850.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 84979 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 85980 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+870.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 86980 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+880.011 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7460 0 0 0 87980 32 0 0 25 0 1 0 482668746 32276480 7437 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7437 603 41 0 7839 0
vsize: 31520
[startup+890.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 88980 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 89980 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+910.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 90980 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+920.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 91980 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+930.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 92980 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+940.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 93981 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+950.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 94981 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+960.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7506 0 0 0 95981 32 0 0 25 0 1 0 482668746 32534528 7483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7483 603 41 0 7902 0
vsize: 31772
[startup+970.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7514 0 0 0 96981 32 0 0 25 0 1 0 482668746 32534528 7491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7943 7491 603 41 0 7902 0
vsize: 31772
[startup+980.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 7836 0 0 0 97980 33 0 0 25 0 1 0 482668746 33873920 7813 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8270 7813 603 41 0 8229 0
vsize: 33080
[startup+990.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8156 0 0 0 98980 34 0 0 25 0 1 0 482668746 35209216 8133 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8596 8133 603 41 0 8555 0
vsize: 34384
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8458 0 0 0 99979 34 0 0 25 0 1 0 482668746 36413440 8435 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8890 8435 603 41 0 8849 0
vsize: 35560
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8821 0 0 0 100978 36 0 0 25 0 1 0 482668746 37892096 8798 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9251 8798 603 41 0 9210 0
vsize: 37004
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 101978 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21368
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 102978 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 103978 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 104979 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223712 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 105979 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223696 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 106979 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 107979 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8920 0 0 0 108979 36 0 0 25 0 1 0 482668746 38297600 8897 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8897 603 41 0 9309 0
vsize: 37400
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 109978 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223632 134554629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 110978 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223632 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 111979 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1130.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 112989 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1140.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 113989 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1150.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 115012 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223684 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1160.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 116013 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1170.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 117013 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1180.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 118013 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1190.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 119013 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
[startup+1200.35 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21370
Raw data (stat): 21313 (minisat+) R 21312 25347 25346 0 -1 0 8922 0 0 0 120013 36 0 0 25 0 1 0 482668746 38297600 8899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8899 603 41 0 9309 0
vsize: 37400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.37 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 21370
Raw data (stat): 21313 (minisat+) Z 21312 25347 25346 0 -1 12 8925 0 0 0 120013 38 0 0 25 0 1 0 482668746 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.37
CPU time (s): 1200.53
CPU user time (s): 1200.14
CPU system time (s): 0.385941
CPU usage (%): 100.013
Max. virtual memory (Kb): 37400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####