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/miplib2003/normalized-mps-v2-20-10-nw04.opb
MD5SUM	5a18ff1f45b144b201f1f80233dc9b6b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	30407
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	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	SAT
Best CPU time to get the best result obtained on this benchmark	1197.16
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 21660

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-22 00:36:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12868 boxname=wulflinc6 idbench=990 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 12868
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        710004 kB
Buffers:         20652 kB
Cached:         282452 kB
SwapCached:        516 kB
Active:          49192 kB
Inactive:       255920 kB
HighTotal:      131008 kB
HighFree:        14924 kB
LowTotal:       903652 kB
LowFree:        695080 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            13760 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:56:14 (client local time) WITH STATUS 0 IN 1162.48 SECONDS
stats: 12868 7 1162.48 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.93 0.97 0.91 2/54 574
Raw data (stat): 574 (runsolver) R 573 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491230123 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 23768 0 0 0 927 65 0 0 25 0 1 0 491230123 69439488 8007 4294967295 134512640 134672761 3221224544 3220347984 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16953 8007 603 41 0 16912 0
vsize: 67812
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 23768 0 0 0 1927 65 0 0 25 0 1 0 491230123 69439488 8007 4294967295 134512640 134672761 3221224544 3220829136 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 8007 603 41 0 16912 0
vsize: 67812
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 24113 0 0 0 2926 66 0 0 25 0 1 0 491230123 70852608 8352 4294967295 134512640 134672761 3221224544 3220721328 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17298 8352 603 41 0 17257 0
vsize: 69192
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 24501 0 0 0 3926 67 0 0 25 0 1 0 491230123 73998336 8740 4294967295 134512640 134672761 3221224544 3220406944 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18066 8740 603 41 0 18025 0
vsize: 72264
[startup+50.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 24742 0 0 0 4926 67 0 0 25 0 1 0 491230123 74629120 8981 4294967295 134512640 134672761 3221224544 3220628128 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18220 8981 603 41 0 18179 0
vsize: 72880
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 25447 0 0 0 5924 69 0 0 25 0 1 0 491230123 75976704 9356 4294967295 134512640 134672761 3221224544 3220968816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 9356 603 41 0 18508 0
vsize: 74196
[startup+70.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 25556 0 0 0 6924 69 0 0 25 0 1 0 491230123 75976704 9465 4294967295 134512640 134672761 3221224544 3221031616 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 9465 603 41 0 18508 0
vsize: 74196
[startup+80.0015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 25636 0 0 0 7924 70 0 0 25 0 1 0 491230123 75976704 9545 4294967295 134512640 134672761 3221224544 3220582048 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 9545 603 41 0 18508 0
vsize: 74196
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 25867 0 0 0 8924 70 0 0 25 0 1 0 491230123 79294464 9693 4294967295 134512640 134672761 3221224544 3220919760 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19359 9693 603 41 0 19318 0
vsize: 77436
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 26075 0 0 0 9924 71 0 0 25 0 1 0 491230123 79867904 9859 4294967295 134512640 134672761 3221224544 3220995792 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19499 9859 603 41 0 19458 0
vsize: 77996
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 26275 0 0 0 10924 71 0 0 25 0 1 0 491230123 80044032 9976 4294967295 134512640 134672761 3221224544 3220348480 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19542 9976 603 41 0 19501 0
vsize: 78168
[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28196 0 0 0 11921 75 0 0 25 0 1 0 491230123 84406272 11113 4294967295 134512640 134672761 3221224544 3219619152 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20607 11113 603 41 0 20566 0
vsize: 82428
[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28349 0 0 0 12921 76 0 0 25 0 1 0 491230123 84709376 11224 4294967295 134512640 134672761 3221224544 3220656336 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20681 11224 603 41 0 20640 0
vsize: 82724
[startup+140.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28395 0 0 0 13923 76 0 0 25 0 1 0 491230123 84844544 11270 4294967295 134512640 134672761 3221224544 3221218512 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 11270 603 41 0 20673 0
vsize: 82856
[startup+150.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28396 0 0 0 14923 76 0 0 25 0 1 0 491230123 84844544 11271 4294967295 134512640 134672761 3221224544 3219999136 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+160.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28396 0 0 0 15923 76 0 0 25 0 1 0 491230123 84844544 11271 4294967295 134512640 134672761 3221224544 3218705248 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+170.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 28828 0 0 0 16923 77 0 0 25 0 1 0 491230123 85991424 11620 4294967295 134512640 134672761 3221224544 3220969872 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20994 11620 603 41 0 20953 0
vsize: 83976
[startup+180.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29048 0 0 0 17923 77 0 0 25 0 1 0 491230123 85868544 11675 4294967295 134512640 134672761 3221224544 3220576176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20964 11675 603 41 0 20923 0
vsize: 83856
[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29185 0 0 0 18923 77 0 0 25 0 1 0 491230123 86171648 11770 4294967295 134512640 134672761 3221224544 3220791808 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+200.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29185 0 0 0 19924 77 0 0 25 0 1 0 491230123 86171648 11770 4294967295 134512640 134672761 3221224544 3220014976 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+210.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29509 0 0 0 20924 78 0 0 25 0 1 0 491230123 86913024 12011 4294967295 134512640 134672761 3221224544 3220757040 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21219 12011 603 41 0 21178 0
vsize: 84876
[startup+220.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29730 0 0 0 21923 79 0 0 25 0 1 0 491230123 86896640 12067 4294967295 134512640 134672761 3221224544 3220820880 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21215 12067 603 41 0 21174 0
vsize: 84860
[startup+230.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29846 0 0 0 22923 79 0 0 25 0 1 0 491230123 87199744 12141 4294967295 134512640 134672761 3221224544 3220722880 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21289 12141 603 41 0 21248 0
vsize: 85156
[startup+240.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 29991 0 0 0 23923 79 0 0 25 0 1 0 491230123 87605248 12286 4294967295 134512640 134672761 3221224544 3220909776 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21388 12286 603 41 0 21347 0
vsize: 85552
[startup+250.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 30374 0 0 0 24923 80 0 0 25 0 1 0 491230123 87785472 12421 4294967295 134512640 134672761 3221224544 3220517712 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21432 12421 603 41 0 21391 0
vsize: 85728
[startup+260.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 30513 0 0 0 25923 81 0 0 25 0 1 0 491230123 88088576 12518 4294967295 134512640 134672761 3221224544 3221192208 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21506 12518 603 41 0 21465 0
vsize: 86024
[startup+270.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 30516 0 0 0 26923 81 0 0 25 0 1 0 491230123 88223744 12521 4294967295 134512640 134672761 3221224544 3220134112 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21539 12521 603 41 0 21498 0
vsize: 86156
[startup+280.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 30614 0 0 0 27923 81 0 0 25 0 1 0 491230123 88358912 12619 4294967295 134512640 134672761 3221224544 3219906672 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21572 12619 603 41 0 21531 0
vsize: 86288
[startup+290.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31038 0 0 0 28923 82 0 0 25 0 1 0 491230123 95150080 12795 4294967295 134512640 134672761 3221224544 3219774864 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23230 12795 603 41 0 23189 0
vsize: 92920
[startup+300.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31192 0 0 0 29923 82 0 0 25 0 1 0 491230123 95453184 12907 4294967295 134512640 134672761 3221224544 3220804176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23304 12907 603 41 0 23263 0
vsize: 93216
[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31226 0 0 0 30923 83 0 0 25 0 1 0 491230123 95588352 12941 4294967295 134512640 134672761 3221224544 3220541536 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23337 12941 603 41 0 23296 0
vsize: 93348
[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31226 0 0 0 31923 83 0 0 25 0 1 0 491230123 95588352 12941 4294967295 134512640 134672761 3221224544 3219824800 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23337 12941 603 41 0 23296 0
vsize: 93348
[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31537 0 0 0 32922 83 0 0 25 0 1 0 491230123 96194560 13169 4294967295 134512640 134672761 3221224544 3220421808 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23485 13169 603 41 0 23444 0
vsize: 93940
[startup+340.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31762 0 0 0 33922 84 0 0 25 0 1 0 491230123 96231424 13229 4294967295 134512640 134672761 3221224544 3220038480 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23494 13229 603 41 0 23453 0
vsize: 93976
[startup+350.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31917 0 0 0 34922 84 0 0 25 0 1 0 491230123 96534528 13342 4294967295 134512640 134672761 3221224544 3220897776 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23568 13342 603 41 0 23527 0
vsize: 94272
[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31944 0 0 0 35922 84 0 0 25 0 1 0 491230123 96669696 13369 4294967295 134512640 134672761 3221224544 3220445248 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 31944 0 0 0 36923 84 0 0 25 0 1 0 491230123 96669696 13369 4294967295 134512640 134672761 3221224544 3219685408 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 32268 0 0 0 37923 85 0 0 25 0 1 0 491230123 97411072 13610 4294967295 134512640 134672761 3221224544 3220562064 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23782 13610 603 41 0 23741 0
vsize: 95128
[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 32489 0 0 0 38922 86 0 0 25 0 1 0 491230123 97353728 13666 4294967295 134512640 134672761 3221224544 3220036944 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23768 13666 603 41 0 23727 0
vsize: 95072
[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 32639 0 0 0 39922 86 0 0 25 0 1 0 491230123 97656832 13774 4294967295 134512640 134672761 3221224544 3220853424 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23842 13774 603 41 0 23801 0
vsize: 95368
[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 32669 0 0 0 40923 86 0 0 25 0 1 0 491230123 97792000 13804 4294967295 134512640 134672761 3221224544 3220434400 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23875 13804 603 41 0 23834 0
vsize: 95500
[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 32669 0 0 0 41923 86 0 0 25 0 1 0 491230123 97792000 13804 4294967295 134512640 134672761 3221224544 3219773632 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23875 13804 603 41 0 23834 0
vsize: 95500
[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 35407 0 0 0 42916 93 0 0 25 0 1 0 491230123 103464960 15224 4294967295 134512640 134672761 3221224544 3219761424 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25260 15224 603 41 0 25219 0
vsize: 101040
[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 35814 0 0 0 43916 94 0 0 25 0 1 0 491230123 103825408 15383 4294967295 134512640 134672761 3221224544 3219147024 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25348 15383 603 41 0 25307 0
vsize: 101392
[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36027 0 0 0 44916 94 0 0 25 0 1 0 491230123 104300544 15554 4294967295 134512640 134672761 3221224544 3220472592 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25464 15554 603 41 0 25423 0
vsize: 101856
[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36076 0 0 0 45916 94 0 0 25 0 1 0 491230123 104435712 15603 4294967295 134512640 134672761 3221224544 3221064624 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15603 603 41 0 25456 0
vsize: 101988
[startup+470.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36089 0 0 0 46917 94 0 0 25 0 1 0 491230123 104435712 15616 4294967295 134512640 134672761 3221224544 3220154944 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36089 0 0 0 47917 94 0 0 25 0 1 0 491230123 104435712 15616 4294967295 134512640 134672761 3221224544 3219439168 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36399 0 0 0 48916 95 0 0 25 0 1 0 491230123 105177088 15843 4294967295 134512640 134672761 3221224544 3220191984 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25678 15843 603 41 0 25637 0
vsize: 102712
[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36816 0 0 0 49916 96 0 0 25 0 1 0 491230123 105820160 16060 4294967295 134512640 134672761 3221224544 3218835984 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25835 16060 603 41 0 25794 0
vsize: 103340
[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 36969 0 0 0 50916 96 0 0 25 0 1 0 491230123 106123264 16171 4294967295 134512640 134672761 3221224544 3219937200 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25909 16171 603 41 0 25868 0
vsize: 103636
[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37017 0 0 0 51917 96 0 0 25 0 1 0 491230123 106258432 16219 4294967295 134512640 134672761 3221224544 3220507056 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25942 16219 603 41 0 25901 0
vsize: 103768
[startup+530.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37052 0 0 0 52917 96 0 0 25 0 1 0 491230123 106393600 16254 4294967295 134512640 134672761 3221224544 3220941936 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16254 603 41 0 25934 0
vsize: 103900
[startup+540.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37076 0 0 0 53917 96 0 0 25 0 1 0 491230123 106393600 16278 4294967295 134512640 134672761 3221224544 3220093888 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37076 0 0 0 54918 96 0 0 25 0 1 0 491230123 106393600 16278 4294967295 134512640 134672761 3221224544 3219516544 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37076 0 0 0 55918 96 0 0 25 0 1 0 491230123 106393600 16278 4294967295 134512640 134672761 3221224544 3219056704 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37076 0 0 0 56918 96 0 0 25 0 1 0 491230123 106393600 16278 4294967295 134512640 134672761 3221224544 3218203840 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37402 0 0 0 57918 97 0 0 25 0 1 0 491230123 107134976 16521 4294967295 134512640 134672761 3221224544 3219776304 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26156 16521 603 41 0 26115 0
vsize: 104624
[startup+590.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37531 0 0 0 58918 97 0 0 25 0 1 0 491230123 107540480 16650 4294967295 134512640 134672761 3221224544 3220910544 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26255 16650 603 41 0 26214 0
vsize: 105020
[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37813 0 0 0 59917 98 0 0 25 0 1 0 491230123 107606016 16730 4294967295 134512640 134672761 3221224544 3219251088 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26271 16730 603 41 0 26230 0
vsize: 105084
[startup+610.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 37960 0 0 0 60917 98 0 0 25 0 1 0 491230123 107909120 16835 4294967295 134512640 134672761 3221224544 3220032432 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26345 16835 603 41 0 26304 0
vsize: 105380
[startup+620.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38001 0 0 0 61918 98 0 0 25 0 1 0 491230123 108044288 16876 4294967295 134512640 134672761 3221224544 3220539600 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26378 16876 603 41 0 26337 0
vsize: 105512
[startup+630.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38034 0 0 0 62918 98 0 0 25 0 1 0 491230123 108179456 16909 4294967295 134512640 134672761 3221224544 3220942224 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16909 603 41 0 26370 0
vsize: 105644
[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38057 0 0 0 63918 98 0 0 25 0 1 0 491230123 108179456 16932 4294967295 134512640 134672761 3221224544 3220244896 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+650.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38057 0 0 0 64919 98 0 0 25 0 1 0 491230123 108179456 16932 4294967295 134512640 134672761 3221224544 3219462880 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+660.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38057 0 0 0 65919 98 0 0 25 0 1 0 491230123 108179456 16932 4294967295 134512640 134672761 3221224544 3219067552 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+670.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38057 0 0 0 66919 98 0 0 25 0 1 0 491230123 108179456 16932 4294967295 134512640 134672761 3221224544 3218421856 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38057 0 0 0 67920 98 0 0 25 0 1 0 491230123 108179456 16932 4294967295 134512640 134672761 3221224544 3217688896 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38440 0 0 0 68919 99 0 0 25 0 1 0 491230123 109056000 17232 4294967295 134512640 134672761 3221224544 3220316400 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26625 17232 603 41 0 26584 0
vsize: 106500
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38514 0 0 0 69919 99 0 0 25 0 1 0 491230123 109326336 17306 4294967295 134512640 134672761 3221224544 3221132784 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26691 17306 603 41 0 26650 0
vsize: 106764
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38755 0 0 0 70919 100 0 0 25 0 1 0 491230123 109268992 17347 4294967295 134512640 134672761 3221224544 3219662832 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26677 17347 603 41 0 26636 0
vsize: 106708
[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38892 0 0 0 71919 100 0 0 25 0 1 0 491230123 109572096 17442 4294967295 134512640 134672761 3221224544 3220322544 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26751 17442 603 41 0 26710 0
vsize: 107004
[startup+730.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38931 0 0 0 72919 100 0 0 25 0 1 0 491230123 109707264 17481 4294967295 134512640 134672761 3221224544 3220793232 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17481 603 41 0 26743 0
vsize: 107136
[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38962 0 0 0 73920 100 0 0 25 0 1 0 491230123 109707264 17512 4294967295 134512640 134672761 3221224544 3221173104 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17512 603 41 0 26743 0
vsize: 107136
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38967 0 0 0 74920 100 0 0 25 0 1 0 491230123 109707264 17517 4294967295 134512640 134672761 3221224544 3219653632 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+760.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38967 0 0 0 75920 100 0 0 25 0 1 0 491230123 109707264 17517 4294967295 134512640 134672761 3221224544 3219239104 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+770.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 38967 0 0 0 76921 100 0 0 25 0 1 0 491230123 109707264 17517 4294967295 134512640 134672761 3221224544 3218529568 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+780.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39213 0 0 0 77921 101 0 0 25 0 1 0 491230123 110313472 17680 4294967295 134512640 134672761 3221224544 3218803824 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26932 17680 603 41 0 26891 0
vsize: 107728
[startup+790.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39357 0 0 0 78920 101 0 0 25 0 1 0 491230123 110583808 17824 4294967295 134512640 134672761 3221224544 3220554192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26998 17824 603 41 0 26957 0
vsize: 107992
[startup+800.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39541 0 0 0 79920 102 0 0 25 0 1 0 491230123 110448640 17808 4294967295 134512640 134672761 3221224544 3218681232 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26965 17808 603 41 0 26924 0
vsize: 107860
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39745 0 0 0 80920 102 0 0 25 0 1 0 491230123 110923776 17970 4294967295 134512640 134672761 3221224544 3219892944 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27081 17970 603 41 0 27040 0
vsize: 108324
[startup+820.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39792 0 0 0 81921 102 0 0 25 0 1 0 491230123 111058944 18017 4294967295 134512640 134672761 3221224544 3220474896 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27114 18017 603 41 0 27073 0
vsize: 108456
[startup+830.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39829 0 0 0 82921 102 0 0 25 0 1 0 491230123 111058944 18054 4294967295 134512640 134672761 3221224544 3220915344 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27114 18054 603 41 0 27073 0
vsize: 108456
[startup+840.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39854 0 0 0 83921 102 0 0 25 0 1 0 491230123 111194112 18079 4294967295 134512640 134672761 3221224544 3220266688 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39854 0 0 0 84921 102 0 0 25 0 1 0 491230123 111194112 18079 4294967295 134512640 134672761 3221224544 3219540832 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+860.056 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39854 0 0 0 85923 102 0 0 25 0 1 0 491230123 111194112 18079 4294967295 134512640 134672761 3221224544 3219090592 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+870.057 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 39854 0 0 0 86923 102 0 0 25 0 1 0 491230123 111194112 18079 4294967295 134512640 134672761 3221224544 3218248960 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+880.057 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40169 0 0 0 87923 103 0 0 25 0 1 0 491230123 111935488 18311 4294967295 134512640 134672761 3221224544 3219632688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27328 18311 603 41 0 27287 0
vsize: 109312
[startup+890.057 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40268 0 0 0 88923 103 0 0 25 0 1 0 491230123 112205824 18410 4294967295 134512640 134672761 3221224544 3220834992 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27394 18410 603 41 0 27353 0
vsize: 109576
[startup+900.057 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40498 0 0 0 89923 104 0 0 25 0 1 0 491230123 124620800 18440 4294967295 134512640 134672761 3221224544 3219270192 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30425 18440 603 41 0 30384 0
vsize: 121700
[startup+910.057 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40650 0 0 0 90923 104 0 0 25 0 1 0 491230123 124923904 18550 4294967295 134512640 134672761 3221224544 3220112976 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30499 18550 603 41 0 30458 0
vsize: 121996
[startup+920.058 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40693 0 0 0 91923 105 0 0 25 0 1 0 491230123 125059072 18593 4294967295 134512640 134672761 3221224544 3220636176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30532 18593 603 41 0 30491 0
vsize: 122128
[startup+930.058 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40726 0 0 0 92923 105 0 0 25 0 1 0 491230123 125194240 18626 4294967295 134512640 134672761 3221224544 3221046864 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18626 603 41 0 30524 0
vsize: 122260
[startup+940.059 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40740 0 0 0 93923 105 0 0 25 0 1 0 491230123 125194240 18640 4294967295 134512640 134672761 3221224544 3219789376 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+950.064 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40740 0 0 0 94924 105 0 0 25 0 1 0 491230123 125194240 18640 4294967295 134512640 134672761 3221224544 3219404992 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+960.068 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40740 0 0 0 95925 105 0 0 25 0 1 0 491230123 125194240 18640 4294967295 134512640 134672761 3221224544 3218904064 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+970.071 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 40740 0 0 0 96926 105 0 0 25 0 1 0 491230123 125194240 18640 4294967295 134512640 134672761 3221224544 3217988128 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+980.072 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41103 0 0 0 97925 105 0 0 25 0 1 0 491230123 126070784 18920 4294967295 134512640 134672761 3221224544 3220218480 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30779 18920 603 41 0 30738 0
vsize: 123116
[startup+990.072 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41177 0 0 0 98926 106 0 0 25 0 1 0 491230123 126205952 18994 4294967295 134512640 134672761 3221224544 3221125584 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30812 18994 603 41 0 30771 0
vsize: 123248
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41542 0 0 0 99925 106 0 0 25 0 1 0 491230123 126595072 19152 4294967295 134512640 134672761 3221224544 3219045552 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30907 19152 603 41 0 30866 0
vsize: 123628
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41679 0 0 0 100925 107 0 0 25 0 1 0 491230123 126898176 19247 4294967295 134512640 134672761 3221224544 3219705840 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30981 19247 603 41 0 30940 0
vsize: 123924
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41719 0 0 0 101926 107 0 0 25 0 1 0 491230123 127033344 19287 4294967295 134512640 134672761 3221224544 3220176432 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31014 19287 603 41 0 30973 0
vsize: 124056
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41749 0 0 0 102926 107 0 0 25 0 1 0 491230123 127168512 19317 4294967295 134512640 134672761 3221224544 3220556304 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31047 19317 603 41 0 31006 0
vsize: 124188
[startup+1040.18 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41776 0 0 0 103937 107 0 0 25 0 1 0 491230123 127168512 19344 4294967295 134512640 134672761 3221224544 3220879728 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31047 19344 603 41 0 31006 0
vsize: 124188
[startup+1050.19 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41798 0 0 0 104938 107 0 0 25 0 1 0 491230123 127303680 19366 4294967295 134512640 134672761 3221224544 3221156688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19366 603 41 0 31039 0
vsize: 124320
[startup+1060.19 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 105938 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3219397216 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1070.19 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 106939 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3218999584 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1080.19 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 107939 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3218707552 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1090.19 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 108940 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3218369824 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1100.21 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 109941 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3217808128 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1110.53 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 41805 0 0 0 110974 107 0 0 25 0 1 0 491230123 127303680 19373 4294967295 134512640 134672761 3221224544 3217309216 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1120.53 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 42165 0 0 0 111974 108 0 0 25 0 1 0 491230123 128180224 19650 4294967295 134512640 134672761 3221224544 3219573552 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31294 19650 603 41 0 31253 0
vsize: 125176
[startup+1130.54 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 42245 0 0 0 112974 108 0 0 25 0 1 0 491230123 128315392 19730 4294967295 134512640 134672761 3221224544 3220466352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31327 19730 603 41 0 31286 0
vsize: 125308
[startup+1140.56 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 42318 0 0 0 113976 109 0 0 25 0 1 0 491230123 128585728 19803 4294967295 134512640 134672761 3221224544 3221059440 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31393 19803 603 41 0 31352 0
vsize: 125572
[startup+1150.56 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 42901 0 0 0 114975 110 0 0 25 0 1 0 491230123 129081344 20095 4294967295 134512640 134672761 3221224544 3221123664 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31514 20095 603 41 0 31473 0
vsize: 126056
[startup+1160.56 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 80811 0 0 0 115878 207 0 0 25 0 1 0 491230123 266842112 55399 4294967295 134512640 134672761 3221224544 3219716592 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65147 55400 603 41 0 65106 0
vsize: 260588
[startup+1162.23 s]
Raw data (loadavg): 1.00 0.99 0.92 1/53 574
Raw data (stat): 574 (minisat+) R 573 29653 29652 0 -1 0 80811 0 0 0 115878 207 0 0 25 0 1 0 491230123 266842112 55399 4294967295 134512640 134672761 3221224544 3219716592 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65147 55400 603 41 0 65106 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1162.23
CPU time (s): 1162.48
CPU user time (s): 1160.05
CPU system time (s): 2.43163
CPU usage (%): 100.021
Max. virtual memory (Kb): 260588
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####