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/routing/normalized-s4-4-3-4pb.opb
MD5SUM	c1a86b94297136b91215b2ae8a8f5643
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	60
Optimality of the best value was proved	NO
Number of terms in the objective function	696
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	696
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	696
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	696
Total number of constraints	2096
Number of constraints which are clauses	2072
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	29
Trace number 5193

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        910636 kB
Buffers:         34888 kB
Cached:          67892 kB
SwapCached:       2144 kB
Active:          60740 kB
Inactive:        47028 kB
HighTotal:      131008 kB
HighFree:        59248 kB
LowTotal:       903652 kB
LowFree:        851388 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10696 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:41:44 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3624 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2096 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2082]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2056]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2034]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2024]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2022]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1996]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1978]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1952]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1950]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1924]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1906]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1880]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1866]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1818]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1794]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1768]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1746]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1699]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1671]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1637]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1557]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1535]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1529]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1474]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1464]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1452]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1428]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1390]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1269]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1209]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1191]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1112]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1029]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1023]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 991]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 965]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 963]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 953]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 951]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 925]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 907]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 881]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 879]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 853]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 835]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 760]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 750]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 738]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 732]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 676]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 629]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 589]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 571]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 533]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 513]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 503]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 414]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 392]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 386]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 370]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 360]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 149]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  22]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  21]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  20]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  19]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  18]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  17]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  16]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  15]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  14]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  13]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  12]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  11]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[  10]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   9]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   8]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   7]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   6]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   5]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   4]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   3]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   2]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   1]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ---[   0]---> Adder-cost: 50   maxlim: 25   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9940    34286 |    3313       0        0     nan |  0.000 % |
c |       100 |    9894    34136 |    3644      92      484     5.3 | 19.929 % |
c |       250 |    9856    34008 |    4008     236     1268     5.4 | 20.194 % |
c |       475 |    9755    33672 |    4409     445     2563     5.8 | 20.988 % |
c |       813 |    9508    32839 |    4850     734     4087     5.6 | 22.928 % |
c |      1319 |    9262    32007 |    5335    1198     7269     6.1 | 24.780 % |
c |      2078 |    9231    31901 |    5869    1950    17325     8.9 | 25.000 % |
c |      3217 |    9044    31267 |    6456    3047    33765    11.1 | 26.455 % |
c |      4926 |    8843    30590 |    7101    4702    70473    15.0 | 28.042 % |
c |      7488 |    8747    30263 |    7811    7233   135255    18.7 | 28.660 % |
c |     11334 |    8565    29646 |    8593    6766   132889    19.6 | 29.982 % |
c |     17101 |    8556    29617 |    9452    7781   172222    22.1 | 30.071 % |
c |     25750 |    8556    29617 |   10397    6217   108164    17.4 | 30.071 % |
c |     38725 |    8485    29379 |   11437    8021   148534    18.5 | 30.644 % |
c |     58186 |    8447    29247 |   12581    9082   155244    17.1 | 30.908 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1358   maxlim: 620   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76106 |   17741    62479 |    5913    6991   101770    14.6 | 30.908 % |
c |     76206 |   17741    62479 |    6504    3596    45196    12.6 | 20.353 % |
c |     76358 |   17741    62479 |    7154    3748    47945    12.8 | 20.353 % |
c |     76585 |   17732    62448 |    7870    3973    50962    12.8 | 20.380 % |
c |     76923 |   17732    62448 |    8657    4311    59694    13.8 | 20.380 % |
c |     77429 |   17732    62448 |    9522    4817    69997    14.5 | 20.380 % |
c |     78188 |   17732    62448 |   10475    5576    93623    16.8 | 20.380 % |
c |     79327 |   17724    62418 |   11522    6714   118513    17.7 | 20.408 % |
c |     81035 |   17724    62418 |   12675    8422   152609    18.1 | 20.408 % |
c |     83599 |   17715    62387 |   13942   10982   342961    31.2 | 20.435 % |
c |     87443 |   17684    62280 |   15336   14818   821434    55.4 | 20.490 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1094   maxlim: 620   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90228 |   25292    89454 |    8430    9215   741309    80.4 | 20.490 % |
c |     90330 |   25292    89454 |    9273    4710   236078    50.1 | 15.920 % |
c |     90482 |   25292    89454 |   10200    4862   240351    49.4 | 15.920 % |
c |     90708 |   25292    89454 |   11220    5088   244512    48.1 | 15.920 % |
c |     91045 |   25292    89454 |   12342    5425   249536    46.0 | 15.920 % |
c |     91552 |   25292    89454 |   13576    5932   258135    43.5 | 15.920 % |
c |     92315 |   25292    89454 |   14934    6695   273496    40.9 | 15.920 % |
c |     93454 |   25292    89454 |   16427    7834   292538    37.3 | 15.920 % |
c |     95163 |   25292    89454 |   18070    9543   328180    34.4 | 15.920 % |
c |     97727 |   25292    89454 |   19877   12107   565087    46.7 | 15.920 % |
c |    101571 |   25276    89402 |   21865   15948   808291    50.7 | 15.983 % |
c |    107337 |   25233    89255 |   24051   21701  1119023    51.6 | 16.068 % |
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1130   maxlim: 620   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    112033 |   33079   117277 |   11026   13890   539017    38.8 | 16.068 % |
c |    112133 |   33079   117277 |   12128    7045   206845    29.4 | 13.129 % |
c |    112285 |   33014   117042 |   13341    7130   207579    29.1 | 13.180 % |
c |    112511 |   33014   117042 |   14675    7356   211278    28.7 | 13.180 % |
c |    112848 |   33014   117042 |   16143    7693   227247    29.5 | 13.180 % |
c |    113356 |   33014   117042 |   17757    8201   245361    29.9 | 13.180 % |
c |    114115 |   33014   117042 |   19533    8960   293502    32.8 | 13.180 % |
c |    115256 |   33014   117042 |   21486   10101   413300    40.9 | 13.180 % |
c |    116965 |   33014   117042 |   23635   11810   469744    39.8 | 13.180 % |
c |    119527 |   33014   117042 |   25998   14372   552623    38.5 | 13.180 % |
c |    123371 |   33014   117042 |   28598   18216   643677    35.3 | 13.180 % |
c |    129138 |   33009   117026 |   31458   23982  1014080    42.3 | 13.197 % |
c |    137787 |   33009   117026 |   34604   32631  1730085    53.0 | 13.197 % |
c |    150761 |   32904   116651 |   38064   25854  2482973    96.0 | 13.316 % |
c |    170222 |   32887   116590 |   41871   24537  1839658    75.0 | 13.350 % |
c |    199414 |   32865   116518 |   46058   30391  2562844    84.3 | 13.419 % |
c |    243204 |   32856   116487 |   50664   45936  6702767   145.9 | 13.436 % |
c |    308888 |   32856   116487 |   55730   46835  7200912   153.8 | 13.436 % |
c |    407419 |   32841   116436 |   61303   32788  2108156    64.3 | 13.470 % |
#### 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 1989
Raw data (stat): 1989 (runsolver) R 1988 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421287406 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.9998 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 936 0 0 0 995 3 0 0 25 0 1 0 421287406 5394432 914 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1317 914 603 41 0 1276 0
vsize: 5268
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 1045 0 0 0 1994 3 0 0 25 0 1 0 421287406 5947392 1023 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1452 1023 603 41 0 1411 0
vsize: 5808
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 1167 0 0 0 2994 4 0 0 25 0 1 0 421287406 6438912 1145 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1572 1145 603 41 0 1531 0
vsize: 6288
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 2128 0 0 0 3990 7 0 0 25 0 1 0 421287406 10575872 2106 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2582 2106 603 41 0 2541 0
vsize: 10328
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 2140 0 0 0 4990 7 0 0 25 0 1 0 421287406 10575872 2118 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2582 2118 603 41 0 2541 0
vsize: 10328
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 2570 0 0 0 5989 8 0 0 25 0 1 0 421287406 12316672 2548 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3007 2548 603 41 0 2966 0
vsize: 12028
[startup+70.0028 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 2570 0 0 0 6988 8 0 0 25 0 1 0 421287406 12316672 2548 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3007 2548 603 41 0 2966 0
vsize: 12028
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 2918 0 0 0 7988 9 0 0 25 0 1 0 421287406 13791232 2896 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3367 2896 603 41 0 3326 0
vsize: 13468
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 3423 0 0 0 8986 11 0 0 25 0 1 0 421287406 15941632 3401 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3892 3401 603 41 0 3851 0
vsize: 15568
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 3588 0 0 0 9986 11 0 0 25 0 1 0 421287406 16613376 3566 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3566 603 41 0 4015 0
vsize: 16224
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 3806 0 0 0 10985 12 0 0 25 0 1 0 421287406 17539072 3784 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4282 3784 603 41 0 4241 0
vsize: 17128
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 4317 0 0 0 11984 13 0 0 25 0 1 0 421287406 19529728 4295 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4768 4295 603 41 0 4727 0
vsize: 19072
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 4839 0 0 0 12982 15 0 0 25 0 1 0 421287406 21790720 4817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5320 4817 603 41 0 5279 0
vsize: 21280
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5268 0 0 0 13981 17 0 0 25 0 1 0 421287406 23523328 5246 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 5246 603 41 0 5702 0
vsize: 22972
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5677 0 0 0 14980 18 0 0 25 0 1 0 421287406 25128960 5655 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5655 603 41 0 6094 0
vsize: 24540
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5677 0 0 0 15980 18 0 0 25 0 1 0 421287406 25128960 5655 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5655 603 41 0 6094 0
vsize: 24540
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5677 0 0 0 16980 18 0 0 25 0 1 0 421287406 25128960 5655 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5655 603 41 0 6094 0
vsize: 24540
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5677 0 0 0 17980 18 0 0 25 0 1 0 421287406 25128960 5655 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5655 603 41 0 6094 0
vsize: 24540
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5680 0 0 0 18980 18 0 0 25 0 1 0 421287406 25128960 5658 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5658 603 41 0 6094 0
vsize: 24540
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5681 0 0 0 19980 18 0 0 25 0 1 0 421287406 25128960 5659 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5659 603 41 0 6094 0
vsize: 24540
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5681 0 0 0 20981 18 0 0 25 0 1 0 421287406 25128960 5659 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5659 603 41 0 6094 0
vsize: 24540
[startup+220.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5681 0 0 0 21981 18 0 0 25 0 1 0 421287406 25128960 5659 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5659 603 41 0 6094 0
vsize: 24540
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5681 0 0 0 22981 18 0 0 25 0 1 0 421287406 25128960 5659 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6135 5659 603 41 0 6094 0
vsize: 24540
[startup+240.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 5830 0 0 0 23981 19 0 0 25 0 1 0 421287406 25800704 5808 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6299 5808 603 41 0 6258 0
vsize: 25196
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 6383 0 0 0 24979 21 0 0 25 0 1 0 421287406 28061696 6361 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6851 6361 603 41 0 6810 0
vsize: 27404
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 6959 0 0 0 25977 22 0 0 25 0 1 0 421287406 30326784 6937 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7404 6937 603 41 0 7363 0
vsize: 29616
[startup+270.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7432 0 0 0 26976 24 0 0 25 0 1 0 421287406 32337920 7410 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7410 603 41 0 7854 0
vsize: 31580
[startup+280.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 27976 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+290.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 28976 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 29977 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223664 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+310.005 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 30977 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+320.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 31977 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+330.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 32977 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7448 0 0 0 33978 24 0 0 25 0 1 0 421287406 32337920 7426 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7895 7426 603 41 0 7854 0
vsize: 31580
[startup+350.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 7664 0 0 0 34977 25 0 0 25 0 1 0 421287406 33280000 7642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8125 7642 603 41 0 8084 0
vsize: 32500
[startup+360.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 8163 0 0 0 35976 26 0 0 25 0 1 0 421287406 35270656 8141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8611 8141 603 41 0 8570 0
vsize: 34444
[startup+370.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 8627 0 0 0 36974 27 0 0 25 0 1 0 421287406 37130240 8605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9065 8605 603 41 0 9024 0
vsize: 36260
[startup+380.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9047 0 0 0 37972 29 0 0 25 0 1 0 421287406 38858752 9025 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9487 9025 603 41 0 9446 0
vsize: 37948
[startup+390.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9467 0 0 0 38971 30 0 0 25 0 1 0 421287406 40583168 9445 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9908 9445 603 41 0 9867 0
vsize: 39632
[startup+400.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 39971 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+410.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 40971 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+420.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 41971 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+430.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 42971 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+440.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 43972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+450.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 44972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+460.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 45972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+470.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 46972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+480.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 47972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+490.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 48972 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+500.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9653 0 0 0 49973 31 0 0 25 0 1 0 421287406 41377792 9631 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9631 603 41 0 10061 0
vsize: 40408
[startup+510.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9654 0 0 0 50973 31 0 0 25 0 1 0 421287406 41377792 9632 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9632 603 41 0 10061 0
vsize: 40408
[startup+520.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9654 0 0 0 51973 31 0 0 25 0 1 0 421287406 41377792 9632 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9632 603 41 0 10061 0
vsize: 40408
[startup+530.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9701 0 0 0 52973 31 0 0 25 0 1 0 421287406 41508864 9679 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10134 9679 603 41 0 10093 0
vsize: 40536
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9906 0 0 0 53972 32 0 0 25 0 1 0 421287406 42438656 9884 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9884 603 41 0 10320 0
vsize: 41444
[startup+550.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9906 0 0 0 54972 32 0 0 25 0 1 0 421287406 42438656 9884 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9884 603 41 0 10320 0
vsize: 41444
[startup+560.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9906 0 0 0 55972 32 0 0 25 0 1 0 421287406 42438656 9884 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9884 603 41 0 10320 0
vsize: 41444
[startup+570.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9906 0 0 0 56973 32 0 0 25 0 1 0 421287406 42438656 9884 4294967295 134512640 134672761 3221224560 3221223744 134558885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9884 603 41 0 10320 0
vsize: 41444
[startup+580.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9906 0 0 0 57973 32 0 0 25 0 1 0 421287406 42438656 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9884 603 41 0 10320 0
vsize: 41444
[startup+590.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9908 0 0 0 58973 32 0 0 25 0 1 0 421287406 42438656 9886 4294967295 134512640 134672761 3221224560 3221223792 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9886 603 41 0 10320 0
vsize: 41444
[startup+600.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9909 0 0 0 59973 32 0 0 25 0 1 0 421287406 42438656 9887 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9887 603 41 0 10320 0
vsize: 41444
[startup+610.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9909 0 0 0 60973 32 0 0 25 0 1 0 421287406 42438656 9887 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9887 603 41 0 10320 0
vsize: 41444
[startup+620.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9917 0 0 0 61973 32 0 0 25 0 1 0 421287406 42438656 9895 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9895 603 41 0 10320 0
vsize: 41444
[startup+630.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9917 0 0 0 62974 32 0 0 25 0 1 0 421287406 42438656 9895 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9895 603 41 0 10320 0
vsize: 41444
[startup+640.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9917 0 0 0 63974 32 0 0 25 0 1 0 421287406 42438656 9895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9895 603 41 0 10320 0
vsize: 41444
[startup+650.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9917 0 0 0 64974 32 0 0 25 0 1 0 421287406 42438656 9895 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9895 603 41 0 10320 0
vsize: 41444
[startup+660.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9917 0 0 0 65973 32 0 0 25 0 1 0 421287406 42438656 9895 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10361 9895 603 41 0 10320 0
vsize: 41444
[startup+670.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 66973 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+680.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 67973 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+690.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 68974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+700.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 69974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+710.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 70974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+720.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 71974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+730.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 72974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+740.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 73974 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+750.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 74975 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+760.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 75975 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+770.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 76975 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+780.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 77975 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+790.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9921 0 0 0 78975 32 0 0 25 0 1 0 421287406 42438656 9899 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10361 9899 603 41 0 10320 0
vsize: 41444
[startup+800.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 79976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+810.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 80976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+820.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 81976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+830.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 82976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+840.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 83976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+850.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 84976 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+860.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 85977 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+870.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9931 0 0 0 86977 32 0 0 25 0 1 0 421287406 42610688 9909 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9909 603 41 0 10362 0
vsize: 41612
[startup+880.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 87977 32 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+890.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 88977 32 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+900.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 89977 32 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+910.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 90977 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+920.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 91977 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+930.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 92977 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+940.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 93977 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+950.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 94978 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+960.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 95978 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+970.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 96978 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223664 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+980.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 97978 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+990.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9932 0 0 0 98978 33 0 0 25 0 1 0 421287406 42610688 9910 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9910 603 41 0 10362 0
vsize: 41612
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9934 0 0 0 99979 33 0 0 25 0 1 0 421287406 42610688 9912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9912 603 41 0 10362 0
vsize: 41612
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9936 0 0 0 100979 33 0 0 25 0 1 0 421287406 42610688 9914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9914 603 41 0 10362 0
vsize: 41612
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 101979 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 102979 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 103979 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 104980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 105980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 106980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 107980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 108980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 109980 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 110981 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 111981 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 112981 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 113981 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 9938 0 0 0 114981 33 0 0 25 0 1 0 421287406 42610688 9916 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10403 9916 603 41 0 10362 0
vsize: 41612
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 10093 0 0 0 115981 33 0 0 25 0 1 0 421287406 43139072 10071 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10532 10071 603 41 0 10491 0
vsize: 42128
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 10320 0 0 0 116981 34 0 0 25 0 1 0 421287406 44064768 10298 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 10298 603 41 0 10717 0
vsize: 43032
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 10320 0 0 0 117981 34 0 0 25 0 1 0 421287406 44064768 10298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 10298 603 41 0 10717 0
vsize: 43032
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 10320 0 0 0 118981 34 0 0 25 0 1 0 421287406 44064768 10298 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 10298 603 41 0 10717 0
vsize: 43032
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 1989
Raw data (stat): 1989 (minisat+) R 1988 29151 29150 0 -1 0 10320 0 0 0 119981 34 0 0 25 0 1 0 421287406 44064768 10298 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 10298 603 41 0 10717 0
vsize: 43032
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 1989
Raw data (stat): 1989 (minisat+) Z 1988 29151 29150 0 -1 12 10323 0 0 0 119981 36 0 0 25 0 1 0 421287406 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.05
CPU time (s): 1200.18
CPU user time (s): 1199.82
CPU system time (s): 0.361944
CPU usage (%): 100.011
Max. virtual memory (Kb): 43032
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####