PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUM	a3dd3cd7dd293e24bffaff8bb73da54c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 15400

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        821868 kB
Buffers:         15472 kB
Cached:         177460 kB
SwapCached:        732 kB
Active:          24616 kB
Inactive:       170284 kB
HighTotal:      131008 kB
HighFree:         2072 kB
LowTotal:       903652 kB
LowFree:        819796 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            12328 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:36:38 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 17690 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> Adder-cost: 114   maxlim: 59   bits: 6/6
c ---[ 233]---> Adder-cost: 114   maxlim: 59   bits: 6/6
c ---[ 200]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 197]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 195]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 193]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 191]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 189]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 187]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 185]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 183]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 181]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 179]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[ 176]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 174]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[ 172]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[ 170]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 168]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[ 166]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 164]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 162]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 160]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[ 158]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 155]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[ 153]---> Adder-cost: 28   maxlim: 8   bits: 5/4
c ---[ 151]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 149]---> Adder-cost: 26   maxlim: 8   bits: 5/4
c ---[ 147]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 145]---> Adder-cost: 30   maxlim: 8   bits: 5/4
c ---[ 144]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 143]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 142]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 141]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 139]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 138]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 137]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 136]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 135]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 134]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 133]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 132]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[ 131]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 130]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 128]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 127]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 126]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 125]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 124]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 123]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 122]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 121]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 120]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 119]---> Adder-cost: 22   maxlim: 16   bits: 5/5
c ---[ 117]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 116]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 115]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 114]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 113]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 112]---> Adder-cost: 22   maxlim: 16   bits: 5/5
c ---[ 111]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 110]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 109]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 108]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 106]---> Adder-cost: 30   maxlim: 26   bits: 5/5
c ---[ 104]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 103]---> Adder-cost: 24   maxlim: 16   bits: 5/5
c ---[ 102]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 101]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[ 100]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  99]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  98]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  97]---> Adder-cost: 20   maxlim: 16   bits: 5/5
c ---[  96]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  95]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  93]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  92]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  91]---> Adder-cost: 16   maxlim: 16   bits: 5/5
c ---[  81]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[  69]---> Adder-cost: 30   maxlim: 26   bits: 5/5
c ---[  57]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[  45]---> Adder-cost: 34   maxlim: 26   bits: 5/5
c ---[  33]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[  21]---> Adder-cost: 32   maxlim: 26   bits: 5/5
c ---[  10]---> Adder-cost: 58   maxlim: 59   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23690    90323 |    7896       0        0     nan |  0.000 % |
c |       101 |   23656    90205 |    8685      99      398     4.0 | 16.870 % |
c |       251 |   23632    90123 |    9554     247     1233     5.0 | 16.962 % |
c |       476 |   23567    89900 |   10509     464     2689     5.8 | 17.170 % |
c |       813 |   23431    89438 |   11560     794     6014     7.6 | 17.493 % |
c |      1319 |   23186    88593 |   12716    1279    11403     8.9 | 18.253 % |
c |      2079 |   22724    87026 |   13988    2004    24337    12.1 | 19.820 % |
c |      3222 |   21976    84430 |   15387    3063    43519    14.2 | 22.263 % |
c |      4930 |   21419    82485 |   16925    4720   107948    22.9 | 23.807 % |
c ==============================================================================
c [1mFound solution: 1666048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 27   maxlim: 3367   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5459 |   21118    81436 |    7039    5213   124733    23.9 | 23.807 % |
c |      5559 |   20969    80925 |    7742    5299   127557    24.1 | 25.578 % |
c ==============================================================================
c [1mFound solution: 1618048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 35   maxlim: 3742   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5702 |   21176    81686 |    7058    5442   135055    24.8 | 25.578 % |
c |      5803 |   21117    81483 |    7763    5542   137125    24.7 | 25.708 % |
c |      5956 |   20893    80701 |    8540    5684   141510    24.9 | 26.365 % |
c |      6182 |   20893    80701 |    9394    5910   151509    25.6 | 26.365 % |
c ==============================================================================
c [1mFound solution: 1611648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 25   maxlim: 3792   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6433 |   20894    80712 |    6964    6155   161879    26.3 | 26.365 % |
c |      6533 |   20843    80531 |    7660    6252   162929    26.1 | 26.872 % |
c |      6684 |   20768    80270 |    8426    6402   171083    26.7 | 27.119 % |
c ==============================================================================
c [1mFound solution: 1607808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 17   maxlim: 3822   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6799 |   20721    80135 |    6907    6511   174719    26.8 | 27.119 % |
c |      6899 |   20721    80135 |    7597    6611   181985    27.5 | 27.614 % |
c ==============================================================================
c [1mFound solution: 1604608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 15   maxlim: 3847   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6996 |   20788    80366 |    6929    6708   189168    28.2 | 27.614 % |
c |      7096 |   20788    80366 |    7621    6808   191226    28.1 | 27.602 % |
c |      7246 |   20788    80366 |    8384    6958   191775    27.6 | 27.602 % |
c |      7472 |   20788    80366 |    9222    7184   204038    28.4 | 27.602 % |
c ==============================================================================
c [1mFound solution: 1527168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 4452   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7616 |   20901    80768 |    6967    7328   220092    30.0 | 27.602 % |
c |      7717 |   20853    80602 |    7663    7426   221580    29.8 | 27.672 % |
c |      7870 |   20853    80602 |    8430    7579   228180    30.1 | 27.672 % |
c |      8097 |   20853    80602 |    9273    7806   242241    31.0 | 27.672 % |
c |      8436 |   20853    80602 |   10200    8145   278339    34.2 | 27.672 % |
c |      8943 |   20853    80602 |   11220    8652   332421    38.4 | 27.672 % |
c ==============================================================================
c [1mFound solution: 1526528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 4457   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9195 |   20961    80989 |    6987    8904   344803    38.7 | 27.672 % |
c |      9295 |   20961    80989 |    7685    4552   192402    42.3 | 27.622 % |
c |      9446 |   20961    80989 |    8454    4703   204741    43.5 | 27.622 % |
c |      9672 |   20961    80989 |    9299    4929   209433    42.5 | 27.622 % |
c |     10010 |   20952    80958 |   10229    5265   263234    50.0 | 27.644 % |
c |     10517 |   20952    80958 |   11252    5772   286425    49.6 | 27.644 % |
c ==============================================================================
c [1mFound solution: 1523328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 4482   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11079 |   21050    81300 |    7016    6334   345674    54.6 | 27.644 % |
c |     11182 |   21050    81300 |    7717    6437   353462    54.9 | 27.578 % |
c ==============================================================================
c [1mFound solution: 1511808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 4572   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11290 |   21160    81723 |    7053    6545   364895    55.8 | 27.578 % |
c |     11391 |   21160    81723 |    7758    6646   366317    55.1 | 27.578 % |
c |     11541 |   21160    81723 |    8534    6796   376781    55.4 | 27.578 % |
c ==============================================================================
c [1mFound solution: 1502208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 20   maxlim: 4647   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11753 |   21238    81986 |    7079    7008   389263    55.5 | 27.578 % |
c |     11855 |   21238    81986 |    7786    7110   395140    55.6 | 27.522 % |
c |     12008 |   21238    81986 |    8565    7263   412654    56.8 | 27.522 % |
c |     12234 |   21238    81986 |    9422    7489   426498    56.9 | 27.522 % |
c ==============================================================================
c [1mFound solution: 1495808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 18   maxlim: 4697   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12335 |   21323    82299 |    7107    7590   440032    58.0 | 27.522 % |
c |     12435 |   21323    82299 |    7817    7690   442600    57.6 | 27.503 % |
c |     12586 |   21323    82299 |    8599    7841   455264    58.1 | 27.503 % |
c |     12813 |   21323    82299 |    9459    8068   465347    57.7 | 27.503 % |
c |     13150 |   21323    82299 |   10405    8405   486709    57.9 | 27.503 % |
c |     13658 |   21323    82299 |   11445    8913   564421    63.3 | 27.503 % |
c |     14420 |   21323    82299 |   12590    9675   611768    63.2 | 27.503 % |
c |     15559 |   21323    82299 |   13849   10814   678973    62.8 | 27.503 % |
c ==============================================================================
c [1mFound solution: 1466368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 14   maxlim: 4927   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16935 |   21386    82517 |    7128   12190   872473    71.6 | 27.503 % |
c |     17038 |   21386    82517 |    7840    6198   364046    58.7 | 27.482 % |
c |     17188 |   21386    82517 |    8624    6348   379821    59.8 | 27.482 % |
c |     17413 |   21386    82517 |    9487    6573   383285    58.3 | 27.482 % |
c |     17750 |   21386    82517 |   10436    6910   391183    56.6 | 27.482 % |
c |     18256 |   21386    82517 |   11479    7416   463774    62.5 | 27.482 % |
c |     19015 |   21379    82494 |   12627    8174   511713    62.6 | 27.504 % |
c |     20154 |   21379    82494 |   13890    9313   660807    71.0 | 27.504 % |
c |     21863 |   21379    82494 |   15279   11022   915355    83.0 | 27.504 % |
c |     24425 |   21355    82412 |   16807   13579  1286232    94.7 | 27.589 % |
c |     28271 |   21329    82322 |   18488   17418  1691881    97.1 | 27.675 % |
c |     34037 |   21283    82163 |   20337   13137  1053406    80.2 | 27.803 % |
c |     42686 |   21209    81911 |   22370   21765  2177098   100.0 | 27.995 % |
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 22   maxlim: 5382   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48952 |   21252    82068 |    7084   15818  1270194    80.3 | 27.995 % |
c |     49052 |   21252    82068 |    7792    8009   454599    56.8 | 28.041 % |
c |     49202 |   21237    82017 |    8571    8156   457000    56.0 | 28.083 % |
c |     49427 |   21230    81994 |    9428    8379   468424    55.9 | 28.104 % |
c |     49765 |   21230    81994 |   10371    8717   485383    55.7 | 28.104 % |
c |     50271 |   21215    81941 |   11408    9217   522471    56.7 | 28.126 % |
c |     51030 |   21215    81941 |   12549    9976   580843    58.2 | 28.126 % |
c |     52169 |   21215    81941 |   13804   11115   656686    59.1 | 28.126 % |
c |     53877 |   21206    81912 |   15185   12822   765841    59.7 | 28.168 % |
c |     56440 |   21179    81821 |   16703   15378   944262    61.4 | 28.253 % |
c |     60284 |   21160    81754 |   18374   19217  1435945    74.7 | 28.295 % |
c |     66050 |   21151    81723 |   20211   14526  1132542    78.0 | 28.317 % |
c |     74700 |   21110    81582 |   22232   12126   988177    81.5 | 28.444 % |
c |     87674 |   21098    81540 |   24455   13161  1421581   108.0 | 28.465 % |
c |    107136 |   21083    81487 |   26901   19136  1702471    89.0 | 28.487 % |
c |    136330 |   21059    81405 |   29591   18944  1444744    76.3 | 28.550 % |
c |    180122 |   21047    81363 |   32550   30196  3041287   100.7 | 28.571 % |
c |    245807 |   20935    80973 |   35805   26413  2462005    93.2 | 28.826 % |
c |    344334 |   20917    80911 |   39386   21232  1819747    85.7 | 28.869 % |
#### 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.92 0.98 0.93 2/54 29039
Raw data (stat): 29039 (runsolver) R 29038 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542140062 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 1362 0 0 0 994 3 0 0 25 0 1 0 542140062 7286784 1339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1779 1339 603 41 0 1738 0
vsize: 7116
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 1829 0 0 0 1992 5 0 0 25 0 1 0 542140062 9162752 1806 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2237 1806 603 41 0 2196 0
vsize: 8948
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 2688 0 0 0 2989 8 0 0 25 0 1 0 542140062 12845056 2665 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3136 2665 603 41 0 3095 0
vsize: 12544
[startup+40.001 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3082 0 0 0 3988 9 0 0 25 0 1 0 542140062 14323712 3059 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3059 603 41 0 3456 0
vsize: 13988
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3082 0 0 0 4988 9 0 0 25 0 1 0 542140062 14323712 3059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3059 603 41 0 3456 0
vsize: 13988
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3541 0 0 0 5986 11 0 0 25 0 1 0 542140062 16187392 3518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3952 3518 603 41 0 3911 0
vsize: 15808
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 6986 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 7986 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 8986 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 9986 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 10987 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 3552 0 0 0 11987 11 0 0 25 0 1 0 542140062 16318464 3529 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3984 3529 603 41 0 3943 0
vsize: 15936
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4003 0 0 0 12986 13 0 0 25 0 1 0 542140062 18186240 3980 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4440 3980 603 41 0 4399 0
vsize: 17760
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4003 0 0 0 13986 13 0 0 25 0 1 0 542140062 18186240 3980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4440 3980 603 41 0 4399 0
vsize: 17760
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4010 0 0 0 14986 13 0 0 25 0 1 0 542140062 18186240 3987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4440 3987 603 41 0 4399 0
vsize: 17760
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4192 0 0 0 15985 14 0 0 25 0 1 0 542140062 18853888 4169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4169 603 41 0 4562 0
vsize: 18412
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4192 0 0 0 16985 14 0 0 25 0 1 0 542140062 18853888 4169 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4169 603 41 0 4562 0
vsize: 18412
[startup+180.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4192 0 0 0 17985 14 0 0 25 0 1 0 542140062 18853888 4169 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4169 603 41 0 4562 0
vsize: 18412
[startup+190.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4195 0 0 0 18986 14 0 0 25 0 1 0 542140062 18853888 4172 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4172 603 41 0 4562 0
vsize: 18412
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4195 0 0 0 19986 14 0 0 25 0 1 0 542140062 18853888 4172 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4172 603 41 0 4562 0
vsize: 18412
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4195 0 0 0 20986 14 0 0 25 0 1 0 542140062 18853888 4172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4172 603 41 0 4562 0
vsize: 18412
[startup+220.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4195 0 0 0 21986 14 0 0 25 0 1 0 542140062 18853888 4172 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4172 603 41 0 4562 0
vsize: 18412
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4195 0 0 0 22986 14 0 0 25 0 1 0 542140062 18853888 4172 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4172 603 41 0 4562 0
vsize: 18412
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4196 0 0 0 23987 14 0 0 25 0 1 0 542140062 18853888 4173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4603 4173 603 41 0 4562 0
vsize: 18412
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4427 0 0 0 24986 14 0 0 25 0 1 0 542140062 19795968 4404 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4833 4404 603 41 0 4792 0
vsize: 19332
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4430 0 0 0 25986 15 0 0 25 0 1 0 542140062 19935232 4407 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4867 4407 603 41 0 4826 0
vsize: 19468
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4448 0 0 0 26986 15 0 0 25 0 1 0 542140062 19935232 4425 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4867 4425 603 41 0 4826 0
vsize: 19468
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4803 0 0 0 27986 15 0 0 25 0 1 0 542140062 21405696 4780 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5226 4780 603 41 0 5185 0
vsize: 20904
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4809 0 0 0 28986 15 0 0 25 0 1 0 542140062 21405696 4786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5226 4786 603 41 0 5185 0
vsize: 20904
[startup+300.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4816 0 0 0 29986 15 0 0 25 0 1 0 542140062 21540864 4793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5259 4793 603 41 0 5218 0
vsize: 21036
[startup+310.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 4820 0 0 0 30986 16 0 0 25 0 1 0 542140062 21540864 4797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5259 4797 603 41 0 5218 0
vsize: 21036
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5081 0 0 0 31985 16 0 0 25 0 1 0 542140062 22740992 5058 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5058 603 41 0 5511 0
vsize: 22208
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5081 0 0 0 32985 17 0 0 25 0 1 0 542140062 22740992 5058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5058 603 41 0 5511 0
vsize: 22208
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5081 0 0 0 33985 17 0 0 25 0 1 0 542140062 22740992 5058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5058 603 41 0 5511 0
vsize: 22208
[startup+350.004 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 34985 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+360.003 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 35985 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+370.003 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 36985 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+380.003 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 37985 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+390.003 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 38985 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+400.004 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5096 0 0 0 39986 17 0 0 25 0 1 0 542140062 22740992 5073 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+410.004 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5097 0 0 0 40986 17 0 0 25 0 1 0 542140062 22740992 5074 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5074 603 41 0 5511 0
vsize: 22208
[startup+420.004 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5097 0 0 0 41986 17 0 0 25 0 1 0 542140062 22740992 5074 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5074 603 41 0 5511 0
vsize: 22208
[startup+430.004 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5103 0 0 0 42986 17 0 0 25 0 1 0 542140062 22740992 5080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5080 603 41 0 5511 0
vsize: 22208
[startup+440.004 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5115 0 0 0 43986 17 0 0 25 0 1 0 542140062 22884352 5092 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5587 5092 603 41 0 5546 0
vsize: 22348
[startup+450.005 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5136 0 0 0 44987 17 0 0 25 0 1 0 542140062 22884352 5113 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5587 5113 603 41 0 5546 0
vsize: 22348
[startup+460.004 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5321 0 0 0 45986 17 0 0 25 0 1 0 542140062 23748608 5298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5798 5298 603 41 0 5757 0
vsize: 23192
[startup+470.004 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5440 0 0 0 46986 18 0 0 25 0 1 0 542140062 24285184 5417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5929 5417 603 41 0 5888 0
vsize: 23716
[startup+480.003 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5440 0 0 0 47986 18 0 0 25 0 1 0 542140062 24285184 5417 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5929 5417 603 41 0 5888 0
vsize: 23716
[startup+490.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5465 0 0 0 48987 18 0 0 25 0 1 0 542140062 24420352 5442 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5962 5442 603 41 0 5921 0
vsize: 23848
[startup+500.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5497 0 0 0 49986 18 0 0 25 0 1 0 542140062 24584192 5474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5474 603 41 0 5961 0
vsize: 24008
[startup+510.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5506 0 0 0 50986 18 0 0 25 0 1 0 542140062 24584192 5483 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5483 603 41 0 5961 0
vsize: 24008
[startup+520.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5531 0 0 0 51986 18 0 0 25 0 1 0 542140062 24748032 5508 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6042 5508 603 41 0 6001 0
vsize: 24168
[startup+530.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5625 0 0 0 52986 18 0 0 25 0 1 0 542140062 25014272 5602 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6107 5602 603 41 0 6066 0
vsize: 24428
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5858 0 0 0 53986 19 0 0 25 0 1 0 542140062 26075136 5835 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6366 5835 603 41 0 6325 0
vsize: 25464
[startup+550.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5858 0 0 0 54986 19 0 0 25 0 1 0 542140062 26075136 5835 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6366 5835 603 41 0 6325 0
vsize: 25464
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5877 0 0 0 55986 19 0 0 25 0 1 0 542140062 26075136 5854 4294967295 134512640 134672761 3221224544 3221223728 134558697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6366 5854 603 41 0 6325 0
vsize: 25464
[startup+570.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5878 0 0 0 56986 19 0 0 25 0 1 0 542140062 26075136 5855 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6366 5855 603 41 0 6325 0
vsize: 25464
[startup+580.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5878 0 0 0 57986 19 0 0 25 0 1 0 542140062 26075136 5855 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6366 5855 603 41 0 6325 0
vsize: 25464
[startup+590.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 5937 0 0 0 58986 20 0 0 25 0 1 0 542140062 26345472 5914 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6432 5914 603 41 0 6391 0
vsize: 25728
[startup+600.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6250 0 0 0 59985 21 0 0 25 0 1 0 542140062 27672576 6227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6756 6227 603 41 0 6715 0
vsize: 27024
[startup+610.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6251 0 0 0 60985 21 0 0 25 0 1 0 542140062 27672576 6228 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6756 6228 603 41 0 6715 0
vsize: 27024
[startup+620.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6256 0 0 0 61986 21 0 0 25 0 1 0 542140062 27672576 6233 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6756 6233 603 41 0 6715 0
vsize: 27024
[startup+630.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6268 0 0 0 62986 21 0 0 25 0 1 0 542140062 27672576 6245 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6756 6245 603 41 0 6715 0
vsize: 27024
[startup+640.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6284 0 0 0 63986 21 0 0 25 0 1 0 542140062 27832320 6261 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6795 6261 603 41 0 6754 0
vsize: 27180
[startup+650.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6293 0 0 0 64986 21 0 0 25 0 1 0 542140062 27832320 6270 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6795 6270 603 41 0 6754 0
vsize: 27180
[startup+660.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6587 0 0 0 65986 21 0 0 25 0 1 0 542140062 29044736 6564 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7091 6564 603 41 0 7050 0
vsize: 28364
[startup+670.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6596 0 0 0 66986 22 0 0 25 0 1 0 542140062 29044736 6573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7091 6573 603 41 0 7050 0
vsize: 28364
[startup+680.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6598 0 0 0 67986 22 0 0 25 0 1 0 542140062 29044736 6575 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7091 6575 603 41 0 7050 0
vsize: 28364
[startup+690.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6599 0 0 0 68986 22 0 0 25 0 1 0 542140062 29044736 6576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7091 6576 603 41 0 7050 0
vsize: 28364
[startup+700.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6599 0 0 0 69986 22 0 0 25 0 1 0 542140062 29044736 6576 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7091 6576 603 41 0 7050 0
vsize: 28364
[startup+710.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6609 0 0 0 70986 22 0 0 25 0 1 0 542140062 29204480 6586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6586 603 41 0 7089 0
vsize: 28520
[startup+720.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 71987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+730.006 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 72987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+740.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 73987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+750.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 74987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+760.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 75987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+770.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 76987 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+780.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6610 0 0 0 77988 22 0 0 25 0 1 0 542140062 29204480 6587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7130 6587 603 41 0 7089 0
vsize: 28520
[startup+790.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6611 0 0 0 78987 22 0 0 25 0 1 0 542140062 29204480 6588 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6588 603 41 0 7089 0
vsize: 28520
[startup+800.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6611 0 0 0 79987 22 0 0 25 0 1 0 542140062 29204480 6588 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6588 603 41 0 7089 0
vsize: 28520
[startup+810.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6612 0 0 0 80988 22 0 0 25 0 1 0 542140062 29204480 6589 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6589 603 41 0 7089 0
vsize: 28520
[startup+820.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6612 0 0 0 81988 22 0 0 25 0 1 0 542140062 29204480 6589 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6589 603 41 0 7089 0
vsize: 28520
[startup+830.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6612 0 0 0 82988 22 0 0 25 0 1 0 542140062 29204480 6589 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6589 603 41 0 7089 0
vsize: 28520
[startup+840.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6616 0 0 0 83988 22 0 0 25 0 1 0 542140062 29204480 6593 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6593 603 41 0 7089 0
vsize: 28520
[startup+850.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 84988 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+860.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 85988 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+870.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 86989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+880.005 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 87989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+890.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 88989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+900.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 89989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+910.004 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 90989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+920.003 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 91989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+930.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 92989 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+940.002 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 93990 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+950.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 94990 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+960.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6617 0 0 0 95990 22 0 0 25 0 1 0 542140062 29204480 6594 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6594 603 41 0 7089 0
vsize: 28520
[startup+970.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6627 0 0 0 96990 22 0 0 25 0 1 0 542140062 29204480 6604 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6604 603 41 0 7089 0
vsize: 28520
[startup+980.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6628 0 0 0 97990 22 0 0 25 0 1 0 542140062 29204480 6605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6605 603 41 0 7089 0
vsize: 28520
[startup+990.001 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6628 0 0 0 98990 22 0 0 25 0 1 0 542140062 29204480 6605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7130 6605 603 41 0 7089 0
vsize: 28520
[startup+1000 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6628 0 0 0 99990 22 0 0 25 0 1 0 542140062 29204480 6605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6605 603 41 0 7089 0
vsize: 28520
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6628 0 0 0 100990 22 0 0 25 0 1 0 542140062 29204480 6605 4294967295 134512640 134672761 3221224544 3221223704 134559749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6605 603 41 0 7089 0
vsize: 28520
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 101990 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 102990 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 103990 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1050 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 104991 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1060 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 105991 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1070 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6630 0 0 0 106991 22 0 0 25 0 1 0 542140062 29204480 6607 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6607 603 41 0 7089 0
vsize: 28520
[startup+1080 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 107991 22 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1090 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 108991 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1100 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 109991 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223648 134560269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1110 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 110991 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1120 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 111991 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1130 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 112992 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1140 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 113992 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223648 134554988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1150 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6631 0 0 0 114992 23 0 0 25 0 1 0 542140062 29204480 6608 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7130 6608 603 41 0 7089 0
vsize: 28520
[startup+1160 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 6998 0 0 0 115991 24 0 0 25 0 1 0 542140062 30801920 6975 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7520 6975 603 41 0 7479 0
vsize: 30080
[startup+1170 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 7178 0 0 0 116991 24 0 0 25 0 1 0 542140062 31461376 7155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7155 603 41 0 7640 0
vsize: 30724
[startup+1180 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 7178 0 0 0 117991 24 0 0 25 0 1 0 542140062 31461376 7155 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7155 603 41 0 7640 0
vsize: 30724
[startup+1190 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 7178 0 0 0 118991 24 0 0 25 0 1 0 542140062 31461376 7155 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7155 603 41 0 7640 0
vsize: 30724
[startup+1200 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 29039
Raw data (stat): 29039 (minisat+) R 29038 28099 28098 0 -1 0 7178 0 0 0 119991 24 0 0 25 0 1 0 542140062 31461376 7155 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7155 603 41 0 7640 0
vsize: 30724
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 29039
Raw data (stat): 29039 (minisat+) Z 29038 28099 28098 0 -1 12 7181 0 0 0 119991 25 0 0 25 0 1 0 542140062 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.01
CPU time (s): 1200.18
CPU user time (s): 1199.92
CPU system time (s): 0.25996
CPU usage (%): 100.014
Max. virtual memory (Kb): 30724
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####