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/miplib/normalized-mps-v2-13-7-mod008.opb
MD5SUM	fbdb3cf321a85412feefcaac30780520
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	307
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	22000
Number of bits of the biggest number in a constraint	15
Biggest sum of numbers in a constraint	1027256
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01684
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 19105

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        530616 kB
Buffers:         21516 kB
Cached:         460672 kB
SwapCached:          0 kB
Active:         277844 kB
Inactive:       206888 kB
HighTotal:      131008 kB
HighFree:         7476 kB
LowTotal:       903652 kB
LowFree:        523140 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13692 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:10:09 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 17029 7 1200.34 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 3314
Raw data (stat): 3314 (runsolver) R 3313 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488798044 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.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 9098 0 0 0 978 20 0 0 25 0 1 0 488798044 27918336 6354 4294967295 134512640 134672761 3221224544 3221214288 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6816 6354 603 41 0 6775 0
vsize: 27264
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 11880 0 0 0 1972 27 0 0 25 0 1 0 488798044 39739392 8971 4294967295 134512640 134672761 3221224544 3221212864 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9702 8971 603 41 0 9661 0
vsize: 38808
[startup+30 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 20364 0 0 0 2952 46 0 0 25 0 1 0 488798044 63680512 14488 4294967295 134512640 134672761 3221224544 3221213824 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15547 14488 603 41 0 15506 0
vsize: 62188
[startup+39.9999 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 24598 0 0 0 3944 54 0 0 25 0 1 0 488798044 75706368 18063 4294967295 134512640 134672761 3221224544 3221209984 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18483 18063 603 41 0 18442 0
vsize: 73932
[startup+50.0002 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 30458 0 0 0 4932 67 0 0 25 0 1 0 488798044 97673216 22605 4294967295 134512640 134672761 3221224544 3221207768 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23846 22605 603 41 0 23805 0
vsize: 95384
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 33742 0 0 0 5924 75 0 0 25 0 1 0 488798044 82284544 18967 4294967295 134512640 134672761 3221224544 3221204704 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20089 18967 603 41 0 20048 0
vsize: 80356
[startup+70.0013 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 73919 0 0 0 6832 167 0 0 25 0 1 0 488798044 273436672 57166 4294967295 134512640 134672761 3221224544 3221200048 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66757 57166 603 41 0 66716 0
vsize: 267028
[startup+80.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93166 0 0 0 7790 209 0 0 25 0 1 0 488798044 346783744 76413 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84664 76413 603 41 0 84623 0
vsize: 338656
[startup+90.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93286 0 0 0 8788 210 0 0 25 0 1 0 488798044 347324416 76533 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93366 0 0 0 9788 210 0 0 25 0 1 0 488798044 347594752 76613 4294967295 134512640 134672761 3221224544 3221223720 134565025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84862 76613 603 41 0 84821 0
vsize: 339448
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93487 0 0 0 10788 210 0 0 25 0 1 0 488798044 348135424 76734 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93571 0 0 0 11788 210 0 0 25 0 1 0 488798044 348405760 76818 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85060 76818 603 41 0 85019 0
vsize: 340240
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93767 0 0 0 12787 211 0 0 25 0 1 0 488798044 351993856 77014 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93775 0 0 0 13788 211 0 0 25 0 1 0 488798044 352129024 77022 4294967295 134512640 134672761 3221224544 3221223712 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93789 0 0 0 14788 211 0 0 25 0 1 0 488798044 352129024 77036 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85969 77036 603 41 0 85928 0
vsize: 343876
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93843 0 0 0 15787 212 0 0 25 0 1 0 488798044 352395264 77090 4294967295 134512640 134672761 3221224544 3221223680 134560718 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93877 0 0 0 16788 212 0 0 25 0 1 0 488798044 352526336 77124 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93895 0 0 0 17787 212 0 0 25 0 1 0 488798044 352526336 77142 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86066 77142 603 41 0 86025 0
vsize: 344264
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93919 0 0 0 18787 212 0 0 25 0 1 0 488798044 352657408 77166 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86098 77166 603 41 0 86057 0
vsize: 344392
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93940 0 0 0 19787 212 0 0 25 0 1 0 488798044 352788480 77187 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86130 77187 603 41 0 86089 0
vsize: 344520
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 93975 0 0 0 20788 212 0 0 25 0 1 0 488798044 352919552 77222 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86162 77222 603 41 0 86121 0
vsize: 344648
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94009 0 0 0 21788 212 0 0 25 0 1 0 488798044 353054720 77256 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86195 77256 603 41 0 86154 0
vsize: 344780
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94050 0 0 0 22788 212 0 0 25 0 1 0 488798044 353189888 77297 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86228 77297 603 41 0 86187 0
vsize: 344912
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94085 0 0 0 23788 212 0 0 25 0 1 0 488798044 353325056 77332 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86261 77332 603 41 0 86220 0
vsize: 345044
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94107 0 0 0 24788 213 0 0 25 0 1 0 488798044 353402880 77354 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86280 77354 603 41 0 86239 0
vsize: 345120
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94133 0 0 0 25788 213 0 0 25 0 1 0 488798044 353402880 77380 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86280 77380 603 41 0 86239 0
vsize: 345120
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94193 0 0 0 26788 213 0 0 25 0 1 0 488798044 353669120 77440 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86345 77440 603 41 0 86304 0
vsize: 345380
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94222 0 0 0 27788 213 0 0 25 0 1 0 488798044 353804288 77469 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86378 77469 603 41 0 86337 0
vsize: 345512
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94286 0 0 0 28788 213 0 0 25 0 1 0 488798044 354152448 77533 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86463 77533 603 41 0 86422 0
vsize: 345852
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94353 0 0 0 29788 214 0 0 25 0 1 0 488798044 354422784 77600 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86529 77600 603 41 0 86488 0
vsize: 346116
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94399 0 0 0 30788 214 0 0 25 0 1 0 488798044 354693120 77646 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86595 77646 603 41 0 86554 0
vsize: 346380
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94447 0 0 0 31788 214 0 0 25 0 1 0 488798044 354828288 77694 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86628 77694 603 41 0 86587 0
vsize: 346512
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94540 0 0 0 32787 215 0 0 25 0 1 0 488798044 355229696 77787 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86726 77787 603 41 0 86685 0
vsize: 346904
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94628 0 0 0 33787 215 0 0 25 0 1 0 488798044 355500032 77875 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86792 77875 603 41 0 86751 0
vsize: 347168
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94655 0 0 0 34787 215 0 0 25 0 1 0 488798044 355635200 77902 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86825 77902 603 41 0 86784 0
vsize: 347300
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94655 0 0 0 35787 215 0 0 25 0 1 0 488798044 355635200 77902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86825 77902 603 41 0 86784 0
vsize: 347300
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94666 0 0 0 36788 215 0 0 25 0 1 0 488798044 355717120 77913 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86845 77913 603 41 0 86804 0
vsize: 347380
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94666 0 0 0 37788 215 0 0 25 0 1 0 488798044 355717120 77913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86845 77913 603 41 0 86804 0
vsize: 347380
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94697 0 0 0 38787 215 0 0 25 0 1 0 488798044 355790848 77944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86863 77944 603 41 0 86822 0
vsize: 347452
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94717 0 0 0 39787 215 0 0 25 0 1 0 488798044 355921920 77964 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86895 77964 603 41 0 86854 0
vsize: 347580
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94721 0 0 0 40787 215 0 0 25 0 1 0 488798044 355921920 77968 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86895 77968 603 41 0 86854 0
vsize: 347580
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94725 0 0 0 41787 215 0 0 25 0 1 0 488798044 355921920 77972 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86895 77972 603 41 0 86854 0
vsize: 347580
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94747 0 0 0 42788 215 0 0 25 0 1 0 488798044 356057088 77994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86928 77994 603 41 0 86887 0
vsize: 347712
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94756 0 0 0 43788 215 0 0 25 0 1 0 488798044 356057088 78003 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86928 78003 603 41 0 86887 0
vsize: 347712
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94773 0 0 0 44788 216 0 0 25 0 1 0 488798044 356184064 78020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86959 78020 603 41 0 86918 0
vsize: 347836
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94785 0 0 0 45788 216 0 0 25 0 1 0 488798044 356184064 78032 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86959 78032 603 41 0 86918 0
vsize: 347836
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94858 0 0 0 46788 216 0 0 25 0 1 0 488798044 356458496 78105 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87026 78105 603 41 0 86985 0
vsize: 348104
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94895 0 0 0 47788 216 0 0 25 0 1 0 488798044 356585472 78142 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87057 78142 603 41 0 87016 0
vsize: 348228
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94903 0 0 0 48788 216 0 0 25 0 1 0 488798044 356712448 78150 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87088 78150 603 41 0 87047 0
vsize: 348352
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94913 0 0 0 49788 216 0 0 25 0 1 0 488798044 356712448 78160 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87088 78160 603 41 0 87047 0
vsize: 348352
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94919 0 0 0 50788 216 0 0 25 0 1 0 488798044 356712448 78166 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87088 78166 603 41 0 87047 0
vsize: 348352
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94929 0 0 0 51789 216 0 0 25 0 1 0 488798044 356712448 78176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87088 78176 603 41 0 87047 0
vsize: 348352
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94942 0 0 0 52789 216 0 0 25 0 1 0 488798044 356843520 78189 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87120 78189 603 41 0 87079 0
vsize: 348480
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94958 0 0 0 53789 216 0 0 25 0 1 0 488798044 356843520 78205 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87120 78205 603 41 0 87079 0
vsize: 348480
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94978 0 0 0 54789 216 0 0 25 0 1 0 488798044 356974592 78225 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87152 78225 603 41 0 87111 0
vsize: 348608
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 94990 0 0 0 55789 216 0 0 25 0 1 0 488798044 356974592 78237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87152 78237 603 41 0 87111 0
vsize: 348608
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95009 0 0 0 56789 216 0 0 25 0 1 0 488798044 357109760 78256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87185 78256 603 41 0 87144 0
vsize: 348740
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95031 0 0 0 57790 216 0 0 25 0 1 0 488798044 357244928 78278 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87218 78278 603 41 0 87177 0
vsize: 348872
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3314
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95061 0 0 0 58789 217 0 0 25 0 1 0 488798044 357244928 78308 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87218 78308 603 41 0 87177 0
vsize: 348872
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 3355
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95080 0 0 0 59790 217 0 0 25 0 1 0 488798044 357380096 78327 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87251 78327 603 41 0 87210 0
vsize: 349004
[startup+610.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95098 0 0 0 60789 217 0 0 25 0 1 0 488798044 357519360 78345 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87285 78345 603 41 0 87244 0
vsize: 349140
[startup+620.007 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95114 0 0 0 61789 217 0 0 25 0 1 0 488798044 357519360 78361 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87285 78361 603 41 0 87244 0
vsize: 349140
[startup+630.007 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95126 0 0 0 62790 217 0 0 25 0 1 0 488798044 357519360 78373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87285 78373 603 41 0 87244 0
vsize: 349140
[startup+640.008 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95138 0 0 0 63790 217 0 0 25 0 1 0 488798044 357654528 78385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 78385 603 41 0 87277 0
vsize: 349272
[startup+650.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95149 0 0 0 64790 217 0 0 25 0 1 0 488798044 357654528 78396 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 78396 603 41 0 87277 0
vsize: 349272
[startup+660.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3367
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95161 0 0 0 65790 217 0 0 25 0 1 0 488798044 357654528 78408 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 78408 603 41 0 87277 0
vsize: 349272
[startup+670.007 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95195 0 0 0 66790 218 0 0 25 0 1 0 488798044 357912576 78442 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87381 78442 603 41 0 87340 0
vsize: 349524
[startup+680.007 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95214 0 0 0 67790 218 0 0 25 0 1 0 488798044 357912576 78461 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87381 78461 603 41 0 87340 0
vsize: 349524
[startup+690.008 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95245 0 0 0 68790 218 0 0 25 0 1 0 488798044 358047744 78492 4294967295 134512640 134672761 3221224544 3221223712 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.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95253 0 0 0 69790 218 0 0 25 0 1 0 488798044 358047744 78500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87414 78500 603 41 0 87373 0
vsize: 349656
[startup+710.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95268 0 0 0 70791 218 0 0 25 0 1 0 488798044 358182912 78515 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87447 78515 603 41 0 87406 0
vsize: 349788
[startup+720.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95292 0 0 0 71791 218 0 0 25 0 1 0 488798044 358182912 78539 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87447 78539 603 41 0 87406 0
vsize: 349788
[startup+730.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95302 0 0 0 72791 218 0 0 25 0 1 0 488798044 358313984 78549 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87479 78549 603 41 0 87438 0
vsize: 349916
[startup+740.009 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95307 0 0 0 73791 218 0 0 25 0 1 0 488798044 358313984 78554 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87479 78554 603 41 0 87438 0
vsize: 349916
[startup+750.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95339 0 0 0 74791 218 0 0 25 0 1 0 488798044 358453248 78586 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87513 78586 603 41 0 87472 0
vsize: 350052
[startup+760.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95397 0 0 0 75791 219 0 0 25 0 1 0 488798044 358727680 78644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87580 78644 603 41 0 87539 0
vsize: 350320
[startup+770.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95429 0 0 0 76791 219 0 0 25 0 1 0 488798044 358854656 78676 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87611 78676 603 41 0 87570 0
vsize: 350444
[startup+780.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95473 0 0 0 77791 219 0 0 25 0 1 0 488798044 358989824 78720 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87644 78720 603 41 0 87603 0
vsize: 350576
[startup+790.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95498 0 0 0 78791 219 0 0 25 0 1 0 488798044 359124992 78745 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87677 78745 603 41 0 87636 0
vsize: 350708
[startup+800.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95526 0 0 0 79791 219 0 0 25 0 1 0 488798044 359124992 78773 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87677 78773 603 41 0 87636 0
vsize: 350708
[startup+810.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95567 0 0 0 80791 220 0 0 25 0 1 0 488798044 359391232 78814 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87742 78814 603 41 0 87701 0
vsize: 350968
[startup+820.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95627 0 0 0 81790 220 0 0 25 0 1 0 488798044 359661568 78874 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87808 78874 603 41 0 87767 0
vsize: 351232
[startup+830.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95679 0 0 0 82790 220 0 0 25 0 1 0 488798044 359784448 78926 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87838 78926 603 41 0 87797 0
vsize: 351352
[startup+840.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95719 0 0 0 83790 220 0 0 25 0 1 0 488798044 359915520 78966 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87870 78966 603 41 0 87829 0
vsize: 351480
[startup+850.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95770 0 0 0 84790 221 0 0 25 0 1 0 488798044 360181760 79017 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87935 79017 603 41 0 87894 0
vsize: 351740
[startup+860.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95834 0 0 0 85790 221 0 0 25 0 1 0 488798044 360452096 79081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88001 79081 603 41 0 87960 0
vsize: 352004
[startup+870.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95898 0 0 0 86790 221 0 0 25 0 1 0 488798044 360718336 79145 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88066 79145 603 41 0 88025 0
vsize: 352264
[startup+880.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95916 0 0 0 87790 221 0 0 25 0 1 0 488798044 360718336 79163 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95934 0 0 0 88790 221 0 0 25 0 1 0 488798044 360849408 79181 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88098 79181 603 41 0 88057 0
vsize: 352392
[startup+900.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95949 0 0 0 89790 221 0 0 25 0 1 0 488798044 360849408 79196 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88098 79196 603 41 0 88057 0
vsize: 352392
[startup+910.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95955 0 0 0 90791 221 0 0 25 0 1 0 488798044 360984576 79202 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79202 603 41 0 88090 0
vsize: 352524
[startup+920.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95964 0 0 0 91792 221 0 0 25 0 1 0 488798044 360984576 79211 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79211 603 41 0 88090 0
vsize: 352524
[startup+930.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95968 0 0 0 92792 221 0 0 25 0 1 0 488798044 360984576 79215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79215 603 41 0 88090 0
vsize: 352524
[startup+940.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3369
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95972 0 0 0 93792 221 0 0 25 0 1 0 488798044 360984576 79219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79219 603 41 0 88090 0
vsize: 352524
[startup+950.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95983 0 0 0 94792 221 0 0 25 0 1 0 488798044 360984576 79230 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88131 79230 603 41 0 88090 0
vsize: 352524
[startup+960.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95992 0 0 0 95792 221 0 0 25 0 1 0 488798044 361119744 79239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79239 603 41 0 88123 0
vsize: 352656
[startup+970.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 95997 0 0 0 96793 221 0 0 25 0 1 0 488798044 361119744 79244 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79244 603 41 0 88123 0
vsize: 352656
[startup+980.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96007 0 0 0 97793 221 0 0 25 0 1 0 488798044 361119744 79254 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79254 603 41 0 88123 0
vsize: 352656
[startup+990.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96016 0 0 0 98793 221 0 0 25 0 1 0 488798044 361119744 79263 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88164 79263 603 41 0 88123 0
vsize: 352656
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96027 0 0 0 99793 221 0 0 25 0 1 0 488798044 361254912 79274 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79274 603 41 0 88156 0
vsize: 352788
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96036 0 0 0 100793 221 0 0 25 0 1 0 488798044 361254912 79283 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79283 603 41 0 88156 0
vsize: 352788
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96048 0 0 0 101793 221 0 0 25 0 1 0 488798044 361254912 79295 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88197 79295 603 41 0 88156 0
vsize: 352788
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96058 0 0 0 102793 221 0 0 25 0 1 0 488798044 361390080 79305 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79305 603 41 0 88189 0
vsize: 352920
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96063 0 0 0 103794 221 0 0 25 0 1 0 488798044 361390080 79310 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79310 603 41 0 88189 0
vsize: 352920
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96079 0 0 0 104793 222 0 0 25 0 1 0 488798044 361390080 79326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88230 79326 603 41 0 88189 0
vsize: 352920
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96102 0 0 0 105794 222 0 0 25 0 1 0 488798044 361521152 79349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88262 79349 603 41 0 88221 0
vsize: 353048
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96122 0 0 0 106794 222 0 0 25 0 1 0 488798044 361521152 79369 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88262 79369 603 41 0 88221 0
vsize: 353048
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96135 0 0 0 107794 222 0 0 25 0 1 0 488798044 361656320 79382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88295 79382 603 41 0 88254 0
vsize: 353180
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96152 0 0 0 108794 222 0 0 25 0 1 0 488798044 361656320 79399 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88295 79399 603 41 0 88254 0
vsize: 353180
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96170 0 0 0 109794 222 0 0 25 0 1 0 488798044 361791488 79417 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88328 79417 603 41 0 88287 0
vsize: 353312
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96185 0 0 0 110794 222 0 0 25 0 1 0 488798044 361791488 79432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88328 79432 603 41 0 88287 0
vsize: 353312
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96204 0 0 0 111794 222 0 0 25 0 1 0 488798044 361926656 79451 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88361 79451 603 41 0 88320 0
vsize: 353444
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96220 0 0 0 112794 222 0 0 25 0 1 0 488798044 361926656 79467 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88361 79467 603 41 0 88320 0
vsize: 353444
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96231 0 0 0 113794 222 0 0 25 0 1 0 488798044 362061824 79478 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88394 79478 603 41 0 88353 0
vsize: 353576
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96244 0 0 0 114795 222 0 0 25 0 1 0 488798044 362061824 79491 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88394 79491 603 41 0 88353 0
vsize: 353576
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96255 0 0 0 115795 222 0 0 25 0 1 0 488798044 362196992 79502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79502 603 41 0 88386 0
vsize: 353708
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96265 0 0 0 116795 222 0 0 25 0 1 0 488798044 362196992 79512 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79512 603 41 0 88386 0
vsize: 353708
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96278 0 0 0 117795 222 0 0 25 0 1 0 488798044 362196992 79525 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88427 79525 603 41 0 88386 0
vsize: 353708
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96288 0 0 0 118795 222 0 0 25 0 1 0 488798044 362332160 79535 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88460 79535 603 41 0 88419 0
vsize: 353840
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3371
Raw data (stat): 3314 (minisat+) R 3313 25347 25346 0 -1 0 96297 0 0 0 119795 223 0 0 25 0 1 0 488798044 362332160 79544 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88460 79544 603 41 0 88419 0
vsize: 353840
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3371
Raw data (stat): 3314 (minisat+) Z 3313 25347 25346 0 -1 12 96300 0 0 0 119795 238 0 0 25 0 1 0 488798044 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.17
CPU time (s): 1200.34
CPU user time (s): 1197.96
CPU system time (s): 2.38564
CPU usage (%): 100.014
Max. virtual memory (Kb): 353840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####