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/primes-dimacs-cnf/normalized-par32-1.opb
MD5SUM	64e81a7b23abbb8a6da4e2377ea69dee
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13453
Number of constraints which are clauses	13453
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	3
Trace number 6295

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 04:09:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4716 boxname=wulflinc24 idbench=204 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64e81a7b23abbb8a6da4e2377ea69dee  /oldhome/oroussel/tmp/wulflinc24/normalized-par32-1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc24/normalized-par32-1.opb /oldhome/oroussel/tmp/wulflinc24/normalized-par32-1.opb
IDLAUNCH: 4716
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        831120 kB
Buffers:         35340 kB
Cached:         125596 kB
SwapCached:       3828 kB
Active:          55792 kB
Inactive:       111880 kB
HighTotal:      131008 kB
HighFree:         3080 kB
LowTotal:       903652 kB
LowFree:        828040 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30360 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:29:53 (client local time) WITH STATUS 0 IN 1200.1 SECONDS
stats: 4716 7 1200.1 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13039 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9878    24638 |    3292       0        0     nan |  0.000 % |
c |       101 |    9878    24638 |    3621     101     1231    12.2 | 23.867 % |
c |       251 |    9878    24638 |    3983     251     5277    21.0 | 23.867 % |
c |       476 |    9878    24638 |    4381     476     8655    18.2 | 23.867 % |
c |       814 |    9878    24638 |    4819     814    19600    24.1 | 23.867 % |
c |      1320 |    9878    24638 |    5301    1320    27899    21.1 | 23.867 % |
c |      2082 |    9878    24638 |    5831    2082    57645    27.7 | 23.867 % |
c |      3221 |    9878    24638 |    6415    3221    93388    29.0 | 23.867 % |
c |      4931 |    9878    24638 |    7056    4931   143848    29.2 | 23.867 % |
c |      7493 |    9878    24638 |    7762    7493   210661    28.1 | 23.867 % |
c |     11338 |    9878    24638 |    8538    6644   169658    25.5 | 23.867 % |
c |     17105 |    9878    24638 |    9392    7285   177959    24.4 | 23.867 % |
c |     25754 |    9878    24638 |   10331   10409   254945    24.5 | 23.867 % |
c |     38729 |    9878    24638 |   11364   11455   286759    25.0 | 23.867 % |
c |     58191 |    9878    24638 |   12501   11386   282530    24.8 | 23.867 % |
c |     87384 |    9878    24638 |   13751   12309   296202    24.1 | 23.867 % |
c |    131173 |    9868    24616 |   15126   10027   237728    23.7 | 23.929 % |
c |    196858 |    9868    24616 |   16639    8659   223250    25.8 | 23.929 % |
c |    295384 |    9868    24616 |   18303   16056   367503    22.9 | 23.929 % |
c |    443174 |    9868    24616 |   20133   14387   321561    22.4 | 23.929 % |
#### 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.83 0.93 0.90 2/54 3939
Raw data (stat): 3939 (runsolver) R 3938 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481597223 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+10.0003 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1255 0 0 0 994 3 0 0 25 0 1 0 481597223 6541312 1194 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+20.0007 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1255 0 0 0 1994 4 0 0 25 0 1 0 481597223 6541312 1194 4294967295 134512640 134672761 3221224560 3221223576 1075352647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+30.0021 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1255 0 0 0 2994 4 0 0 25 0 1 0 481597223 6541312 1194 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+40.0025 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1255 0 0 0 3994 4 0 0 25 0 1 0 481597223 6541312 1194 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1597 1194 603 41 0 1556 0
vsize: 6388
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1293 0 0 0 4994 4 0 0 25 0 1 0 481597223 6811648 1232 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1663 1232 603 41 0 1622 0
vsize: 6652
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1309 0 0 0 5994 4 0 0 25 0 1 0 481597223 6815744 1248 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1664 1248 603 41 0 1623 0
vsize: 6656
[startup+70.0036 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1324 0 0 0 6994 4 0 0 25 0 1 0 481597223 6950912 1263 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1697 1263 603 41 0 1656 0
vsize: 6788
[startup+80.0039 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1375 0 0 0 7994 4 0 0 25 0 1 0 481597223 7081984 1314 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1729 1314 603 41 0 1688 0
vsize: 6916
[startup+90.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1385 0 0 0 8994 4 0 0 25 0 1 0 481597223 7221248 1324 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1324 603 41 0 1722 0
vsize: 7052
[startup+100.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1393 0 0 0 9994 4 0 0 25 0 1 0 481597223 7221248 1332 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1332 603 41 0 1722 0
vsize: 7052
[startup+110.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1396 0 0 0 10995 4 0 0 25 0 1 0 481597223 7221248 1335 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1763 1335 603 41 0 1722 0
vsize: 7052
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1409 0 0 0 11995 4 0 0 25 0 1 0 481597223 7368704 1348 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1348 603 41 0 1758 0
vsize: 7196
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1441 0 0 0 12995 4 0 0 25 0 1 0 481597223 7368704 1380 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1380 603 41 0 1758 0
vsize: 7196
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1447 0 0 0 13995 4 0 0 25 0 1 0 481597223 7516160 1386 4294967295 134512640 134672761 3221224560 3221223696 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1386 603 41 0 1794 0
vsize: 7340
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1448 0 0 0 14995 4 0 0 25 0 1 0 481597223 7516160 1387 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1387 603 41 0 1794 0
vsize: 7340
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1451 0 0 0 15995 4 0 0 25 0 1 0 481597223 7516160 1390 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1390 603 41 0 1794 0
vsize: 7340
[startup+170.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1459 0 0 0 16996 4 0 0 25 0 1 0 481597223 7516160 1398 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1398 603 41 0 1794 0
vsize: 7340
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1467 0 0 0 17996 4 0 0 25 0 1 0 481597223 7516160 1406 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1406 603 41 0 1794 0
vsize: 7340
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1471 0 0 0 18996 4 0 0 25 0 1 0 481597223 7516160 1410 4294967295 134512640 134672761 3221224560 3221223712 134565029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1835 1410 603 41 0 1794 0
vsize: 7340
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1507 0 0 0 19996 4 0 0 25 0 1 0 481597223 7798784 1446 4294967295 134512640 134672761 3221224560 3221223744 134558641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1446 603 41 0 1863 0
vsize: 7616
[startup+210.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1510 0 0 0 20996 4 0 0 25 0 1 0 481597223 7798784 1449 4294967295 134512640 134672761 3221224560 3221223744 134558700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1449 603 41 0 1863 0
vsize: 7616
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1515 0 0 0 21997 4 0 0 25 0 1 0 481597223 7798784 1454 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1454 603 41 0 1863 0
vsize: 7616
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1516 0 0 0 22997 4 0 0 25 0 1 0 481597223 7798784 1455 4294967295 134512640 134672761 3221224560 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1455 603 41 0 1863 0
vsize: 7616
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1529 0 0 0 23997 4 0 0 25 0 1 0 481597223 7798784 1468 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1904 1468 603 41 0 1863 0
vsize: 7616
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1548 0 0 0 24997 4 0 0 25 0 1 0 481597223 7933952 1487 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1487 603 41 0 1896 0
vsize: 7748
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1549 0 0 0 25997 4 0 0 25 0 1 0 481597223 7933952 1488 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1488 603 41 0 1896 0
vsize: 7748
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1555 0 0 0 26997 4 0 0 25 0 1 0 481597223 7933952 1494 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1937 1494 603 41 0 1896 0
vsize: 7748
[startup+280.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1555 0 0 0 27998 4 0 0 25 0 1 0 481597223 7933952 1494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1937 1494 603 41 0 1896 0
vsize: 7748
[startup+290.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1634 0 0 0 28997 5 0 0 25 0 1 0 481597223 8429568 1573 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2058 1573 603 41 0 2017 0
vsize: 8232
[startup+300.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1637 0 0 0 29997 5 0 0 25 0 1 0 481597223 8429568 1576 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2058 1576 603 41 0 2017 0
vsize: 8232
[startup+310.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1678 0 0 0 30997 5 0 0 25 0 1 0 481597223 8564736 1617 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1617 603 41 0 2050 0
vsize: 8364
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1684 0 0 0 31997 5 0 0 25 0 1 0 481597223 8564736 1623 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1623 603 41 0 2050 0
vsize: 8364
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1692 0 0 0 32997 5 0 0 25 0 1 0 481597223 8564736 1631 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1692 0 0 0 33998 5 0 0 25 0 1 0 481597223 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1692 0 0 0 34998 5 0 0 25 0 1 0 481597223 8564736 1631 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1692 0 0 0 35998 5 0 0 25 0 1 0 481597223 8564736 1631 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1692 0 0 0 36998 5 0 0 25 0 1 0 481597223 8564736 1631 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1631 603 41 0 2050 0
vsize: 8364
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1693 0 0 0 37998 5 0 0 25 0 1 0 481597223 8564736 1632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1632 603 41 0 2050 0
vsize: 8364
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1694 0 0 0 38999 5 0 0 25 0 1 0 481597223 8564736 1633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1633 603 41 0 2050 0
vsize: 8364
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1695 0 0 0 39999 5 0 0 25 0 1 0 481597223 8564736 1634 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1634 603 41 0 2050 0
vsize: 8364
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1696 0 0 0 40999 5 0 0 25 0 1 0 481597223 8564736 1635 4294967295 134512640 134672761 3221224560 3221223684 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1635 603 41 0 2050 0
vsize: 8364
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1697 0 0 0 41999 5 0 0 25 0 1 0 481597223 8564736 1636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1636 603 41 0 2050 0
vsize: 8364
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1698 0 0 0 42999 5 0 0 25 0 1 0 481597223 8564736 1637 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1698 0 0 0 43999 5 0 0 25 0 1 0 481597223 8564736 1637 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2091 1637 603 41 0 2050 0
vsize: 8364
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1713 0 0 0 44999 6 0 0 25 0 1 0 481597223 8695808 1652 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1652 603 41 0 2082 0
vsize: 8492
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1721 0 0 0 45999 6 0 0 25 0 1 0 481597223 8695808 1660 4294967295 134512640 134672761 3221224560 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1660 603 41 0 2082 0
vsize: 8492
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1729 0 0 0 46999 6 0 0 25 0 1 0 481597223 8695808 1668 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1729 0 0 0 48000 6 0 0 25 0 1 0 481597223 8695808 1668 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1668 603 41 0 2082 0
vsize: 8492
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1730 0 0 0 49000 6 0 0 25 0 1 0 481597223 8695808 1669 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2123 1669 603 41 0 2082 0
vsize: 8492
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1737 0 0 0 50000 6 0 0 25 0 1 0 481597223 8859648 1676 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1676 603 41 0 2122 0
vsize: 8652
[startup+510.016 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 51000 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+520.016 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 52000 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+530.016 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 53000 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+540.017 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 54000 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+550.016 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 55001 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+560.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 56001 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+570.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 57001 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+580.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1742 0 0 0 58001 6 0 0 25 0 1 0 481597223 8859648 1681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1681 603 41 0 2122 0
vsize: 8652
[startup+590.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1748 0 0 0 59001 6 0 0 25 0 1 0 481597223 8859648 1687 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1687 603 41 0 2122 0
vsize: 8652
[startup+600.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1756 0 0 0 60001 6 0 0 25 0 1 0 481597223 8859648 1695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1695 603 41 0 2122 0
vsize: 8652
[startup+610.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1758 0 0 0 61002 6 0 0 25 0 1 0 481597223 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+620.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1758 0 0 0 62001 6 0 0 25 0 1 0 481597223 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+630.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1758 0 0 0 63002 6 0 0 25 0 1 0 481597223 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+640.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1758 0 0 0 64002 6 0 0 25 0 1 0 481597223 8859648 1697 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2163 1697 603 41 0 2122 0
vsize: 8652
[startup+650.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1759 0 0 0 65001 6 0 0 25 0 1 0 481597223 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+660.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1759 0 0 0 66001 7 0 0 25 0 1 0 481597223 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+670.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1759 0 0 0 67001 7 0 0 25 0 1 0 481597223 8859648 1698 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+680.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1759 0 0 0 68001 7 0 0 25 0 1 0 481597223 8859648 1698 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1698 603 41 0 2122 0
vsize: 8652
[startup+690.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1761 0 0 0 69000 7 0 0 25 0 1 0 481597223 8859648 1700 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2163 1700 603 41 0 2122 0
vsize: 8652
[startup+700.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1771 0 0 0 70000 8 0 0 25 0 1 0 481597223 9023488 1710 4294967295 134512640 134672761 3221224560 3221223684 134566089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1710 603 41 0 2162 0
vsize: 8812
[startup+710.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1772 0 0 0 71000 8 0 0 25 0 1 0 481597223 9023488 1711 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1711 603 41 0 2162 0
vsize: 8812
[startup+720.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 71999 8 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+730.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 72999 9 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+740.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 73999 9 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223744 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+750.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 74998 9 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+760.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 75998 9 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+770.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 76998 10 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+780.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1784 0 0 0 77997 11 0 0 25 0 1 0 481597223 9023488 1723 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1723 603 41 0 2162 0
vsize: 8812
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1785 0 0 0 78997 11 0 0 25 0 1 0 481597223 9023488 1724 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+800.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1785 0 0 0 79996 11 0 0 25 0 1 0 481597223 9023488 1724 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+810.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1785 0 0 0 80996 12 0 0 25 0 1 0 481597223 9023488 1724 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1724 603 41 0 2162 0
vsize: 8812
[startup+820.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1796 0 0 0 81995 12 0 0 25 0 1 0 481597223 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+830.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1796 0 0 0 82995 12 0 0 25 0 1 0 481597223 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+840.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1796 0 0 0 83996 12 0 0 25 0 1 0 481597223 9023488 1735 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+850.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1796 0 0 0 84995 13 0 0 25 0 1 0 481597223 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1796 0 0 0 85995 13 0 0 25 0 1 0 481597223 9023488 1735 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1735 603 41 0 2162 0
vsize: 8812
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1797 0 0 0 86994 13 0 0 25 0 1 0 481597223 9023488 1736 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2203 1736 603 41 0 2162 0
vsize: 8812
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1805 0 0 0 87994 13 0 0 25 0 1 0 481597223 9187328 1744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+890.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1805 0 0 0 88994 13 0 0 25 0 1 0 481597223 9187328 1744 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1744 603 41 0 2202 0
vsize: 8972
[startup+900.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1807 0 0 0 89994 14 0 0 25 0 1 0 481597223 9187328 1746 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1746 603 41 0 2202 0
vsize: 8972
[startup+910.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1807 0 0 0 90993 14 0 0 25 0 1 0 481597223 9187328 1746 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1746 603 41 0 2202 0
vsize: 8972
[startup+920.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1813 0 0 0 91993 14 0 0 25 0 1 0 481597223 9187328 1752 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1752 603 41 0 2202 0
vsize: 8972
[startup+930.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1815 0 0 0 92993 15 0 0 25 0 1 0 481597223 9187328 1754 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1754 603 41 0 2202 0
vsize: 8972
[startup+940.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1815 0 0 0 93992 16 0 0 25 0 1 0 481597223 9187328 1754 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1754 603 41 0 2202 0
vsize: 8972
[startup+950.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1816 0 0 0 94992 16 0 0 25 0 1 0 481597223 9187328 1755 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1755 603 41 0 2202 0
vsize: 8972
[startup+960.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1826 0 0 0 95992 16 0 0 25 0 1 0 481597223 9187328 1765 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1765 603 41 0 2202 0
vsize: 8972
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1828 0 0 0 96991 16 0 0 25 0 1 0 481597223 9187328 1767 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1767 603 41 0 2202 0
vsize: 8972
[startup+980.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1838 0 0 0 97991 17 0 0 25 0 1 0 481597223 9351168 1777 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1777 603 41 0 2242 0
vsize: 9132
[startup+990.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1838 0 0 0 98990 17 0 0 25 0 1 0 481597223 9351168 1777 4294967295 134512640 134672761 3221224560 3221223516 1075349836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1777 603 41 0 2242 0
vsize: 9132
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1846 0 0 0 99990 17 0 0 25 0 1 0 481597223 9351168 1785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2283 1785 603 41 0 2242 0
vsize: 9132
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1874 0 0 0 100990 18 0 0 25 0 1 0 481597223 9482240 1813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2315 1813 603 41 0 2274 0
vsize: 9260
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1898 0 0 0 101989 18 0 0 25 0 1 0 481597223 9482240 1837 4294967295 134512640 134672761 3221224560 3221223696 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2315 1837 603 41 0 2274 0
vsize: 9260
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1913 0 0 0 102989 18 0 0 25 0 1 0 481597223 9621504 1852 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1852 603 41 0 2308 0
vsize: 9396
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1917 0 0 0 103989 19 0 0 25 0 1 0 481597223 9621504 1856 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1856 603 41 0 2308 0
vsize: 9396
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1917 0 0 0 104989 19 0 0 25 0 1 0 481597223 9621504 1856 4294967295 134512640 134672761 3221224560 3221223744 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1856 603 41 0 2308 0
vsize: 9396
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1924 0 0 0 105988 19 0 0 25 0 1 0 481597223 9621504 1863 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1924 0 0 0 106988 19 0 0 25 0 1 0 481597223 9621504 1863 4294967295 134512640 134672761 3221224560 3221223728 134561259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1924 0 0 0 107988 19 0 0 25 0 1 0 481597223 9621504 1863 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1924 0 0 0 108988 20 0 0 25 0 1 0 481597223 9621504 1863 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1863 603 41 0 2308 0
vsize: 9396
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1929 0 0 0 109987 20 0 0 25 0 1 0 481597223 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1929 0 0 0 110987 21 0 0 25 0 1 0 481597223 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1929 0 0 0 111986 21 0 0 25 0 1 0 481597223 9621504 1868 4294967295 134512640 134672761 3221224560 3221223744 134559179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1929 0 0 0 112986 22 0 0 25 0 1 0 481597223 9621504 1868 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1868 603 41 0 2308 0
vsize: 9396
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1930 0 0 0 113987 22 0 0 25 0 1 0 481597223 9621504 1869 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2349 1869 603 41 0 2308 0
vsize: 9396
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1936 0 0 0 114986 22 0 0 25 0 1 0 481597223 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1936 0 0 0 115986 23 0 0 25 0 1 0 481597223 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1936 0 0 0 116986 23 0 0 25 0 1 0 481597223 9752576 1875 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1875 603 41 0 2340 0
vsize: 9524
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1947 0 0 0 117986 23 0 0 25 0 1 0 481597223 9752576 1886 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1947 0 0 0 118985 24 0 0 25 0 1 0 481597223 9752576 1886 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3939
Raw data (stat): 3939 (minisat+) R 3938 28546 28545 0 -1 0 1947 0 0 0 119985 24 0 0 25 0 1 0 481597223 9752576 1886 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2381 1886 603 41 0 2340 0
vsize: 9524
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3939
Raw data (stat): 3939 (minisat+) Z 3938 28546 28545 0 -1 12 1949 0 0 0 119985 24 0 0 25 0 1 0 481597223 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: 0
Real time (s): 1200.06
CPU time (s): 1200.1
CPU user time (s): 1199.85
CPU system time (s): 0.249962
CPU usage (%): 100.003
Max. virtual memory (Kb): 9524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####