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/miplib3/normalized-mps-v2-20-10-mod008.opb
MD5SUM	581d778a36086562107993896110e0a2
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.01784
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 16331

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 06:59:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13636 boxname=wulflinc27 idbench=1049 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod008.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod008.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-mod008.opb
IDLAUNCH: 13636
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        779488 kB
Buffers:         27436 kB
Cached:         199216 kB
SwapCached:        604 kB
Active:          43144 kB
Inactive:       185556 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        779236 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5236 kB
Slab:            20816 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:19:30 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 13636 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 13697
Raw data (stat): 13697 (runsolver) R 13696 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543104096 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 13697
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 9138 0 0 0 980 18 0 0 25 0 1 0 543104096 28053504 6394 4294967295 134512640 134672761 3221224528 3221207280 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6394 603 41 0 6808 0
vsize: 27396
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 13697
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 11945 0 0 0 1975 23 0 0 25 0 1 0 543104096 40009728 9036 4294967295 134512640 134672761 3221224528 3221208424 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9768 9036 603 41 0 9727 0
vsize: 39072
[startup+30.0019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13697
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 20444 0 0 0 2957 41 0 0 25 0 1 0 543104096 63815680 14568 4294967295 134512640 134672761 3221224528 3221207184 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15580 14568 603 41 0 15539 0
vsize: 62320
[startup+40.0018 s]
Raw data (loadavg): 1.15 0.99 0.92 2/57 13736
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 24660 0 0 0 3948 49 0 0 25 0 1 0 543104096 82132992 18125 4294967295 134512640 134672761 3221224528 3221215248 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20052 18125 603 41 0 20011 0
vsize: 80208
[startup+50.0268 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 30555 0 0 0 4940 61 0 0 25 0 1 0 543104096 97943552 22702 4294967295 134512640 134672761 3221224528 3221207280 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23912 22702 603 41 0 23871 0
vsize: 95648
[startup+60.0274 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 33744 0 0 0 5932 69 0 0 25 0 1 0 543104096 82284544 18969 4294967295 134512640 134672761 3221224528 3221206992 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20089 18969 603 41 0 20048 0
vsize: 80356
[startup+70.0275 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 75019 0 0 0 6840 161 0 0 25 0 1 0 543104096 276824064 58266 4294967295 134512640 134672761 3221224528 3221207136 134556762 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67584 58267 603 41 0 67543 0
vsize: 270336
[startup+80.0286 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93170 0 0 0 7800 201 0 0 25 0 1 0 543104096 346783744 76417 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84664 76417 603 41 0 84623 0
vsize: 338656
[startup+90.0289 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93286 0 0 0 8800 201 0 0 25 0 1 0 543104096 347324416 76533 4294967295 134512640 134672761 3221224528 3221223724 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84796 76533 603 41 0 84755 0
vsize: 339184
[startup+100.029 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 13750
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93368 0 0 0 9799 201 0 0 25 0 1 0 543104096 347594752 76615 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84862 76615 603 41 0 84821 0
vsize: 339448
[startup+110.03 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93487 0 0 0 10799 202 0 0 25 0 1 0 543104096 348135424 76734 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84994 76734 603 41 0 84953 0
vsize: 339976
[startup+120.029 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93572 0 0 0 11798 202 0 0 25 0 1 0 543104096 348405760 76819 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85060 76819 603 41 0 85019 0
vsize: 340240
[startup+130.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93767 0 0 0 12798 203 0 0 25 0 1 0 543104096 351993856 77014 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85936 77014 603 41 0 85895 0
vsize: 343744
[startup+140.03 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93775 0 0 0 13799 203 0 0 25 0 1 0 543104096 352129024 77022 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85969 77022 603 41 0 85928 0
vsize: 343876
[startup+150.03 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93790 0 0 0 14799 203 0 0 25 0 1 0 543104096 352129024 77037 4294967295 134512640 134672761 3221224528 3221223652 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85969 77037 603 41 0 85928 0
vsize: 343876
[startup+160.031 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93843 0 0 0 15799 203 0 0 25 0 1 0 543104096 352395264 77090 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86034 77090 603 41 0 85993 0
vsize: 344136
[startup+170.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93877 0 0 0 16799 203 0 0 25 0 1 0 543104096 352526336 77124 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86066 77124 603 41 0 86025 0
vsize: 344264
[startup+180.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93896 0 0 0 17798 203 0 0 25 0 1 0 543104096 352526336 77143 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86066 77143 603 41 0 86025 0
vsize: 344264
[startup+190.032 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93919 0 0 0 18798 203 0 0 25 0 1 0 543104096 352657408 77166 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86098 77166 603 41 0 86057 0
vsize: 344392
[startup+200.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93940 0 0 0 19797 203 0 0 25 0 1 0 543104096 352788480 77187 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86130 77187 603 41 0 86089 0
vsize: 344520
[startup+210.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 93975 0 0 0 20797 204 0 0 25 0 1 0 543104096 352919552 77222 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86162 77222 603 41 0 86121 0
vsize: 344648
[startup+220.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94011 0 0 0 21796 204 0 0 25 0 1 0 543104096 353054720 77258 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86195 77258 603 41 0 86154 0
vsize: 344780
[startup+230.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94053 0 0 0 22796 205 0 0 25 0 1 0 543104096 353189888 77300 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86228 77300 603 41 0 86187 0
vsize: 344912
[startup+240.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94090 0 0 0 23796 205 0 0 25 0 1 0 543104096 353325056 77337 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86261 77337 603 41 0 86220 0
vsize: 345044
[startup+250.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94107 0 0 0 24795 206 0 0 25 0 1 0 543104096 353402880 77354 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86280 77354 603 41 0 86239 0
vsize: 345120
[startup+260.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94140 0 0 0 25795 206 0 0 25 0 1 0 543104096 353538048 77387 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86313 77387 603 41 0 86272 0
vsize: 345252
[startup+270.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94194 0 0 0 26794 207 0 0 25 0 1 0 543104096 353669120 77441 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86345 77441 603 41 0 86304 0
vsize: 345380
[startup+280.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94227 0 0 0 27794 207 0 0 25 0 1 0 543104096 353804288 77474 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94293 0 0 0 28794 207 0 0 25 0 1 0 543104096 354152448 77540 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86463 77540 603 41 0 86422 0
vsize: 345852
[startup+300.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94356 0 0 0 29793 208 0 0 25 0 1 0 543104096 354422784 77603 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86529 77603 603 41 0 86488 0
vsize: 346116
[startup+310.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94402 0 0 0 30793 208 0 0 25 0 1 0 543104096 354693120 77649 4294967295 134512640 134672761 3221224528 3221223728 134557842 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.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94470 0 0 0 31792 209 0 0 25 0 1 0 543104096 354963456 77717 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86661 77717 603 41 0 86620 0
vsize: 346644
[startup+330.037 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94548 0 0 0 32792 209 0 0 25 0 1 0 543104096 355229696 77795 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86726 77795 603 41 0 86685 0
vsize: 346904
[startup+340.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94639 0 0 0 33792 210 0 0 25 0 1 0 543104096 355635200 77886 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86825 77886 603 41 0 86784 0
vsize: 347300
[startup+350.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94655 0 0 0 34791 211 0 0 25 0 1 0 543104096 355635200 77902 4294967295 134512640 134672761 3221224528 3221223696 134560806 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.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94655 0 0 0 35791 211 0 0 25 0 1 0 543104096 355635200 77902 4294967295 134512640 134672761 3221224528 3221223728 134557842 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.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94666 0 0 0 36791 212 0 0 25 0 1 0 543104096 355717120 77913 4294967295 134512640 134672761 3221224528 3221223696 134561391 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.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13752
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94668 0 0 0 37791 212 0 0 25 0 1 0 543104096 355717120 77915 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86845 77915 603 41 0 86804 0
vsize: 347380
[startup+390.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94701 0 0 0 38790 212 0 0 25 0 1 0 543104096 355790848 77948 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86863 77948 603 41 0 86822 0
vsize: 347452
[startup+400.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94718 0 0 0 39790 212 0 0 25 0 1 0 543104096 355921920 77965 4294967295 134512640 134672761 3221224528 3221223696 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77965 603 41 0 86854 0
vsize: 347580
[startup+410.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94721 0 0 0 40789 213 0 0 25 0 1 0 543104096 355921920 77968 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77968 603 41 0 86854 0
vsize: 347580
[startup+420.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94729 0 0 0 41789 213 0 0 25 0 1 0 543104096 355921920 77976 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86895 77976 603 41 0 86854 0
vsize: 347580
[startup+430.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94747 0 0 0 42789 214 0 0 25 0 1 0 543104096 356057088 77994 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86928 77994 603 41 0 86887 0
vsize: 347712
[startup+440.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94763 0 0 0 43788 214 0 0 25 0 1 0 543104096 356057088 78010 4294967295 134512640 134672761 3221224528 3221223696 134560898 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.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94777 0 0 0 44788 215 0 0 25 0 1 0 543104096 356184064 78024 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86959 78024 603 41 0 86918 0
vsize: 347836
[startup+460.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94789 0 0 0 45788 215 0 0 25 0 1 0 543104096 356184064 78036 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86959 78036 603 41 0 86918 0
vsize: 347836
[startup+470.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94889 0 0 0 46787 216 0 0 25 0 1 0 543104096 356585472 78136 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87057 78136 603 41 0 87016 0
vsize: 348228
[startup+480.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94900 0 0 0 47787 216 0 0 25 0 1 0 543104096 356712448 78147 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94905 0 0 0 48787 216 0 0 25 0 1 0 543104096 356712448 78152 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78152 603 41 0 87047 0
vsize: 348352
[startup+500.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94914 0 0 0 49787 217 0 0 25 0 1 0 543104096 356712448 78161 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78161 603 41 0 87047 0
vsize: 348352
[startup+510.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94924 0 0 0 50787 217 0 0 25 0 1 0 543104096 356712448 78171 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78171 603 41 0 87047 0
vsize: 348352
[startup+520.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94932 0 0 0 51786 217 0 0 25 0 1 0 543104096 356843520 78179 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87120 78179 603 41 0 87079 0
vsize: 348480
[startup+530.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94946 0 0 0 52786 218 0 0 25 0 1 0 543104096 356843520 78193 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87120 78193 603 41 0 87079 0
vsize: 348480
[startup+540.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94968 0 0 0 53786 218 0 0 25 0 1 0 543104096 356974592 78215 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78215 603 41 0 87111 0
vsize: 348608
[startup+550.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94980 0 0 0 54786 218 0 0 25 0 1 0 543104096 356974592 78227 4294967295 134512640 134672761 3221224528 3221223632 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78227 603 41 0 87111 0
vsize: 348608
[startup+560.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 94994 0 0 0 55786 218 0 0 25 0 1 0 543104096 356974592 78241 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78241 603 41 0 87111 0
vsize: 348608
[startup+570.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95014 0 0 0 56786 218 0 0 25 0 1 0 543104096 357109760 78261 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87185 78261 603 41 0 87144 0
vsize: 348740
[startup+580.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95042 0 0 0 57786 219 0 0 25 0 1 0 543104096 357244928 78289 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87218 78289 603 41 0 87177 0
vsize: 348872
[startup+590.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95067 0 0 0 58785 219 0 0 25 0 1 0 543104096 357380096 78314 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78314 603 41 0 87210 0
vsize: 349004
[startup+600.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95083 0 0 0 59785 219 0 0 25 0 1 0 543104096 357380096 78330 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78330 603 41 0 87210 0
vsize: 349004
[startup+610.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95104 0 0 0 60784 220 0 0 25 0 1 0 543104096 357519360 78351 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87285 78351 603 41 0 87244 0
vsize: 349140
[startup+620.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95116 0 0 0 61784 221 0 0 25 0 1 0 543104096 357519360 78363 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87285 78363 603 41 0 87244 0
vsize: 349140
[startup+630.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95132 0 0 0 62784 221 0 0 25 0 1 0 543104096 357654528 78379 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78379 603 41 0 87277 0
vsize: 349272
[startup+640.054 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95140 0 0 0 63784 221 0 0 25 0 1 0 543104096 357654528 78387 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78387 603 41 0 87277 0
vsize: 349272
[startup+650.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95153 0 0 0 64784 221 0 0 25 0 1 0 543104096 357654528 78400 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 78400 603 41 0 87277 0
vsize: 349272
[startup+660.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95169 0 0 0 65784 221 0 0 25 0 1 0 543104096 357785600 78416 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87350 78416 603 41 0 87309 0
vsize: 349400
[startup+670.054 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95204 0 0 0 66784 222 0 0 25 0 1 0 543104096 357912576 78451 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87381 78451 603 41 0 87340 0
vsize: 349524
[startup+680.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95230 0 0 0 67784 222 0 0 25 0 1 0 543104096 358047744 78477 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87414 78477 603 41 0 87373 0
vsize: 349656
[startup+690.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95245 0 0 0 68784 222 0 0 25 0 1 0 543104096 358047744 78492 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87414 78492 603 41 0 87373 0
vsize: 349656
[startup+700.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95260 0 0 0 69784 222 0 0 25 0 1 0 543104096 358182912 78507 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87447 78507 603 41 0 87406 0
vsize: 349788
[startup+710.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95274 0 0 0 70784 222 0 0 25 0 1 0 543104096 358182912 78521 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87447 78521 603 41 0 87406 0
vsize: 349788
[startup+720.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95295 0 0 0 71785 222 0 0 25 0 1 0 543104096 358182912 78542 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87447 78542 603 41 0 87406 0
vsize: 349788
[startup+730.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95305 0 0 0 72785 222 0 0 25 0 1 0 543104096 358313984 78552 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87479 78552 603 41 0 87438 0
vsize: 349916
[startup+740.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95309 0 0 0 73785 222 0 0 25 0 1 0 543104096 358313984 78556 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87479 78556 603 41 0 87438 0
vsize: 349916
[startup+750.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95364 0 0 0 74785 222 0 0 25 0 1 0 543104096 358592512 78611 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87547 78611 603 41 0 87506 0
vsize: 350188
[startup+760.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95406 0 0 0 75785 222 0 0 25 0 1 0 543104096 358727680 78653 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87580 78653 603 41 0 87539 0
vsize: 350320
[startup+770.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95446 0 0 0 76786 222 0 0 25 0 1 0 543104096 358854656 78693 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87611 78693 603 41 0 87570 0
vsize: 350444
[startup+780.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95481 0 0 0 77786 222 0 0 25 0 1 0 543104096 358989824 78728 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87644 78728 603 41 0 87603 0
vsize: 350576
[startup+790.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95509 0 0 0 78785 222 0 0 25 0 1 0 543104096 359124992 78756 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87677 78756 603 41 0 87636 0
vsize: 350708
[startup+800.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95540 0 0 0 79785 222 0 0 25 0 1 0 543104096 359260160 78787 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87710 78787 603 41 0 87669 0
vsize: 350840
[startup+810.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95579 0 0 0 80785 223 0 0 25 0 1 0 543104096 359391232 78826 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87742 78826 603 41 0 87701 0
vsize: 350968
[startup+820.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95659 0 0 0 81785 223 0 0 25 0 1 0 543104096 359784448 78906 4294967295 134512640 134672761 3221224528 3221223712 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87838 78906 603 41 0 87797 0
vsize: 351352
[startup+830.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95686 0 0 0 82785 223 0 0 25 0 1 0 543104096 359784448 78933 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87838 78933 603 41 0 87797 0
vsize: 351352
[startup+840.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95734 0 0 0 83785 223 0 0 25 0 1 0 543104096 360046592 78981 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87902 78981 603 41 0 87861 0
vsize: 351608
[startup+850.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95786 0 0 0 84786 223 0 0 25 0 1 0 543104096 360181760 79033 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87935 79033 603 41 0 87894 0
vsize: 351740
[startup+860.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95855 0 0 0 85786 223 0 0 25 0 1 0 543104096 360452096 79102 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88001 79102 603 41 0 87960 0
vsize: 352004
[startup+870.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95912 0 0 0 86786 224 0 0 25 0 1 0 543104096 360718336 79159 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88066 79159 603 41 0 88025 0
vsize: 352264
[startup+880.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95916 0 0 0 87786 224 0 0 25 0 1 0 543104096 360718336 79163 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88066 79163 603 41 0 88025 0
vsize: 352264
[startup+890.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95943 0 0 0 88786 224 0 0 25 0 1 0 543104096 360849408 79190 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88098 79190 603 41 0 88057 0
vsize: 352392
[startup+900.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95951 0 0 0 89786 224 0 0 25 0 1 0 543104096 360849408 79198 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88098 79198 603 41 0 88057 0
vsize: 352392
[startup+910.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95958 0 0 0 90786 224 0 0 25 0 1 0 543104096 360984576 79205 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79205 603 41 0 88090 0
vsize: 352524
[startup+920.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95965 0 0 0 91786 224 0 0 25 0 1 0 543104096 360984576 79212 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79212 603 41 0 88090 0
vsize: 352524
[startup+930.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95969 0 0 0 92786 224 0 0 25 0 1 0 543104096 360984576 79216 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79216 603 41 0 88090 0
vsize: 352524
[startup+940.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95975 0 0 0 93787 224 0 0 25 0 1 0 543104096 360984576 79222 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79222 603 41 0 88090 0
vsize: 352524
[startup+950.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95985 0 0 0 94787 224 0 0 25 0 1 0 543104096 360984576 79232 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79232 603 41 0 88090 0
vsize: 352524
[startup+960.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 95994 0 0 0 95787 224 0 0 25 0 1 0 543104096 361119744 79241 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79241 603 41 0 88123 0
vsize: 352656
[startup+970.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96001 0 0 0 96787 224 0 0 25 0 1 0 543104096 361119744 79248 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79248 603 41 0 88123 0
vsize: 352656
[startup+980.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96010 0 0 0 97787 224 0 0 25 0 1 0 543104096 361119744 79257 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79257 603 41 0 88123 0
vsize: 352656
[startup+990.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96019 0 0 0 98787 224 0 0 25 0 1 0 543104096 361119744 79266 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79266 603 41 0 88123 0
vsize: 352656
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96030 0 0 0 99787 224 0 0 25 0 1 0 543104096 361254912 79277 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79277 603 41 0 88156 0
vsize: 352788
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96039 0 0 0 100787 225 0 0 25 0 1 0 543104096 361254912 79286 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79286 603 41 0 88156 0
vsize: 352788
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96052 0 0 0 101787 225 0 0 25 0 1 0 543104096 361254912 79299 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79299 603 41 0 88156 0
vsize: 352788
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96059 0 0 0 102788 225 0 0 25 0 1 0 543104096 361390080 79306 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79306 603 41 0 88189 0
vsize: 352920
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96066 0 0 0 103788 225 0 0 25 0 1 0 543104096 361390080 79313 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79313 603 41 0 88189 0
vsize: 352920
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96082 0 0 0 104788 225 0 0 25 0 1 0 543104096 361390080 79329 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79329 603 41 0 88189 0
vsize: 352920
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96109 0 0 0 105788 225 0 0 25 0 1 0 543104096 361521152 79356 4294967295 134512640 134672761 3221224528 3221223728 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88262 79356 603 41 0 88221 0
vsize: 353048
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96126 0 0 0 106788 225 0 0 25 0 1 0 543104096 361656320 79373 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88295 79373 603 41 0 88254 0
vsize: 353180
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96139 0 0 0 107788 225 0 0 25 0 1 0 543104096 361656320 79386 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88295 79386 603 41 0 88254 0
vsize: 353180
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96156 0 0 0 108789 225 0 0 25 0 1 0 543104096 361656320 79403 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88295 79403 603 41 0 88254 0
vsize: 353180
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96173 0 0 0 109789 225 0 0 25 0 1 0 543104096 361791488 79420 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88328 79420 603 41 0 88287 0
vsize: 353312
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96186 0 0 0 110789 225 0 0 25 0 1 0 543104096 361791488 79433 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88328 79433 603 41 0 88287 0
vsize: 353312
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96209 0 0 0 111789 225 0 0 25 0 1 0 543104096 361926656 79456 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88361 79456 603 41 0 88320 0
vsize: 353444
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96225 0 0 0 112789 225 0 0 25 0 1 0 543104096 362061824 79472 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88394 79472 603 41 0 88353 0
vsize: 353576
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96235 0 0 0 113789 225 0 0 25 0 1 0 543104096 362061824 79482 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88394 79482 603 41 0 88353 0
vsize: 353576
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96247 0 0 0 114789 225 0 0 25 0 1 0 543104096 362061824 79494 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88394 79494 603 41 0 88353 0
vsize: 353576
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96256 0 0 0 115789 226 0 0 25 0 1 0 543104096 362196992 79503 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79503 603 41 0 88386 0
vsize: 353708
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96268 0 0 0 116789 226 0 0 25 0 1 0 543104096 362196992 79515 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79515 603 41 0 88386 0
vsize: 353708
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96280 0 0 0 117790 226 0 0 25 0 1 0 543104096 362196992 79527 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79527 603 41 0 88386 0
vsize: 353708
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96289 0 0 0 118790 226 0 0 25 0 1 0 543104096 362332160 79536 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88460 79536 603 41 0 88419 0
vsize: 353840
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 13754
Raw data (stat): 13697 (minisat+) R 13696 18865 18864 0 -1 0 96300 0 0 0 119790 226 0 0 25 0 1 0 543104096 362332160 79547 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88460 79547 603 41 0 88419 0
vsize: 353840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 13754
Raw data (stat): 13697 (minisat+) Z 13696 18865 18864 0 -1 12 96303 0 0 0 119790 241 0 0 25 0 1 0 543104096 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.23
CPU time (s): 1200.32
CPU user time (s): 1197.91
CPU system time (s): 2.41763
CPU usage (%): 100.008
Max. virtual memory (Kb): 353840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####