PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01584
Number of variables	319
Total number of constraints	325
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	319
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	231
Trace number 22151

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-22 02:20:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12037 boxname=wulflinc3 idbench=926 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fbdb3cf321a85412feefcaac30780520  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 12037
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        488044 kB
Buffers:         34648 kB
Cached:         489428 kB
SwapCached:          0 kB
Active:          56856 kB
Inactive:       470052 kB
HighTotal:      131008 kB
HighFree:        23744 kB
LowTotal:       903652 kB
LowFree:        464300 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13952 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:40:12 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 12037 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss
c ---[   8]---> BDD-cost:777098
c ---[   5]---> BDD-cost: 5719
c ---[   4]---> BDD-cost:24274
c ---[   2]---> BDD-cost:  478
c ---[   1]---> BDD-cost: 2553
c ---[   0]---> BDD-cost: 7307
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2386590  7171332 |  795530       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61665     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2537120  7522847 |  845706       0        0     nan |  0.000 % |
c |       103 | 2537120  7522847 |  930276     103     2421    23.5 |  0.001 % |
c |       254 | 2537120  7522847 | 1023304     254    12318    48.5 |  0.001 % |
c |       479 | 2537120  7522847 | 1125634     479    14776    30.8 |  0.001 % |
c |       816 | 2537120  7522847 | 1238198     816    25056    30.7 |  0.001 % |
c |      1323 | 2537120  7522847 | 1362017    1323    33177    25.1 |  0.001 % |
c |      2082 | 2537120  7522847 | 1498219    2082    68922    33.1 |  0.001 % |
c |      3221 | 2536930  7522420 | 1648041    3118    83012    26.6 |  0.007 % |
c |      4930 | 2536930  7522420 | 1812845    4827   117257    24.3 |  0.007 % |
c |      7492 | 2536930  7522420 | 1994130    7389   151151    20.5 |  0.007 % |
c |     11337 | 2536930  7522420 | 2193543   11234   199352    17.7 |  0.007 % |
c |     17103 | 2536930  7522420 | 2412897   17000   291674    17.2 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2359[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19729 | 2537972  7525048 |  845990   19626   321546    16.4 |  0.007 % |
c |     19829 | 2537972  7525048 |  930589   19726   322143    16.3 |  0.007 % |
c |     19979 | 2537972  7525048 | 1023647   19876   323106    16.3 |  0.007 % |
c |     20207 | 2537972  7525048 | 1126012   20104   327986    16.3 |  0.007 % |
c |     20544 | 2537972  7525048 | 1238613   20441   336109    16.4 |  0.007 % |
c |     21050 | 2537972  7525048 | 1362475   20947   347397    16.6 |  0.007 % |
c |     21812 | 2537972  7525048 | 1498722   21709   369904    17.0 |  0.007 % |
c |     22952 | 2537972  7525048 | 1648595   22849   409663    17.9 |  0.007 % |
c |     24661 | 2537972  7525048 | 1813454   24558   456229    18.6 |  0.007 % |
c |     27223 | 2537972  7525048 | 1994800   27120   543521    20.0 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28130 | 2537982  7525075 |  845994   28027   571748    20.4 |  0.007 % |
c ==============================================================================
c [1mFound solution: 2268[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28200 | 2538600  7526620 |  846200   28097   576554    20.5 |  0.007 % |
c |     28300 | 2538600  7526620 |  930820   28197   577583    20.5 |  0.007 % |
c |     28452 | 2538600  7526620 | 1023902   28349   580020    20.5 |  0.007 % |
c |     28678 | 2538600  7526620 | 1126292   28575   583723    20.4 |  0.007 % |
c |     29015 | 2538600  7526620 | 1238921   28912   589799    20.4 |  0.007 % |
c ==============================================================================
c [1mFound solution: 1774[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29389 | 2538666  7526861 |  846222   29286   596861    20.4 |  0.007 % |
c |     29490 | 2538666  7526861 |  930844   29387   597305    20.3 |  0.008 % |
c |     29640 | 2538666  7526861 | 1023928   29537   601370    20.4 |  0.008 % |
c |     29866 | 2538666  7526861 | 1126321   29763   605027    20.3 |  0.008 % |
c |     30203 | 2538666  7526861 | 1238953   30100   609517    20.2 |  0.008 % |
c |     30710 | 2538666  7526861 | 1362848   30607   620907    20.3 |  0.008 % |
c |     31470 | 2538646  7526816 | 1499133   31360   634128    20.2 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31804 | 2538658  7526847 |  846219   31694   644703    20.3 |  0.008 % |
c |     31904 | 2538658  7526847 |  930840   31794   653680    20.6 |  0.008 % |
c |     32054 | 2538658  7526847 | 1023924   31944   655505    20.5 |  0.008 % |
c |     32279 | 2538658  7526847 | 1126317   32169   657038    20.4 |  0.008 % |
c |     32616 | 2538658  7526847 | 1238949   32506   660050    20.3 |  0.008 % |
c |     33124 | 2538658  7526847 | 1362844   33014   665670    20.2 |  0.008 % |
c |     33883 | 2538658  7526847 | 1499128   33773   682971    20.2 |  0.008 % |
c |     35022 | 2538658  7526847 | 1649041   34912   697748    20.0 |  0.008 % |
c |     36730 | 2538658  7526847 | 1813945   36620   727400    19.9 |  0.008 % |
c |     39292 | 2538658  7526847 | 1995340   39182   812482    20.7 |  0.008 % |
c |     43136 | 2538658  7526847 | 2194874   43026   977964    22.7 |  0.008 % |
c ==============================================================================
c [1mFound solution: 1519[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43236 | 2538693  7526935 |  846231   43126   979511    22.7 |  0.008 % |
c |     43336 | 2538693  7526935 |  930854   43226   986637    22.8 |  0.008 % |
c ==============================================================================
c [1mFound solution: 936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43345 | 2538740  7527044 |  846246   43235   987190    22.8 |  0.008 % |
c |     43445 | 2538740  7527044 |  930870   43335   994189    22.9 |  0.008 % |
c |     43595 | 2538740  7527044 | 1023957   43485   998827    23.0 |  0.008 % |
c ==============================================================================
c [1mFound solution: 814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43628 | 2538769  7527114 |  846256   43518   999616    23.0 |  0.008 % |
c ==============================================================================
c [1mFound solution: 804[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43685 | 2538780  7527143 |  846260   43575  1001178    23.0 |  0.008 % |
c |     43785 | 2538780  7527143 |  930886   43675  1028207    23.5 |  0.009 % |
c |     43935 | 2538780  7527143 | 1023974   43825  1030963    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 739[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43968 | 2538786  7527159 |  846262   43858  1031377    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 674[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43980 | 2538805  7527207 |  846268   43870  1031641    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43987 | 2538810  7527222 |  846270   43877  1031873    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 649[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44003 | 2538817  7527238 |  846272   43893  1032613    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 496[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44021 | 2538840  7527293 |  846280   43911  1033912    23.5 |  0.009 % |
c ==============================================================================
c [1mFound solution: 489[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44023 | 2538846  7527307 |  846282   43913  1034858    23.6 |  0.009 % |
c |     44124 | 2538846  7527307 |  930910   44014  1046891    23.8 |  0.009 % |
c |     44274 | 2538846  7527307 | 1024001   44164  1052996    23.8 |  0.009 % |
c |     44503 | 2538846  7527307 | 1126401   44393  1105198    24.9 |  0.009 % |
c |     44841 | 2538846  7527307 | 1239041   44731  1207157    27.0 |  0.009 % |
c |     45349 | 2538846  7527307 | 1362945   45239  1241301    27.4 |  0.009 % |
c |     46108 | 2538846  7527307 | 1499240   45998  1292536    28.1 |  0.009 % |
c |     47248 | 2538846  7527307 | 1649164   47138  1354106    28.7 |  0.009 % |
c |     48956 | 2538846  7527307 | 1814080   48846  1777892    36.4 |  0.009 % |
c |     51519 | 2538846  7527307 | 1995488   51409  1945080    37.8 |  0.009 % |
c |     55363 | 2538693  7526960 | 2195037   55100  2139380    38.8 |  0.014 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 -C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 -C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 -C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 -C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 C112_0x2e__bit0 C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 -C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 -C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 C189_0x2e__bit0 C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 -C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 -C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 -C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -C2#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 25490
Raw data (stat): 25490 (runsolver) R 25489 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491846123 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 9087 0 0 0 978 20 0 0 25 0 1 0 491846123 27783168 6343 4294967295 134512640 134672761 3221224544 3221207200 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6783 6343 603 41 0 6742 0
vsize: 27132
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 11893 0 0 0 1974 25 0 0 25 0 1 0 491846123 39874560 8984 4294967295 134512640 134672761 3221224544 3221214112 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9735 8984 603 41 0 9694 0
vsize: 38940
[startup+30.0003 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 20413 0 0 0 2956 42 0 0 25 0 1 0 491846123 63815680 14537 4294967295 134512640 134672761 3221224544 3221210412 134594032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15580 14537 603 41 0 15539 0
vsize: 62320
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 24673 0 0 0 3949 50 0 0 25 0 1 0 491846123 82268160 18138 4294967295 134512640 134672761 3221224544 3221214248 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20085 18138 603 41 0 20044 0
vsize: 80340
[startup+50.001 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 30624 0 0 0 4938 61 0 0 25 0 1 0 491846123 98213888 22771 4294967295 134512640 134672761 3221224544 3221204416 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23978 22771 603 41 0 23937 0
vsize: 95912
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 33746 0 0 0 5931 69 0 0 25 0 1 0 491846123 82284544 18971 4294967295 134512640 134672761 3221224544 3221205280 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20089 18971 603 41 0 20048 0
vsize: 80356
[startup+70.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 77531 0 0 0 6829 170 0 0 25 0 1 0 491846123 284397568 60778 4294967295 134512640 134672761 3221224544 3221157376 1075349701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69433 60778 603 41 0 69392 0
vsize: 277732
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93178 0 0 0 7791 207 0 0 25 0 1 0 491846123 346783744 76425 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84664 76425 603 41 0 84623 0
vsize: 338656
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93286 0 0 0 8791 208 0 0 25 0 1 0 491846123 347324416 76533 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84796 76533 603 41 0 84755 0
vsize: 339184
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93372 0 0 0 9791 208 0 0 25 0 1 0 491846123 347594752 76619 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84862 76619 603 41 0 84821 0
vsize: 339448
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93488 0 0 0 10790 209 0 0 25 0 1 0 491846123 348135424 76735 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84994 76735 603 41 0 84953 0
vsize: 339976
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93590 0 0 0 11790 209 0 0 25 0 1 0 491846123 348635136 76837 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85116 76837 603 41 0 85075 0
vsize: 340464
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93773 0 0 0 12790 209 0 0 25 0 1 0 491846123 351993856 77020 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85936 77020 603 41 0 85895 0
vsize: 343744
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93775 0 0 0 13790 209 0 0 25 0 1 0 491846123 352129024 77022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85969 77022 603 41 0 85928 0
vsize: 343876
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93799 0 0 0 14790 209 0 0 25 0 1 0 491846123 352129024 77046 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85969 77046 603 41 0 85928 0
vsize: 343876
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93849 0 0 0 15790 209 0 0 25 0 1 0 491846123 352395264 77096 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86034 77096 603 41 0 85993 0
vsize: 344136
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93878 0 0 0 16790 210 0 0 25 0 1 0 491846123 352526336 77125 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86066 77125 603 41 0 86025 0
vsize: 344264
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93899 0 0 0 17790 210 0 0 25 0 1 0 491846123 352526336 77146 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86066 77146 603 41 0 86025 0
vsize: 344264
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93926 0 0 0 18790 210 0 0 25 0 1 0 491846123 352657408 77173 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86098 77173 603 41 0 86057 0
vsize: 344392
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93941 0 0 0 19790 210 0 0 25 0 1 0 491846123 352788480 77188 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86130 77188 603 41 0 86089 0
vsize: 344520
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 93980 0 0 0 20790 210 0 0 25 0 1 0 491846123 352919552 77227 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86162 77227 603 41 0 86121 0
vsize: 344648
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94018 0 0 0 21789 211 0 0 25 0 1 0 491846123 353054720 77265 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86195 77265 603 41 0 86154 0
vsize: 344780
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94059 0 0 0 22788 211 0 0 25 0 1 0 491846123 353189888 77306 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86228 77306 603 41 0 86187 0
vsize: 344912
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94092 0 0 0 23788 211 0 0 25 0 1 0 491846123 353325056 77339 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86261 77339 603 41 0 86220 0
vsize: 345044
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94108 0 0 0 24787 211 0 0 25 0 1 0 491846123 353402880 77355 4294967295 134512640 134672761 3221224544 3221223712 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86280 77355 603 41 0 86239 0
vsize: 345120
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94150 0 0 0 25787 211 0 0 25 0 1 0 491846123 353538048 77397 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86313 77397 603 41 0 86272 0
vsize: 345252
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94198 0 0 0 26787 211 0 0 25 0 1 0 491846123 353669120 77445 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86345 77445 603 41 0 86304 0
vsize: 345380
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94227 0 0 0 27787 211 0 0 25 0 1 0 491846123 353804288 77474 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86378 77474 603 41 0 86337 0
vsize: 345512
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94301 0 0 0 28788 212 0 0 25 0 1 0 491846123 354287616 77548 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86496 77548 603 41 0 86455 0
vsize: 345984
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94358 0 0 0 29788 212 0 0 25 0 1 0 491846123 354422784 77605 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86529 77605 603 41 0 86488 0
vsize: 346116
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94402 0 0 0 30787 212 0 0 25 0 1 0 491846123 354693120 77649 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86595 77649 603 41 0 86554 0
vsize: 346380
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94482 0 0 0 31787 212 0 0 25 0 1 0 491846123 354963456 77729 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86661 77729 603 41 0 86620 0
vsize: 346644
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94559 0 0 0 32787 213 0 0 25 0 1 0 491846123 355229696 77806 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86726 77806 603 41 0 86685 0
vsize: 346904
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94640 0 0 0 33787 213 0 0 25 0 1 0 491846123 355635200 77887 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86825 77887 603 41 0 86784 0
vsize: 347300
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94655 0 0 0 34787 213 0 0 25 0 1 0 491846123 355635200 77902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86825 77902 603 41 0 86784 0
vsize: 347300
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94655 0 0 0 35787 213 0 0 25 0 1 0 491846123 355635200 77902 4294967295 134512640 134672761 3221224544 3221223692 1074733103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86825 77902 603 41 0 86784 0
vsize: 347300
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94666 0 0 0 36787 213 0 0 25 0 1 0 491846123 355717120 77913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86845 77913 603 41 0 86804 0
vsize: 347380
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94682 0 0 0 37787 213 0 0 25 0 1 0 491846123 355717120 77929 4294967295 134512640 134672761 3221224544 3221223844 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86845 77929 603 41 0 86804 0
vsize: 347380
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94702 0 0 0 38788 213 0 0 25 0 1 0 491846123 355790848 77949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86863 77949 603 41 0 86822 0
vsize: 347452
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94719 0 0 0 39788 213 0 0 25 0 1 0 491846123 355921920 77966 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77966 603 41 0 86854 0
vsize: 347580
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94723 0 0 0 40788 213 0 0 25 0 1 0 491846123 355921920 77970 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77970 603 41 0 86854 0
vsize: 347580
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94731 0 0 0 41788 213 0 0 25 0 1 0 491846123 355921920 77978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77978 603 41 0 86854 0
vsize: 347580
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94753 0 0 0 42788 213 0 0 25 0 1 0 491846123 356057088 78000 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86928 78000 603 41 0 86887 0
vsize: 347712
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94763 0 0 0 43788 213 0 0 25 0 1 0 491846123 356057088 78010 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86928 78010 603 41 0 86887 0
vsize: 347712
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94782 0 0 0 44789 213 0 0 25 0 1 0 491846123 356184064 78029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86959 78029 603 41 0 86918 0
vsize: 347836
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94805 0 0 0 45789 213 0 0 25 0 1 0 491846123 356319232 78052 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86992 78052 603 41 0 86951 0
vsize: 347968
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94890 0 0 0 46789 214 0 0 25 0 1 0 491846123 356585472 78137 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87057 78137 603 41 0 87016 0
vsize: 348228
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94900 0 0 0 47789 214 0 0 25 0 1 0 491846123 356712448 78147 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78147 603 41 0 87047 0
vsize: 348352
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94906 0 0 0 48789 214 0 0 25 0 1 0 491846123 356712448 78153 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78153 603 41 0 87047 0
vsize: 348352
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94916 0 0 0 49789 214 0 0 25 0 1 0 491846123 356712448 78163 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78163 603 41 0 87047 0
vsize: 348352
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94925 0 0 0 50789 214 0 0 25 0 1 0 491846123 356712448 78172 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78172 603 41 0 87047 0
vsize: 348352
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94933 0 0 0 51790 214 0 0 25 0 1 0 491846123 356843520 78180 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87120 78180 603 41 0 87079 0
vsize: 348480
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94952 0 0 0 52790 214 0 0 25 0 1 0 491846123 356843520 78199 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87120 78199 603 41 0 87079 0
vsize: 348480
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94974 0 0 0 53790 214 0 0 25 0 1 0 491846123 356974592 78221 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78221 603 41 0 87111 0
vsize: 348608
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 94984 0 0 0 54790 214 0 0 25 0 1 0 491846123 356974592 78231 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78231 603 41 0 87111 0
vsize: 348608
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95000 0 0 0 55790 214 0 0 25 0 1 0 491846123 357109760 78247 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87185 78247 603 41 0 87144 0
vsize: 348740
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95018 0 0 0 56790 214 0 0 25 0 1 0 491846123 357109760 78265 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87185 78265 603 41 0 87144 0
vsize: 348740
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95048 0 0 0 57791 214 0 0 25 0 1 0 491846123 357244928 78295 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87218 78295 603 41 0 87177 0
vsize: 348872
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95071 0 0 0 58791 214 0 0 25 0 1 0 491846123 357380096 78318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78318 603 41 0 87210 0
vsize: 349004
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95086 0 0 0 59791 214 0 0 25 0 1 0 491846123 357380096 78333 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78333 603 41 0 87210 0
vsize: 349004
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95111 0 0 0 60791 214 0 0 25 0 1 0 491846123 357519360 78358 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87285 78358 603 41 0 87244 0
vsize: 349140
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95124 0 0 0 61791 214 0 0 25 0 1 0 491846123 357519360 78371 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87285 78371 603 41 0 87244 0
vsize: 349140
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95135 0 0 0 62791 214 0 0 25 0 1 0 491846123 357654528 78382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78382 603 41 0 87277 0
vsize: 349272
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95142 0 0 0 63791 214 0 0 25 0 1 0 491846123 357654528 78389 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78389 603 41 0 87277 0
vsize: 349272
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95154 0 0 0 64791 214 0 0 25 0 1 0 491846123 357654528 78401 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78401 603 41 0 87277 0
vsize: 349272
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95172 0 0 0 65791 215 0 0 25 0 1 0 491846123 357785600 78419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87350 78419 603 41 0 87309 0
vsize: 349400
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95207 0 0 0 66792 215 0 0 25 0 1 0 491846123 357912576 78454 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87381 78454 603 41 0 87340 0
vsize: 349524
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95241 0 0 0 67792 215 0 0 25 0 1 0 491846123 358047744 78488 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87414 78488 603 41 0 87373 0
vsize: 349656
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95252 0 0 0 68792 215 0 0 25 0 1 0 491846123 358047744 78499 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87414 78499 603 41 0 87373 0
vsize: 349656
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95265 0 0 0 69792 215 0 0 25 0 1 0 491846123 358182912 78512 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87447 78512 603 41 0 87406 0
vsize: 349788
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95278 0 0 0 70792 215 0 0 25 0 1 0 491846123 358182912 78525 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87447 78525 603 41 0 87406 0
vsize: 349788
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95299 0 0 0 71792 215 0 0 25 0 1 0 491846123 358313984 78546 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87479 78546 603 41 0 87438 0
vsize: 349916
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95306 0 0 0 72792 215 0 0 25 0 1 0 491846123 358313984 78553 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87479 78553 603 41 0 87438 0
vsize: 349916
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95325 0 0 0 73793 215 0 0 25 0 1 0 491846123 358313984 78572 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87479 78572 603 41 0 87438 0
vsize: 349916
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95386 0 0 0 74793 215 0 0 25 0 1 0 491846123 358592512 78633 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87547 78633 603 41 0 87506 0
vsize: 350188
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95417 0 0 0 75793 215 0 0 25 0 1 0 491846123 358727680 78664 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87580 78664 603 41 0 87539 0
vsize: 350320
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95460 0 0 0 76793 216 0 0 25 0 1 0 491846123 358989824 78707 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87644 78707 603 41 0 87603 0
vsize: 350576
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95496 0 0 0 77793 216 0 0 25 0 1 0 491846123 359124992 78743 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87677 78743 603 41 0 87636 0
vsize: 350708
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95519 0 0 0 78792 216 0 0 25 0 1 0 491846123 359124992 78766 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87677 78766 603 41 0 87636 0
vsize: 350708
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95561 0 0 0 79792 216 0 0 25 0 1 0 491846123 359391232 78808 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87742 78808 603 41 0 87701 0
vsize: 350968
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95607 0 0 0 80792 216 0 0 25 0 1 0 491846123 359526400 78854 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87775 78854 603 41 0 87734 0
vsize: 351100
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95672 0 0 0 81792 216 0 0 25 0 1 0 491846123 359784448 78919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87838 78919 603 41 0 87797 0
vsize: 351352
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95711 0 0 0 82792 216 0 0 25 0 1 0 491846123 359915520 78958 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87870 78958 603 41 0 87829 0
vsize: 351480
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95760 0 0 0 83792 216 0 0 25 0 1 0 491846123 360181760 79007 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87935 79007 603 41 0 87894 0
vsize: 351740
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95825 0 0 0 84792 216 0 0 25 0 1 0 491846123 360452096 79072 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88001 79072 603 41 0 87960 0
vsize: 352004
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95893 0 0 0 85792 217 0 0 25 0 1 0 491846123 360718336 79140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88066 79140 603 41 0 88025 0
vsize: 352264
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95916 0 0 0 86792 217 0 0 25 0 1 0 491846123 360718336 79163 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88066 79163 603 41 0 88025 0
vsize: 352264
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95930 0 0 0 87792 217 0 0 25 0 1 0 491846123 360849408 79177 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88098 79177 603 41 0 88057 0
vsize: 352392
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95949 0 0 0 88793 217 0 0 25 0 1 0 491846123 360849408 79196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88098 79196 603 41 0 88057 0
vsize: 352392
[startup+900.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95955 0 0 0 89793 217 0 0 25 0 1 0 491846123 360984576 79202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79202 603 41 0 88090 0
vsize: 352524
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95964 0 0 0 90793 217 0 0 25 0 1 0 491846123 360984576 79211 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79211 603 41 0 88090 0
vsize: 352524
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95966 0 0 0 91793 217 0 0 25 0 1 0 491846123 360984576 79213 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79213 603 41 0 88090 0
vsize: 352524
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95972 0 0 0 92793 217 0 0 25 0 1 0 491846123 360984576 79219 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79219 603 41 0 88090 0
vsize: 352524
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95982 0 0 0 93794 217 0 0 25 0 1 0 491846123 360984576 79229 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79229 603 41 0 88090 0
vsize: 352524
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95992 0 0 0 94794 217 0 0 25 0 1 0 491846123 361119744 79239 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88164 79239 603 41 0 88123 0
vsize: 352656
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 95997 0 0 0 95794 217 0 0 25 0 1 0 491846123 361119744 79244 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88164 79244 603 41 0 88123 0
vsize: 352656
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96007 0 0 0 96794 217 0 0 25 0 1 0 491846123 361119744 79254 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88164 79254 603 41 0 88123 0
vsize: 352656
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96016 0 0 0 97794 217 0 0 25 0 1 0 491846123 361119744 79263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88164 79263 603 41 0 88123 0
vsize: 352656
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96027 0 0 0 98794 217 0 0 25 0 1 0 491846123 361254912 79274 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88197 79274 603 41 0 88156 0
vsize: 352788
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96036 0 0 0 99795 217 0 0 25 0 1 0 491846123 361254912 79283 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88197 79283 603 41 0 88156 0
vsize: 352788
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96048 0 0 0 100795 217 0 0 25 0 1 0 491846123 361254912 79295 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88197 79295 603 41 0 88156 0
vsize: 352788
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96058 0 0 0 101795 217 0 0 25 0 1 0 491846123 361390080 79305 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88230 79305 603 41 0 88189 0
vsize: 352920
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96063 0 0 0 102795 217 0 0 25 0 1 0 491846123 361390080 79310 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88230 79310 603 41 0 88189 0
vsize: 352920
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96079 0 0 0 103794 218 0 0 25 0 1 0 491846123 361390080 79326 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79326 603 41 0 88189 0
vsize: 352920
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96103 0 0 0 104794 218 0 0 25 0 1 0 491846123 361521152 79350 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88262 79350 603 41 0 88221 0
vsize: 353048
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96123 0 0 0 105794 218 0 0 25 0 1 0 491846123 361521152 79370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88262 79370 603 41 0 88221 0
vsize: 353048
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96136 0 0 0 106794 218 0 0 25 0 1 0 491846123 361656320 79383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88295 79383 603 41 0 88254 0
vsize: 353180
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96153 0 0 0 107795 218 0 0 25 0 1 0 491846123 361656320 79400 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88295 79400 603 41 0 88254 0
vsize: 353180
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96171 0 0 0 108795 218 0 0 25 0 1 0 491846123 361791488 79418 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88328 79418 603 41 0 88287 0
vsize: 353312
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96185 0 0 0 109795 218 0 0 25 0 1 0 491846123 361791488 79432 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88328 79432 603 41 0 88287 0
vsize: 353312
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96206 0 0 0 110795 218 0 0 25 0 1 0 491846123 361926656 79453 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88361 79453 603 41 0 88320 0
vsize: 353444
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96222 0 0 0 111795 218 0 0 25 0 1 0 491846123 362061824 79469 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79469 603 41 0 88353 0
vsize: 353576
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96232 0 0 0 112795 218 0 0 25 0 1 0 491846123 362061824 79479 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79479 603 41 0 88353 0
vsize: 353576
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96245 0 0 0 113796 218 0 0 25 0 1 0 491846123 362061824 79492 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79492 603 41 0 88353 0
vsize: 353576
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96256 0 0 0 114796 218 0 0 25 0 1 0 491846123 362196992 79503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88427 79503 603 41 0 88386 0
vsize: 353708
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96268 0 0 0 115796 218 0 0 25 0 1 0 491846123 362196992 79515 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88427 79515 603 41 0 88386 0
vsize: 353708
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96280 0 0 0 116796 218 0 0 25 0 1 0 491846123 362196992 79527 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88427 79527 603 41 0 88386 0
vsize: 353708
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96289 0 0 0 117796 218 0 0 25 0 1 0 491846123 362332160 79536 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88460 79536 603 41 0 88419 0
vsize: 353840
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96300 0 0 0 118797 218 0 0 25 0 1 0 491846123 362332160 79547 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88460 79547 603 41 0 88419 0
vsize: 353840
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25490
Raw data (stat): 25490 (minisat+) R 25489 10720 10719 0 -1 0 96311 0 0 0 119797 218 0 0 25 0 1 0 491846123 362332160 79558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88460 79558 603 41 0 88419 0
vsize: 353840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25490
Raw data (stat): 25490 (minisat+) Z 25489 10720 10719 0 -1 12 96314 0 0 0 119797 234 0 0 25 0 1 0 491846123 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.2
CPU time (s): 1200.32
CPU user time (s): 1197.97
CPU system time (s): 2.34464
CPU usage (%): 100.01
Max. virtual memory (Kb): 353840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####