PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
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	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 5800

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 01:50:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4202 boxname=wulflinc5 idbench=66 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc5/normalized-e64.b.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-e64.b.opb /oldhome/oroussel/tmp/wulflinc5/normalized-e64.b.opb
IDLAUNCH: 4202
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        899160 kB
Buffers:         34320 kB
Cached:          79620 kB
SwapCached:       2272 kB
Active:          54064 kB
Inactive:        65016 kB
HighTotal:      131008 kB
HighFree:        47460 kB
LowTotal:       903652 kB
LowFree:        851700 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10812 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:10:44 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4202 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27428     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   32888    82605 |   10962       1       16    16.0 |  0.000 % |
c |       101 |   32731    82280 |   12058      94     1328    14.1 |  0.441 % |
c |       251 |   32731    82280 |   13264     244     4888    20.0 |  0.441 % |
c |       476 |   32693    82200 |   14590     467     9207    19.7 |  0.538 % |
c |       815 |   32655    82120 |   16049     805    14538    18.1 |  0.636 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1118 |   32544    81867 |   10848    1108    20015    18.1 |  0.636 % |
c |      1219 |   32544    81867 |   11932    1209    21890    18.1 |  1.342 % |
c |      1371 |   32544    81867 |   13126    1361    27251    20.0 |  1.342 % |
c |      1597 |   32544    81867 |   14438    1587    32001    20.2 |  1.342 % |
c |      1935 |   32544    81867 |   15882    1925    44062    22.9 |  1.342 % |
c |      2442 |   32526    81825 |   17470    2426    58440    24.1 |  1.397 % |
c |      3201 |   32524    81821 |   19217    3182    81772    25.7 |  1.402 % |
c |      4340 |   32524    81821 |   21139    4321   124438    28.8 |  1.402 % |
c |      6049 |   32524    81821 |   23253    6030   236669    39.2 |  1.402 % |
c |      8611 |   32524    81821 |   25579    8592   404633    47.1 |  1.402 % |
c |     12456 |   32524    81821 |   28136   12437   881628    70.9 |  1.402 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17530 |   32583    81971 |   10861   17511  1261267    72.0 |  1.402 % |
c |     17631 |   32583    81971 |   11947    8857   728551    82.3 |  1.404 % |
c |     17781 |   32557    81915 |   13141    9005   733381    81.4 |  1.474 % |
c |     18007 |   32557    81915 |   14455    9231   741448    80.3 |  1.474 % |
c |     18344 |   32557    81915 |   15901    9568   749366    78.3 |  1.474 % |
c |     18850 |   32557    81915 |   17491   10074   785392    78.0 |  1.474 % |
c |     19609 |   32557    81915 |   19240   10833   859333    79.3 |  1.474 % |
c |     20748 |   32557    81915 |   21165   11972   919844    76.8 |  1.474 % |
c |     22458 |   32557    81915 |   23281   13682  1056358    77.2 |  1.474 % |
c |     25020 |   32557    81915 |   25609   16244  1287855    79.3 |  1.474 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25537 |   32576    81969 |   10858   16761  1329272    79.3 |  1.474 % |
c |     25637 |   32576    81969 |   11943    8481   589547    69.5 |  1.477 % |
c |     25787 |   32576    81969 |   13138    8631   595037    68.9 |  1.477 % |
c |     26012 |   32576    81969 |   14451    8856   607205    68.6 |  1.477 % |
c |     26349 |   32576    81969 |   15897    9193   625383    68.0 |  1.477 % |
c |     26855 |   32576    81969 |   17486    9699   645599    66.6 |  1.477 % |
c |     27616 |   32576    81969 |   19235   10460   688721    65.8 |  1.477 % |
c |     28755 |   32576    81969 |   21159   11599   760883    65.6 |  1.477 % |
c |     30463 |   32576    81969 |   23275   13307   926598    69.6 |  1.477 % |
c |     33026 |   32576    81969 |   25602   15870  1052589    66.3 |  1.477 % |
c |     36872 |   32576    81969 |   28162   19716  1313125    66.6 |  1.477 % |
c |     42638 |   32540    81893 |   30979   25472  1707177    67.0 |  1.570 % |
c |     51288 |   32540    81893 |   34077   13453   850735    63.2 |  1.570 % |
c |     64262 |   32540    81893 |   37484   26427  1854535    70.2 |  1.570 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71120 |   32558    81945 |   10852   33285  2473346    74.3 |  1.570 % |
c |     71222 |   32558    81945 |   11937    6680   548160    82.1 |  1.583 % |
c |     71372 |   32558    81945 |   13130    6830   551418    80.7 |  1.583 % |
c |     71597 |   32558    81945 |   14444    7055   563546    79.9 |  1.583 % |
c |     71934 |   32558    81945 |   15888    7392   572407    77.4 |  1.583 % |
c |     72440 |   32558    81945 |   17477    7898   589289    74.6 |  1.583 % |
c |     73199 |   32558    81945 |   19224    8657   630654    72.8 |  1.583 % |
c |     74340 |   32558    81945 |   21147    9798   684750    69.9 |  1.583 % |
c |     76048 |   32558    81945 |   23262   11506   842785    73.2 |  1.583 % |
c |     78611 |   32558    81945 |   25588   14069  1080790    76.8 |  1.583 % |
c |     82457 |   32558    81945 |   28147   17915  1447445    80.8 |  1.583 % |
c |     88223 |   32558    81945 |   30962   23681  1883985    79.6 |  1.583 % |
c |     96872 |   32558    81945 |   34058   32330  2567295    79.4 |  1.583 % |
c |    109848 |   32558    81945 |   37464   21298  1707483    80.2 |  1.583 % |
c |    129309 |   32558    81945 |   41210   13470  1145174    85.0 |  1.583 % |
c |    158501 |   32558    81945 |   45331   42662  3823977    89.6 |  1.583 % |
c |    202290 |   32558    81945 |   49864   18699  1418328    75.9 |  1.583 % |
c |    267976 |   32558    81945 |   54851   46288  3760997    81.3 |  1.583 % |
c |    366502 |   32558    81945 |   60336   17595  1604710    91.2 |  1.583 % |
#### 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.83 0.93 0.90 2/54 28532
Raw data (stat): 28532 (runsolver) R 28531 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422544841 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99969 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 2460 0 0 0 993 5 0 0 25 0 1 0 422544841 12300288 2385 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3003 2385 603 41 0 2962 0
vsize: 12012
[startup+20.0009 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 3064 0 0 0 1990 7 0 0 25 0 1 0 422544841 14704640 2989 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3590 2989 603 41 0 3549 0
vsize: 14360
[startup+30.0017 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 3435 0 0 0 2989 8 0 0 25 0 1 0 422544841 16285696 3360 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3976 3360 603 41 0 3935 0
vsize: 15904
[startup+40.0007 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 3435 0 0 0 3988 8 0 0 25 0 1 0 422544841 16285696 3360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3976 3360 603 41 0 3935 0
vsize: 15904
[startup+50.0018 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 3547 0 0 0 4988 9 0 0 25 0 1 0 422544841 16814080 3472 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4105 3472 603 41 0 4064 0
vsize: 16420
[startup+60.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 3550 0 0 0 5988 9 0 0 25 0 1 0 422544841 16814080 3475 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4105 3475 603 41 0 4064 0
vsize: 16420
[startup+70.002 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4002 0 0 0 6986 10 0 0 25 0 1 0 422544841 18558976 3927 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4531 3927 603 41 0 4490 0
vsize: 18124
[startup+80.002 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4343 0 0 0 7985 11 0 0 25 0 1 0 422544841 20041728 4268 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4893 4268 603 41 0 4852 0
vsize: 19572
[startup+90.0018 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4677 0 0 0 8984 12 0 0 25 0 1 0 422544841 21495808 4602 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4602 603 41 0 5207 0
vsize: 20992
[startup+100.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4677 0 0 0 9985 12 0 0 25 0 1 0 422544841 21495808 4602 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4602 603 41 0 5207 0
vsize: 20992
[startup+110.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4677 0 0 0 10985 12 0 0 25 0 1 0 422544841 21495808 4602 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4602 603 41 0 5207 0
vsize: 20992
[startup+120.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4677 0 0 0 11985 12 0 0 25 0 1 0 422544841 21495808 4602 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5248 4602 603 41 0 5207 0
vsize: 20992
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4940 0 0 0 12984 13 0 0 25 0 1 0 422544841 22560768 4865 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5508 4865 603 41 0 5467 0
vsize: 22032
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4984 0 0 0 13984 14 0 0 25 0 1 0 422544841 22695936 4909 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4909 603 41 0 5500 0
vsize: 22164
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4984 0 0 0 14984 14 0 0 25 0 1 0 422544841 22695936 4909 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4909 603 41 0 5500 0
vsize: 22164
[startup+160.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4984 0 0 0 15984 14 0 0 25 0 1 0 422544841 22695936 4909 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4909 603 41 0 5500 0
vsize: 22164
[startup+170.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 4984 0 0 0 16984 14 0 0 25 0 1 0 422544841 22695936 4909 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5541 4909 603 41 0 5500 0
vsize: 22164
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5172 0 0 0 17984 14 0 0 25 0 1 0 422544841 23498752 5097 4294967295 134512640 134672761 3221224560 3221223716 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5737 5097 603 41 0 5696 0
vsize: 22948
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5600 0 0 0 18982 16 0 0 25 0 1 0 422544841 25235456 5525 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5525 603 41 0 6120 0
vsize: 24644
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5600 0 0 0 19982 16 0 0 25 0 1 0 422544841 25235456 5525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5525 603 41 0 6120 0
vsize: 24644
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5600 0 0 0 20982 16 0 0 25 0 1 0 422544841 25235456 5525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5525 603 41 0 6120 0
vsize: 24644
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5600 0 0 0 21982 16 0 0 25 0 1 0 422544841 25235456 5525 4294967295 134512640 134672761 3221224560 3221223728 134561136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5525 603 41 0 6120 0
vsize: 24644
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5600 0 0 0 22983 16 0 0 25 0 1 0 422544841 25235456 5525 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6161 5525 603 41 0 6120 0
vsize: 24644
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 5854 0 0 0 23982 17 0 0 25 0 1 0 422544841 26320896 5779 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5779 603 41 0 6385 0
vsize: 25704
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 24981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+260.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 25981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 26981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+280.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 27981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+290.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 28981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+300.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6175 0 0 0 29981 19 0 0 25 0 1 0 422544841 27668480 6100 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6755 6100 603 41 0 6714 0
vsize: 27020
[startup+310.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6401 0 0 0 30981 19 0 0 25 0 1 0 422544841 28602368 6326 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6983 6326 603 41 0 6942 0
vsize: 27932
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 6775 0 0 0 31980 21 0 0 25 0 1 0 422544841 30138368 6700 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7358 6700 603 41 0 7317 0
vsize: 29432
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7145 0 0 0 32979 21 0 0 25 0 1 0 422544841 31612928 7070 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7718 7070 603 41 0 7677 0
vsize: 30872
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 33979 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 34979 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 35979 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 36979 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 37979 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 38980 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 39980 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223744 134559159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7312 0 0 0 40980 22 0 0 25 0 1 0 422544841 32280576 7237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7237 603 41 0 7840 0
vsize: 31524
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7349 0 0 0 41980 22 0 0 25 0 1 0 422544841 32415744 7274 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7274 603 41 0 7873 0
vsize: 31656
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 42980 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 43980 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 44981 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 45981 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 46981 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 47981 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 48981 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 49982 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7357 0 0 0 50982 22 0 0 25 0 1 0 422544841 32415744 7282 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7914 7282 603 41 0 7873 0
vsize: 31656
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7388 0 0 0 51982 23 0 0 25 0 1 0 422544841 32546816 7313 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7946 7313 603 41 0 7905 0
vsize: 31784
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7638 0 0 0 52981 24 0 0 25 0 1 0 422544841 33636352 7563 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8212 7563 603 41 0 8171 0
vsize: 32848
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7684 0 0 0 53981 24 0 0 25 0 1 0 422544841 33771520 7609 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8245 7609 603 41 0 8204 0
vsize: 32980
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7684 0 0 0 54981 24 0 0 25 0 1 0 422544841 33771520 7609 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8245 7609 603 41 0 8204 0
vsize: 32980
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28532
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7684 0 0 0 55981 24 0 0 25 0 1 0 422544841 33771520 7609 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8245 7609 603 41 0 8204 0
vsize: 32980
[startup+570.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7684 0 0 0 56981 24 0 0 25 0 1 0 422544841 33771520 7609 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8245 7609 603 41 0 8204 0
vsize: 32980
[startup+580.037 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 57984 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+590.037 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 58984 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+600.038 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 59984 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+610.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 60985 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+620.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 61985 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+630.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28585
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 62985 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+640.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7696 0 0 0 63985 24 0 0 25 0 1 0 422544841 33927168 7621 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7621 603 41 0 8242 0
vsize: 33132
[startup+650.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7702 0 0 0 64985 24 0 0 25 0 1 0 422544841 33927168 7627 4294967295 134512640 134672761 3221224560 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7627 603 41 0 8242 0
vsize: 33132
[startup+660.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7707 0 0 0 65985 24 0 0 25 0 1 0 422544841 33927168 7632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8283 7632 603 41 0 8242 0
vsize: 33132
[startup+670.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 7859 0 0 0 66985 24 0 0 25 0 1 0 422544841 34594816 7784 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8446 7784 603 41 0 8405 0
vsize: 33784
[startup+680.04 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8116 0 0 0 67984 26 0 0 25 0 1 0 422544841 35663872 8041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8707 8041 603 41 0 8666 0
vsize: 34828
[startup+690.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8275 0 0 0 68983 26 0 0 25 0 1 0 422544841 36200448 8200 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8838 8200 603 41 0 8797 0
vsize: 35352
[startup+700.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8275 0 0 0 69983 26 0 0 25 0 1 0 422544841 36200448 8200 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8838 8200 603 41 0 8797 0
vsize: 35352
[startup+710.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8282 0 0 0 70984 26 0 0 25 0 1 0 422544841 36347904 8207 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8207 603 41 0 8833 0
vsize: 35496
[startup+720.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8290 0 0 0 71984 27 0 0 25 0 1 0 422544841 36347904 8215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8215 603 41 0 8833 0
vsize: 35496
[startup+730.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8290 0 0 0 72984 27 0 0 25 0 1 0 422544841 36347904 8215 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8215 603 41 0 8833 0
vsize: 35496
[startup+740.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8296 0 0 0 73984 27 0 0 25 0 1 0 422544841 36347904 8221 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8221 603 41 0 8833 0
vsize: 35496
[startup+750.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8297 0 0 0 74984 27 0 0 25 0 1 0 422544841 36347904 8222 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8222 603 41 0 8833 0
vsize: 35496
[startup+760.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8298 0 0 0 75984 27 0 0 25 0 1 0 422544841 36347904 8223 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8223 603 41 0 8833 0
vsize: 35496
[startup+770.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8304 0 0 0 76984 27 0 0 25 0 1 0 422544841 36347904 8229 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8229 603 41 0 8833 0
vsize: 35496
[startup+780.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8304 0 0 0 77985 27 0 0 25 0 1 0 422544841 36347904 8229 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8229 603 41 0 8833 0
vsize: 35496
[startup+790.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8304 0 0 0 78985 27 0 0 25 0 1 0 422544841 36347904 8229 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8874 8229 603 41 0 8833 0
vsize: 35496
[startup+800.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8318 0 0 0 79985 27 0 0 25 0 1 0 422544841 36511744 8243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8914 8243 603 41 0 8873 0
vsize: 35656
[startup+810.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8527 0 0 0 80984 28 0 0 25 0 1 0 422544841 37322752 8452 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9112 8452 603 41 0 9071 0
vsize: 36448
[startup+820.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 8776 0 0 0 81984 28 0 0 25 0 1 0 422544841 38395904 8701 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9374 8701 603 41 0 9333 0
vsize: 37496
[startup+830.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9015 0 0 0 82983 30 0 0 25 0 1 0 422544841 39329792 8940 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8940 603 41 0 9561 0
vsize: 38408
[startup+840.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9015 0 0 0 83983 30 0 0 25 0 1 0 422544841 39329792 8940 4294967295 134512640 134672761 3221224560 3221223744 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8940 603 41 0 9561 0
vsize: 38408
[startup+850.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9015 0 0 0 84983 30 0 0 25 0 1 0 422544841 39329792 8940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8940 603 41 0 9561 0
vsize: 38408
[startup+860.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9026 0 0 0 85983 30 0 0 25 0 1 0 422544841 39329792 8951 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8951 603 41 0 9561 0
vsize: 38408
[startup+870.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9035 0 0 0 86983 30 0 0 25 0 1 0 422544841 39514112 8960 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8960 603 41 0 9606 0
vsize: 38588
[startup+880.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9040 0 0 0 87984 30 0 0 25 0 1 0 422544841 39514112 8965 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8965 603 41 0 9606 0
vsize: 38588
[startup+890.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28587
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9041 0 0 0 88984 30 0 0 25 0 1 0 422544841 39514112 8966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8966 603 41 0 9606 0
vsize: 38588
[startup+900.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9041 0 0 0 89984 30 0 0 25 0 1 0 422544841 39514112 8966 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8966 603 41 0 9606 0
vsize: 38588
[startup+910.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9041 0 0 0 90984 30 0 0 25 0 1 0 422544841 39514112 8966 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8966 603 41 0 9606 0
vsize: 38588
[startup+920.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9041 0 0 0 91984 30 0 0 25 0 1 0 422544841 39514112 8966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8966 603 41 0 9606 0
vsize: 38588
[startup+930.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9054 0 0 0 92984 30 0 0 25 0 1 0 422544841 39514112 8979 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8979 603 41 0 9606 0
vsize: 38588
[startup+940.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9055 0 0 0 93985 30 0 0 25 0 1 0 422544841 39514112 8980 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8980 603 41 0 9606 0
vsize: 38588
[startup+950.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9056 0 0 0 94985 30 0 0 25 0 1 0 422544841 39514112 8981 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8981 603 41 0 9606 0
vsize: 38588
[startup+960.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9056 0 0 0 95985 30 0 0 25 0 1 0 422544841 39514112 8981 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8981 603 41 0 9606 0
vsize: 38588
[startup+970.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9058 0 0 0 96985 30 0 0 25 0 1 0 422544841 39514112 8983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8983 603 41 0 9606 0
vsize: 38588
[startup+980.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9062 0 0 0 97985 30 0 0 25 0 1 0 422544841 39514112 8987 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9647 8987 603 41 0 9606 0
vsize: 38588
[startup+990.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9264 0 0 0 98985 31 0 0 25 0 1 0 422544841 40321024 9189 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9844 9189 603 41 0 9803 0
vsize: 39376
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 99984 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 100984 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 101983 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 102983 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 103983 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9400 0 0 0 104983 32 0 0 25 0 1 0 422544841 40992768 9325 4294967295 134512640 134672761 3221224560 3221223760 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9325 603 41 0 9967 0
vsize: 40032
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 105983 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 106984 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 107984 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 108984 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 109984 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 110984 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9401 0 0 0 111985 32 0 0 25 0 1 0 422544841 40992768 9326 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9326 603 41 0 9967 0
vsize: 40032
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9410 0 0 0 112985 32 0 0 25 0 1 0 422544841 40992768 9335 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10008 9335 603 41 0 9967 0
vsize: 40032
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9421 0 0 0 113985 32 0 0 25 0 1 0 422544841 41127936 9346 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10041 9346 603 41 0 10000 0
vsize: 40164
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9430 0 0 0 114985 32 0 0 25 0 1 0 422544841 41127936 9355 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10041 9355 603 41 0 10000 0
vsize: 40164
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9443 0 0 0 115985 32 0 0 25 0 1 0 422544841 41127936 9368 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10041 9368 603 41 0 10000 0
vsize: 40164
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9452 0 0 0 116986 32 0 0 25 0 1 0 422544841 41324544 9377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10089 9377 603 41 0 10048 0
vsize: 40356
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9454 0 0 0 117986 32 0 0 25 0 1 0 422544841 41324544 9379 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10089 9379 603 41 0 10048 0
vsize: 40356
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9477 0 0 0 118986 32 0 0 25 0 1 0 422544841 41324544 9402 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10089 9402 603 41 0 10048 0
vsize: 40356
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28589
Raw data (stat): 28532 (minisat+) R 28531 24215 24214 0 -1 0 9657 0 0 0 119985 33 0 0 25 0 1 0 422544841 42143744 9582 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10289 9582 603 41 0 10248 0
vsize: 41156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28589
Raw data (stat): 28532 (minisat+) Z 28531 24215 24214 0 -1 12 9660 0 0 0 119986 35 0 0 25 0 1 0 422544841 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.07
CPU time (s): 1200.22
CPU user time (s): 1199.86
CPU system time (s): 0.354946
CPU usage (%): 100.012
Max. virtual memory (Kb): 41156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####