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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb
MD5SUM	375b355299c9fbf8170e172bcbc73eb2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16728
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.23
Number of variables	242
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	122
Trace number 14170

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        573436 kB
Buffers:         37064 kB
Cached:         400516 kB
SwapCached:          0 kB
Active:         187396 kB
Inactive:       253044 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        573184 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            15176 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:26:40 (client local time) WITH STATUS 10 IN 1200.49 SECONDS
stats: 19499 7 1200.49 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  12]---> BDD-cost:66836
c ---[  10]---> BDD-cost:95787
c ---[   8]---> BDD-cost:84392
c ---[   6]---> BDD-cost:96629
c ---[   4]---> BDD-cost:73107
c ---[   2]---> BDD-cost:101010
c ---[   0]---> BDD-cost:61606
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1663587  4853486 |  554529       0        0     nan |  0.000 % |
c |       100 | 1663573  4853458 |  609981      99    22244   224.7 |  0.006 % |
c ==============================================================================
c [1mFound solution: 1268596[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1831     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       174 | 1668226  4864330 |  556075     173    25196   145.6 |  0.006 % |
c ==============================================================================
c [1mFound solution: 1256968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       175 | 1668254  4864454 |  556084     174    25198   144.8 |  0.006 % |
c |       275 | 1668254  4864454 |  611692     274    29457   107.5 |  0.006 % |
c |       425 | 1668254  4864454 |  672861     424   247224   583.1 |  0.006 % |
c ==============================================================================
c [1mFound solution: 869404[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       432 | 1668299  4864560 |  556099     431   255074   591.8 |  0.006 % |
c ==============================================================================
c [1mFound solution: 540570[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       445 | 1668317  4864608 |  556105     444   266203   599.6 |  0.006 % |
c ==============================================================================
c [1mFound solution: 147729[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       452 | 1668359  4864706 |  556119     451   278175   616.8 |  0.006 % |
c |       553 | 1668359  4864706 |  611730     552   356801   646.4 |  0.007 % |
c |       703 | 1668359  4864706 |  672903     702   375277   534.6 |  0.007 % |
c |       928 | 1668359  4864706 |  740194     927   386529   417.0 |  0.007 % |
c ==============================================================================
c [1mFound solution: 147594[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1232 | 1668363  4864715 |  556121    1226   398478   325.0 |  0.007 % |
c |      1334 | 1668363  4864715 |  611733    1328   624282   470.1 |  0.007 % |
c |      1484 | 1668363  4864715 |  672906    1478   669960   453.3 |  0.007 % |
c |      1709 | 1668357  4864703 |  740197    1700   683076   401.8 |  0.008 % |
c |      2049 | 1668357  4864703 |  814216    2040   703387   344.8 |  0.008 % |
c |      2555 | 1668136  4864257 |  895638    2539   732681   288.6 |  0.025 % |
c |      3314 | 1668136  4864257 |  985202    3298   789054   239.3 |  0.025 % |
c |      4453 | 1668054  4864093 | 1083722    4436   863463   194.6 |  0.032 % |
c |      6162 | 1668054  4864093 | 1192094    6145   987222   160.7 |  0.032 % |
#### 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.98 0.97 0.96 2/54 27770
Raw data (stat): 27770 (runsolver) R 27769 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482043718 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.0007 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 50831 0 0 0 880 118 0 0 25 0 1 0 482043718 234582016 46177 4294967295 134512640 134672761 3221224528 3221223608 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57271 46177 603 41 0 57230 0
vsize: 229084
[startup+20.0009 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 53142 0 0 0 1874 124 0 0 25 0 1 0 482043718 242548736 48488 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59216 48488 603 41 0 59175 0
vsize: 236864
[startup+30.0017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54116 0 0 0 2870 128 0 0 25 0 1 0 482043718 248107008 49462 4294967295 134512640 134672761 3221224528 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60573 49462 603 41 0 60532 0
vsize: 242292
[startup+40.0012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54214 0 0 0 3870 128 0 0 25 0 1 0 482043718 248492032 49552 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60667 49552 603 41 0 60626 0
vsize: 242668
[startup+50.0025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54232 0 0 0 4869 128 0 0 25 0 1 0 482043718 248594432 49570 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60692 49570 603 41 0 60651 0
vsize: 242768
[startup+60.0033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54256 0 0 0 5869 129 0 0 25 0 1 0 482043718 248729600 49594 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60725 49594 603 41 0 60684 0
vsize: 242900
[startup+70.0038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54287 0 0 0 6868 129 0 0 25 0 1 0 482043718 248856576 49625 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60756 49625 603 41 0 60715 0
vsize: 243024
[startup+80.0051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54317 0 0 0 7868 130 0 0 25 0 1 0 482043718 248995840 49655 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60790 49655 603 41 0 60749 0
vsize: 243160
[startup+90.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54335 0 0 0 8868 130 0 0 25 0 1 0 482043718 248995840 49673 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60790 49673 603 41 0 60749 0
vsize: 243160
[startup+100.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54364 0 0 0 9867 131 0 0 25 0 1 0 482043718 249135104 49702 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60824 49702 603 41 0 60783 0
vsize: 243296
[startup+110.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54401 0 0 0 10867 131 0 0 25 0 1 0 482043718 249282560 49739 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60860 49739 603 41 0 60819 0
vsize: 243440
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54434 0 0 0 11867 131 0 0 25 0 1 0 482043718 249409536 49772 4294967295 134512640 134672761 3221224528 3221223652 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60891 49772 603 41 0 60850 0
vsize: 243564
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54501 0 0 0 12866 131 0 0 25 0 1 0 482043718 249692160 49839 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60960 49839 603 41 0 60919 0
vsize: 243840
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54536 0 0 0 13866 131 0 0 25 0 1 0 482043718 249827328 49874 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60993 49874 603 41 0 60952 0
vsize: 243972
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54569 0 0 0 14866 132 0 0 25 0 1 0 482043718 250220544 49907 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49907 603 41 0 61048 0
vsize: 244356
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54578 0 0 0 15866 132 0 0 25 0 1 0 482043718 250220544 49916 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49916 603 41 0 61048 0
vsize: 244356
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54592 0 0 0 16866 132 0 0 25 0 1 0 482043718 250220544 49930 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49930 603 41 0 61048 0
vsize: 244356
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54596 0 0 0 17865 133 0 0 25 0 1 0 482043718 250220544 49934 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49934 603 41 0 61048 0
vsize: 244356
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54602 0 0 0 18865 133 0 0 25 0 1 0 482043718 250220544 49940 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49940 603 41 0 61048 0
vsize: 244356
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54608 0 0 0 19865 133 0 0 25 0 1 0 482043718 250220544 49946 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61089 49946 603 41 0 61048 0
vsize: 244356
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54615 0 0 0 20865 133 0 0 25 0 1 0 482043718 250351616 49953 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61121 49953 603 41 0 61080 0
vsize: 244484
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54760 0 0 0 21864 134 0 0 25 0 1 0 482043718 250863616 50098 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61246 50098 603 41 0 61205 0
vsize: 244984
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54861 0 0 0 22864 134 0 0 25 0 1 0 482043718 251367424 50199 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61369 50199 603 41 0 61328 0
vsize: 245476
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54897 0 0 0 23863 135 0 0 25 0 1 0 482043718 251473920 50235 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61395 50235 603 41 0 61354 0
vsize: 245580
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54971 0 0 0 24863 135 0 0 25 0 1 0 482043718 251998208 50309 4294967295 134512640 134672761 3221224528 3221223596 1074717812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50309 603 41 0 61482 0
vsize: 246092
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54971 0 0 0 25863 135 0 0 25 0 1 0 482043718 251998208 50309 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50309 603 41 0 61482 0
vsize: 246092
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54973 0 0 0 26862 136 0 0 25 0 1 0 482043718 251998208 50311 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50311 603 41 0 61482 0
vsize: 246092
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54976 0 0 0 27862 136 0 0 25 0 1 0 482043718 251998208 50314 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50314 603 41 0 61482 0
vsize: 246092
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54985 0 0 0 28861 136 0 0 25 0 1 0 482043718 251998208 50323 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50323 603 41 0 61482 0
vsize: 246092
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54987 0 0 0 29861 137 0 0 25 0 1 0 482043718 251998208 50325 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50325 603 41 0 61482 0
vsize: 246092
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54992 0 0 0 30861 137 0 0 25 0 1 0 482043718 251998208 50330 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61523 50330 603 41 0 61482 0
vsize: 246092
[startup+320.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 54997 0 0 0 31860 138 0 0 25 0 1 0 482043718 252108800 50335 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61550 50335 603 41 0 61509 0
vsize: 246200
[startup+330.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55000 0 0 0 32861 138 0 0 25 0 1 0 482043718 252108800 50338 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61550 50338 603 41 0 61509 0
vsize: 246200
[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55011 0 0 0 33861 139 0 0 25 0 1 0 482043718 252108800 50349 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61550 50349 603 41 0 61509 0
vsize: 246200
[startup+350.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55011 0 0 0 34862 139 0 0 25 0 1 0 482043718 252108800 50349 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61550 50349 603 41 0 61509 0
vsize: 246200
[startup+360.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55015 0 0 0 35862 139 0 0 25 0 1 0 482043718 252108800 50353 4294967295 134512640 134672761 3221224528 3221223724 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61550 50353 603 41 0 61509 0
vsize: 246200
[startup+370.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55022 0 0 0 36861 140 0 0 25 0 1 0 482043718 252235776 50360 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 50360 603 41 0 61540 0
vsize: 246324
[startup+380.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55035 0 0 0 37861 140 0 0 25 0 1 0 482043718 252235776 50373 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 50373 603 41 0 61540 0
vsize: 246324
[startup+390.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55035 0 0 0 38862 140 0 0 25 0 1 0 482043718 252235776 50373 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 50373 603 41 0 61540 0
vsize: 246324
[startup+400.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55037 0 0 0 39864 141 0 0 25 0 1 0 482043718 252235776 50375 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 50375 603 41 0 61540 0
vsize: 246324
[startup+410.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55041 0 0 0 40864 142 0 0 25 0 1 0 482043718 252235776 50379 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 50379 603 41 0 61540 0
vsize: 246324
[startup+420.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55045 0 0 0 41864 142 0 0 25 0 1 0 482043718 252235776 50383 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61581 50383 603 41 0 61540 0
vsize: 246324
[startup+430.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55057 0 0 0 42863 142 0 0 25 0 1 0 482043718 252354560 50395 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61610 50395 603 41 0 61569 0
vsize: 246440
[startup+440.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55061 0 0 0 43863 143 0 0 25 0 1 0 482043718 252354560 50399 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61610 50399 603 41 0 61569 0
vsize: 246440
[startup+450.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55065 0 0 0 44862 143 0 0 25 0 1 0 482043718 252354560 50403 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61610 50403 603 41 0 61569 0
vsize: 246440
[startup+460.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55068 0 0 0 45862 143 0 0 25 0 1 0 482043718 252354560 50406 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61610 50406 603 41 0 61569 0
vsize: 246440
[startup+470.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55079 0 0 0 46862 144 0 0 25 0 1 0 482043718 252354560 50417 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61610 50417 603 41 0 61569 0
vsize: 246440
[startup+480.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55084 0 0 0 47861 144 0 0 25 0 1 0 482043718 252477440 50422 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50422 603 41 0 61599 0
vsize: 246560
[startup+490.099 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55089 0 0 0 48862 144 0 0 25 0 1 0 482043718 252477440 50427 4294967295 134512640 134672761 3221224528 3221223712 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50427 603 41 0 61599 0
vsize: 246560
[startup+500.212 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55099 0 0 0 49873 145 0 0 25 0 1 0 482043718 252477440 50437 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50437 603 41 0 61599 0
vsize: 246560
[startup+510.213 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55099 0 0 0 50874 145 0 0 25 0 1 0 482043718 252477440 50437 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50437 603 41 0 61599 0
vsize: 246560
[startup+520.212 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55111 0 0 0 51873 145 0 0 25 0 1 0 482043718 252477440 50449 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50449 603 41 0 61599 0
vsize: 246560
[startup+530.228 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55111 0 0 0 52875 146 0 0 25 0 1 0 482043718 252477440 50449 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50449 603 41 0 61599 0
vsize: 246560
[startup+540.228 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55111 0 0 0 53875 146 0 0 25 0 1 0 482043718 252477440 50449 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61640 50449 603 41 0 61599 0
vsize: 246560
[startup+550.228 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55119 0 0 0 54874 146 0 0 25 0 1 0 482043718 252608512 50457 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 50457 603 41 0 61631 0
vsize: 246688
[startup+560.228 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55124 0 0 0 55874 146 0 0 25 0 1 0 482043718 252608512 50462 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 50462 603 41 0 61631 0
vsize: 246688
[startup+570.228 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55127 0 0 0 56874 147 0 0 25 0 1 0 482043718 252608512 50465 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 50465 603 41 0 61631 0
vsize: 246688
[startup+580.229 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55135 0 0 0 57874 147 0 0 25 0 1 0 482043718 252608512 50473 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 50473 603 41 0 61631 0
vsize: 246688
[startup+590.229 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55140 0 0 0 58874 147 0 0 25 0 1 0 482043718 252608512 50478 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61672 50478 603 41 0 61631 0
vsize: 246688
[startup+600.23 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55145 0 0 0 59874 147 0 0 25 0 1 0 482043718 252731392 50483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50483 603 41 0 61661 0
vsize: 246808
[startup+610.231 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55150 0 0 0 60874 147 0 0 25 0 1 0 482043718 252731392 50488 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50488 603 41 0 61661 0
vsize: 246808
[startup+620.23 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55155 0 0 0 61874 148 0 0 25 0 1 0 482043718 252731392 50493 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50493 603 41 0 61661 0
vsize: 246808
[startup+630.23 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55161 0 0 0 62874 148 0 0 25 0 1 0 482043718 252731392 50499 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50499 603 41 0 61661 0
vsize: 246808
[startup+640.234 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55166 0 0 0 63874 148 0 0 25 0 1 0 482043718 252731392 50504 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50504 603 41 0 61661 0
vsize: 246808
[startup+650.235 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55169 0 0 0 64874 148 0 0 25 0 1 0 482043718 252731392 50507 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50507 603 41 0 61661 0
vsize: 246808
[startup+660.236 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55170 0 0 0 65874 149 0 0 25 0 1 0 482043718 252731392 50508 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61702 50508 603 41 0 61661 0
vsize: 246808
[startup+670.237 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55172 0 0 0 66874 149 0 0 25 0 1 0 482043718 252850176 50510 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61731 50510 603 41 0 61690 0
vsize: 246924
[startup+680.237 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55183 0 0 0 67874 149 0 0 25 0 1 0 482043718 252850176 50521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61731 50521 603 41 0 61690 0
vsize: 246924
[startup+690.237 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55183 0 0 0 68874 149 0 0 25 0 1 0 482043718 252850176 50521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61731 50521 603 41 0 61690 0
vsize: 246924
[startup+700.238 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55188 0 0 0 69874 149 0 0 25 0 1 0 482043718 252850176 50526 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61731 50526 603 41 0 61690 0
vsize: 246924
[startup+710.239 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55192 0 0 0 70874 150 0 0 25 0 1 0 482043718 252850176 50530 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61731 50530 603 41 0 61690 0
vsize: 246924
[startup+720.239 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55200 0 0 0 71874 150 0 0 25 0 1 0 482043718 252956672 50538 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50538 603 41 0 61716 0
vsize: 247028
[startup+730.24 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55201 0 0 0 72874 150 0 0 25 0 1 0 482043718 252956672 50539 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50539 603 41 0 61716 0
vsize: 247028
[startup+740.24 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55209 0 0 0 73874 151 0 0 25 0 1 0 482043718 252956672 50547 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50547 603 41 0 61716 0
vsize: 247028
[startup+750.242 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55214 0 0 0 74874 151 0 0 25 0 1 0 482043718 252956672 50552 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50552 603 41 0 61716 0
vsize: 247028
[startup+760.242 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55217 0 0 0 75874 151 0 0 25 0 1 0 482043718 252956672 50555 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50555 603 41 0 61716 0
vsize: 247028
[startup+770.242 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55223 0 0 0 76874 151 0 0 25 0 1 0 482043718 252956672 50561 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61757 50561 603 41 0 61716 0
vsize: 247028
[startup+780.243 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55233 0 0 0 77874 152 0 0 25 0 1 0 482043718 253091840 50571 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50571 603 41 0 61749 0
vsize: 247160
[startup+790.243 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55240 0 0 0 78874 152 0 0 25 0 1 0 482043718 253091840 50578 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50578 603 41 0 61749 0
vsize: 247160
[startup+800.244 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55243 0 0 0 79873 153 0 0 25 0 1 0 482043718 253091840 50581 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50581 603 41 0 61749 0
vsize: 247160
[startup+810.245 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55246 0 0 0 80874 153 0 0 25 0 1 0 482043718 253091840 50584 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50584 603 41 0 61749 0
vsize: 247160
[startup+820.245 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55248 0 0 0 81873 153 0 0 25 0 1 0 482043718 253091840 50586 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50586 603 41 0 61749 0
vsize: 247160
[startup+830.25 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55254 0 0 0 82874 153 0 0 25 0 1 0 482043718 253091840 50592 4294967295 134512640 134672761 3221224528 3221223632 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61790 50592 603 41 0 61749 0
vsize: 247160
[startup+840.25 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55266 0 0 0 83874 154 0 0 25 0 1 0 482043718 253218816 50604 4294967295 134512640 134672761 3221224528 3221223712 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50604 603 41 0 61780 0
vsize: 247284
[startup+850.251 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55266 0 0 0 84874 154 0 0 25 0 1 0 482043718 253218816 50604 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50604 603 41 0 61780 0
vsize: 247284
[startup+860.251 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55270 0 0 0 85873 154 0 0 25 0 1 0 482043718 253218816 50608 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50608 603 41 0 61780 0
vsize: 247284
[startup+870.251 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55274 0 0 0 86873 154 0 0 25 0 1 0 482043718 253218816 50612 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50612 603 41 0 61780 0
vsize: 247284
[startup+880.251 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55279 0 0 0 87874 154 0 0 25 0 1 0 482043718 253218816 50617 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50617 603 41 0 61780 0
vsize: 247284
[startup+890.252 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55284 0 0 0 88874 154 0 0 25 0 1 0 482043718 253218816 50622 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50622 603 41 0 61780 0
vsize: 247284
[startup+900.252 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55290 0 0 0 89873 155 0 0 25 0 1 0 482043718 253218816 50628 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61821 50628 603 41 0 61780 0
vsize: 247284
[startup+910.253 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55298 0 0 0 90873 155 0 0 25 0 1 0 482043718 253349888 50636 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61853 50636 603 41 0 61812 0
vsize: 247412
[startup+920.253 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55304 0 0 0 91873 155 0 0 25 0 1 0 482043718 253349888 50642 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61853 50642 603 41 0 61812 0
vsize: 247412
[startup+930.254 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55309 0 0 0 92873 156 0 0 25 0 1 0 482043718 253349888 50647 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61853 50647 603 41 0 61812 0
vsize: 247412
[startup+940.254 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55315 0 0 0 93873 156 0 0 25 0 1 0 482043718 253349888 50653 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61853 50653 603 41 0 61812 0
vsize: 247412
[startup+950.255 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55321 0 0 0 94873 156 0 0 25 0 1 0 482043718 253349888 50659 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61853 50659 603 41 0 61812 0
vsize: 247412
[startup+960.256 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55327 0 0 0 95873 157 0 0 25 0 1 0 482043718 253476864 50665 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61884 50665 603 41 0 61843 0
vsize: 247536
[startup+970.255 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55333 0 0 0 96872 157 0 0 25 0 1 0 482043718 253476864 50671 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61884 50671 603 41 0 61843 0
vsize: 247536
[startup+980.256 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55345 0 0 0 97873 157 0 0 25 0 1 0 482043718 253476864 50683 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61884 50683 603 41 0 61843 0
vsize: 247536
[startup+990.256 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55347 0 0 0 98873 157 0 0 25 0 1 0 482043718 253476864 50685 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61884 50685 603 41 0 61843 0
vsize: 247536
[startup+1000.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55349 0 0 0 99872 158 0 0 25 0 1 0 482043718 253476864 50687 4294967295 134512640 134672761 3221224528 3221223712 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61884 50687 603 41 0 61843 0
vsize: 247536
[startup+1010.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55355 0 0 0 100872 158 0 0 25 0 1 0 482043718 253595648 50693 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50693 603 41 0 61872 0
vsize: 247652
[startup+1020.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55361 0 0 0 101872 158 0 0 25 0 1 0 482043718 253595648 50699 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50699 603 41 0 61872 0
vsize: 247652
[startup+1030.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55361 0 0 0 102872 159 0 0 25 0 1 0 482043718 253595648 50699 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50699 603 41 0 61872 0
vsize: 247652
[startup+1040.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55366 0 0 0 103872 159 0 0 25 0 1 0 482043718 253595648 50704 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50704 603 41 0 61872 0
vsize: 247652
[startup+1050.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55373 0 0 0 104872 160 0 0 25 0 1 0 482043718 253595648 50711 4294967295 134512640 134672761 3221224528 3221223688 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50711 603 41 0 61872 0
vsize: 247652
[startup+1060.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55381 0 0 0 105872 160 0 0 25 0 1 0 482043718 253595648 50719 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50719 603 41 0 61872 0
vsize: 247652
[startup+1070.26 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55381 0 0 0 106871 160 0 0 25 0 1 0 482043718 253595648 50719 4294967295 134512640 134672761 3221224528 3221223632 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50719 603 41 0 61872 0
vsize: 247652
[startup+1080.27 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55384 0 0 0 107872 161 0 0 25 0 1 0 482043718 253595648 50722 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 50722 603 41 0 61872 0
vsize: 247652
[startup+1090.28 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55391 0 0 0 108873 161 0 0 25 0 1 0 482043718 253730816 50729 4294967295 134512640 134672761 3221224528 3221223712 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50729 603 41 0 61905 0
vsize: 247784
[startup+1100.28 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55394 0 0 0 109873 161 0 0 25 0 1 0 482043718 253730816 50732 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50732 603 41 0 61905 0
vsize: 247784
[startup+1110.29 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55402 0 0 0 110874 162 0 0 25 0 1 0 482043718 253730816 50740 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50740 603 41 0 61905 0
vsize: 247784
[startup+1120.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55404 0 0 0 111875 162 0 0 25 0 1 0 482043718 253730816 50742 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50742 603 41 0 61905 0
vsize: 247784
[startup+1130.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55408 0 0 0 112874 162 0 0 25 0 1 0 482043718 253730816 50746 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50746 603 41 0 61905 0
vsize: 247784
[startup+1140.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55411 0 0 0 113874 163 0 0 25 0 1 0 482043718 253730816 50749 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50749 603 41 0 61905 0
vsize: 247784
[startup+1150.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55416 0 0 0 114874 163 0 0 25 0 1 0 482043718 253730816 50754 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61946 50754 603 41 0 61905 0
vsize: 247784
[startup+1160.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55419 0 0 0 115874 164 0 0 25 0 1 0 482043718 253861888 50757 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61978 50757 603 41 0 61937 0
vsize: 247912
[startup+1170.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55432 0 0 0 116874 164 0 0 25 0 1 0 482043718 253861888 50770 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61978 50770 603 41 0 61937 0
vsize: 247912
[startup+1180.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55432 0 0 0 117873 164 0 0 25 0 1 0 482043718 253861888 50770 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61978 50770 603 41 0 61937 0
vsize: 247912
[startup+1190.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55435 0 0 0 118873 164 0 0 25 0 1 0 482043718 253861888 50773 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61978 50773 603 41 0 61937 0
vsize: 247912
[startup+1200.3 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 27770
Raw data (stat): 27770 (minisat+) R 27769 5897 5896 0 -1 0 55441 0 0 0 119873 165 0 0 25 0 1 0 482043718 253861888 50779 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61978 50779 603 41 0 61937 0
vsize: 247912
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.41 s]
Raw data (loadavg): 0.99 0.97 0.96 1/54 27770
Raw data (stat): 27770 (minisat+) Z 27769 5897 5896 0 -1 12 55444 0 0 0 119873 175 0 0 25 0 1 0 482043718 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.41
CPU time (s): 1200.49
CPU user time (s): 1198.74
CPU system time (s): 1.75373
CPU usage (%): 100.007
Max. virtual memory (Kb): 247912
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####