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/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cc.opb
MD5SUM	0493ba9e257fafbb54efa7af2eeb7bf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1567
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	5699
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	5699
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.134979
Number of variables	133
Total number of constraints	229
Number of constraints which are clauses	229
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	31
Trace number 5586

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 00:37:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4011 boxname=wulflinc4 idbench=251 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0493ba9e257fafbb54efa7af2eeb7bf2  /oldhome/oroussel/tmp/wulflinc4/normalized-cc.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc4/normalized-cc.opb /oldhome/oroussel/tmp/wulflinc4/normalized-cc.opb
IDLAUNCH: 4011
/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:        901212 kB
Buffers:         35168 kB
Cached:          78664 kB
SwapCached:          0 kB
Active:          54080 kB
Inactive:        62588 kB
HighTotal:      131008 kB
HighFree:        48524 kB
LowTotal:       903652 kB
LowFree:        852688 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10972 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:57:38 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4011 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 199 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     186      734 |      55       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  93/93          
c |         0 |     170      674 |      --       0       --      -- |     --   | -16/-60
c |         0 |     170      674 |      68       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.015997 s)
c ==============================================================================
c [1mFound solution: 1846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10637     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   23625    55476 |    7087       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9215          
c   -- var.elim.:  2000/9215          
c   -- var.elim.:  3000/9215          
c   -- var.elim.:  4000/9215          
c   -- var.elim.:  5000/9215          
c   -- var.elim.:  6000/9215          
c   -- var.elim.:  7000/9215          
c   -- var.elim.:  8000/9215          
c   -- var.elim.:  9000/9215          
c   -- var.elim.:  9215/9215          
c   -- var.elim.:  1000/4932          
c   -- var.elim.:  2000/4932          
c   -- var.elim.:  3000/4932          
c   -- var.elim.:  4000/4932          
c   -- var.elim.:  4932/4932          
c   -- subsuming                       
c   -- var.elim.:  1000/1243          
c   -- var.elim.:  1243/1243          
c   -- var.elim.:  403/403          
c   -- subsuming                       
c   -- var.elim.:  14/14          
c |         0 |   20509    68874 |      --       0       --      -- |     --   | -3116/13399
c |         0 |   20509    68874 |    8203       0        0     nan |  0.000 % |
c |       100 |   20509    68874 |    9023     100     5331    53.3 |  0.406 % |
c |       251 |   20509    68874 |    9926     251     7306    29.1 |  0.405 % |
c |       477 |   20509    68874 |   10918     477    15050    31.6 |  0.405 % |
c |       814 |   20509    68874 |   12010     814    50659    62.2 |  0.405 % |
c ==============================================================================
c (current CPU-time: 3.48547 s)
c ==============================================================================
c [1mFound solution: 1823[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1084 |   20779    69226 |    6233    1083    67309    62.2 |  0.405 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1142          
c   -- var.elim.:  1142/1142          
c   -- var.elim.:  525/525          
c   -- subsuming                       
c   -- var.elim.:  45/45          
c |      1084 |   20490    69073 |      --    1083       --      -- |     --   | -289/-152
c |      1084 |   20490    69073 |    8196    1040    61028    58.7 |  0.405 % |
c |      1186 |   20490    69073 |    9015    1142    64538    56.5 |  1.068 % |
c |      1336 |   20462    68978 |    9903    1290    65464    50.7 |  1.169 % |
c |      1561 |   20462    68978 |   10893    1515    79062    52.2 |  1.169 % |
c |      1900 |   20462    68978 |   11983    1854   105074    56.7 |  1.169 % |
c |      2407 |   20381    68699 |   13129    2356   151327    64.2 |  1.431 % |
c |      3168 |   20381    68699 |   14442    3117   168643    54.1 |  1.431 % |
c |      4310 |   20271    68336 |   15800    4257   350738    82.4 |  1.754 % |
c ==============================================================================
c (current CPU-time: 6.99494 s)
c ==============================================================================
c [1mFound solution: 1741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4535 |   20358    68677 |    6107    4482   363149    81.0 |  1.754 % |
c   -- subsuming                       
c   -- var.elim.:  419/419          
c   -- var.elim.:  244/244          
c |      4535 |   20287    68729 |      --    4482       --      -- |     --   | -71/53
c |      4535 |   20287    68729 |    8114    3818   203736    53.4 |  1.754 % |
c |      4636 |   20287    68729 |    8926    3919   205922    52.5 |  1.796 % |
c ==============================================================================
c (current CPU-time: 7.33289 s)
c ==============================================================================
c [1mFound solution: 1660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4652 |   20642    69747 |    6192    3935   206182    52.4 |  1.796 % |
c   -- subsuming                       
c   -- var.elim.:  662/662          
c   -- var.elim.:  322/322          
c   -- var.elim.:  4/4          
c |      4652 |   20334    69224 |      --    3935       --      -- |     --   | -308/-522
c |      4652 |   20334    69224 |    8133    3935   206182    52.4 |  1.796 % |
c ==============================================================================
c (current CPU-time: 7.68683 s)
c ==============================================================================
c [1mFound solution: 1626[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4671 |   20376    69457 |    6112    3954   207201    52.4 |  1.796 % |
c   -- subsuming                       
c   -- var.elim.:  406/406          
c   -- var.elim.:  158/158          
c |      4671 |   20347    69488 |      --    3954       --      -- |     --   | -29/32
c |      4671 |   20347    69488 |    8138    3954 #### 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): 1.16 1.04 0.94 2/54 10577
Raw data (stat): 10577 (runsolver) R 10576 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422102019 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 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 s]
Raw data (loadavg): 1.13 1.04 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 3310 0 0 0 986 11 0 0 25 0 1 0 422102019 11616256 2253 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2836 2253 603 41 0 2795 0
vsize: 11344
[startup+20.001 s]
Raw data (loadavg): 1.11 1.04 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 3650 0 0 0 1985 12 0 0 25 0 1 0 422102019 12812288 2593 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3128 2593 603 41 0 3087 0
vsize: 12512
[startup+30.0018 s]
Raw data (loadavg): 1.09 1.04 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 4372 0 0 0 2982 15 0 0 25 0 1 0 422102019 15872000 3315 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3875 3315 603 41 0 3834 0
vsize: 15500
[startup+40.0024 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 5618 0 0 0 3979 19 0 0 25 0 1 0 422102019 20860928 4561 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5093 4561 603 41 0 5052 0
vsize: 20372
[startup+50.0026 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6207 0 0 0 4977 21 0 0 25 0 1 0 422102019 23269376 5150 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5681 5150 603 41 0 5640 0
vsize: 22724
[startup+60.0025 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6207 0 0 0 5977 21 0 0 25 0 1 0 422102019 23269376 5150 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5681 5150 603 41 0 5640 0
vsize: 22724
[startup+70.003 s]
Raw data (loadavg): 1.05 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6368 0 0 0 6976 22 0 0 25 0 1 0 422102019 23928832 5311 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5842 5311 603 41 0 5801 0
vsize: 23368
[startup+80.0032 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6752 0 0 0 7974 24 0 0 25 0 1 0 422102019 25489408 5695 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 5695 603 41 0 6182 0
vsize: 24892
[startup+90.004 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6752 0 0 0 8975 24 0 0 25 0 1 0 422102019 25489408 5695 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 5695 603 41 0 6182 0
vsize: 24892
[startup+100.004 s]
Raw data (loadavg): 1.18 1.06 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6752 0 0 0 9975 24 0 0 25 0 1 0 422102019 25489408 5695 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 5695 603 41 0 6182 0
vsize: 24892
[startup+110.004 s]
Raw data (loadavg): 1.15 1.06 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 6752 0 0 0 10975 24 0 0 25 0 1 0 422102019 25489408 5695 4294967295 134512640 134672761 3221224576 3221223760 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6223 5695 603 41 0 6182 0
vsize: 24892
[startup+120.005 s]
Raw data (loadavg): 1.13 1.05 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7024 0 0 0 11974 25 0 0 25 0 1 0 422102019 26681344 5967 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6514 5967 603 41 0 6473 0
vsize: 26056
[startup+130.004 s]
Raw data (loadavg): 1.11 1.05 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7131 0 0 0 12974 25 0 0 25 0 1 0 422102019 27017216 6074 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6596 6074 603 41 0 6555 0
vsize: 26384
[startup+140.004 s]
Raw data (loadavg): 1.09 1.05 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7131 0 0 0 13974 25 0 0 25 0 1 0 422102019 27017216 6074 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6596 6074 603 41 0 6555 0
vsize: 26384
[startup+150.005 s]
Raw data (loadavg): 1.08 1.05 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7131 0 0 0 14974 25 0 0 25 0 1 0 422102019 27017216 6074 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6596 6074 603 41 0 6555 0
vsize: 26384
[startup+160.005 s]
Raw data (loadavg): 1.06 1.05 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7131 0 0 0 15974 25 0 0 25 0 1 0 422102019 27017216 6074 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6596 6074 603 41 0 6555 0
vsize: 26384
[startup+170.005 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7498 0 0 0 16974 26 0 0 25 0 1 0 422102019 28610560 6441 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6985 6441 603 41 0 6944 0
vsize: 27940
[startup+180.005 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 17974 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+190.005 s]
Raw data (loadavg): 1.04 1.04 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 18974 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+200.006 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 19974 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+210.005 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 20974 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+220.006 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 21974 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+230.006 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 22975 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+240.007 s]
Raw data (loadavg): 1.02 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 23975 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+250.007 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 24975 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+260.007 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7556 0 0 0 25975 26 0 0 25 0 1 0 422102019 28794880 6499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7030 6499 603 41 0 6989 0
vsize: 28120
[startup+270.007 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7589 0 0 0 26975 26 0 0 25 0 1 0 422102019 29057024 6532 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7094 6532 603 41 0 7053 0
vsize: 28376
[startup+280.007 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7718 0 0 0 27975 26 0 0 25 0 1 0 422102019 29429760 6627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7185 6627 603 41 0 7144 0
vsize: 28740
[startup+290.008 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7718 0 0 0 28976 26 0 0 25 0 1 0 422102019 29429760 6627 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7185 6627 603 41 0 7144 0
vsize: 28740
[startup+300.008 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7718 0 0 0 29976 26 0 0 25 0 1 0 422102019 29429760 6627 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7185 6627 603 41 0 7144 0
vsize: 28740
[startup+310.008 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7718 0 0 0 30976 26 0 0 25 0 1 0 422102019 29429760 6627 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7185 6627 603 41 0 7144 0
vsize: 28740
[startup+320.009 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7724 0 0 0 31976 26 0 0 25 0 1 0 422102019 29593600 6633 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6633 603 41 0 7184 0
vsize: 28900
[startup+330.008 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7737 0 0 0 32976 26 0 0 25 0 1 0 422102019 29593600 6646 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7225 6646 603 41 0 7184 0
vsize: 28900
[startup+340.009 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7773 0 0 0 33977 26 0 0 25 0 1 0 422102019 29659136 6678 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6678 603 41 0 7200 0
vsize: 28964
[startup+350.009 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7773 0 0 0 34977 26 0 0 25 0 1 0 422102019 29659136 6678 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6678 603 41 0 7200 0
vsize: 28964
[startup+360.009 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7773 0 0 0 35977 26 0 0 25 0 1 0 422102019 29659136 6678 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6678 603 41 0 7200 0
vsize: 28964
[startup+370.01 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7773 0 0 0 36977 26 0 0 25 0 1 0 422102019 29659136 6678 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6678 603 41 0 7200 0
vsize: 28964
[startup+380.011 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 7773 0 0 0 37977 26 0 0 25 0 1 0 422102019 29659136 6678 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6678 603 41 0 7200 0
vsize: 28964
[startup+390.012 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8184 0 0 0 38976 28 0 0 25 0 1 0 422102019 31367168 7089 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 7089 603 41 0 7617 0
vsize: 30632
[startup+400.012 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8664 0 0 0 39975 30 0 0 25 0 1 0 422102019 33255424 7561 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8119 7561 603 41 0 8078 0
vsize: 32476
[startup+410.012 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8664 0 0 0 40975 30 0 0 25 0 1 0 422102019 33255424 7561 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8119 7561 603 41 0 8078 0
vsize: 32476
[startup+420.012 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8664 0 0 0 41975 30 0 0 25 0 1 0 422102019 33255424 7561 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8119 7561 603 41 0 8078 0
vsize: 32476
[startup+430.012 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8664 0 0 0 42975 30 0 0 25 0 1 0 422102019 33255424 7561 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8119 7561 603 41 0 8078 0
vsize: 32476
[startup+440.013 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 8664 0 0 0 43975 30 0 0 25 0 1 0 422102019 33255424 7561 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8119 7561 603 41 0 8078 0
vsize: 32476
[startup+450.013 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 9160 0 0 0 44974 31 0 0 25 0 1 0 422102019 35352576 8057 4294967295 134512640 134672761 3221224576 3221223568 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8631 8057 603 41 0 8590 0
vsize: 34524
[startup+460.013 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 9720 0 0 0 45972 34 0 0 25 0 1 0 422102019 37609472 8617 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9182 8617 603 41 0 9141 0
vsize: 36728
[startup+470.014 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10232 0 0 0 46971 35 0 0 25 0 1 0 422102019 39710720 9129 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9695 9129 603 41 0 9654 0
vsize: 38780
[startup+480.014 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 47969 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+490.014 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 48969 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223616 134612869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+500.014 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 49970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+510.014 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 50970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+520.014 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 51970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+530.014 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 52970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+540.015 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 53970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+550.015 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 10754 0 0 0 54970 37 0 0 25 0 1 0 422102019 41701376 9613 4294967295 134512640 134672761 3221224576 3221223616 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9613 603 41 0 10140 0
vsize: 40724
[startup+560.014 s]
Raw data (loadavg): 1.01 1.02 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11063 0 0 0 55970 37 0 0 25 0 1 0 422102019 43012096 9922 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10501 9922 603 41 0 10460 0
vsize: 42004
[startup+570.015 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11659 0 0 0 56968 39 0 0 25 0 1 0 422102019 45527040 10518 4294967295 134512640 134672761 3221224576 3221223760 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11115 10518 603 41 0 11074 0
vsize: 44460
[startup+580.015 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11840 0 0 0 57968 39 0 0 25 0 1 0 422102019 46084096 10688 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10688 603 41 0 11210 0
vsize: 45004
[startup+590.018 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11840 0 0 0 58969 39 0 0 25 0 1 0 422102019 46084096 10688 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10688 603 41 0 11210 0
vsize: 45004
[startup+600.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11840 0 0 0 59969 39 0 0 25 0 1 0 422102019 46084096 10688 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10688 603 41 0 11210 0
vsize: 45004
[startup+610.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11841 0 0 0 60969 39 0 0 25 0 1 0 422102019 46084096 10689 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10689 603 41 0 11210 0
vsize: 45004
[startup+620.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11841 0 0 0 61969 39 0 0 25 0 1 0 422102019 46084096 10689 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10689 603 41 0 11210 0
vsize: 45004
[startup+630.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11841 0 0 0 62970 39 0 0 25 0 1 0 422102019 46084096 10689 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10689 603 41 0 11210 0
vsize: 45004
[startup+640.018 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 11842 0 0 0 63970 39 0 0 25 0 1 0 422102019 46084096 10690 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11251 10690 603 41 0 11210 0
vsize: 45004
[startup+650.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12068 0 0 0 64969 40 0 0 25 0 1 0 422102019 47026176 10916 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11481 10916 603 41 0 11440 0
vsize: 45924
[startup+660.019 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12651 0 0 0 65967 42 0 0 25 0 1 0 422102019 49405952 11499 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12062 11499 603 41 0 12021 0
vsize: 48248
[startup+670.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12811 0 0 0 66967 42 0 0 25 0 1 0 422102019 49876992 11617 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11617 603 41 0 12136 0
vsize: 48708
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12811 0 0 0 67967 42 0 0 25 0 1 0 422102019 49876992 11617 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11617 603 41 0 12136 0
vsize: 48708
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12811 0 0 0 68968 42 0 0 25 0 1 0 422102019 49876992 11617 4294967295 134512640 134672761 3221224576 3221223760 134615544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11617 603 41 0 12136 0
vsize: 48708
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12811 0 0 0 69968 42 0 0 25 0 1 0 422102019 49876992 11617 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11617 603 41 0 12136 0
vsize: 48708
[startup+710.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12812 0 0 0 70968 42 0 0 25 0 1 0 422102019 49876992 11618 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11618 603 41 0 12136 0
vsize: 48708
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12812 0 0 0 71968 42 0 0 25 0 1 0 422102019 49876992 11618 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11618 603 41 0 12136 0
vsize: 48708
[startup+730.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12812 0 0 0 72968 42 0 0 25 0 1 0 422102019 49876992 11618 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11618 603 41 0 12136 0
vsize: 48708
[startup+740.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12812 0 0 0 73969 42 0 0 25 0 1 0 422102019 49876992 11618 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11618 603 41 0 12136 0
vsize: 48708
[startup+750.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 74969 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223740 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+760.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 75969 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+770.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 76969 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+780.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 77969 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+790.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 78970 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+800.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 79970 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+810.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 80970 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+820.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12830 0 0 0 81970 42 0 0 25 0 1 0 422102019 49889280 11624 4294967295 134512640 134672761 3221224576 3221223760 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12180 11624 603 41 0 12139 0
vsize: 48720
[startup+830.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 12958 0 0 0 82970 43 0 0 25 0 1 0 422102019 50417664 11752 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12309 11752 603 41 0 12268 0
vsize: 49236
[startup+840.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 83969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+850.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 84969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+860.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 85969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+870.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 86969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+880.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 87969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+890.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 88969 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+900.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 89970 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 90970 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+920.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 91970 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13505 0 0 0 92970 44 0 0 25 0 1 0 422102019 52477952 12257 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12257 603 41 0 12771 0
vsize: 51248
[startup+940.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13507 0 0 0 93970 44 0 0 25 0 1 0 422102019 52477952 12259 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12812 12259 603 41 0 12771 0
vsize: 51248
[startup+950.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13858 0 0 0 94969 46 0 0 25 0 1 0 422102019 53936128 12610 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13168 12610 603 41 0 13127 0
vsize: 52672
[startup+960.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13962 0 0 0 95969 46 0 0 25 0 1 0 422102019 54177792 12668 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12668 603 41 0 13186 0
vsize: 52908
[startup+970.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13962 0 0 0 96969 46 0 0 25 0 1 0 422102019 54177792 12668 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12668 603 41 0 13186 0
vsize: 52908
[startup+980.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 97970 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+990.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 98970 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 99970 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 100970 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 101970 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 102971 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 103971 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13963 0 0 0 104971 46 0 0 25 0 1 0 422102019 54177792 12669 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12669 603 41 0 13186 0
vsize: 52908
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 13965 0 0 0 105971 46 0 0 25 0 1 0 422102019 54177792 12671 4294967295 134512640 134672761 3221224576 3221223616 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12671 603 41 0 13186 0
vsize: 52908
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 106971 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223616 134603565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 107971 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 108972 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 109972 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 110972 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 111972 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 112973 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 113973 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 114973 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14012 0 0 0 115973 46 0 0 25 0 1 0 422102019 54177792 12672 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12672 603 41 0 13186 0
vsize: 52908
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14014 0 0 0 116973 46 0 0 25 0 1 0 422102019 54177792 12674 4294967295 134512640 134672761 3221224576 3221223760 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12674 603 41 0 13186 0
vsize: 52908
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14014 0 0 0 117973 46 0 0 25 0 1 0 422102019 54177792 12674 4294967295 134512640 134672761 3221224576 3221223616 134614307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12674 603 41 0 13186 0
vsize: 52908
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14014 0 0 0 118974 46 0 0 25 0 1 0 422102019 54177792 12674 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12674 603 41 0 13186 0
vsize: 52908
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10577
Raw data (stat): 10577 (minisat+) R 10576 5897 5896 0 -1 0 14014 0 0 0 119974 46 0 0 25 0 1 0 422102019 54177792 12674 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13227 12674 603 41 0 13186 0
vsize: 52908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 10577
Raw data (stat): 10577 (minisat+) Z 10576 5897 5896 0 -1 12 14015 0 0 0 119974 49 0 0 25 0 1 0 422102019 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.07
CPU time (s): 1200.24
CPU user time (s): 1199.75
CPU system time (s): 0.492925
CPU usage (%): 100.014
Max. virtual memory (Kb): 52908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####