PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.02084
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 18077

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 13:24:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18628 boxname=wulflinc26 idbench=1433 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  581d778a36086562107993896110e0a2  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-mod008.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-mod008.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-mod008.opb
IDLAUNCH: 18628
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        534592 kB
Buffers:         29564 kB
Cached:         440384 kB
SwapCached:         68 kB
Active:          55872 kB
Inactive:       416932 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        534284 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            21620 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:44:27 (client local time) WITH STATUS 10 IN 1200.36 SECONDS
stats: 18628 7 1200.36 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.84 0.94 0.90 2/54 31852
Raw data (stat): 31852 (runsolver) R 31851 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545421992 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 9126 0 0 0 980 18 0 0 25 0 1 0 545421992 28053504 6382 4294967295 134512640 134672761 3221224544 3221213616 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6382 603 41 0 6808 0
vsize: 27396
[startup+20.001 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 11964 0 0 0 1975 23 0 0 25 0 1 0 545421992 40144896 9055 4294967295 134512640 134672761 3221224544 3221208544 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9801 9055 603 41 0 9760 0
vsize: 39204
[startup+30.0006 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 20494 0 0 0 2958 40 0 0 25 0 1 0 545421992 64086016 14618 4294967295 134512640 134672761 3221224544 3221217840 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15646 14618 603 41 0 15605 0
vsize: 62584
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 24762 0 0 0 3951 47 0 0 25 0 1 0 545421992 82538496 18227 4294967295 134512640 134672761 3221224544 3221207864 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20151 18228 603 41 0 20110 0
vsize: 80604
[startup+50.0011 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 30692 0 0 0 4939 59 0 0 25 0 1 0 545421992 98484224 22839 4294967295 134512640 134672761 3221224544 3221223840 134593983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24044 22839 603 41 0 24003 0
vsize: 96176
[startup+60.0017 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 33753 0 0 0 5932 67 0 0 25 0 1 0 545421992 76886016 17660 4294967295 134512640 134672761 3221224544 3221212240 134522981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18771 17660 603 41 0 18730 0
vsize: 75084
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 79006 0 0 0 6831 168 0 0 25 0 1 0 545421992 289148928 62253 4294967295 134512640 134672761 3221224544 3221210368 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70593 62253 603 41 0 70552 0
vsize: 282372
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93185 0 0 0 7802 197 0 0 25 0 1 0 545421992 346783744 76432 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84664 76432 603 41 0 84623 0
vsize: 338656
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93286 0 0 0 8801 198 0 0 25 0 1 0 545421992 347324416 76533 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93375 0 0 0 9800 198 0 0 25 0 1 0 545421992 347594752 76622 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84862 76622 603 41 0 84821 0
vsize: 339448
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93491 0 0 0 10799 199 0 0 25 0 1 0 545421992 348135424 76738 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84994 76738 603 41 0 84953 0
vsize: 339976
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93591 0 0 0 11800 199 0 0 25 0 1 0 545421992 348635136 76838 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85116 76838 603 41 0 85075 0
vsize: 340464
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93773 0 0 0 12799 200 0 0 25 0 1 0 545421992 351993856 77020 4294967295 134512640 134672761 3221224544 3221223712 134560942 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93775 0 0 0 13799 200 0 0 25 0 1 0 545421992 352129024 77022 4294967295 134512640 134672761 3221224544 3221223712 134560852 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93803 0 0 0 14799 200 0 0 25 0 1 0 545421992 352129024 77050 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85969 77050 603 41 0 85928 0
vsize: 343876
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93850 0 0 0 15799 200 0 0 25 0 1 0 545421992 352395264 77097 4294967295 134512640 134672761 3221224544 3221223728 134558365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86034 77097 603 41 0 85993 0
vsize: 344136
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93878 0 0 0 16799 200 0 0 25 0 1 0 545421992 352526336 77125 4294967295 134512640 134672761 3221224544 3221223712 134560830 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93899 0 0 0 17799 201 0 0 25 0 1 0 545421992 352526336 77146 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93926 0 0 0 18799 201 0 0 25 0 1 0 545421992 352657408 77173 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93941 0 0 0 19799 201 0 0 25 0 1 0 545421992 352788480 77188 4294967295 134512640 134672761 3221224544 3221223744 134557836 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 93982 0 0 0 20799 201 0 0 25 0 1 0 545421992 352919552 77229 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86162 77229 603 41 0 86121 0
vsize: 344648
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94020 0 0 0 21800 201 0 0 25 0 1 0 545421992 353054720 77267 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86195 77267 603 41 0 86154 0
vsize: 344780
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94061 0 0 0 22800 201 0 0 25 0 1 0 545421992 353189888 77308 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86228 77308 603 41 0 86187 0
vsize: 344912
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94092 0 0 0 23800 201 0 0 25 0 1 0 545421992 353325056 77339 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94108 0 0 0 24799 202 0 0 25 0 1 0 545421992 353402880 77355 4294967295 134512640 134672761 3221224544 3221223712 134561400 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94151 0 0 0 25799 202 0 0 25 0 1 0 545421992 353538048 77398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86313 77398 603 41 0 86272 0
vsize: 345252
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94198 0 0 0 26799 202 0 0 25 0 1 0 545421992 353669120 77445 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94240 0 0 0 27799 202 0 0 25 0 1 0 545421992 353890304 77487 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86399 77487 603 41 0 86358 0
vsize: 345596
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94305 0 0 0 28799 203 0 0 25 0 1 0 545421992 354287616 77552 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86496 77552 603 41 0 86455 0
vsize: 345984
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94361 0 0 0 29799 203 0 0 25 0 1 0 545421992 354422784 77608 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86529 77608 603 41 0 86488 0
vsize: 346116
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94402 0 0 0 30799 203 0 0 25 0 1 0 545421992 354693120 77649 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94486 0 0 0 31799 203 0 0 25 0 1 0 545421992 354963456 77733 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86661 77733 603 41 0 86620 0
vsize: 346644
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94577 0 0 0 32800 203 0 0 25 0 1 0 545421992 355364864 77824 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86759 77824 603 41 0 86718 0
vsize: 347036
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94640 0 0 0 33799 204 0 0 25 0 1 0 545421992 355635200 77887 4294967295 134512640 134672761 3221224544 3221223744 134557903 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94655 0 0 0 34799 204 0 0 25 0 1 0 545421992 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94655 0 0 0 35800 204 0 0 25 0 1 0 545421992 355635200 77902 4294967295 134512640 134672761 3221224544 3221223668 134566034 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94666 0 0 0 36800 204 0 0 25 0 1 0 545421992 355717120 77913 4294967295 134512640 134672761 3221224544 3221223744 134557852 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94682 0 0 0 37800 204 0 0 25 0 1 0 545421992 355717120 77929 4294967295 134512640 134672761 3221224544 3221223712 134560869 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94703 0 0 0 38800 204 0 0 25 0 1 0 545421992 355790848 77950 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86863 77950 603 41 0 86822 0
vsize: 347452
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94719 0 0 0 39800 204 0 0 25 0 1 0 545421992 355921920 77966 4294967295 134512640 134672761 3221224544 3221223844 134556649 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94723 0 0 0 40800 204 0 0 25 0 1 0 545421992 355921920 77970 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94737 0 0 0 41801 204 0 0 25 0 1 0 545421992 356057088 77984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86928 77984 603 41 0 86887 0
vsize: 347712
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94754 0 0 0 42801 204 0 0 25 0 1 0 545421992 356057088 78001 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86928 78001 603 41 0 86887 0
vsize: 347712
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94763 0 0 0 43801 204 0 0 25 0 1 0 545421992 356057088 78010 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94782 0 0 0 44801 204 0 0 25 0 1 0 545421992 356184064 78029 4294967295 134512640 134672761 3221224544 3221223728 134558656 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94809 0 0 0 45801 205 0 0 25 0 1 0 545421992 356319232 78056 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86992 78056 603 41 0 86951 0
vsize: 347968
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94891 0 0 0 46801 205 0 0 25 0 1 0 545421992 356585472 78138 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87057 78138 603 41 0 87016 0
vsize: 348228
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94900 0 0 0 47801 205 0 0 25 0 1 0 545421992 356712448 78147 4294967295 134512640 134672761 3221224544 3221223712 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94907 0 0 0 48801 206 0 0 25 0 1 0 545421992 356712448 78154 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78154 603 41 0 87047 0
vsize: 348352
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94916 0 0 0 49801 206 0 0 25 0 1 0 545421992 356712448 78163 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94927 0 0 0 50801 206 0 0 25 0 1 0 545421992 356712448 78174 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87088 78174 603 41 0 87047 0
vsize: 348352
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94934 0 0 0 51801 206 0 0 25 0 1 0 545421992 356843520 78181 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87120 78181 603 41 0 87079 0
vsize: 348480
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94952 0 0 0 52801 206 0 0 25 0 1 0 545421992 356843520 78199 4294967295 134512640 134672761 3221224544 3221223680 134560688 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.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94975 0 0 0 53801 206 0 0 25 0 1 0 545421992 356974592 78222 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78222 603 41 0 87111 0
vsize: 348608
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 94985 0 0 0 54802 206 0 0 25 0 1 0 545421992 356974592 78232 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87152 78232 603 41 0 87111 0
vsize: 348608
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95001 0 0 0 55802 206 0 0 25 0 1 0 545421992 357109760 78248 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87185 78248 603 41 0 87144 0
vsize: 348740
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95019 0 0 0 56802 206 0 0 25 0 1 0 545421992 357109760 78266 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87185 78266 603 41 0 87144 0
vsize: 348740
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95049 0 0 0 57802 206 0 0 25 0 1 0 545421992 357244928 78296 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87218 78296 603 41 0 87177 0
vsize: 348872
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95077 0 0 0 58802 206 0 0 25 0 1 0 545421992 357380096 78324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78324 603 41 0 87210 0
vsize: 349004
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95087 0 0 0 59802 206 0 0 25 0 1 0 545421992 357380096 78334 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87251 78334 603 41 0 87210 0
vsize: 349004
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95111 0 0 0 60802 207 0 0 25 0 1 0 545421992 357519360 78358 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95124 0 0 0 61802 207 0 0 25 0 1 0 545421992 357519360 78371 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95135 0 0 0 62802 207 0 0 25 0 1 0 545421992 357654528 78382 4294967295 134512640 134672761 3221224544 3221223728 134559041 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95142 0 0 0 63803 207 0 0 25 0 1 0 545421992 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95155 0 0 0 64803 207 0 0 25 0 1 0 545421992 357654528 78402 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 78402 603 41 0 87277 0
vsize: 349272
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95176 0 0 0 65803 207 0 0 25 0 1 0 545421992 357785600 78423 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87350 78423 603 41 0 87309 0
vsize: 349400
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95209 0 0 0 66803 207 0 0 25 0 1 0 545421992 357912576 78456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87381 78456 603 41 0 87340 0
vsize: 349524
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95242 0 0 0 67803 207 0 0 25 0 1 0 545421992 358047744 78489 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87414 78489 603 41 0 87373 0
vsize: 349656
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95253 0 0 0 68803 207 0 0 25 0 1 0 545421992 358047744 78500 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87414 78500 603 41 0 87373 0
vsize: 349656
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95265 0 0 0 69803 207 0 0 25 0 1 0 545421992 358182912 78512 4294967295 134512640 134672761 3221224544 3221223744 134557885 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95280 0 0 0 70804 207 0 0 25 0 1 0 545421992 358182912 78527 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87447 78527 603 41 0 87406 0
vsize: 349788
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95299 0 0 0 71804 207 0 0 25 0 1 0 545421992 358313984 78546 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95306 0 0 0 72804 207 0 0 25 0 1 0 545421992 358313984 78553 4294967295 134512640 134672761 3221224544 3221223712 134561188 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95327 0 0 0 73804 207 0 0 25 0 1 0 545421992 358313984 78574 4294967295 134512640 134672761 3221224544 3221223600 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87479 78574 603 41 0 87438 0
vsize: 349916
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95386 0 0 0 74804 208 0 0 25 0 1 0 545421992 358592512 78633 4294967295 134512640 134672761 3221224544 3221223700 134561241 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95418 0 0 0 75804 208 0 0 25 0 1 0 545421992 358727680 78665 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87580 78665 603 41 0 87539 0
vsize: 350320
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95462 0 0 0 76804 208 0 0 25 0 1 0 545421992 358989824 78709 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87644 78709 603 41 0 87603 0
vsize: 350576
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95497 0 0 0 77804 208 0 0 25 0 1 0 545421992 359124992 78744 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87677 78744 603 41 0 87636 0
vsize: 350708
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95521 0 0 0 78803 209 0 0 25 0 1 0 545421992 359124992 78768 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87677 78768 603 41 0 87636 0
vsize: 350708
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95564 0 0 0 79803 209 0 0 25 0 1 0 545421992 359391232 78811 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87742 78811 603 41 0 87701 0
vsize: 350968
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95609 0 0 0 80803 209 0 0 25 0 1 0 545421992 359526400 78856 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87775 78856 603 41 0 87734 0
vsize: 351100
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95676 0 0 0 81803 209 0 0 25 0 1 0 545421992 359784448 78923 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87838 78923 603 41 0 87797 0
vsize: 351352
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95713 0 0 0 82803 209 0 0 25 0 1 0 545421992 359915520 78960 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87870 78960 603 41 0 87829 0
vsize: 351480
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95763 0 0 0 83803 210 0 0 25 0 1 0 545421992 360181760 79010 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87935 79010 603 41 0 87894 0
vsize: 351740
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95829 0 0 0 84803 210 0 0 25 0 1 0 545421992 360452096 79076 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88001 79076 603 41 0 87960 0
vsize: 352004
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95897 0 0 0 85803 211 0 0 25 0 1 0 545421992 360718336 79144 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88066 79144 603 41 0 88025 0
vsize: 352264
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95916 0 0 0 86803 211 0 0 25 0 1 0 545421992 360718336 79163 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95934 0 0 0 87803 211 0 0 25 0 1 0 545421992 360849408 79181 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88098 79181 603 41 0 88057 0
vsize: 352392
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95949 0 0 0 88803 211 0 0 25 0 1 0 545421992 360849408 79196 4294967295 134512640 134672761 3221224544 3221223744 134557852 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95955 0 0 0 89803 211 0 0 25 0 1 0 545421992 360984576 79202 4294967295 134512640 134672761 3221224544 3221223744 134557836 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95964 0 0 0 90803 211 0 0 25 0 1 0 545421992 360984576 79211 4294967295 134512640 134672761 3221224544 3221223744 134557842 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95967 0 0 0 91803 211 0 0 25 0 1 0 545421992 360984576 79214 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79214 603 41 0 88090 0
vsize: 352524
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95972 0 0 0 92803 211 0 0 25 0 1 0 545421992 360984576 79219 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95983 0 0 0 93804 211 0 0 25 0 1 0 545421992 360984576 79230 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88131 79230 603 41 0 88090 0
vsize: 352524
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95992 0 0 0 94804 211 0 0 25 0 1 0 545421992 361119744 79239 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 95997 0 0 0 95804 211 0 0 25 0 1 0 545421992 361119744 79244 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96007 0 0 0 96804 211 0 0 25 0 1 0 545421992 361119744 79254 4294967295 134512640 134672761 3221224544 3221223680 134560703 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96016 0 0 0 97804 211 0 0 25 0 1 0 545421992 361119744 79263 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96028 0 0 0 98804 211 0 0 25 0 1 0 545421992 361254912 79275 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88197 79275 603 41 0 88156 0
vsize: 352788
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96036 0 0 0 99804 211 0 0 25 0 1 0 545421992 361254912 79283 4294967295 134512640 134672761 3221224544 3221223712 134560830 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96050 0 0 0 100804 211 0 0 25 0 1 0 545421992 361254912 79297 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88197 79297 603 41 0 88156 0
vsize: 352788
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96058 0 0 0 101805 211 0 0 25 0 1 0 545421992 361390080 79305 4294967295 134512640 134672761 3221224544 3221223712 134560869 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96064 0 0 0 102805 212 0 0 25 0 1 0 545421992 361390080 79311 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88230 79311 603 41 0 88189 0
vsize: 352920
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96079 0 0 0 103805 212 0 0 25 0 1 0 545421992 361390080 79326 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 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 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96107 0 0 0 104805 212 0 0 25 0 1 0 545421992 361521152 79354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88262 79354 603 41 0 88221 0
vsize: 353048
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96125 0 0 0 105805 212 0 0 25 0 1 0 545421992 361656320 79372 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88295 79372 603 41 0 88254 0
vsize: 353180
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96138 0 0 0 106805 212 0 0 25 0 1 0 545421992 361656320 79385 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88295 79385 603 41 0 88254 0
vsize: 353180
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96154 0 0 0 107805 212 0 0 25 0 1 0 545421992 361656320 79401 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88295 79401 603 41 0 88254 0
vsize: 353180
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96171 0 0 0 108805 213 0 0 25 0 1 0 545421992 361791488 79418 4294967295 134512640 134672761 3221224544 3221223744 134557852 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96185 0 0 0 109805 213 0 0 25 0 1 0 545421992 361791488 79432 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96207 0 0 0 110805 213 0 0 25 0 1 0 545421992 361926656 79454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88361 79454 603 41 0 88320 0
vsize: 353444
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96223 0 0 0 111805 213 0 0 25 0 1 0 545421992 362061824 79470 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79470 603 41 0 88353 0
vsize: 353576
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96234 0 0 0 112805 213 0 0 25 0 1 0 545421992 362061824 79481 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79481 603 41 0 88353 0
vsize: 353576
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96247 0 0 0 113806 213 0 0 25 0 1 0 545421992 362061824 79494 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88394 79494 603 41 0 88353 0
vsize: 353576
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96256 0 0 0 114806 213 0 0 25 0 1 0 545421992 362196992 79503 4294967295 134512640 134672761 3221224544 3221223712 134560806 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96268 0 0 0 115806 213 0 0 25 0 1 0 545421992 362196992 79515 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96280 0 0 0 116806 213 0 0 25 0 1 0 545421992 362196992 79527 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96289 0 0 0 117806 213 0 0 25 0 1 0 545421992 362332160 79536 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96301 0 0 0 118806 213 0 0 25 0 1 0 545421992 362332160 79548 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88460 79548 603 41 0 88419 0
vsize: 353840
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31852
Raw data (stat): 31852 (minisat+) R 31851 22612 22611 0 -1 0 96311 0 0 0 119806 213 0 0 25 0 1 0 545421992 362332160 79558 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.19 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31852
Raw data (stat): 31852 (minisat+) Z 31851 22612 22611 0 -1 12 96314 0 0 0 119806 229 0 0 25 0 1 0 545421992 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.19
CPU time (s): 1200.36
CPU user time (s): 1198.07
CPU system time (s): 2.29065
CPU usage (%): 100.014
Max. virtual memory (Kb): 353840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####