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/synthesis-ptl-cmos-circuits/normalized-9symml.opb
MD5SUM	48809ba02390b1184dab90aed89aff8e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4517
Optimality of the best value was proved	NO
Number of terms in the objective function	651
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	28138
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	28138
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02684
Number of variables	651
Total number of constraints	1658
Number of constraints which are clauses	1656
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	1
Maximum length of a constraint	42
Trace number 5960

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 02:30:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4382 boxname=wulflinc18 idbench=246 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  48809ba02390b1184dab90aed89aff8e  /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb
IDLAUNCH: 4382
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 3
cpu MHz		: 451.177
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:        861252 kB
Buffers:         35236 kB
Cached:         102144 kB
SwapCached:        320 kB
Active:          55688 kB
Inactive:        84884 kB
HighTotal:      131008 kB
HighFree:        24836 kB
LowTotal:       903652 kB
LowFree:        836416 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27128 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:50:28 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4382 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1579 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 |    1552     6592 |     517       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6227[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:101537     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  240640   564833 |   80213       0        0     nan |  0.000 % |
c |       100 |  240294   564068 |   88234      97      554     5.7 |  0.124 % |
c |       250 |  239475   562211 |   97057     242     1239     5.1 |  0.372 % |
c |       475 |  239475   562211 |  106763     467     2772     5.9 |  0.372 % |
c |       812 |  239475   562211 |  117439     804     5080     6.3 |  0.372 % |
c |      1318 |  239344   561924 |  129183    1306    10185     7.8 |  0.418 % |
c |      2077 |  239154   561493 |  142102    2061    21860    10.6 |  0.491 % |
c |      3217 |  238924   560969 |  156312    3195    43126    13.5 |  0.574 % |
c |      4925 |  238870   560853 |  171943    4898   147580    30.1 |  0.598 % |
c |      7488 |  238545   560119 |  189138    7447   199936    26.8 |  0.694 % |
c |     11333 |  238182   559291 |  208051   11252   264258    23.5 |  0.811 % |
c |     17099 |  237688   558162 |  228857   16994   352844    20.8 |  0.969 % |
c |     25751 |  237623   558014 |  251742   25643   903840    35.2 |  0.991 % |
c ==============================================================================
c [1mFound solution: 5682[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:81756     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29821 |  435689  1020432 |  145229   29713  1042028    35.1 |  0.991 % |
c |     29922 |  435689  1020432 |  159751   29814  1042915    35.0 |  0.570 % |
c |     30072 |  435689  1020432 |  175727   29964  1043798    34.8 |  0.570 % |
c |     30297 |  435410  1019814 |  193299   30186  1047211    34.7 |  0.617 % |
c |     30635 |  434343  1017394 |  212629   30492  1053024    34.5 |  0.811 % |
c |     31141 |  434343  1017394 |  233892   30998  1066445    34.4 |  0.811 % |
c |     31900 |  434343  1017394 |  257282   31757  1076013    33.9 |  0.811 % |
c |     33039 |  434343  1017394 |  283010   32896  1253111    38.1 |  0.811 % |
c |     34748 |  434343  1017394 |  311311   34605  1301864    37.6 |  0.811 % |
c |     37311 |  434331  1017367 |  342442   37166  1344836    36.2 |  0.813 % |
c |     41155 |  434331  1017367 |  376686   41010  1457843    35.5 |  0.813 % |
c |     46922 |  434331  1017367 |  414355   46777  2162173    46.2 |  0.813 % |
c |     55572 |  434242  1017165 |  455790   55424  3473368    62.7 |  0.830 % |
c |     68546 |  434242  1017165 |  501369   68398  6520599    95.3 |  0.830 % |
c |     88008 |  434235  1017150 |  551506   87857  9667702   110.0 |  0.832 % |
c |    117200 |  433771  1016104 |  606657  117042 19603779   167.5 |  0.911 % |
#### 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.91 0.91 0.89 2/55 28749
Raw data (stat): 28749 (runsolver) R 28748 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480996665 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.92 0.91 0.89 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 7937 0 0 0 978 20 0 0 25 0 1 0 480996665 35844096 7589 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8751 7589 603 41 0 8710 0
vsize: 35004
[startup+20.0018 s]
Raw data (loadavg): 0.93 0.92 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8060 0 0 0 1977 21 0 0 25 0 1 0 480996665 36249600 7712 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8850 7712 603 41 0 8809 0
vsize: 35400
[startup+30.0017 s]
Raw data (loadavg): 0.94 0.92 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8158 0 0 0 2976 22 0 0 25 0 1 0 480996665 36675584 7810 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8954 7810 603 41 0 8913 0
vsize: 35816
[startup+40.003 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8241 0 0 0 3975 23 0 0 25 0 1 0 480996665 37003264 7893 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9034 7893 603 41 0 8993 0
vsize: 36136
[startup+50.004 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8377 0 0 0 4975 23 0 0 25 0 1 0 480996665 37539840 8029 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9165 8029 603 41 0 9124 0
vsize: 36660
[startup+60.0045 s]
Raw data (loadavg): 0.96 0.92 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8646 0 0 0 5974 24 0 0 25 0 1 0 480996665 38711296 8298 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9451 8298 603 41 0 9410 0
vsize: 37804
[startup+70.0054 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8819 0 0 0 6973 25 0 0 25 0 1 0 480996665 39387136 8471 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9616 8471 603 41 0 9575 0
vsize: 38464
[startup+80.0057 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 28749
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 8915 0 0 0 7973 25 0 0 25 0 1 0 480996665 39788544 8567 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 8567 603 41 0 9673 0
vsize: 38856
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 9016 0 0 0 8972 26 0 0 25 0 1 0 480996665 40189952 8668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9812 8668 603 41 0 9771 0
vsize: 39248
[startup+100.006 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 9164 0 0 0 9971 27 0 0 25 0 1 0 480996665 40730624 8816 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9944 8816 603 41 0 9903 0
vsize: 39776
[startup+110.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15384 0 0 0 10956 42 0 0 25 0 1 0 480996665 70361088 14706 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17178 14706 603 41 0 17137 0
vsize: 68712
[startup+120.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15468 0 0 0 11956 42 0 0 25 0 1 0 480996665 70627328 14790 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17243 14790 603 41 0 17202 0
vsize: 68972
[startup+130.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15659 0 0 0 12955 43 0 0 25 0 1 0 480996665 71561216 14981 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17471 14981 603 41 0 17430 0
vsize: 69884
[startup+140.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15700 0 0 0 13955 43 0 0 25 0 1 0 480996665 71696384 15022 4294967295 134512640 134672761 3221224560 3221223744 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17504 15022 603 41 0 17463 0
vsize: 70016
[startup+150.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15761 0 0 0 14954 44 0 0 25 0 1 0 480996665 71831552 15083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17537 15083 603 41 0 17496 0
vsize: 70148
[startup+160.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15830 0 0 0 15953 45 0 0 25 0 1 0 480996665 72101888 15152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17603 15152 603 41 0 17562 0
vsize: 70412
[startup+170.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15905 0 0 0 16953 45 0 0 25 0 1 0 480996665 72372224 15227 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17669 15227 603 41 0 17628 0
vsize: 70676
[startup+180.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 15950 0 0 0 17952 46 0 0 25 0 1 0 480996665 72638464 15272 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17734 15272 603 41 0 17693 0
vsize: 70936
[startup+190.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16043 0 0 0 18951 46 0 0 25 0 1 0 480996665 73043968 15365 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17833 15365 603 41 0 17792 0
vsize: 71332
[startup+200.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16160 0 0 0 19951 47 0 0 25 0 1 0 480996665 73449472 15482 4294967295 134512640 134672761 3221224560 3221223744 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17932 15482 603 41 0 17891 0
vsize: 71728
[startup+210.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16309 0 0 0 20950 48 0 0 25 0 1 0 480996665 74117120 15631 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18095 15631 603 41 0 18054 0
vsize: 72380
[startup+220.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16427 0 0 0 21949 49 0 0 25 0 1 0 480996665 74518528 15749 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18193 15749 603 41 0 18152 0
vsize: 72772
[startup+230.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16537 0 0 0 22948 50 0 0 25 0 1 0 480996665 75051008 15859 4294967295 134512640 134672761 3221224560 3221223664 134559818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18323 15859 603 41 0 18282 0
vsize: 73292
[startup+240.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16681 0 0 0 23947 51 0 0 25 0 1 0 480996665 75583488 16003 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 16003 603 41 0 18412 0
vsize: 73812
[startup+250.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16753 0 0 0 24946 52 0 0 25 0 1 0 480996665 75853824 16075 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18519 16075 603 41 0 18478 0
vsize: 74076
[startup+260.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16847 0 0 0 25946 52 0 0 25 0 1 0 480996665 76255232 16169 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18617 16169 603 41 0 18576 0
vsize: 74468
[startup+270.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 16921 0 0 0 26945 53 0 0 25 0 1 0 480996665 76525568 16243 4294967295 134512640 134672761 3221224560 3221223664 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18683 16243 603 41 0 18642 0
vsize: 74732
[startup+280.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17055 0 0 0 27944 54 0 0 25 0 1 0 480996665 77049856 16377 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18811 16377 603 41 0 18770 0
vsize: 75244
[startup+290.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17165 0 0 0 28944 54 0 0 25 0 1 0 480996665 77582336 16487 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18941 16487 603 41 0 18900 0
vsize: 75764
[startup+300.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17380 0 0 0 29942 55 0 0 25 0 1 0 480996665 78389248 16702 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19138 16702 603 41 0 19097 0
vsize: 76552
[startup+310.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17547 0 0 0 30942 56 0 0 25 0 1 0 480996665 79052800 16869 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19300 16869 603 41 0 19259 0
vsize: 77200
[startup+320.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17681 0 0 0 31942 56 0 0 25 0 1 0 480996665 79577088 17003 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19428 17003 603 41 0 19387 0
vsize: 77712
[startup+330.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17819 0 0 0 32942 56 0 0 25 0 1 0 480996665 80216064 17141 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19584 17141 603 41 0 19543 0
vsize: 78336
[startup+340.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 17969 0 0 0 33942 57 0 0 25 0 1 0 480996665 80756736 17291 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19716 17291 603 41 0 19675 0
vsize: 78864
[startup+350.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18077 0 0 0 34941 57 0 0 25 0 1 0 480996665 81285120 17399 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19845 17399 603 41 0 19804 0
vsize: 79380
[startup+360.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18123 0 0 0 35941 58 0 0 25 0 1 0 480996665 81420288 17445 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19878 17445 603 41 0 19837 0
vsize: 79512
[startup+370.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18164 0 0 0 36941 58 0 0 25 0 1 0 480996665 81555456 17486 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19911 17486 603 41 0 19870 0
vsize: 79644
[startup+380.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28751
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18207 0 0 0 37941 58 0 0 25 0 1 0 480996665 81821696 17529 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19976 17529 603 41 0 19935 0
vsize: 79904
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18266 0 0 0 38941 58 0 0 25 0 1 0 480996665 81952768 17588 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20008 17588 603 41 0 19967 0
vsize: 80032
[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18310 0 0 0 39941 58 0 0 25 0 1 0 480996665 82214912 17632 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20072 17632 603 41 0 20031 0
vsize: 80288
[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18385 0 0 0 40940 59 0 0 25 0 1 0 480996665 82481152 17707 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20137 17707 603 41 0 20096 0
vsize: 80548
[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18449 0 0 0 41940 59 0 0 25 0 1 0 480996665 82751488 17771 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 17771 603 41 0 20162 0
vsize: 80812
[startup+430.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 18754 0 0 0 42939 61 0 0 25 0 1 0 480996665 83976192 18076 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20502 18076 603 41 0 20461 0
vsize: 82008
[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 19155 0 0 0 43938 61 0 0 25 0 1 0 480996665 85594112 18477 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20897 18477 603 41 0 20856 0
vsize: 83588
[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 19585 0 0 0 44938 62 0 0 25 0 1 0 480996665 87371776 18907 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21331 18907 603 41 0 21290 0
vsize: 85324
[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 20096 0 0 0 45937 63 0 0 25 0 1 0 480996665 89497600 19418 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21850 19418 603 41 0 21809 0
vsize: 87400
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 20591 0 0 0 46936 64 0 0 25 0 1 0 480996665 91799552 19913 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22412 19913 603 41 0 22371 0
vsize: 89648
[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 20998 0 0 0 47935 66 0 0 25 0 1 0 480996665 93388800 20320 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22800 20320 603 41 0 22759 0
vsize: 91200
[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21144 0 0 0 48935 66 0 0 25 0 1 0 480996665 94068736 20466 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22966 20466 603 41 0 22925 0
vsize: 91864
[startup+500.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21227 0 0 0 49934 66 0 0 25 0 1 0 480996665 94339072 20549 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23032 20549 603 41 0 22991 0
vsize: 92128
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21282 0 0 0 50934 67 0 0 25 0 1 0 480996665 94609408 20604 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23098 20604 603 41 0 23057 0
vsize: 92392
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21402 0 0 0 51934 67 0 0 25 0 1 0 480996665 95010816 20724 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23196 20724 603 41 0 23155 0
vsize: 92784
[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21644 0 0 0 52934 67 0 0 25 0 1 0 480996665 96079872 20966 4294967295 134512640 134672761 3221224560 3221223664 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23457 20966 603 41 0 23416 0
vsize: 93828
[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 21906 0 0 0 53934 67 0 0 25 0 1 0 480996665 97144832 21228 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23717 21228 603 41 0 23676 0
vsize: 94868
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 22161 0 0 0 54934 68 0 0 25 0 1 0 480996665 98197504 21483 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23974 21483 603 41 0 23933 0
vsize: 95896
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 22457 0 0 0 55933 69 0 0 25 0 1 0 480996665 99385344 21779 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24264 21779 603 41 0 24223 0
vsize: 97056
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 22718 0 0 0 56932 70 0 0 25 0 1 0 480996665 100438016 22040 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24521 22040 603 41 0 24480 0
vsize: 98084
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 22988 0 0 0 57932 70 0 0 25 0 1 0 480996665 101646336 22310 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24816 22310 603 41 0 24775 0
vsize: 99264
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 23223 0 0 0 58931 71 0 0 25 0 1 0 480996665 102588416 22545 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25046 22545 603 41 0 25005 0
vsize: 100184
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 23477 0 0 0 59931 71 0 0 25 0 1 0 480996665 103632896 22799 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25301 22799 603 41 0 25260 0
vsize: 101204
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 23685 0 0 0 60931 72 0 0 25 0 1 0 480996665 104415232 23007 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25492 23007 603 41 0 25451 0
vsize: 101968
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 23899 0 0 0 61930 72 0 0 25 0 1 0 480996665 105345024 23221 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25719 23221 603 41 0 25678 0
vsize: 102876
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24148 0 0 0 62930 73 0 0 25 0 1 0 480996665 106283008 23470 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25948 23470 603 41 0 25907 0
vsize: 103792
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24306 0 0 0 63930 73 0 0 25 0 1 0 480996665 106930176 23628 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26106 23628 603 41 0 26065 0
vsize: 104424
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24449 0 0 0 64929 74 0 0 25 0 1 0 480996665 107470848 23771 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26238 23772 603 41 0 26197 0
vsize: 104952
[startup+660.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24556 0 0 0 65929 74 0 0 25 0 1 0 480996665 108003328 23878 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26368 23878 603 41 0 26327 0
vsize: 105472
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24616 0 0 0 66929 74 0 0 25 0 1 0 480996665 108138496 23938 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26401 23938 603 41 0 26360 0
vsize: 105604
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28753
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24686 0 0 0 67929 74 0 0 25 0 1 0 480996665 108535808 24008 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26498 24008 603 41 0 26457 0
vsize: 105992
[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24809 0 0 0 68929 75 0 0 25 0 1 0 480996665 108937216 24131 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26596 24131 603 41 0 26555 0
vsize: 106384
[startup+700.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 24926 0 0 0 69929 75 0 0 25 0 1 0 480996665 109473792 24248 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26727 24248 603 41 0 26686 0
vsize: 106908
[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25036 0 0 0 70929 75 0 0 25 0 1 0 480996665 109879296 24358 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26826 24358 603 41 0 26785 0
vsize: 107304
[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25134 0 0 0 71929 76 0 0 25 0 1 0 480996665 110280704 24456 4294967295 134512640 134672761 3221224560 3221223696 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26924 24456 603 41 0 26883 0
vsize: 107696
[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25278 0 0 0 72929 76 0 0 25 0 1 0 480996665 110952448 24600 4294967295 134512640 134672761 3221224560 3221223696 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27088 24600 603 41 0 27047 0
vsize: 108352
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25435 0 0 0 73928 76 0 0 25 0 1 0 480996665 111493120 24757 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27220 24757 603 41 0 27179 0
vsize: 108880
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25635 0 0 0 74928 77 0 0 25 0 1 0 480996665 112414720 24957 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27445 24957 603 41 0 27404 0
vsize: 109780
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 25847 0 0 0 75928 77 0 0 25 0 1 0 480996665 113217536 25169 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27641 25169 603 41 0 27600 0
vsize: 110564
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26042 0 0 0 76928 78 0 0 25 0 1 0 480996665 113999872 25364 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27832 25364 603 41 0 27791 0
vsize: 111328
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26255 0 0 0 77927 78 0 0 25 0 1 0 480996665 114900992 25577 4294967295 134512640 134672761 3221224560 3221223664 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28052 25577 603 41 0 28011 0
vsize: 112208
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26368 0 0 0 78927 79 0 0 25 0 1 0 480996665 115298304 25690 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28149 25690 603 41 0 28108 0
vsize: 112596
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26545 0 0 0 79927 79 0 0 25 0 1 0 480996665 116092928 25867 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28343 25867 603 41 0 28302 0
vsize: 113372
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26704 0 0 0 80926 80 0 0 25 0 1 0 480996665 116760576 26026 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28506 26026 603 41 0 28465 0
vsize: 114024
[startup+820.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 26879 0 0 0 81926 80 0 0 25 0 1 0 480996665 117424128 26201 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28668 26201 603 41 0 28627 0
vsize: 114672
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27048 0 0 0 82925 81 0 0 25 0 1 0 480996665 118091776 26370 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28831 26370 603 41 0 28790 0
vsize: 115324
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27182 0 0 0 83925 82 0 0 25 0 1 0 480996665 118620160 26504 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28960 26504 603 41 0 28919 0
vsize: 115840
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27338 0 0 0 84924 83 0 0 25 0 1 0 480996665 119279616 26660 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29121 26660 603 41 0 29080 0
vsize: 116484
[startup+860.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27521 0 0 0 85924 83 0 0 25 0 1 0 480996665 120082432 26843 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29317 26843 603 41 0 29276 0
vsize: 117268
[startup+870.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27700 0 0 0 86924 83 0 0 25 0 1 0 480996665 120750080 27022 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29480 27022 603 41 0 29439 0
vsize: 117920
[startup+880.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 27884 0 0 0 87924 84 0 0 25 0 1 0 480996665 121544704 27206 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29674 27206 603 41 0 29633 0
vsize: 118696
[startup+890.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28028 0 0 0 88923 84 0 0 25 0 1 0 480996665 122081280 27350 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29805 27350 603 41 0 29764 0
vsize: 119220
[startup+900.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28215 0 0 0 89923 85 0 0 25 0 1 0 480996665 122884096 27537 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30001 27537 603 41 0 29960 0
vsize: 120004
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28371 0 0 0 90923 85 0 0 25 0 1 0 480996665 123551744 27693 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30164 27693 603 41 0 30123 0
vsize: 120656
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28561 0 0 0 91923 85 0 0 25 0 1 0 480996665 124346368 27883 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30358 27883 603 41 0 30317 0
vsize: 121432
[startup+930.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28729 0 0 0 92922 86 0 0 25 0 1 0 480996665 125014016 28051 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30521 28051 603 41 0 30480 0
vsize: 122084
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 28928 0 0 0 93922 87 0 0 25 0 1 0 480996665 125812736 28250 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30716 28250 603 41 0 30675 0
vsize: 122864
[startup+950.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29086 0 0 0 94922 87 0 0 25 0 1 0 480996665 126488576 28408 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30881 28408 603 41 0 30840 0
vsize: 123524
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29212 0 0 0 95922 87 0 0 25 0 1 0 480996665 127025152 28534 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31012 28534 603 41 0 30971 0
vsize: 124048
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29344 0 0 0 96921 88 0 0 25 0 1 0 480996665 127561728 28666 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31143 28666 603 41 0 31102 0
vsize: 124572
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28755
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29478 0 0 0 97921 89 0 0 25 0 1 0 480996665 128102400 28800 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31275 28800 603 41 0 31234 0
vsize: 125100
[startup+990.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29640 0 0 0 98920 90 0 0 25 0 1 0 480996665 128761856 28962 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31436 28962 603 41 0 31395 0
vsize: 125744
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29789 0 0 0 99920 90 0 0 25 0 1 0 480996665 129294336 29111 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31566 29111 603 41 0 31525 0
vsize: 126264
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 29951 0 0 0 100919 91 0 0 25 0 1 0 480996665 129966080 29273 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31730 29273 603 41 0 31689 0
vsize: 126920
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30102 0 0 0 101919 91 0 0 25 0 1 0 480996665 130617344 29424 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31889 29424 603 41 0 31848 0
vsize: 127556
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30275 0 0 0 102919 92 0 0 25 0 1 0 480996665 131289088 29597 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32053 29597 603 41 0 32012 0
vsize: 128212
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30461 0 0 0 103919 92 0 0 25 0 1 0 480996665 132079616 29783 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32246 29783 603 41 0 32205 0
vsize: 128984
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30516 0 0 0 104918 92 0 0 25 0 1 0 480996665 132349952 29838 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32312 29838 603 41 0 32271 0
vsize: 129248
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30627 0 0 0 105918 93 0 0 25 0 1 0 480996665 132755456 29949 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32411 29949 603 41 0 32370 0
vsize: 129644
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 30964 0 0 0 106918 94 0 0 25 0 1 0 480996665 134135808 30286 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32748 30286 603 41 0 32707 0
vsize: 130992
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 31324 0 0 0 107917 95 0 0 25 0 1 0 480996665 135659520 30646 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33120 30646 603 41 0 33079 0
vsize: 132480
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 31654 0 0 0 108916 95 0 0 25 0 1 0 480996665 136884224 30976 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33419 30976 603 41 0 33378 0
vsize: 133676
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 32000 0 0 0 109916 96 0 0 25 0 1 0 480996665 138383360 31322 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33785 31322 603 41 0 33744 0
vsize: 135140
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 32387 0 0 0 110916 97 0 0 25 0 1 0 480996665 139894784 31709 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34154 31709 603 41 0 34113 0
vsize: 136616
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 32806 0 0 0 111915 97 0 0 25 0 1 0 480996665 141668352 32128 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34587 32128 603 41 0 34546 0
vsize: 138348
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 33136 0 0 0 112914 99 0 0 25 0 1 0 480996665 143040512 32458 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34922 32458 603 41 0 34881 0
vsize: 139688
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 33530 0 0 0 113913 100 0 0 25 0 1 0 480996665 144674816 32852 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35321 32852 603 41 0 35280 0
vsize: 141284
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 33839 0 0 0 114912 101 0 0 25 0 1 0 480996665 145903616 33161 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35621 33161 603 41 0 35580 0
vsize: 142484
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 34206 0 0 0 115912 101 0 0 25 0 1 0 480996665 147390464 33528 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35984 33528 603 41 0 35943 0
vsize: 143936
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 34478 0 0 0 116911 102 0 0 25 0 1 0 480996665 148488192 33800 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36252 33800 603 41 0 36211 0
vsize: 145008
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 34496 0 0 0 117911 102 0 0 25 0 1 0 480996665 148488192 33818 4294967295 134512640 134672761 3221224560 3221223760 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36252 33818 603 41 0 36211 0
vsize: 145008
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 34529 0 0 0 118911 102 0 0 25 0 1 0 480996665 148623360 33851 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36285 33851 603 41 0 36244 0
vsize: 145140
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28757
Raw data (stat): 28749 (minisat+) R 28748 20024 20023 0 -1 0 34695 0 0 0 119911 103 0 0 25 0 1 0 480996665 149282816 34017 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36446 34017 603 41 0 36405 0
vsize: 145784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 28757
Raw data (stat): 28749 (minisat+) Z 28748 20024 20023 0 -1 12 34698 0 0 0 119911 109 0 0 25 0 1 0 480996665 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.13
CPU time (s): 1200.21
CPU user time (s): 1199.12
CPU system time (s): 1.09583
CPU usage (%): 100.007
Max. virtual memory (Kb): 145784
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####