PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/een/normalized-nw04.opb
MD5SUM	c4c13764e2ea959929790d6ef6d0273c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	42031
Number of bits of the biggest number in a constraint	16
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	18.0483
Number of variables	87482
Total number of constraints	72
Number of constraints which are clauses	36
Number of constraints which are cardinality constraints (but not clauses)	36
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	599
Maximum length of a constraint	42032
Trace number 7049

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 21:06:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5095 boxname=wulflinc2 idbench=392 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c4c13764e2ea959929790d6ef6d0273c  /oldhome/oroussel/tmp/wulflinc2/normalized-nw04.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc2/normalized-nw04.opb /oldhome/oroussel/tmp/wulflinc2/normalized-nw04.opb
IDLAUNCH: 5095
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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	: 2
cpu MHz		: 451.191
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:        849816 kB
Buffers:         36052 kB
Cached:         127076 kB
SwapCached:          4 kB
Active:          75396 kB
Inactive:        90640 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        849564 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            13140 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:25:42 (client local time) WITH STATUS 0 IN 1130.14 SECONDS
stats: 5095 7 1130.14 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): 1.01 0.99 0.89 2/54 32646
Raw data (stat): 32646 (runsolver) R 32645 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429484336 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0014 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 24768 0 0 0 934 64 0 0 25 0 1 0 429484336 64999424 7295 4294967295 134512640 134672761 3221224560 3221107936 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15869 7295 603 41 0 15828 0
vsize: 63476
[startup+20.0015 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 24837 0 0 0 1934 64 0 0 25 0 1 0 429484336 65282048 7364 4294967295 134512640 134672761 3221224560 3220546256 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15938 7364 603 41 0 15897 0
vsize: 63752
[startup+30.0022 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 25304 0 0 0 2933 66 0 0 25 0 1 0 429484336 68685824 7831 4294967295 134512640 134672761 3221224560 3220873600 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16769 7831 603 41 0 16728 0
vsize: 67076
[startup+40.0034 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26061 0 0 0 3931 68 0 0 25 0 1 0 429484336 71401472 8588 4294967295 134512640 134672761 3221224560 3220734496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17432 8588 603 41 0 17391 0
vsize: 69728
[startup+50.0036 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26178 0 0 0 4931 68 0 0 25 0 1 0 429484336 71413760 8705 4294967295 134512640 134672761 3221224560 3220991024 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17435 8705 603 41 0 17394 0
vsize: 69740
[startup+60.0043 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26309 0 0 0 5931 68 0 0 25 0 1 0 429484336 71462912 8836 4294967295 134512640 134672761 3221224560 3220673536 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17447 8836 603 41 0 17406 0
vsize: 69788
[startup+70.0046 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26499 0 0 0 6930 69 0 0 25 0 1 0 429484336 75001856 9026 4294967295 134512640 134672761 3221224560 3221064256 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18311 9026 603 41 0 18270 0
vsize: 73244
[startup+80.0057 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26581 0 0 0 7930 70 0 0 25 0 1 0 429484336 75038720 9108 4294967295 134512640 134672761 3221224560 3220350400 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18320 9108 603 41 0 18279 0
vsize: 73280
[startup+90.0054 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 26723 0 0 0 8929 71 0 0 25 0 1 0 429484336 75513856 9250 4294967295 134512640 134672761 3221224560 3220113568 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18436 9250 603 41 0 18395 0
vsize: 73744
[startup+100.006 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 28300 0 0 0 9925 75 0 0 25 0 1 0 429484336 78548992 10085 4294967295 134512640 134672761 3221224560 3220584272 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19177 10085 603 41 0 19136 0
vsize: 76708
[startup+110.006 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 28641 0 0 0 10925 76 0 0 25 0 1 0 429484336 79187968 10301 4294967295 134512640 134672761 3221224560 3220266304 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19333 10301 603 41 0 19292 0
vsize: 77332
[startup+120.007 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 28742 0 0 0 11925 76 0 0 25 0 1 0 429484336 79495168 10402 4294967295 134512640 134672761 3221224560 3220064048 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19408 10402 603 41 0 19367 0
vsize: 77632
[startup+130.008 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 29208 0 0 0 12923 77 0 0 25 0 1 0 429484336 80482304 10743 4294967295 134512640 134672761 3221224560 3220394272 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19649 10743 603 41 0 19608 0
vsize: 78596
[startup+140.008 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 29352 0 0 0 13923 78 0 0 25 0 1 0 429484336 80785408 10845 4294967295 134512640 134672761 3221224560 3220913840 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19723 10845 603 41 0 19682 0
vsize: 78892
[startup+150.008 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 29468 0 0 0 14923 78 0 0 25 0 1 0 429484336 81055744 10961 4294967295 134512640 134672761 3221224560 3220556704 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19789 10961 603 41 0 19748 0
vsize: 79156
[startup+160.009 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 29975 0 0 0 15922 79 0 0 25 0 1 0 429484336 81801216 11220 4294967295 134512640 134672761 3221224560 3220475104 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19971 11220 603 41 0 19930 0
vsize: 79884
[startup+170.009 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30120 0 0 0 16922 80 0 0 25 0 1 0 429484336 82104320 11323 4294967295 134512640 134672761 3221224560 3220764848 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20045 11323 603 41 0 20004 0
vsize: 80180
[startup+180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30120 0 0 0 17921 80 0 0 25 0 1 0 429484336 82104320 11323 4294967295 134512640 134672761 3221224560 3219819728 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20045 11323 603 41 0 20004 0
vsize: 80180
[startup+190.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30469 0 0 0 18920 81 0 0 25 0 1 0 429484336 82980864 11589 4294967295 134512640 134672761 3221224560 3220883296 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20259 11589 603 41 0 20218 0
vsize: 81036
[startup+200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30724 0 0 0 19919 83 0 0 25 0 1 0 429484336 83161088 11679 4294967295 134512640 134672761 3221224560 3220447744 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20303 11679 603 41 0 20262 0
vsize: 81212
[startup+210.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30870 0 0 0 20919 83 0 0 25 0 1 0 429484336 83464192 11783 4294967295 134512640 134672761 3221224560 3220889360 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20377 11783 603 41 0 20336 0
vsize: 81508
[startup+220.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 30870 0 0 0 21919 83 0 0 25 0 1 0 429484336 83464192 11783 4294967295 134512640 134672761 3221224560 3219949232 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20377 11783 603 41 0 20336 0
vsize: 81508
[startup+230.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31179 0 0 0 22918 84 0 0 25 0 1 0 429484336 90497024 12009 4294967295 134512640 134672761 3221224560 3220451008 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22094 12009 603 41 0 22053 0
vsize: 88376
[startup+240.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31423 0 0 0 23918 85 0 0 25 0 1 0 429484336 90480640 12088 4294967295 134512640 134672761 3221224560 3220058368 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22090 12088 603 41 0 22049 0
vsize: 88360
[startup+250.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31584 0 0 0 24917 85 0 0 25 0 1 0 429484336 90918912 12207 4294967295 134512640 134672761 3221224560 3221007136 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22197 12207 603 41 0 22156 0
vsize: 88788
[startup+260.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31602 0 0 0 25917 86 0 0 25 0 1 0 429484336 90918912 12225 4294967295 134512640 134672761 3221224560 3220281968 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22197 12225 603 41 0 22156 0
vsize: 88788
[startup+270.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31602 0 0 0 26917 86 0 0 25 0 1 0 429484336 90918912 12225 4294967295 134512640 134672761 3221224560 3218765648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22197 12225 603 41 0 22156 0
vsize: 88788
[startup+280.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 31971 0 0 0 27916 87 0 0 25 0 1 0 429484336 91795456 12511 4294967295 134512640 134672761 3221224560 3221128576 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22411 12511 603 41 0 22370 0
vsize: 89644
[startup+290.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 32192 0 0 0 28915 88 0 0 25 0 1 0 429484336 91746304 12567 4294967295 134512640 134672761 3221224560 3220570144 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22399 12567 603 41 0 22358 0
vsize: 89596
[startup+300.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 32328 0 0 0 29915 88 0 0 25 0 1 0 429484336 92049408 12661 4294967295 134512640 134672761 3221224560 3220625072 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22473 12661 603 41 0 22432 0
vsize: 89892
[startup+310.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 32328 0 0 0 30915 89 0 0 25 0 1 0 429484336 92049408 12661 4294967295 134512640 134672761 3221224560 3219884240 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22473 12661 603 41 0 22432 0
vsize: 89892
[startup+320.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 32627 0 0 0 31914 90 0 0 25 0 1 0 429484336 92655616 12877 4294967295 134512640 134672761 3221224560 3220248832 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22621 12877 603 41 0 22580 0
vsize: 90484
[startup+330.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 32882 0 0 0 32913 90 0 0 25 0 1 0 429484336 92815360 12967 4294967295 134512640 134672761 3221224560 3219715744 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22660 12967 603 41 0 22619 0
vsize: 90640
[startup+340.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 35677 0 0 0 33906 98 0 0 25 0 1 0 429484336 98521088 14402 4294967295 134512640 134672761 3221224560 3220762336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24053 14402 603 41 0 24012 0
vsize: 96212
[startup+350.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 35715 0 0 0 34905 98 0 0 25 0 1 0 429484336 98656256 14440 4294967295 134512640 134672761 3221224560 3220461584 134594103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24086 14440 603 41 0 24045 0
vsize: 96344
[startup+360.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 35715 0 0 0 35905 98 0 0 25 0 1 0 429484336 98656256 14440 4294967295 134512640 134672761 3221224560 3219754160 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24086 14440 603 41 0 24045 0
vsize: 96344
[startup+370.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36007 0 0 0 36904 100 0 0 25 0 1 0 429484336 99262464 14649 4294967295 134512640 134672761 3221224560 3220082464 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24234 14649 603 41 0 24193 0
vsize: 96936
[startup+380.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36211 0 0 0 37904 100 0 0 25 0 1 0 429484336 99160064 14688 4294967295 134512640 134672761 3221224560 3219419872 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24209 14688 603 41 0 24168 0
vsize: 96836
[startup+390.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36419 0 0 0 38903 101 0 0 25 0 1 0 429484336 99770368 14854 4294967295 134512640 134672761 3221224560 3220679584 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24358 14854 603 41 0 24317 0
vsize: 97432
[startup+400.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36464 0 0 0 39904 101 0 0 25 0 1 0 429484336 99905536 14899 4294967295 134512640 134672761 3221224560 3220498544 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24391 14899 603 41 0 24350 0
vsize: 97564
[startup+410.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36464 0 0 0 40904 101 0 0 25 0 1 0 429484336 99905536 14899 4294967295 134512640 134672761 3221224560 3219863120 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24391 14899 603 41 0 24350 0
vsize: 97564
[startup+420.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36551 0 0 0 41903 101 0 0 25 0 1 0 429484336 100040704 14986 4294967295 134512640 134672761 3221224560 3219550912 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24424 14986 603 41 0 24383 0
vsize: 97696
[startup+430.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 36855 0 0 0 42903 102 0 0 25 0 1 0 429484336 100782080 15207 4294967295 134512640 134672761 3221224560 3221221408 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24605 15207 603 41 0 24564 0
vsize: 98420
[startup+440.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37170 0 0 0 43903 103 0 0 25 0 1 0 429484336 100970496 15315 4294967295 134512640 134672761 3221224560 3220463872 134594231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24651 15315 603 41 0 24610 0
vsize: 98604
[startup+450.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37224 0 0 0 44903 103 0 0 25 0 1 0 429484336 101105664 15369 4294967295 134512640 134672761 3221224560 3221128096 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24684 15369 603 41 0 24643 0
vsize: 98736
[startup+460.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37232 0 0 0 45903 103 0 0 25 0 1 0 429484336 101105664 15377 4294967295 134512640 134672761 3221224560 3220066160 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24684 15377 603 41 0 24643 0
vsize: 98736
[startup+470.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37232 0 0 0 46903 103 0 0 25 0 1 0 429484336 101105664 15377 4294967295 134512640 134672761 3221224560 3218956016 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24684 15377 603 41 0 24643 0
vsize: 98736
[startup+480.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37569 0 0 0 47903 103 0 0 25 0 1 0 429484336 101847040 15631 4294967295 134512640 134672761 3221224560 3220513888 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24865 15631 603 41 0 24824 0
vsize: 99460
[startup+490.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 37936 0 0 0 48902 104 0 0 25 0 1 0 429484336 102494208 15833 4294967295 134512640 134672761 3221224560 3219189376 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25023 15833 603 41 0 24982 0
vsize: 100092
[startup+500.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38099 0 0 0 49902 104 0 0 25 0 1 0 429484336 102797312 15954 4294967295 134512640 134672761 3221224560 3220171072 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25097 15954 603 41 0 25056 0
vsize: 100388
[startup+510.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38144 0 0 0 50902 104 0 0 25 0 1 0 429484336 102932480 15999 4294967295 134512640 134672761 3221224560 3220713856 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25130 15999 603 41 0 25089 0
vsize: 100520
[startup+520.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38175 0 0 0 51902 105 0 0 25 0 1 0 429484336 103067648 16030 4294967295 134512640 134672761 3221224560 3221101408 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 16030 603 41 0 25122 0
vsize: 100652
[startup+530.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38185 0 0 0 52902 105 0 0 25 0 1 0 429484336 103067648 16040 4294967295 134512640 134672761 3221224560 3219754736 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 16040 603 41 0 25122 0
vsize: 100652
[startup+540.015 s]
Raw data (loadavg): 1.08 1.00 0.91 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38185 0 0 0 53902 105 0 0 25 0 1 0 429484336 103067648 16040 4294967295 134512640 134672761 3221224560 3219374960 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 16040 603 41 0 25122 0
vsize: 100652
[startup+550.015 s]
Raw data (loadavg): 1.14 1.02 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38185 0 0 0 54903 105 0 0 25 0 1 0 429484336 103067648 16040 4294967295 134512640 134672761 3221224560 3218873456 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 16040 603 41 0 25122 0
vsize: 100652
[startup+560.015 s]
Raw data (loadavg): 1.12 1.02 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38185 0 0 0 55903 105 0 0 25 0 1 0 429484336 103067648 16040 4294967295 134512640 134672761 3221224560 3218002544 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25163 16040 603 41 0 25122 0
vsize: 100652
[startup+570.015 s]
Raw data (loadavg): 1.10 1.02 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38561 0 0 0 56902 105 0 0 25 0 1 0 429484336 103944192 16333 4294967295 134512640 134672761 3221224560 3220270816 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25377 16333 603 41 0 25336 0
vsize: 101508
[startup+580.015 s]
Raw data (loadavg): 1.08 1.02 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38670 0 0 0 57902 105 0 0 25 0 1 0 429484336 104349696 16442 4294967295 134512640 134672761 3221224560 3221150368 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25476 16442 603 41 0 25435 0
vsize: 101904
[startup+590.015 s]
Raw data (loadavg): 1.07 1.02 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 38885 0 0 0 58902 106 0 0 25 0 1 0 429484336 104288256 16492 4294967295 134512640 134672761 3221224560 3219756832 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25461 16492 603 41 0 25420 0
vsize: 101844
[startup+600.015 s]
Raw data (loadavg): 1.06 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39025 0 0 0 59901 107 0 0 25 0 1 0 429484336 104591360 16590 4294967295 134512640 134672761 3221224560 3220463776 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25535 16590 603 41 0 25494 0
vsize: 102140
[startup+610.016 s]
Raw data (loadavg): 1.05 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39062 0 0 0 60901 107 0 0 25 0 1 0 429484336 104726528 16627 4294967295 134512640 134672761 3221224560 3220910176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16627 603 41 0 25527 0
vsize: 102272
[startup+620.015 s]
Raw data (loadavg): 1.04 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39087 0 0 0 61901 107 0 0 25 0 1 0 429484336 104726528 16652 4294967295 134512640 134672761 3221224560 3220469360 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+630.015 s]
Raw data (loadavg): 1.04 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39087 0 0 0 62902 107 0 0 25 0 1 0 429484336 104726528 16652 4294967295 134512640 134672761 3221224560 3219580496 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+640.016 s]
Raw data (loadavg): 1.03 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39087 0 0 0 63902 107 0 0 25 0 1 0 429484336 104726528 16652 4294967295 134512640 134672761 3221224560 3219157136 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+650.015 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39087 0 0 0 64902 107 0 0 25 0 1 0 429484336 104726528 16652 4294967295 134512640 134672761 3221224560 3218378384 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25568 16652 603 41 0 25527 0
vsize: 102272
[startup+660.015 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39368 0 0 0 65901 108 0 0 25 0 1 0 429484336 105332736 16850 4294967295 134512640 134672761 3221224560 3219220768 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25716 16850 603 41 0 25675 0
vsize: 102864
[startup+670.015 s]
Raw data (loadavg): 1.02 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39494 0 0 0 66901 108 0 0 25 0 1 0 429484336 105738240 16976 4294967295 134512640 134672761 3221224560 3220755232 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25815 16976 603 41 0 25774 0
vsize: 103260
[startup+680.014 s]
Raw data (loadavg): 1.01 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39690 0 0 0 67901 109 0 0 25 0 1 0 429484336 105586688 17007 4294967295 134512640 134672761 3221224560 3219142912 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25778 17007 603 41 0 25737 0
vsize: 103112
[startup+690.014 s]
Raw data (loadavg): 1.01 1.01 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39853 0 0 0 68901 109 0 0 25 0 1 0 429484336 105889792 17128 4294967295 134512640 134672761 3221224560 3220144960 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25852 17128 603 41 0 25811 0
vsize: 103408
[startup+700.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39898 0 0 0 69901 109 0 0 25 0 1 0 429484336 106024960 17173 4294967295 134512640 134672761 3221224560 3220693024 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25885 17173 603 41 0 25844 0
vsize: 103540
[startup+710.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39929 0 0 0 70901 109 0 0 25 0 1 0 429484336 106160128 17204 4294967295 134512640 134672761 3221224560 3221082400 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17204 603 41 0 25877 0
vsize: 103672
[startup+720.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39941 0 0 0 71901 109 0 0 25 0 1 0 429484336 106160128 17216 4294967295 134512640 134672761 3221224560 3219764912 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39941 0 0 0 72901 109 0 0 25 0 1 0 429484336 106160128 17216 4294967295 134512640 134672761 3221224560 3219394928 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+740.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39941 0 0 0 73901 109 0 0 25 0 1 0 429484336 106160128 17216 4294967295 134512640 134672761 3221224560 3218907440 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+750.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 39941 0 0 0 74902 109 0 0 25 0 1 0 429484336 106160128 17216 4294967295 134512640 134672761 3221224560 3218059376 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25918 17216 603 41 0 25877 0
vsize: 103672
[startup+760.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40300 0 0 0 75901 110 0 0 25 0 1 0 429484336 107036672 17492 4294967295 134512640 134672761 3221224560 3220162240 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26132 17492 603 41 0 26091 0
vsize: 104528
[startup+770.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40376 0 0 0 76901 110 0 0 25 0 1 0 429484336 107171840 17568 4294967295 134512640 134672761 3221224560 3221104576 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26165 17568 603 41 0 26124 0
vsize: 104660
[startup+780.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40585 0 0 0 77901 110 0 0 25 0 1 0 429484336 119660544 17612 4294967295 134512640 134672761 3221224560 3219683968 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29214 17612 603 41 0 29173 0
vsize: 116856
[startup+790.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40729 0 0 0 78901 110 0 0 25 0 1 0 429484336 120098816 17714 4294967295 134512640 134672761 3221224560 3220420384 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29321 17714 603 41 0 29280 0
vsize: 117284
[startup+800.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40766 0 0 0 79901 111 0 0 25 0 1 0 429484336 120098816 17751 4294967295 134512640 134672761 3221224560 3220877056 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29321 17751 603 41 0 29280 0
vsize: 117284
[startup+810.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40795 0 0 0 80901 111 0 0 25 0 1 0 429484336 120233984 17780 4294967295 134512640 134672761 3221224560 3220865360 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+820.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40795 0 0 0 81901 111 0 0 25 0 1 0 429484336 120233984 17780 4294967295 134512640 134672761 3221224560 3219609776 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+830.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40795 0 0 0 82901 111 0 0 25 0 1 0 429484336 120233984 17780 4294967295 134512640 134672761 3221224560 3219198992 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+840.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 40795 0 0 0 83902 111 0 0 25 0 1 0 429484336 120233984 17780 4294967295 134512640 134672761 3221224560 3218467088 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29354 17780 603 41 0 29313 0
vsize: 117416
[startup+850.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41043 0 0 0 84901 111 0 0 25 0 1 0 429484336 120705024 17945 4294967295 134512640 134672761 3221224560 3218820928 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29469 17945 603 41 0 29428 0
vsize: 117876
[startup+860.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41194 0 0 0 85901 112 0 0 25 0 1 0 429484336 121110528 18096 4294967295 134512640 134672761 3221224560 3220653280 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29568 18096 603 41 0 29527 0
vsize: 118272
[startup+870.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41422 0 0 0 86901 112 0 0 25 0 1 0 429484336 121204736 18159 4294967295 134512640 134672761 3221224560 3218799424 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29591 18159 603 41 0 29550 0
vsize: 118364
[startup+880.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41584 0 0 0 87901 112 0 0 25 0 1 0 429484336 121507840 18279 4294967295 134512640 134672761 3221224560 3219931648 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29665 18279 603 41 0 29624 0
vsize: 118660
[startup+890.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41631 0 0 0 88901 112 0 0 25 0 1 0 429484336 121643008 18326 4294967295 134512640 134672761 3221224560 3220510432 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29698 18326 603 41 0 29657 0
vsize: 118792
[startup+900.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41663 0 0 0 89901 112 0 0 25 0 1 0 429484336 121778176 18358 4294967295 134512640 134672761 3221224560 3220911136 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18358 603 41 0 29690 0
vsize: 118924
[startup+910.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41690 0 0 0 90901 112 0 0 25 0 1 0 429484336 121778176 18385 4294967295 134512640 134672761 3221224560 3220673936 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41690 0 0 0 91901 112 0 0 25 0 1 0 429484336 121778176 18385 4294967295 134512640 134672761 3221224560 3219511856 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+930.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41690 0 0 0 92902 112 0 0 25 0 1 0 429484336 121778176 18385 4294967295 134512640 134672761 3221224560 3219143888 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41690 0 0 0 93902 112 0 0 25 0 1 0 429484336 121778176 18385 4294967295 134512640 134672761 3221224560 3218637488 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+950.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 41690 0 0 0 94902 112 0 0 25 0 1 0 429484336 121778176 18385 4294967295 134512640 134672761 3221224560 3217854896 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29731 18385 603 41 0 29690 0
vsize: 118924
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42053 0 0 0 95902 113 0 0 25 0 1 0 429484336 122654720 18665 4294967295 134512640 134672761 3221224560 3220097728 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29945 18665 603 41 0 29904 0
vsize: 119780
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42127 0 0 0 96901 113 0 0 25 0 1 0 429484336 122925056 18739 4294967295 134512640 134672761 3221224560 3220996000 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30011 18739 603 41 0 29970 0
vsize: 120044
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42456 0 0 0 97901 114 0 0 25 0 1 0 429484336 123228160 18903 4294967295 134512640 134672761 3221224560 3218887360 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30085 18903 603 41 0 30044 0
vsize: 120340
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42606 0 0 0 98901 114 0 0 25 0 1 0 429484336 123666432 19011 4294967295 134512640 134672761 3221224560 3219704224 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30192 19011 603 41 0 30151 0
vsize: 120768
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42646 0 0 0 99901 114 0 0 25 0 1 0 429484336 123801600 19051 4294967295 134512640 134672761 3221224560 3220192192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30225 19051 603 41 0 30184 0
vsize: 120900
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42676 0 0 0 100901 114 0 0 25 0 1 0 429484336 123801600 19081 4294967295 134512640 134672761 3221224560 3220559008 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30225 19081 603 41 0 30184 0
vsize: 120900
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42702 0 0 0 101901 114 0 0 25 0 1 0 429484336 123936768 19107 4294967295 134512640 134672761 3221224560 3220869664 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19107 603 41 0 30217 0
vsize: 121032
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42724 0 0 0 102901 114 0 0 25 0 1 0 429484336 123936768 19129 4294967295 134512640 134672761 3221224560 3221139232 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19129 603 41 0 30217 0
vsize: 121032
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 103902 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3219585584 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 104902 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3219058832 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 105902 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3218774384 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 106902 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3218439344 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 107902 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3217936592 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 42730 0 0 0 108903 114 0 0 25 0 1 0 429484336 123936768 19135 4294967295 134512640 134672761 3221224560 3217430000 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30258 19135 603 41 0 30217 0
vsize: 121032
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 43072 0 0 0 109902 115 0 0 25 0 1 0 429484336 124678144 19394 4294967295 134512640 134672761 3221224560 3219333184 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30439 19394 603 41 0 30398 0
vsize: 121756
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 43165 0 0 0 110902 115 0 0 25 0 1 0 429484336 124948480 19487 4294967295 134512640 134672761 3221224560 3220402720 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30505 19487 603 41 0 30464 0
vsize: 122020
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 43243 0 0 0 111902 115 0 0 25 0 1 0 429484336 125218816 19565 4294967295 134512640 134672761 3221224560 3221028352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30571 19565 603 41 0 30530 0
vsize: 122284
[startup+1129.97 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 32646
Raw data (stat): 32646 (minisat+) R 32645 20937 20936 0 -1 0 43243 0 0 0 111902 115 0 0 25 0 1 0 429484336 125218816 19565 4294967295 134512640 134672761 3221224560 3221028352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30571 19565 603 41 0 30530 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1129.97
CPU time (s): 1130.14
CPU user time (s): 1128.04
CPU system time (s): 2.10368
CPU usage (%): 100.015
Max. virtual memory (Kb): 122284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####