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 21343

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        576944 kB
Buffers:         30164 kB
Cached:         402572 kB
SwapCached:        560 kB
Active:         158848 kB
Inactive:       275984 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        576692 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5168 kB
Slab:            17128 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 23:47:26 (client local time) WITH STATUS 0 IN 969.544 SECONDS
stats: 13689 7 969.544 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.83 0.89 0.88 2/55 11343
Raw data (stat): 11343 (runsolver) R 11342 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549053430 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.85 0.89 0.88 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 22973 0 0 0 939 59 0 0 25 0 1 0 549053430 64581632 7176 4294967295 134512640 134672761 3221224544 3220423920 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+20.0009 s]
Raw data (loadavg): 0.88 0.89 0.88 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 22973 0 0 0 1939 60 0 0 25 0 1 0 549053430 64581632 7176 4294967295 134512640 134672761 3221224544 3220870032 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+30.0005 s]
Raw data (loadavg): 0.89 0.90 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 23318 0 0 0 2939 60 0 0 25 0 1 0 549053430 65994752 7521 4294967295 134512640 134672761 3221224544 3220866672 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16112 7521 603 41 0 16071 0
vsize: 64448
[startup+40.0013 s]
Raw data (loadavg): 0.91 0.90 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 23723 0 0 0 3938 61 0 0 25 0 1 0 549053430 69140480 7926 4294967295 134512640 134672761 3221224544 3220707792 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 7926 603 41 0 16839 0
vsize: 67520
[startup+50.0021 s]
Raw data (loadavg): 0.92 0.90 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 23947 0 0 0 4937 62 0 0 25 0 1 0 549053430 69771264 8150 4294967295 134512640 134672761 3221224544 3220222912 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17034 8150 603 41 0 16993 0
vsize: 68136
[startup+60.0019 s]
Raw data (loadavg): 0.93 0.91 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 24694 0 0 0 5936 63 0 0 25 0 1 0 549053430 71118848 8567 4294967295 134512640 134672761 3221224544 3220931104 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8567 603 41 0 17322 0
vsize: 69452
[startup+70.0018 s]
Raw data (loadavg): 0.94 0.91 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 24820 0 0 0 6936 64 0 0 25 0 1 0 549053430 71118848 8693 4294967295 134512640 134672761 3221224544 3220513872 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8693 603 41 0 17322 0
vsize: 69452
[startup+80.0015 s]
Raw data (loadavg): 0.95 0.91 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 24968 0 0 0 7935 64 0 0 25 0 1 0 549053430 71458816 8841 4294967295 134512640 134672761 3221224544 3221116464 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17446 8841 603 41 0 17405 0
vsize: 69784
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.91 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 25111 0 0 0 8935 65 0 0 25 0 1 0 549053430 74571776 8901 4294967295 134512640 134672761 3221224544 3219950736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18206 8902 603 41 0 18165 0
vsize: 72824
[startup+100.002 s]
Raw data (loadavg): 0.96 0.92 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 25480 0 0 0 9935 66 0 0 25 0 1 0 549053430 75186176 9145 4294967295 134512640 134672761 3221224544 3220383040 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18356 9145 603 41 0 18315 0
vsize: 73424
[startup+110.002 s]
Raw data (loadavg): 0.97 0.92 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 27407 0 0 0 10931 70 0 0 25 0 1 0 549053430 79548416 10288 4294967295 134512640 134672761 3221224544 3219814800 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19421 10288 603 41 0 19380 0
vsize: 77684
[startup+120.003 s]
Raw data (loadavg): 0.97 0.92 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 27577 0 0 0 11930 70 0 0 25 0 1 0 549053430 79851520 10416 4294967295 134512640 134672761 3221224544 3220928592 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19495 10416 603 41 0 19454 0
vsize: 77980
[startup+130.003 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 27601 0 0 0 12930 70 0 0 25 0 1 0 549053430 79986688 10440 4294967295 134512640 134672761 3221224544 3220197472 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+140.003 s]
Raw data (loadavg): 0.98 0.92 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 27601 0 0 0 13931 70 0 0 25 0 1 0 549053430 79986688 10440 4294967295 134512640 134672761 3221224544 3218636128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+150.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 28058 0 0 0 14930 71 0 0 25 0 1 0 549053430 81133568 10814 4294967295 134512640 134672761 3221224544 3221176080 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19808 10814 603 41 0 19767 0
vsize: 79232
[startup+160.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 28364 0 0 0 15929 72 0 0 25 0 1 0 549053430 81313792 10913 4294967295 134512640 134672761 3221224544 3220918416 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10913 603 41 0 19811 0
vsize: 79408
[startup+170.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 28389 0 0 0 16930 72 0 0 25 0 1 0 549053430 81313792 10938 4294967295 134512640 134672761 3221224544 3220258816 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+180.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 28711 0 0 0 17929 73 0 0 25 0 1 0 549053430 82055168 11177 4294967295 134512640 134672761 3221224544 3220705872 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20033 11177 603 41 0 19992 0
vsize: 80132
[startup+190.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 28949 0 0 0 18929 73 0 0 25 0 1 0 549053430 82038784 11250 4294967295 134512640 134672761 3221224544 3220997424 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20029 11250 603 41 0 19988 0
vsize: 80116
[startup+200.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 29050 0 0 0 19928 74 0 0 25 0 1 0 549053430 82341888 11309 4294967295 134512640 134672761 3221224544 3219567136 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 11309 603 41 0 20062 0
vsize: 80412
[startup+210.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 11343
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 29549 0 0 0 20928 75 0 0 25 0 1 0 549053430 82927616 11560 4294967295 134512640 134672761 3221224544 3220150128 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20246 11560 603 41 0 20205 0
vsize: 80984
[startup+220.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 29716 0 0 0 21928 75 0 0 25 0 1 0 549053430 83230720 11685 4294967295 134512640 134672761 3221224544 3221182992 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20320 11685 603 41 0 20279 0
vsize: 81280
[startup+230.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 29721 0 0 0 22928 75 0 0 25 0 1 0 549053430 83365888 11690 4294967295 134512640 134672761 3221224544 3219818464 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+240.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 30070 0 0 0 23927 75 0 0 25 0 1 0 549053430 90398720 11956 4294967295 134512640 134672761 3221224544 3220953744 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22070 11956 603 41 0 22029 0
vsize: 88280
[startup+250.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 30298 0 0 0 24927 76 0 0 25 0 1 0 549053430 90427392 12019 4294967295 134512640 134672761 3221224544 3220610064 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 12019 603 41 0 22036 0
vsize: 88308
[startup+260.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 30431 0 0 0 25927 77 0 0 25 0 1 0 549053430 90730496 12110 4294967295 134512640 134672761 3221224544 3220525024 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+270.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 30431 0 0 0 26927 77 0 0 25 0 1 0 549053430 90730496 12110 4294967295 134512640 134672761 3221224544 3219080128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+280.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 30807 0 0 0 27926 77 0 0 25 0 1 0 549053430 91607040 12403 4294967295 134512640 134672761 3221224544 3221205456 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22365 12403 603 41 0 22324 0
vsize: 89460
[startup+290.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31109 0 0 0 28926 78 0 0 25 0 1 0 549053430 91676672 12498 4294967295 134512640 134672761 3221224544 3220759248 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22382 12498 603 41 0 22341 0
vsize: 89528
[startup+300.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31148 0 0 0 29926 78 0 0 25 0 1 0 549053430 91811840 12537 4294967295 134512640 134672761 3221224544 3220400992 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+310.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31148 0 0 0 30926 78 0 0 25 0 1 0 549053430 91811840 12537 4294967295 134512640 134672761 3221224544 3218836576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+320.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31601 0 0 0 31925 79 0 0 25 0 1 0 549053430 92188672 12742 4294967295 134512640 134672761 3221224544 3219088848 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22507 12742 603 41 0 22466 0
vsize: 90028
[startup+330.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31836 0 0 0 32924 80 0 0 25 0 1 0 549053430 92798976 12935 4294967295 134512640 134672761 3221224544 3220743024 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12935 603 41 0 22615 0
vsize: 90624
[startup+340.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31874 0 0 0 33924 80 0 0 25 0 1 0 549053430 92934144 12973 4294967295 134512640 134672761 3221224544 3220382464 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+350.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 31874 0 0 0 34925 80 0 0 25 0 1 0 549053430 92934144 12973 4294967295 134512640 134672761 3221224544 3219040576 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+360.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 34875 0 0 0 35918 87 0 0 25 0 1 0 549053430 99213312 14573 4294967295 134512640 134672761 3221224544 3220950096 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24222 14573 603 41 0 24181 0
vsize: 96888
[startup+370.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 35139 0 0 0 36917 88 0 0 25 0 1 0 549053430 99274752 14672 4294967295 134512640 134672761 3221224544 3220357584 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24237 14672 603 41 0 24196 0
vsize: 96948
[startup+380.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 35287 0 0 0 37917 88 0 0 25 0 1 0 549053430 99577856 14778 4294967295 134512640 134672761 3221224544 3221138160 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14778 603 41 0 24270 0
vsize: 97244
[startup+390.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 35294 0 0 0 38917 88 0 0 25 0 1 0 549053430 99577856 14785 4294967295 134512640 134672761 3221224544 3219907072 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+400.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 35385 0 0 0 39917 88 0 0 25 0 1 0 549053430 99848192 14876 4294967295 134512640 134672761 3221224544 3219531792 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24377 14876 603 41 0 24336 0
vsize: 97508
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 35952 0 0 0 40917 89 0 0 25 0 1 0 549053430 100655104 15160 4294967295 134512640 134672761 3221224544 3218467632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24574 15160 603 41 0 24533 0
vsize: 98296
[startup+420.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36184 0 0 0 41916 90 0 0 25 0 1 0 549053430 101265408 15350 4294967295 134512640 134672761 3221224544 3220039824 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24723 15350 603 41 0 24682 0
vsize: 98892
[startup+430.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36238 0 0 0 42916 90 0 0 25 0 1 0 549053430 101400576 15404 4294967295 134512640 134672761 3221224544 3220706832 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15404 603 41 0 24715 0
vsize: 99024
[startup+440.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36276 0 0 0 43916 90 0 0 25 0 1 0 549053430 101535744 15442 4294967295 134512640 134672761 3221224544 3221164176 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15442 603 41 0 24748 0
vsize: 99156
[startup+450.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36281 0 0 0 44916 90 0 0 25 0 1 0 549053430 101535744 15447 4294967295 134512640 134672761 3221224544 3219624256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+460.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36281 0 0 0 45916 90 0 0 25 0 1 0 549053430 101535744 15447 4294967295 134512640 134672761 3221224544 3219121120 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+470.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36281 0 0 0 46916 90 0 0 25 0 1 0 549053430 101535744 15447 4294967295 134512640 134672761 3221224544 3217983616 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36675 0 0 0 47915 92 0 0 25 0 1 0 549053430 102547456 15758 4294967295 134512640 134672761 3221224544 3220420368 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25036 15758 603 41 0 24995 0
vsize: 100144
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 36919 0 0 0 48915 92 0 0 25 0 1 0 549053430 102436864 15800 4294967295 134512640 134672761 3221224544 3218232240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25009 15800 603 41 0 24968 0
vsize: 100036
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37152 0 0 0 49914 93 0 0 25 0 1 0 549053430 103047168 15991 4294967295 134512640 134672761 3221224544 3219885264 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 15991 603 41 0 25117 0
vsize: 100632
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11345
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37208 0 0 0 50914 93 0 0 25 0 1 0 549053430 103182336 16047 4294967295 134512640 134672761 3221224544 3220559856 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16047 603 41 0 25150 0
vsize: 100764
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37246 0 0 0 51915 93 0 0 25 0 1 0 549053430 103317504 16085 4294967295 134512640 134672761 3221224544 3221020944 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16085 603 41 0 25183 0
vsize: 100896
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37262 0 0 0 52915 93 0 0 25 0 1 0 549053430 103317504 16101 4294967295 134512640 134672761 3221224544 3219681856 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37262 0 0 0 53915 93 0 0 25 0 1 0 549053430 103317504 16101 4294967295 134512640 134672761 3221224544 3219301984 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37262 0 0 0 54915 93 0 0 25 0 1 0 549053430 103317504 16101 4294967295 134512640 134672761 3221224544 3218774176 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37473 0 0 0 55914 94 0 0 25 0 1 0 549053430 103788544 16229 4294967295 134512640 134672761 3221224544 3218226672 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25339 16229 603 41 0 25298 0
vsize: 101356
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37658 0 0 0 56914 94 0 0 25 0 1 0 549053430 104329216 16414 4294967295 134512640 134672761 3221224544 3220488048 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25471 16414 603 41 0 25430 0
vsize: 101884
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 37842 0 0 0 57914 95 0 0 25 0 1 0 549053430 104103936 16398 4294967295 134512640 134672761 3221224544 3218479440 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25416 16398 603 41 0 25375 0
vsize: 101664
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38073 0 0 0 58913 95 0 0 25 0 1 0 549053430 104579072 16587 4294967295 134512640 134672761 3221224544 3220037520 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25532 16587 603 41 0 25491 0
vsize: 102128
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38128 0 0 0 59913 96 0 0 25 0 1 0 549053430 104714240 16642 4294967295 134512640 134672761 3221224544 3220703376 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16642 603 41 0 25524 0
vsize: 102260
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38166 0 0 0 60914 96 0 0 25 0 1 0 549053430 104849408 16680 4294967295 134512640 134672761 3221224544 3221159760 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16680 603 41 0 25557 0
vsize: 102392
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38171 0 0 0 61914 96 0 0 25 0 1 0 549053430 104849408 16685 4294967295 134512640 134672761 3221224544 3219625120 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38171 0 0 0 62914 96 0 0 25 0 1 0 549053430 104849408 16685 4294967295 134512640 134672761 3221224544 3219128128 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+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38171 0 0 0 63914 96 0 0 25 0 1 0 549053430 104849408 16685 4294967295 134512640 134672761 3221224544 3218022016 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38546 0 0 0 64913 96 0 0 25 0 1 0 549053430 105725952 16977 4294967295 134512640 134672761 3221224544 3220362192 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25812 16977 603 41 0 25771 0
vsize: 103248
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38726 0 0 0 65913 97 0 0 25 0 1 0 549053430 105455616 16957 4294967295 134512640 134672761 3221224544 3218376720 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25746 16957 603 41 0 25705 0
vsize: 102984
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 38960 0 0 0 66913 97 0 0 25 0 1 0 549053430 106065920 17149 4294967295 134512640 134672761 3221224544 3220018608 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 17149 603 41 0 25854 0
vsize: 103580
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39015 0 0 0 67913 98 0 0 25 0 1 0 549053430 106201088 17204 4294967295 134512640 134672761 3221224544 3220692144 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17204 603 41 0 25887 0
vsize: 103712
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39053 0 0 0 68913 98 0 0 25 0 1 0 549053430 106336256 17242 4294967295 134512640 134672761 3221224544 3221152368 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17242 603 41 0 25920 0
vsize: 103844
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39058 0 0 0 69913 98 0 0 25 0 1 0 549053430 106336256 17247 4294967295 134512640 134672761 3221224544 3219634144 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+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39058 0 0 0 70913 98 0 0 25 0 1 0 549053430 106336256 17247 4294967295 134512640 134672761 3221224544 3219139744 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+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39058 0 0 0 71913 98 0 0 25 0 1 0 549053430 106336256 17247 4294967295 134512640 134672761 3221224544 3218044000 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+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39433 0 0 0 72913 99 0 0 25 0 1 0 549053430 107212800 17539 4294967295 134512640 134672761 3221224544 3220349424 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26175 17539 603 41 0 26134 0
vsize: 104700
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39613 0 0 0 73913 99 0 0 25 0 1 0 549053430 107003904 17519 4294967295 134512640 134672761 3221224544 3218341488 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26124 17519 603 41 0 26083 0
vsize: 104496
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39847 0 0 0 74912 100 0 0 25 0 1 0 549053430 120061952 17711 4294967295 134512640 134672761 3221224544 3220021488 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29312 17711 603 41 0 29271 0
vsize: 117248
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39902 0 0 0 75912 100 0 0 25 0 1 0 549053430 120197120 17766 4294967295 134512640 134672761 3221224544 3220697808 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17766 603 41 0 29304 0
vsize: 117380
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39941 0 0 0 76912 100 0 0 25 0 1 0 549053430 120332288 17805 4294967295 134512640 134672761 3221224544 3221159664 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17805 603 41 0 29337 0
vsize: 117512
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39945 0 0 0 77912 100 0 0 25 0 1 0 549053430 120332288 17809 4294967295 134512640 134672761 3221224544 3219633088 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+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39945 0 0 0 78912 100 0 0 25 0 1 0 549053430 120332288 17809 4294967295 134512640 134672761 3221224544 3219124384 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+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 39945 0 0 0 79912 101 0 0 25 0 1 0 549053430 120332288 17809 4294967295 134512640 134672761 3221224544 3217973152 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+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11347
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40325 0 0 0 80911 101 0 0 25 0 1 0 549053430 121208832 18106 4294967295 134512640 134672761 3221224544 3220433808 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29592 18106 603 41 0 29551 0
vsize: 118368
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40641 0 0 0 81911 102 0 0 25 0 1 0 549053430 121425920 18215 4294967295 134512640 134672761 3221224544 3218019984 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29645 18215 603 41 0 29604 0
vsize: 118580
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40864 0 0 0 82911 103 0 0 25 0 1 0 549053430 122036224 18396 4294967295 134512640 134672761 3221224544 3219458928 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18396 603 41 0 29753 0
vsize: 119176
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40918 0 0 0 83911 103 0 0 25 0 1 0 549053430 122171392 18450 4294967295 134512640 134672761 3221224544 3220111152 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18450 603 41 0 29786 0
vsize: 119308
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40954 0 0 0 84911 103 0 0 25 0 1 0 549053430 122306560 18486 4294967295 134512640 134672761 3221224544 3220560816 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18486 603 41 0 29819 0
vsize: 119440
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 40983 0 0 0 85911 103 0 0 25 0 1 0 549053430 122306560 18515 4294967295 134512640 134672761 3221224544 3220898448 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18515 603 41 0 29819 0
vsize: 119440
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41005 0 0 0 86911 103 0 0 25 0 1 0 549053430 122441728 18537 4294967295 134512640 134672761 3221224544 3221178288 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18537 603 41 0 29852 0
vsize: 119572
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41009 0 0 0 87911 103 0 0 25 0 1 0 549053430 122441728 18541 4294967295 134512640 134672761 3221224544 3219193792 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+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41009 0 0 0 88911 104 0 0 25 0 1 0 549053430 122441728 18541 4294967295 134512640 134672761 3221224544 3218919232 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+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41009 0 0 0 89911 104 0 0 25 0 1 0 549053430 122441728 18541 4294967295 134512640 134672761 3221224544 3218595328 134594092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41009 0 0 0 90911 104 0 0 25 0 1 0 549053430 122441728 18541 4294967295 134512640 134672761 3221224544 3218168512 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+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41009 0 0 0 91911 104 0 0 25 0 1 0 549053430 122441728 18541 4294967295 134512640 134672761 3221224544 3217441312 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+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41359 0 0 0 92911 105 0 0 25 0 1 0 549053430 123183104 18808 4294967295 134512640 134672761 3221224544 3219438096 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 18808 603 41 0 30033 0
vsize: 120296
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41452 0 0 0 93911 105 0 0 25 0 1 0 549053430 123453440 18901 4294967295 134512640 134672761 3221224544 3220485168 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30140 18901 603 41 0 30099 0
vsize: 120560
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 41528 0 0 0 94911 105 0 0 25 0 1 0 549053430 123723776 18977 4294967295 134512640 134672761 3221224544 3221105712 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 18977 603 41 0 30165 0
vsize: 120824
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 42114 0 0 0 95909 107 0 0 25 0 1 0 549053430 124223488 19272 4294967295 134512640 134672761 3221224544 3220619872 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30328 19272 603 41 0 30287 0
vsize: 121312
[startup+969.39 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 11349
Raw data (stat): 11343 (minisat+) R 11342 22929 22928 0 -1 0 42114 0 0 0 95909 107 0 0 25 0 1 0 549053430 124223488 19272 4294967295 134512640 134672761 3221224544 3220619872 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30328 19272 603 41 0 30287 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 969.389
CPU time (s): 969.544
CPU user time (s): 967.669
CPU system time (s): 1.87471
CPU usage (%): 100.016
Max. virtual memory (Kb): 121312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####