PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	5220
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.13683
Number of variables	87482
Total number of constraints	87518
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	87518
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	42032
Trace number 16314

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 06:54:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13688 boxname=wulflinc31 idbench=1053 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 13688
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        643424 kB
Buffers:         29284 kB
Cached:         333432 kB
SwapCached:        540 kB
Active:         129540 kB
Inactive:       235196 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        643172 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20772 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:13:31 (client local time) WITH STATUS 0 IN 1120.18 SECONDS
stats: 13688 7 1120.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.94 0.90 2/54 24041
Raw data (stat): 24041 (runsolver) R 24040 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543065170 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 22973 0 0 0 935 63 0 0 25 0 1 0 543065170 64581632 7176 4294967295 134512640 134672761 3221224544 3220346640 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+20.0017 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 22973 0 0 0 1935 64 0 0 25 0 1 0 543065170 64581632 7176 4294967295 134512640 134672761 3221224544 3220610544 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 23303 0 0 0 2934 65 0 0 25 0 1 0 543065170 65933312 7506 4294967295 134512640 134672761 3221224544 3221206992 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16097 7506 603 41 0 16056 0
vsize: 64388
[startup+40.003 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 23706 0 0 0 3932 67 0 0 25 0 1 0 543065170 69140480 7909 4294967295 134512640 134672761 3221224544 3221041024 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 7909 603 41 0 16839 0
vsize: 67520
[startup+50.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 23944 0 0 0 4932 67 0 0 25 0 1 0 543065170 69771264 8147 4294967295 134512640 134672761 3221224544 3221138928 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17034 8147 603 41 0 16993 0
vsize: 68136
[startup+60.0049 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 24650 0 0 0 5930 69 0 0 25 0 1 0 543065170 71118848 8523 4294967295 134512640 134672761 3221224544 3220892976 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8523 603 41 0 17322 0
vsize: 69452
[startup+70.0058 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 24759 0 0 0 6929 70 0 0 25 0 1 0 543065170 71118848 8632 4294967295 134512640 134672761 3221224544 3221162544 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8632 603 41 0 17322 0
vsize: 69452
[startup+80.0063 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 24841 0 0 0 7929 71 0 0 25 0 1 0 543065170 71118848 8714 4294967295 134512640 134672761 3221224544 3220826464 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8714 603 41 0 17322 0
vsize: 69452
[startup+90.0072 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 25069 0 0 0 8928 72 0 0 25 0 1 0 543065170 74436608 8859 4294967295 134512640 134672761 3221224544 3220821072 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18173 8859 603 41 0 18132 0
vsize: 72692
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 25288 0 0 0 9928 72 0 0 25 0 1 0 543065170 75010048 9036 4294967295 134512640 134672761 3221224544 3221077392 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18313 9036 603 41 0 18272 0
vsize: 73252
[startup+110.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 25480 0 0 0 10927 73 0 0 25 0 1 0 543065170 75153408 9145 4294967295 134512640 134672761 3221224544 3220315264 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18348 9145 603 41 0 18307 0
vsize: 73392
[startup+120.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 27404 0 0 0 11922 78 0 0 25 0 1 0 543065170 79515648 10285 4294967295 134512640 134672761 3221224544 3219732240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19413 10285 603 41 0 19372 0
vsize: 77652
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 27560 0 0 0 12922 79 0 0 25 0 1 0 543065170 79818752 10399 4294967295 134512640 134672761 3221224544 3220721808 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19487 10399 603 41 0 19446 0
vsize: 77948
[startup+140.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 27601 0 0 0 13922 79 0 0 25 0 1 0 543065170 79953920 10440 4294967295 134512640 134672761 3221224544 3220484800 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+150.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 27601 0 0 0 14921 80 0 0 25 0 1 0 543065170 79953920 10440 4294967295 134512640 134672761 3221224544 3219773056 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19520 10440 603 41 0 19479 0
vsize: 78080
[startup+160.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 27920 0 0 0 15921 80 0 0 25 0 1 0 543065170 80695296 10676 4294967295 134512640 134672761 3221224544 3220056912 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19701 10676 603 41 0 19660 0
vsize: 78804
[startup+170.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 28156 0 0 0 16919 82 0 0 25 0 1 0 543065170 80830464 10747 4294967295 134512640 134672761 3221224544 3219671280 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19734 10747 603 41 0 19693 0
vsize: 78936
[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 28361 0 0 0 17919 82 0 0 25 0 1 0 543065170 81305600 10910 4294967295 134512640 134672761 3221224544 3220892688 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19850 10910 603 41 0 19809 0
vsize: 79400
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 28389 0 0 0 18919 83 0 0 25 0 1 0 543065170 81305600 10938 4294967295 134512640 134672761 3221224544 3220491616 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19850 10938 603 41 0 19809 0
vsize: 79400
[startup+200.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 28439 0 0 0 19918 84 0 0 25 0 1 0 543065170 81440768 10988 4294967295 134512640 134672761 3221224544 3219420048 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19883 10988 603 41 0 19842 0
vsize: 79532
[startup+210.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 28856 0 0 0 20917 85 0 0 25 0 1 0 543065170 81829888 11157 4294967295 134512640 134672761 3221224544 3220134192 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19978 11157 603 41 0 19937 0
vsize: 79912
[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29050 0 0 0 21916 85 0 0 25 0 1 0 543065170 82305024 11309 4294967295 134512640 134672761 3221224544 3221112352 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 11309 603 41 0 20053 0
vsize: 80376
[startup+230.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29050 0 0 0 22916 86 0 0 25 0 1 0 543065170 82305024 11309 4294967295 134512640 134672761 3221224544 3219254752 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20094 11309 603 41 0 20053 0
vsize: 80376
[startup+240.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29540 0 0 0 23915 87 0 0 25 0 1 0 543065170 82890752 11551 4294967295 134512640 134672761 3221224544 3219944208 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20237 11551 603 41 0 20196 0
vsize: 80948
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29696 0 0 0 24914 88 0 0 25 0 1 0 543065170 83193856 11665 4294967295 134512640 134672761 3221224544 3220925136 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20311 11665 603 41 0 20270 0
vsize: 81244
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29721 0 0 0 25914 88 0 0 25 0 1 0 543065170 83329024 11690 4294967295 134512640 134672761 3221224544 3220401472 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20344 11690 603 41 0 20303 0
vsize: 81376
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 29721 0 0 0 26914 88 0 0 25 0 1 0 543065170 83329024 11690 4294967295 134512640 134672761 3221224544 3218842912 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20344 11690 603 41 0 20303 0
vsize: 81376
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30091 0 0 0 27913 90 0 0 25 0 1 0 543065170 90497024 11977 4294967295 134512640 134672761 3221224544 3221209584 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22094 11977 603 41 0 22053 0
vsize: 88376
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30298 0 0 0 28912 91 0 0 25 0 1 0 543065170 90411008 12019 4294967295 134512640 134672761 3221224544 3220608336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22073 12019 603 41 0 22032 0
vsize: 88292
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30431 0 0 0 29911 91 0 0 25 0 1 0 543065170 90714112 12110 4294967295 134512640 134672761 3221224544 3220656256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22147 12110 603 41 0 22106 0
vsize: 88588
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24041
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30431 0 0 0 30911 92 0 0 25 0 1 0 543065170 90714112 12110 4294967295 134512640 134672761 3221224544 3219883264 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22147 12110 603 41 0 22106 0
vsize: 88588
[startup+320.021 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30743 0 0 0 31907 95 0 0 25 0 1 0 543065170 91455488 12339 4294967295 134512640 134672761 3221224544 3220432464 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22328 12339 603 41 0 22287 0
vsize: 89312
[startup+330.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 30963 0 0 0 32907 96 0 0 25 0 1 0 543065170 91369472 12394 4294967295 134512640 134672761 3221224544 3219935088 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22307 12394 603 41 0 22266 0
vsize: 89228
[startup+340.021 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31120 0 0 0 33907 96 0 0 25 0 1 0 543065170 91672576 12509 4294967295 134512640 134672761 3221224544 3220879344 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22381 12509 603 41 0 22340 0
vsize: 89524
[startup+350.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31148 0 0 0 34907 96 0 0 25 0 1 0 543065170 91807744 12537 4294967295 134512640 134672761 3221224544 3220411648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22414 12537 603 41 0 22373 0
vsize: 89656
[startup+360.022 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31148 0 0 0 35907 96 0 0 25 0 1 0 543065170 91807744 12537 4294967295 134512640 134672761 3221224544 3219138496 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22414 12537 603 41 0 22373 0
vsize: 89656
[startup+370.022 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31497 0 0 0 36907 97 0 0 25 0 1 0 543065170 92549120 12803 4294967295 134512640 134672761 3221224544 3220860720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22595 12803 603 41 0 22554 0
vsize: 90380
[startup+380.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31708 0 0 0 37906 97 0 0 25 0 1 0 543065170 92479488 12849 4294967295 134512640 134672761 3221224544 3220214448 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22578 12849 603 41 0 22537 0
vsize: 90312
[startup+390.023 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 24094
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31854 0 0 0 38906 97 0 0 25 0 1 0 543065170 92782592 12953 4294967295 134512640 134672761 3221224544 3220973040 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22652 12953 603 41 0 22611 0
vsize: 90608
[startup+400.023 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31874 0 0 0 39907 98 0 0 25 0 1 0 543065170 92917760 12973 4294967295 134512640 134672761 3221224544 3220266784 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+410.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 31874 0 0 0 40907 98 0 0 25 0 1 0 543065170 92917760 12973 4294967295 134512640 134672761 3221224544 3218996320 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22685 12973 603 41 0 22644 0
vsize: 90740
[startup+420.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 34859 0 0 0 41900 104 0 0 25 0 1 0 543065170 99061760 14557 4294967295 134512640 134672761 3221224544 3220759440 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24185 14557 603 41 0 24144 0
vsize: 96740
[startup+430.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35109 0 0 0 42900 105 0 0 25 0 1 0 543065170 99180544 14642 4294967295 134512640 134672761 3221224544 3219992880 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24214 14642 603 41 0 24173 0
vsize: 96856
[startup+440.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35259 0 0 0 43899 106 0 0 25 0 1 0 543065170 99483648 14750 4294967295 134512640 134672761 3221224544 3220802256 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24288 14750 603 41 0 24247 0
vsize: 97152
[startup+450.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35294 0 0 0 44900 106 0 0 25 0 1 0 543065170 99618816 14785 4294967295 134512640 134672761 3221224544 3220369408 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+460.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35294 0 0 0 45900 106 0 0 25 0 1 0 543065170 99618816 14785 4294967295 134512640 134672761 3221224544 3219699040 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24321 14785 603 41 0 24280 0
vsize: 97284
[startup+470.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35578 0 0 0 46900 106 0 0 25 0 1 0 543065170 100225024 14986 4294967295 134512640 134672761 3221224544 3219878640 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24469 14986 603 41 0 24428 0
vsize: 97876
[startup+480.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 35914 0 0 0 47899 107 0 0 25 0 1 0 543065170 100773888 15157 4294967295 134512640 134672761 3221224544 3218383536 134594231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24603 15157 603 41 0 24562 0
vsize: 98412
[startup+490.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36131 0 0 0 48899 107 0 0 25 0 1 0 543065170 101249024 15332 4294967295 134512640 134672761 3221224544 3219839568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24719 15332 603 41 0 24678 0
vsize: 98876
[startup+500.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36184 0 0 0 49899 108 0 0 25 0 1 0 543065170 101384192 15385 4294967295 134512640 134672761 3221224544 3220471728 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24752 15385 603 41 0 24711 0
vsize: 99008
[startup+510.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36222 0 0 0 50898 108 0 0 25 0 1 0 543065170 101519360 15423 4294967295 134512640 134672761 3221224544 3220936464 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15423 603 41 0 24744 0
vsize: 99140
[startup+520.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36246 0 0 0 51898 108 0 0 25 0 1 0 543065170 101519360 15447 4294967295 134512640 134672761 3221224544 3220130560 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+530.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36246 0 0 0 52898 108 0 0 25 0 1 0 543065170 101519360 15447 4294967295 134512640 134672761 3221224544 3219538336 134594103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+540.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36246 0 0 0 53899 108 0 0 25 0 1 0 543065170 101519360 15447 4294967295 134512640 134672761 3221224544 3219066496 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+550.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36246 0 0 0 54899 108 0 0 25 0 1 0 543065170 101519360 15447 4294967295 134512640 134672761 3221224544 3218200096 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24785 15447 603 41 0 24744 0
vsize: 99140
[startup+560.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36589 0 0 0 55898 109 0 0 25 0 1 0 543065170 102395904 15707 4294967295 134512640 134672761 3221224544 3219976848 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24999 15707 603 41 0 24958 0
vsize: 99996
[startup+570.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36717 0 0 0 56898 110 0 0 25 0 1 0 543065170 102666240 15835 4294967295 134512640 134672761 3221224544 3221037840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25065 15835 603 41 0 25024 0
vsize: 100260
[startup+580.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 36959 0 0 0 57897 111 0 0 25 0 1 0 543065170 102862848 15912 4294967295 134512640 134672761 3221224544 3219417744 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25113 15912 603 41 0 25072 0
vsize: 100452
[startup+590.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37102 0 0 0 58897 111 0 0 25 0 1 0 543065170 103165952 16013 4294967295 134512640 134672761 3221224544 3220151472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16013 603 41 0 25146 0
vsize: 100748
[startup+600.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37144 0 0 0 59897 111 0 0 25 0 1 0 543065170 103165952 16055 4294967295 134512640 134672761 3221224544 3220662960 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25187 16055 603 41 0 25146 0
vsize: 100748
[startup+610.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37176 0 0 0 60897 111 0 0 25 0 1 0 543065170 103301120 16087 4294967295 134512640 134672761 3221224544 3221049168 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16087 603 41 0 25179 0
vsize: 100880
[startup+620.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24096
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37190 0 0 0 61897 111 0 0 25 0 1 0 543065170 103301120 16101 4294967295 134512640 134672761 3221224544 3219714592 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+630.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37190 0 0 0 62897 111 0 0 25 0 1 0 543065170 103301120 16101 4294967295 134512640 134672761 3221224544 3219357856 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+640.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37190 0 0 0 63897 112 0 0 25 0 1 0 543065170 103301120 16101 4294967295 134512640 134672761 3221224544 3218915104 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+650.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37190 0 0 0 64898 112 0 0 25 0 1 0 543065170 103301120 16101 4294967295 134512640 134672761 3221224544 3218102848 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25220 16101 603 41 0 25179 0
vsize: 100880
[startup+660.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37519 0 0 0 65897 112 0 0 25 0 1 0 543065170 104042496 16347 4294967295 134512640 134672761 3221224544 3219658224 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25401 16347 603 41 0 25360 0
vsize: 101604
[startup+670.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37616 0 0 0 66897 112 0 0 25 0 1 0 543065170 104312832 16444 4294967295 134512640 134672761 3221224544 3220842480 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25467 16444 603 41 0 25426 0
vsize: 101868
[startup+680.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37815 0 0 0 67897 113 0 0 25 0 1 0 543065170 104275968 16478 4294967295 134512640 134672761 3221224544 3219201072 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25458 16478 603 41 0 25417 0
vsize: 101832
[startup+690.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 37972 0 0 0 68897 113 0 0 25 0 1 0 543065170 104579072 16593 4294967295 134512640 134672761 3221224544 3220103280 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25532 16593 603 41 0 25491 0
vsize: 102128
[startup+700.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38017 0 0 0 69897 113 0 0 25 0 1 0 543065170 104714240 16638 4294967295 134512640 134672761 3221224544 3220659600 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16638 603 41 0 25524 0
vsize: 102260
[startup+710.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38052 0 0 0 70897 113 0 0 25 0 1 0 543065170 104849408 16673 4294967295 134512640 134672761 3221224544 3221076720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16673 603 41 0 25557 0
vsize: 102392
[startup+720.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38064 0 0 0 71897 114 0 0 25 0 1 0 543065170 104849408 16685 4294967295 134512640 134672761 3221224544 3219766816 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+730.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38064 0 0 0 72897 114 0 0 25 0 1 0 543065170 104849408 16685 4294967295 134512640 134672761 3221224544 3219380800 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+740.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38064 0 0 0 73897 114 0 0 25 0 1 0 543065170 104849408 16685 4294967295 134512640 134672761 3221224544 3218842240 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+750.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38064 0 0 0 74897 114 0 0 25 0 1 0 543065170 104849408 16685 4294967295 134512640 134672761 3221224544 3217896832 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+760.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38448 0 0 0 75897 114 0 0 25 0 1 0 543065170 105725952 16986 4294967295 134512640 134672761 3221224544 3220466064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25812 16986 603 41 0 25771 0
vsize: 103248
[startup+770.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38591 0 0 0 76897 114 0 0 25 0 1 0 543065170 105455616 16964 4294967295 134512640 134672761 3221224544 3218534928 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25746 16964 603 41 0 25705 0
vsize: 102984
[startup+780.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38806 0 0 0 77897 115 0 0 25 0 1 0 543065170 106065920 17137 4294967295 134512640 134672761 3221224544 3219866064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 17137 603 41 0 25854 0
vsize: 103580
[startup+790.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38857 0 0 0 78897 115 0 0 25 0 1 0 543065170 106201088 17188 4294967295 134512640 134672761 3221224544 3220488912 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17188 603 41 0 25887 0
vsize: 103712
[startup+800.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38894 0 0 0 79897 115 0 0 25 0 1 0 543065170 106201088 17225 4294967295 134512640 134672761 3221224544 3220948080 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17225 603 41 0 25887 0
vsize: 103712
[startup+810.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38916 0 0 0 80897 116 0 0 25 0 1 0 543065170 106336256 17247 4294967295 134512640 134672761 3221224544 3220080256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+820.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38916 0 0 0 81897 116 0 0 25 0 1 0 543065170 106336256 17247 4294967295 134512640 134672761 3221224544 3219524608 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+830.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38916 0 0 0 82897 116 0 0 25 0 1 0 543065170 106336256 17247 4294967295 134512640 134672761 3221224544 3219049312 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+840.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 38916 0 0 0 83897 116 0 0 25 0 1 0 543065170 106336256 17247 4294967295 134512640 134672761 3221224544 3218180320 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+850.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39264 0 0 0 84897 116 0 0 25 0 1 0 543065170 107077632 17512 4294967295 134512640 134672761 3221224544 3220023792 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26142 17512 603 41 0 26101 0
vsize: 104568
[startup+860.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39350 0 0 0 85897 117 0 0 25 0 1 0 543065170 107347968 17598 4294967295 134512640 134672761 3221224544 3221069616 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26208 17598 603 41 0 26167 0
vsize: 104832
[startup+870.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39553 0 0 0 86896 118 0 0 25 0 1 0 543065170 119894016 17636 4294967295 134512640 134672761 3221224544 3219601680 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29271 17636 603 41 0 29230 0
vsize: 117084
[startup+880.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39694 0 0 0 87895 118 0 0 25 0 1 0 543065170 120197120 17735 4294967295 134512640 134672761 3221224544 3220318128 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17735 603 41 0 29304 0
vsize: 117380
[startup+890.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39735 0 0 0 88896 119 0 0 25 0 1 0 543065170 120332288 17776 4294967295 134512640 134672761 3221224544 3220823088 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17776 603 41 0 29337 0
vsize: 117512
[startup+900.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39767 0 0 0 89896 119 0 0 25 0 1 0 543065170 120332288 17808 4294967295 134512640 134672761 3221224544 3221205072 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17808 603 41 0 29337 0
vsize: 117512
[startup+910.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39768 0 0 0 90896 119 0 0 25 0 1 0 543065170 120332288 17809 4294967295 134512640 134672761 3221224544 3219645568 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+920.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39768 0 0 0 91896 119 0 0 25 0 1 0 543065170 120332288 17809 4294967295 134512640 134672761 3221224544 3219210016 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+930.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 39768 0 0 0 92896 119 0 0 25 0 1 0 543065170 120332288 17809 4294967295 134512640 134672761 3221224544 3218411104 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+940.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40068 0 0 0 93895 120 0 0 25 0 1 0 543065170 121073664 18026 4294967295 134512640 134672761 3221224544 3219455952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29559 18026 603 41 0 29518 0
vsize: 118236
[startup+950.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40183 0 0 0 94895 120 0 0 25 0 1 0 543065170 121344000 18141 4294967295 134512640 134672761 3221224544 3220855632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 18141 603 41 0 29584 0
vsize: 118500
[startup+960.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40498 0 0 0 95895 121 0 0 25 0 1 0 543065170 121733120 18291 4294967295 134512640 134672761 3221224544 3218670960 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29720 18291 603 41 0 29679 0
vsize: 118880
[startup+970.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40651 0 0 0 96895 121 0 0 25 0 1 0 543065170 122036224 18402 4294967295 134512640 134672761 3221224544 3219527856 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18402 603 41 0 29753 0
vsize: 119176
[startup+980.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40695 0 0 0 97895 121 0 0 25 0 1 0 543065170 122171392 18446 4294967295 134512640 134672761 3221224544 3220073616 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18446 603 41 0 29786 0
vsize: 119308
[startup+990.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40729 0 0 0 98895 121 0 0 25 0 1 0 543065170 122306560 18480 4294967295 134512640 134672761 3221224544 3220483536 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18480 603 41 0 29819 0
vsize: 119440
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40756 0 0 0 99895 121 0 0 25 0 1 0 543065170 122306560 18507 4294967295 134512640 134672761 3221224544 3220810992 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18507 603 41 0 29819 0
vsize: 119440
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40779 0 0 0 100895 121 0 0 25 0 1 0 543065170 122441728 18530 4294967295 134512640 134672761 3221224544 3221091024 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18530 603 41 0 29852 0
vsize: 119572
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 101895 121 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3219689248 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 102896 121 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3219074464 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 103896 121 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3218794816 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 104896 121 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3218464480 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 105896 121 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3217954624 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 40790 0 0 0 106896 122 0 0 25 0 1 0 543065170 122441728 18541 4294967295 134512640 134672761 3221224544 3217407616 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 41136 0 0 0 107896 122 0 0 25 0 1 0 543065170 123183104 18804 4294967295 134512640 134672761 3221224544 3219395568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 18804 603 41 0 30033 0
vsize: 120296
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 41221 0 0 0 108896 123 0 0 25 0 1 0 543065170 123453440 18889 4294967295 134512640 134672761 3221224544 3220392432 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30140 18889 603 41 0 30099 0
vsize: 120560
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 41298 0 0 0 109895 123 0 0 25 0 1 0 543065170 123723776 18966 4294967295 134512640 134672761 3221224544 3221014512 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 18966 603 41 0 30165 0
vsize: 120824
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 41846 0 0 0 110894 124 0 0 25 0 1 0 543065170 124088320 19223 4294967295 134512640 134672761 3221224544 3220723792 134523140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30295 19223 603 41 0 30254 0
vsize: 121180
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 24098
Raw data (stat): 24041 (minisat+) R 24040 23176 23175 0 -1 0 41846 0 0 0 110894 124 0 0 25 0 1 0 543065170 124088320 19223 4294967295 134512640 134672761 3221224544 3220723792 134523140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30295 19223 603 41 0 30254 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1120.04
CPU time (s): 1120.18
CPU user time (s): 1118.19
CPU system time (s): 1.9817
CPU usage (%): 100.012
Max. virtual memory (Kb): 121180
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####