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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-pilot.we.opb
MD5SUM21cca5e58499fc8c195476eedca15203
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
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 2760
Biggest coefficient in the objective function 114621939712000000000
Number of bits for the biggest coefficient in the objective function 67
Sum of the numbers in the objective function 6133849937192095318016
Number of bits of the sum of numbers in the objective function 73
Biggest number in a constraint 114621939712000000000
Number of bits of the biggest number in a constraint 67
Biggest sum of numbers in a constraint 6133849937192095318016
Number of bits of the biggest sum of numbers73
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables77678
Total number of constraints1016
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1016
Minimum length of a constraint10
Maximum length of a constraint2430

Trace number 2665

Launcher Data

LAUNCH ON wulflinc20 THE 2005-09-18 20:30:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2795 boxname=wulflinc20 idbench=451 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  21cca5e58499fc8c195476eedca15203  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-pilot.we.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-pilot.we.opb
IDLAUNCH: 2795
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898852 kB
Buffers:         35644 kB
Cached:          70692 kB
SwapCached:        832 kB
Active:          75324 kB
Inactive:        33680 kB
HighTotal:      131008 kB
HighFree:        56952 kB
LowTotal:       903652 kB
LowFree:        841900 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21132 kB
Committed_AS:    64140 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 20:50:11 (client local time) WITH STATUS 0 IN 1209.48 SECONDS
stats: 2795 7 1209.48 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 2793] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1522 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssss.ssssssssssssssssss.sss
c ---[1547]---> BDD-cost:    7
c ---[1546]---> BDD-cost:    8
c ---[1545]---> BDD-cost:    7
c ---[1544]---> BDD-cost:   11
c ---[1543]---> BDD-cost:   21
c ---[1542]---> BDD-cost:   21
c ---[1540]---> BDD-cost:   21
c ---[1539]---> BDD-cost:   21
c ---[1538]---> BDD-cost:   22
c ---[1530]---> BDD-cost:   18
c ---[1529]---> BDD-cost:   17
c ---[1528]---> BDD-cost:   17
c ---[1527]---> BDD-cost:   17
c ---[1526]---> BDD-cost:   21
c ---[1525]---> BDD-cost:   18
c ---[1524]---> BDD-cost:   17
c ---[1523]---> BDD-cost:   17
c ---[1521]---> BDD-cost:   21
c ---[1520]---> BDD-cost:    4
c ---[1519]---> BDD-cost:    3
c ---[1518]---> BDD-cost:    9
c ---[1517]---> BDD-cost:    8
c ---[1516]---> BDD-cost:    8
c ---[1515]---> BDD-cost:    5
c ---[1514]---> BDD-cost:   13
c ---[1513]---> BDD-cost:   21
c ---[1512]---> BDD-cost:   21
c ---[1510]---> BDD-cost:   23
c ---[1509]---> BDD-cost:   20
c ---[1508]---> BDD-cost:   22
c ---[1507]---> BDD-cost:   26
c ---[1506]---> BDD-cost:   19
c ---[1505]---> BDD-cost:   18
c ---[1504]---> BDD-cost:   19
c ---[1503]---> BDD-cost:   17
c ---[1502]---> BDD-cost:   20
c ---[1500]---> BDD-cost:   18
c ---[1499]---> BDD-cost:   17
c ---[1498]---> BDD-cost:   17
c ---[1497]---> BDD-cost:   17
c ---[1496]---> BDD-cost:   21
c ---[1495]---> BDD-cost:   18
c ---[1494]---> BDD-cost:   17
c ---[1493]---> BDD-cost:   17
c ---[1491]---> BDD-cost:   21
c ---[1490]---> BDD-cost:    8
c ---[1488]---> BDD-cost:    3
c ---[1487]---> BDD-cost:   10
c ---[1485]---> BDD-cost:    9
c ---[1484]---> BDD-cost:   14
c ---[1483]---> BDD-cost:   20
c ---[1482]---> BDD-cost:   21
c ---[1481]---> BDD-cost:   24
c ---[1480]---> BDD-cost:   23
c ---[1479]---> BDD-cost:   20
c ---[1478]---> BDD-cost:   22
c ---[1477]---> BDD-cost:   26
c ---[1476]---> BDD-cost:   19
c ---[1475]---> BDD-cost:   18
c ---[1474]---> BDD-cost:   19
c ---[1473]---> BDD-cost:   17
c ---[1472]---> BDD-cost:   20
c ---[1470]---> BDD-cost:   18
c ---[1469]---> BDD-cost:   17
c ---[1468]---> BDD-cost:   17
c ---[1467]---> BDD-cost:   17
c ---[1466]---> BDD-cost:   21
c ---[1465]---> BDD-cost:   18
c ---[1464]---> BDD-cost:   17
c ---[1463]---> BDD-cost:   17
c ---[1461]---> BDD-cost:   21
c ---[1460]---> BDD-cost:    6
c ---[1459]---> BDD-cost:    4
c ---[1458]---> BDD-cost:   11
c ---[1457]---> BDD-cost:   10
c ---[1456]---> BDD-cost:    9
c ---[1455]---> BDD-cost:    5
c ---[1454]---> BDD-cost:   12
c ---[1453]---> BDD-cost:   21
c ---[1452]---> BDD-cost:   21
c ---[1451]---> BDD-cost:   22
c ---[1450]---> BDD-cost:   23
c ---[1449]---> BDD-cost:   21
c ---[1448]---> BDD-cost:   22
c ---[1447]---> BDD-cost:   26
c ---[1446]---> BDD-cost:   19
c ---[1445]---> BDD-cost:   18
c ---[1444]---> BDD-cost:   19
c ---[1443]---> BDD-cost:   17
c ---[1442]---> BDD-cost:   20
c ---[1440]---> BDD-cost:   18
c ---[1439]---> BDD-cost:   17
c ---[1438]---> BDD-cost:   17
c ---[1437]---> BDD-cost:   17
c ---[1436]---> BDD-cost:   21
c ---[1435]---> BDD-cost:   18
c ---[1434]---> BDD-cost:   17
c ---[1433]---> BDD-cost:   17
c ---[1431]---> BDD-cost:   21
c ---[1430]---> BDD-cost:    8
c ---[1428]---> BDD-cost:   12
c ---[1427]---> BDD-cost:   11
c ---[1425]---> BDD-cost:    7
c ---[1424]---> BDD-cost:   14
c ---[1423]---> BDD-cost:   18
c ---[1422]---> BDD-cost:   20
c ---[1421]---> BDD-cost:   22
c ---[1420]---> BDD-cost:   23
c ---[1419]---> BDD-cost:   20
c ---[1418]---> BDD-cost:   22
c ---[1417]---> BDD-cost:   27
c ---[1416]---> BDD-cost:   19
c ---[1415]---> BDD-cost:   18
c ---[1414]---> BDD-cost:   19
c ---[1413]---> BDD-cost:   17
c ---[1412]---> BDD-cost:   20
c ---[1410]---> BDD-cost:   18
c ---[1409]---> BDD-cost:   17
c ---[1408]---> BDD-cost:   17
c ---[1407]---> BDD-cost:   17
c ---[1406]---> BDD-cost:   21
c ---[1405]---> BDD-cost:   18
c ---[1404]---> BDD-cost:   17
c ---[1403]---> BDD-cost:   17
c ---[1401]---> BDD-cost:   21
c ---[1400]---> BDD-cost:    8
c ---[1399]---> BDD-cost:    5
c ---[1398]---> BDD-cost:    5
c ---[1397]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    5
c ---[1395]---> BDD-cost:   12
c ---[1394]---> BDD-cost:   11
c ---[1393]---> BDD-cost:   10
c ---[1392]---> BDD-cost:    7
c ---[1390]---> BDD-cost:   16
c ---[1389]---> BDD-cost:   20
c ---[1388]---> BDD-cost:   21
c ---[1387]---> BDD-cost:   20
c ---[1386]---> BDD-cost:   21
c ---[1385]---> BDD-cost:   22
c ---[1384]---> BDD-cost:   27
c ---[1383]---> BDD-cost:   19
c ---[1382]---> BDD-cost:   18
c ---[1381]---> BDD-cost:   19
c ---[1380]---> BDD-cost:   17
c ---[1379]---> BDD-cost:   20
c ---[1378]---> BDD-cost:   26
c ---[1377]---> BDD-cost:   18
c ---[1376]---> BDD-cost:   17
c ---[1375]---> BDD-cost:   17
c ---[1374]---> BDD-cost:   17
c ---[1373]---> BDD-cost:   21
c ---[1372]---> BDD-cost:   18
c ---[1371]---> BDD-cost:   17
c ---[1370]---> BDD-cost:   17
c ---[1368]---> BDD-cost:   21
c ---[1366]---> BDD-cost:    6
c ---[1364]---> BDD-cost:    1
c ---[1362]---> BDD-cost:    1
c ---[1361]---> BDD-cost:    9
c ---[1360]---> BDD-cost:   13
c ---[1359]---> BDD-cost:    9
c ---[1358]---> BDD-cost:    9
c ---[1356]---> BDD-cost:   14
c ---[1355]---> BDD-cost:   20
c ---[1354]---> BDD-cost:   21
c ---[1353]---> BDD-cost:   22
c ---[1352]---> BDD-cost:   23
c ---[1350]---> BDD-cost:   22
c ---[1349]---> BDD-cost:   27
c ---[1348]---> BDD-cost:   19
c ---[1347]---> BDD-cost:   18
c ---[1346]---> BDD-cost:   19
c ---[1345]---> BDD-cost:   17
c ---[1344]---> BDD-cost:   20
c ---[1343]---> BDD-cost:   26
c ---[1342]---> BDD-cost:   18
c ---[1341]---> BDD-cost:   17
c ---[1340]---> BDD-cost:   17
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   21
c ---[1337]---> BDD-cost:   18
c ---[1336]---> BDD-cost:   17
c ---[1335]---> BDD-cost:   17
c ---[1333]---> BDD-cost:   21
c ---[1331]---> BDD-cost:    7
c ---[1330]---> BDD-cost:   11
c ---[1329]---> BDD-cost:    8
c ---[1328]---> BDD-cost:   11
c ---[1327]---> BDD-cost:    1
c ---[1326]---> BDD-cost:   11
c ---[1325]---> BDD-cost:   13
c ---[1324]---> BDD-cost:    7
c ---[1323]---> BDD-cost:    9
c ---[1322]---> BDD-cost:    7
c ---[1321]---> BDD-cost:   12
c ---[1320]---> BDD-cost:   21
c ---[1319]---> BDD-cost:   18
c ---[1318]---> BDD-cost:   24
c ---[1317]---> BDD-cost:   23
c ---[1315]---> BDD-cost:   22
c ---[1313]---> BDD-cost:   19
c ---[1312]---> BDD-cost:   18
c ---[1311]---> BDD-cost:   19
c ---[1310]---> BDD-cost:   17
c ---[1309]---> BDD-cost:   20
c ---[1308]---> BDD-cost:   26
c ---[1307]---> BDD-cost:   18
c ---[1306]---> BDD-cost:   17
c ---[1305]---> BDD-cost:   17
c ---[1304]---> BDD-cost:   17
c ---[1303]---> BDD-cost:   21
c ---[1302]---> BDD-cost:   18
c ---[1301]---> BDD-cost:   17
c ---[1300]---> BDD-cost:   17
c ---[1298]---> BDD-cost:   21
c ---[1297]---> BDD-cost:    9
c ---[1295]---> BDD-cost:   13
c ---[1293]---> BDD-cost:   13
c ---[1292]---> BDD-cost:    8
c ---[1291]---> BDD-cost:    9
c ---[1290]---> BDD-cost:   13
c ---[1289]---> BDD-cost:   12
c ---[1287]---> BDD-cost:    8
c ---[1286]---> Sorter-cost:  203     Base: 2 2 2 2 2 2 2 2 2
c ---[1285]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1284]---> Sorter-cost:  294     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c -

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/15525/stat): 15525 (minisat+_script) R 15524 15525 2660 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1844145914 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/15525/statm): 174 3 169 147 0 27 0
[pid=15525] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=15526
New process pid=15527
New process pid=15528
execve syscall for /bin/sed executable
One traced child (pid=15527) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=15528) exited with status: 0
One traced child (pid=15526) exited with status: 0
New process pid=15529
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-pilot.we.opb
One traced child (pid=15529) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=15530
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-pilot.we.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) T 15525 15525 2660 0 -1 0 3716 0 0 0 951 21 0 0 25 0 1 0 1844145921 16412672 3552 4294967295 134512640 135167914 3221224448 3221222252 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15530/statm): 4007 3552 162 162 0 3845 0
[pid=15530] vsize: 16028
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 18156

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 7416 0 0 0 1911 41 0 0 25 0 1 0 1844145921 31621120 6640 4294967295 134512640 135167914 3221224448 3221222904 134591306 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 7720 6640 162 162 0 7558 0
[pid=15530] vsize: 30880
Current children cumulated CPU time (s) 19.54
Current children cumulated vsize (Kb) 33008

[startup+30.0046 s]
Raw data (loadavg): 0.95 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 10655 0 0 0 2873 60 0 0 25 0 1 0 1844145921 44716032 9879 4294967295 134512640 135167914 3221224448 3221223204 134697185 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 10917 9879 162 162 0 10755 0
[pid=15530] vsize: 43668
Current children cumulated CPU time (s) 29.35
Current children cumulated vsize (Kb) 45796

[startup+40.0053 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) T 15525 15525 2660 0 -1 0 11744 0 0 0 3865 65 0 0 25 0 1 0 1844145921 46710784 10347 4294967295 134512640 135167914 3221224448 3221185020 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/15530/statm): 11404 10347 162 162 0 11242 0
[pid=15530] vsize: 45616
Current children cumulated CPU time (s) 39.32
Current children cumulated vsize (Kb) 47744

[startup+50.006 s]
Raw data (loadavg): 0.96 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 4844 74 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215152 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 49.2
Current children cumulated vsize (Kb) 53100

[startup+60.0068 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 5844 75 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214524 134723251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 59.21
Current children cumulated vsize (Kb) 53100

[startup+70.0075 s]
Raw data (loadavg): 0.97 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 6844 75 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214864 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 69.21
Current children cumulated vsize (Kb) 53100

[startup+80.0082 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 7844 75 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215244 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 79.21
Current children cumulated vsize (Kb) 53100

[startup+90.0089 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 8844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215408 134696264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 89.22
Current children cumulated vsize (Kb) 53100

[startup+100.01 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 9844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215440 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 99.22
Current children cumulated vsize (Kb) 53100

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 10844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215424 134722532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 109.22
Current children cumulated vsize (Kb) 53100

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 11844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215232 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 119.22
Current children cumulated vsize (Kb) 53100

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 12844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215216 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 129.22
Current children cumulated vsize (Kb) 53100

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 13844 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214864 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 139.22
Current children cumulated vsize (Kb) 53100

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 14845 76 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215640 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 149.23
Current children cumulated vsize (Kb) 53100

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 15845 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215760 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 53100

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 16845 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215856 134844682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 169.24
Current children cumulated vsize (Kb) 53100

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 17845 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215264 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 179.24
Current children cumulated vsize (Kb) 53100

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 18845 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215400 134693615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 189.24
Current children cumulated vsize (Kb) 53100

[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 19845 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215392 134843010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 199.24
Current children cumulated vsize (Kb) 53100

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 20846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215740 134718176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 209.25
Current children cumulated vsize (Kb) 53100

[startup+220.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 21846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215680 134844689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 219.25
Current children cumulated vsize (Kb) 53100

[startup+230.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 22846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216000 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 229.25
Current children cumulated vsize (Kb) 53100

[startup+240.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 23846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215744 134843064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 239.25
Current children cumulated vsize (Kb) 53100

[startup+250.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 24846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215456 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 249.25
Current children cumulated vsize (Kb) 53100

[startup+260.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 25846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215568 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 259.25
Current children cumulated vsize (Kb) 53100

[startup+270.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 26847 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216188 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 269.26
Current children cumulated vsize (Kb) 53100

[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 27846 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214952 134693783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 279.25
Current children cumulated vsize (Kb) 53100

[startup+290.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 28847 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214940 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 289.26
Current children cumulated vsize (Kb) 53100

[startup+300.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 29847 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215200 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 299.26
Current children cumulated vsize (Kb) 53100

[startup+310.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 30847 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215328 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 309.26
Current children cumulated vsize (Kb) 53100

[startup+320.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 31847 77 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215628 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 319.26
Current children cumulated vsize (Kb) 53100

[startup+330.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 32847 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215120 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 329.27
Current children cumulated vsize (Kb) 53100

[startup+340.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 33848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215552 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 339.28
Current children cumulated vsize (Kb) 53100

[startup+350.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 34848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215532 134844638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 349.28
Current children cumulated vsize (Kb) 53100

[startup+360.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 35848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216256 134845927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 359.28
Current children cumulated vsize (Kb) 53100

[startup+370.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 36848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215392 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 369.28
Current children cumulated vsize (Kb) 53100

[startup+380.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 37848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215776 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 379.28
Current children cumulated vsize (Kb) 53100

[startup+390.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 38848 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216196 134629227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 389.28
Current children cumulated vsize (Kb) 53100

[startup+400.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 39849 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215772 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 399.29
Current children cumulated vsize (Kb) 53100

[startup+410.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 40849 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215596 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 409.29
Current children cumulated vsize (Kb) 53100

[startup+420.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 41849 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215772 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 419.29
Current children cumulated vsize (Kb) 53100

[startup+430.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 42849 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215780 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 429.29
Current children cumulated vsize (Kb) 53100

[startup+440.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 43850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215584 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 439.3
Current children cumulated vsize (Kb) 53100

[startup+450.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 44850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215064 134723211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 449.3
Current children cumulated vsize (Kb) 53100

[startup+460.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 45850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216300 134722208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 459.3
Current children cumulated vsize (Kb) 53100

[startup+470.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 46850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216160 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 469.3
Current children cumulated vsize (Kb) 53100

[startup+480.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 47850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215824 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 479.3
Current children cumulated vsize (Kb) 53100

[startup+490.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 48850 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216032 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 489.3
Current children cumulated vsize (Kb) 53100

[startup+500.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 49851 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215024 134845890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 499.31
Current children cumulated vsize (Kb) 53100

[startup+510.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 50851 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215640 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 509.31
Current children cumulated vsize (Kb) 53100

[startup+520.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 51851 78 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214896 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 519.31
Current children cumulated vsize (Kb) 53100

[startup+530.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 52851 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215056 134723225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 529.32
Current children cumulated vsize (Kb) 53100

[startup+540.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 53851 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215920 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 539.32
Current children cumulated vsize (Kb) 53100

[startup+550.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 54851 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215728 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 549.32
Current children cumulated vsize (Kb) 53100

[startup+560.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 55852 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216432 134845893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 559.33
Current children cumulated vsize (Kb) 53100

[startup+570.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 56852 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216816 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 569.33
Current children cumulated vsize (Kb) 53100

[startup+580.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 57852 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215616 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 579.33
Current children cumulated vsize (Kb) 53100

[startup+590.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 58852 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215216 134844676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 589.33
Current children cumulated vsize (Kb) 53100

[startup+600.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 59853 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215568 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 599.34
Current children cumulated vsize (Kb) 53100

[startup+610.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 60853 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215984 134849092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 609.34
Current children cumulated vsize (Kb) 53100

[startup+620.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 61853 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215980 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 619.34
Current children cumulated vsize (Kb) 53100

[startup+630.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 62853 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215808 134694511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 629.34
Current children cumulated vsize (Kb) 53100

[startup+640.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 63853 79 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215856 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 639.34
Current children cumulated vsize (Kb) 53100

[startup+650.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 64852 80 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215840 134629172 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 649.34
Current children cumulated vsize (Kb) 53100

[startup+660.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 65852 81 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215648 134849071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 659.35
Current children cumulated vsize (Kb) 53100

[startup+670.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 66852 81 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215632 134522812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 669.35
Current children cumulated vsize (Kb) 53100

[startup+680.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 67852 81 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216012 134522184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 679.35
Current children cumulated vsize (Kb) 53100

[startup+690.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 68852 81 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215644 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 689.35
Current children cumulated vsize (Kb) 53100

[startup+700.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 69852 81 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215936 134696653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 699.35
Current children cumulated vsize (Kb) 53100

[startup+710.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 70852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215920 134696733 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 709.36
Current children cumulated vsize (Kb) 53100

[startup+720.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 71852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216160 134522732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 719.36
Current children cumulated vsize (Kb) 53100

[startup+730.043 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 72852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215792 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 729.36
Current children cumulated vsize (Kb) 53100

[startup+740.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 73852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215308 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 739.36
Current children cumulated vsize (Kb) 53100

[startup+750.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 74852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215220 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 749.36
Current children cumulated vsize (Kb) 53100

[startup+760.044 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 75852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216188 134694320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 759.36
Current children cumulated vsize (Kb) 53100

[startup+770.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 76852 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221214924 134845940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 769.36
Current children cumulated vsize (Kb) 53100

[startup+780.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 77853 82 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215744 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 779.37
Current children cumulated vsize (Kb) 53100

[startup+790.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 78853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215484 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 789.38
Current children cumulated vsize (Kb) 53100

[startup+800.045 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 79853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215632 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 799.38
Current children cumulated vsize (Kb) 53100

[startup+810.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 80853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215680 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 809.38
Current children cumulated vsize (Kb) 53100

[startup+820.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 81853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216012 134849088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 819.38
Current children cumulated vsize (Kb) 53100

[startup+830.046 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 82853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216188 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 829.38
Current children cumulated vsize (Kb) 53100

[startup+840.047 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 83853 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216224 134845921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 839.38
Current children cumulated vsize (Kb) 53100

[startup+850.048 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 84854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215632 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 849.39
Current children cumulated vsize (Kb) 53100

[startup+860.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 85854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215824 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 859.39
Current children cumulated vsize (Kb) 53100

[startup+870.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 86854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215728 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 869.39
Current children cumulated vsize (Kb) 53100

[startup+880.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 87854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216320 134522338 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 879.39
Current children cumulated vsize (Kb) 53100

[startup+890.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 88854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215804 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 889.39
Current children cumulated vsize (Kb) 53100

[startup+900.049 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 89854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216000 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 899.39
Current children cumulated vsize (Kb) 53100

[startup+910.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 90854 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215168 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 909.39
Current children cumulated vsize (Kb) 53100

[startup+920.051 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 91855 83 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216512 134849068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 919.4
Current children cumulated vsize (Kb) 53100

[startup+930.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 92855 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216384 134629489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 929.41
Current children cumulated vsize (Kb) 53100

[startup+940.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 93855 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215960 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 939.41
Current children cumulated vsize (Kb) 53100

[startup+950.052 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 94855 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215804 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 949.41
Current children cumulated vsize (Kb) 53100

[startup+960.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 95855 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215424 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 959.41
Current children cumulated vsize (Kb) 53100

[startup+970.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 96856 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216828 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 969.42
Current children cumulated vsize (Kb) 53100

[startup+980.053 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 97856 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216016 134631194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 979.42
Current children cumulated vsize (Kb) 53100

[startup+990.054 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 98856 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215824 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 989.42
Current children cumulated vsize (Kb) 53100

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 99856 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215844 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 999.42
Current children cumulated vsize (Kb) 53100

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 100856 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215744 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1009.42
Current children cumulated vsize (Kb) 53100

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 101857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215948 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1019.43
Current children cumulated vsize (Kb) 53100

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 102857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216476 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1029.43
Current children cumulated vsize (Kb) 53100

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 103857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215856 134629451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1039.43
Current children cumulated vsize (Kb) 53100

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 104857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216160 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1049.43
Current children cumulated vsize (Kb) 53100

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 105857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216000 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1059.43
Current children cumulated vsize (Kb) 53100

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 106857 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216000 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1069.43
Current children cumulated vsize (Kb) 53100

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 107858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216208 134628730 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1079.44
Current children cumulated vsize (Kb) 53100

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 108858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215568 134696342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1089.44
Current children cumulated vsize (Kb) 53100

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 109858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215648 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1099.44
Current children cumulated vsize (Kb) 53100

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 110858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215920 134845903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1109.44
Current children cumulated vsize (Kb) 53100

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 111858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215788 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1119.44
Current children cumulated vsize (Kb) 53100

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 112858 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215648 134849061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1129.44
Current children cumulated vsize (Kb) 53100

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 113859 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216256 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1139.45
Current children cumulated vsize (Kb) 53100

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 114859 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215664 134629080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1149.45
Current children cumulated vsize (Kb) 53100

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 115859 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216112 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1159.45
Current children cumulated vsize (Kb) 53100

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 116859 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215344 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1169.45
Current children cumulated vsize (Kb) 53100

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 117860 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215484 134694480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1179.46
Current children cumulated vsize (Kb) 53100

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 118860 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216248 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1189.46
Current children cumulated vsize (Kb) 53100

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 119860 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215984 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1199.46
Current children cumulated vsize (Kb) 53100

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 120860 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221215932 134723267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1209.46
Current children cumulated vsize (Kb) 53100



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 15530
Raw data (/proc/15525/stat): 15525 (minisat+_script) S 15524 15525 2660 0 -1 0 314 331 0 0 0 1 0 1 20 0 1 0 1844145914 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/15525/statm): 532 234 485 147 0 385 0
[pid=15525] vsize: 2128
Raw data (/proc/15530/stat): 15530 (minisat+_bignum) R 15525 15525 2660 0 -1 0 14080 0 0 0 120860 84 0 0 25 0 1 0 1844145921 52195328 11694 4294967295 134512640 135167914 3221224448 3221216192 134631224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/15530/statm): 12743 11694 162 162 0 12581 0
[pid=15530] vsize: 50972
Current children cumulated CPU time (s) 1209.46
Current children cumulated vsize (Kb) 53100

Sending SIGTERM to -15525
Sleeping 2 seconds
One traced child (pid=15525) ended because it received signal 15 (SIGTERM)
One traced child (pid=15530) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.48
CPU user time (s): 1208.61
CPU system time (s): 0.871867
CPU usage (%): 99.9494
Max. virtual memory (cumulated for all children) (Kb): 53100

Verifier Data

ERROR: no interpretation found !