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 7047

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 21:06:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5094 boxname=wulflinc11 idbench=392 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c4c13764e2ea959929790d6ef6d0273c  /oldhome/oroussel/tmp/wulflinc11/normalized-nw04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-nw04.opb /oldhome/oroussel/tmp/wulflinc11/normalized-nw04.opb
IDLAUNCH: 5094
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        832276 kB
Buffers:         36964 kB
Cached:         139936 kB
SwapCached:       4932 kB
Active:          91224 kB
Inactive:        93484 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        832024 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            12004 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:25:30 (client local time) WITH STATUS 0 IN 1139.8 SECONDS
stats: 5094 7 1139.8 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.97 0.88 1/54 12679
Raw data (stat): 12679 (runsolver) D 12678 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 429478118 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.90 0.97 0.88 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 25561 0 0 0 919 69 0 0 25 0 1 0 429478118 69857280 8128 4294967295 134512640 134672761 3221224576 3220976624 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17055 8128 603 41 0 17014 0
vsize: 68220
[startup+20.0012 s]
Raw data (loadavg): 0.91 0.97 0.88 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 25630 0 0 0 1919 70 0 0 25 0 1 0 429478118 70139904 8197 4294967295 134512640 134672761 3221224576 3220721760 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17124 8197 603 41 0 17083 0
vsize: 68496
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 26090 0 0 0 2918 71 0 0 25 0 1 0 429478118 73543680 8657 4294967295 134512640 134672761 3221224576 3220673936 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17955 8657 603 41 0 17914 0
vsize: 71820
[startup+40.0013 s]
Raw data (loadavg): 0.94 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 26177 0 0 0 3918 71 0 0 25 0 1 0 429478118 73560064 8744 4294967295 134512640 134672761 3221224576 3220354080 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17959 8744 603 41 0 17918 0
vsize: 71836
[startup+50.0019 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 26968 0 0 0 4917 72 0 0 25 0 1 0 429478118 76271616 9535 4294967295 134512640 134672761 3221224576 3221116208 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18621 9535 603 41 0 18580 0
vsize: 74484
[startup+60.0017 s]
Raw data (loadavg): 0.95 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 27064 0 0 0 5917 73 0 0 25 0 1 0 429478118 76283904 9631 4294967295 134512640 134672761 3221224576 3220869584 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18624 9631 603 41 0 18583 0
vsize: 74496
[startup+70.0015 s]
Raw data (loadavg): 0.96 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 27282 0 0 0 6916 73 0 0 25 0 1 0 429478118 79859712 9849 4294967295 134512640 134672761 3221224576 3220740560 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19497 9849 603 41 0 19456 0
vsize: 77988
[startup+80.0013 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 27337 0 0 0 7916 74 0 0 25 0 1 0 429478118 79859712 9904 4294967295 134512640 134672761 3221224576 3221004560 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19497 9904 603 41 0 19456 0
vsize: 77988
[startup+90.0011 s]
Raw data (loadavg): 0.97 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 27401 0 0 0 8915 74 0 0 25 0 1 0 429478118 79896576 9968 4294967295 134512640 134672761 3221224576 3220174272 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19506 9968 603 41 0 19465 0
vsize: 78024
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 29080 0 0 0 9911 79 0 0 25 0 1 0 429478118 83406848 10905 4294967295 134512640 134672761 3221224576 3221084912 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20363 10905 603 41 0 20322 0
vsize: 81452
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 29312 0 0 0 10911 79 0 0 25 0 1 0 429478118 83980288 11095 4294967295 134512640 134672761 3221224576 3221157392 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20503 11095 603 41 0 20462 0
vsize: 82012
[startup+120 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 29534 0 0 0 11910 80 0 0 25 0 1 0 429478118 84250624 11234 4294967295 134512640 134672761 3221224576 3220307520 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20569 11234 603 41 0 20528 0
vsize: 82276
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 29944 0 0 0 12909 81 0 0 25 0 1 0 429478118 85176320 11519 4294967295 134512640 134672761 3221224576 3220067984 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20795 11519 603 41 0 20754 0
vsize: 83180
[startup+140 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 30144 0 0 0 13909 82 0 0 25 0 1 0 429478118 85651456 11677 4294967295 134512640 134672761 3221224576 3221062560 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20911 11677 603 41 0 20870 0
vsize: 83644
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 30220 0 0 0 14909 82 0 0 25 0 1 0 429478118 85786624 11753 4294967295 134512640 134672761 3221224576 3220073456 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20944 11753 603 41 0 20903 0
vsize: 83776
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 30750 0 0 0 15908 83 0 0 25 0 1 0 429478118 86675456 12035 4294967295 134512640 134672761 3221224576 3220270736 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21161 12035 603 41 0 21120 0
vsize: 84644
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 30908 0 0 0 16907 83 0 0 25 0 1 0 429478118 86978560 12151 4294967295 134512640 134672761 3221224576 3221173424 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21235 12151 603 41 0 21194 0
vsize: 84940
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 30912 0 0 0 17907 84 0 0 25 0 1 0 429478118 86978560 12155 4294967295 134512640 134672761 3221224576 3220054752 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21235 12155 603 41 0 21194 0
vsize: 84940
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 31231 0 0 0 18906 85 0 0 25 0 1 0 429478118 87719936 12391 4294967295 134512640 134672761 3221224576 3220640048 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21416 12391 603 41 0 21375 0
vsize: 85664
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 31501 0 0 0 19905 86 0 0 25 0 1 0 429478118 87920640 12496 4294967295 134512640 134672761 3221224576 3220271024 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21465 12496 603 41 0 21424 0
vsize: 85860
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 31654 0 0 0 20905 87 0 0 25 0 1 0 429478118 88223744 12607 4294967295 134512640 134672761 3221224576 3221119472 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21539 12607 603 41 0 21498 0
vsize: 86156
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 31662 0 0 0 21904 87 0 0 25 0 1 0 429478118 88358912 12615 4294967295 134512640 134672761 3221224576 3220122048 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21572 12615 603 41 0 21531 0
vsize: 86288
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 31770 0 0 0 22904 88 0 0 25 0 1 0 429478118 94920704 12723 4294967295 134512640 134672761 3221224576 3220012688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23174 12723 603 41 0 23133 0
vsize: 92696
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32205 0 0 0 23903 89 0 0 25 0 1 0 429478118 95375360 12910 4294967295 134512640 134672761 3221224576 3219738032 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23285 12910 603 41 0 23244 0
vsize: 93140
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32365 0 0 0 24902 90 0 0 25 0 1 0 429478118 95678464 13028 4294967295 134512640 134672761 3221224576 3220866416 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23359 13028 603 41 0 23318 0
vsize: 93436
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32394 0 0 0 25902 90 0 0 25 0 1 0 429478118 95813632 13057 4294967295 134512640 134672761 3221224576 3220423392 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23392 13057 603 41 0 23351 0
vsize: 93568
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32394 0 0 0 26902 90 0 0 25 0 1 0 429478118 95813632 13057 4294967295 134512640 134672761 3221224576 3219214560 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23392 13057 603 41 0 23351 0
vsize: 93568
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32741 0 0 0 27901 92 0 0 25 0 1 0 429478118 96555008 13321 4294967295 134512640 134672761 3221224576 3220858256 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23573 13321 603 41 0 23532 0
vsize: 94292
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 32964 0 0 0 28901 92 0 0 25 0 1 0 429478118 96505856 13379 4294967295 134512640 134672761 3221224576 3220336592 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23561 13379 603 41 0 23520 0
vsize: 94244
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 33112 0 0 0 29901 93 0 0 25 0 1 0 429478118 96808960 13485 4294967295 134512640 134672761 3221224576 3221114096 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23635 13485 603 41 0 23594 0
vsize: 94540
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 33120 0 0 0 30901 93 0 0 25 0 1 0 429478118 96944128 13493 4294967295 134512640 134672761 3221224576 3220122624 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23668 13493 603 41 0 23627 0
vsize: 94672
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 33164 0 0 0 31901 93 0 0 25 0 1 0 429478118 96944128 13537 4294967295 134512640 134672761 3221224576 3219149456 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23668 13537 603 41 0 23627 0
vsize: 94672
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 33567 0 0 0 32899 95 0 0 25 0 1 0 429478118 97267712 13692 4294967295 134512640 134672761 3221224576 3218946800 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23747 13692 603 41 0 23706 0
vsize: 94988
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 36368 0 0 0 33892 102 0 0 25 0 1 0 429478118 103247872 15175 4294967295 134512640 134672761 3221224576 3220551248 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25207 15175 603 41 0 25166 0
vsize: 100828
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 36505 0 0 0 34891 103 0 0 25 0 1 0 429478118 103550976 15270 4294967295 134512640 134672761 3221224576 3221201648 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25281 15270 603 41 0 25240 0
vsize: 101124
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 36507 0 0 0 35891 103 0 0 25 0 1 0 429478118 103550976 15272 4294967295 134512640 134672761 3221224576 3219984384 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25281 15272 603 41 0 25240 0
vsize: 101124
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 36553 0 0 0 36891 104 0 0 25 0 1 0 429478118 103686144 15318 4294967295 134512640 134672761 3221224576 3219090032 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25314 15318 603 41 0 25273 0
vsize: 101256
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 36944 0 0 0 37891 104 0 0 25 0 1 0 429478118 103870464 15461 4294967295 134512640 134672761 3221224576 3218806832 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25359 15461 603 41 0 25318 0
vsize: 101436
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37201 0 0 0 38890 105 0 0 25 0 1 0 429478118 104615936 15676 4294967295 134512640 134672761 3221224576 3220549136 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25541 15676 603 41 0 25500 0
vsize: 102164
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37254 0 0 0 39889 106 0 0 25 0 1 0 429478118 104751104 15729 4294967295 134512640 134672761 3221224576 3221188592 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25574 15729 603 41 0 25533 0
vsize: 102296
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37257 0 0 0 40889 106 0 0 25 0 1 0 429478118 104751104 15732 4294967295 134512640 134672761 3221224576 3220007328 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25574 15732 603 41 0 25533 0
vsize: 102296
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37257 0 0 0 41889 106 0 0 25 0 1 0 429478118 104751104 15732 4294967295 134512640 134672761 3221224576 3218632032 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25574 15732 603 41 0 25533 0
vsize: 102296
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37637 0 0 0 42888 107 0 0 25 0 1 0 429478118 105627648 16029 4294967295 134512640 134672761 3221224576 3221126384 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25788 16029 603 41 0 25747 0
vsize: 103152
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 37871 0 0 0 43888 108 0 0 25 0 1 0 429478118 105693184 16098 4294967295 134512640 134672761 3221224576 3220366352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25804 16098 603 41 0 25763 0
vsize: 103216
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38009 0 0 0 44888 108 0 0 25 0 1 0 429478118 105996288 16194 4294967295 134512640 134672761 3221224576 3221042192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25878 16194 603 41 0 25837 0
vsize: 103512
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38024 0 0 0 45887 109 0 0 25 0 1 0 429478118 105996288 16209 4294967295 134512640 134672761 3221224576 3220158720 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25878 16209 603 41 0 25837 0
vsize: 103512
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38024 0 0 0 46887 109 0 0 25 0 1 0 429478118 105996288 16209 4294967295 134512640 134672761 3221224576 3219466752 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25878 16209 603 41 0 25837 0
vsize: 103512
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38346 0 0 0 47886 110 0 0 25 0 1 0 429478118 106737664 16448 4294967295 134512640 134672761 3221224576 3220317872 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26059 16448 603 41 0 26018 0
vsize: 104236
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38760 0 0 0 48884 112 0 0 25 0 1 0 429478118 107372544 16662 4294967295 134512640 134672761 3221224576 3219041456 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26214 16662 603 41 0 26173 0
vsize: 104856
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38920 0 0 0 49884 112 0 0 25 0 1 0 429478118 107675648 16780 4294967295 134512640 134672761 3221224576 3220086704 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26288 16780 603 41 0 26247 0
vsize: 105152
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 38966 0 0 0 50884 113 0 0 25 0 1 0 429478118 107810816 16826 4294967295 134512640 134672761 3221224576 3220655600 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26321 16826 603 41 0 26280 0
vsize: 105284
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39000 0 0 0 51884 113 0 0 25 0 1 0 429478118 107945984 16860 4294967295 134512640 134672761 3221224576 3221069936 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26354 16860 603 41 0 26313 0
vsize: 105416
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39012 0 0 0 52884 113 0 0 25 0 1 0 429478118 107945984 16872 4294967295 134512640 134672761 3221224576 3219791136 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26354 16872 603 41 0 26313 0
vsize: 105416
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39012 0 0 0 53884 114 0 0 25 0 1 0 429478118 107945984 16872 4294967295 134512640 134672761 3221224576 3219413184 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26354 16872 603 41 0 26313 0
vsize: 105416
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39012 0 0 0 54883 114 0 0 25 0 1 0 429478118 107945984 16872 4294967295 134512640 134672761 3221224576 3218947392 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26354 16872 603 41 0 26313 0
vsize: 105416
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39012 0 0 0 55884 114 0 0 25 0 1 0 429478118 107945984 16872 4294967295 134512640 134672761 3221224576 3218125056 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26354 16872 603 41 0 26313 0
vsize: 105416
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39356 0 0 0 56883 115 0 0 25 0 1 0 429478118 108687360 17133 4294967295 134512640 134672761 3221224576 3219991856 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26535 17133 603 41 0 26494 0
vsize: 106140
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39481 0 0 0 57883 116 0 0 25 0 1 0 429478118 109092864 17258 4294967295 134512640 134672761 3221224576 3221016944 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26634 17258 603 41 0 26593 0
vsize: 106536
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39729 0 0 0 58882 116 0 0 25 0 1 0 429478118 109010944 17306 4294967295 134512640 134672761 3221224576 3219545744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26614 17306 603 41 0 26573 0
vsize: 106456
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39876 0 0 0 59881 118 0 0 25 0 1 0 429478118 109449216 17411 4294967295 134512640 134672761 3221224576 3220315472 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26721 17411 603 41 0 26680 0
vsize: 106884
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39917 0 0 0 60881 118 0 0 25 0 1 0 429478118 109449216 17452 4294967295 134512640 134672761 3221224576 3220812040 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26721 17452 603 41 0 26680 0
vsize: 106884
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39947 0 0 0 61881 118 0 0 25 0 1 0 429478118 109584384 17482 4294967295 134512640 134672761 3221224576 3221193584 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26754 17482 603 41 0 26713 0
vsize: 107016
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39950 0 0 0 62881 118 0 0 25 0 1 0 429478118 109584384 17485 4294967295 134512640 134672761 3221224576 3219662016 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26754 17485 603 41 0 26713 0
vsize: 107016
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39950 0 0 0 63881 118 0 0 25 0 1 0 429478118 109584384 17485 4294967295 134512640 134672761 3221224576 3219264288 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26754 17485 603 41 0 26713 0
vsize: 107016
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39950 0 0 0 64881 118 0 0 25 0 1 0 429478118 109584384 17485 4294967295 134512640 134672761 3221224576 3218670432 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26754 17485 603 41 0 26713 0
vsize: 107016
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 39950 0 0 0 65880 119 0 0 25 0 1 0 429478118 109584384 17485 4294967295 134512640 134672761 3221224576 3217876320 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26754 17485 603 41 0 26713 0
vsize: 107016
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40329 0 0 0 66879 121 0 0 25 0 1 0 429478118 110460928 17781 4294967295 134512640 134672761 3221224576 3220410224 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26968 17781 603 41 0 26927 0
vsize: 107872
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40457 0 0 0 67878 121 0 0 25 0 1 0 429478118 110067712 17709 4294967295 134512640 134672761 3221224576 3218045744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26872 17709 603 41 0 26831 0
vsize: 107488
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40726 0 0 0 68878 122 0 0 25 0 1 0 429478118 110747648 17936 4294967295 134512640 134672761 3221224576 3219848816 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27038 17936 603 41 0 26997 0
vsize: 108152
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40778 0 0 0 69877 123 0 0 25 0 1 0 429478118 110882816 17988 4294967295 134512640 134672761 3221224576 3220490672 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27071 17988 603 41 0 27030 0
vsize: 108284
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40815 0 0 0 70877 123 0 0 25 0 1 0 429478118 111017984 18025 4294967295 134512640 134672761 3221224576 3220938512 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27104 18025 603 41 0 27063 0
vsize: 108416
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40838 0 0 0 71877 124 0 0 25 0 1 0 429478118 111017984 18048 4294967295 134512640 134672761 3221224576 3220199424 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27104 18048 603 41 0 27063 0
vsize: 108416
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40838 0 0 0 72876 124 0 0 25 0 1 0 429478118 111017984 18048 4294967295 134512640 134672761 3221224576 3219546432 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27104 18048 603 41 0 27063 0
vsize: 108416
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40838 0 0 0 73876 125 0 0 25 0 1 0 429478118 111017984 18048 4294967295 134512640 134672761 3221224576 3219123936 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27104 18048 603 41 0 27063 0
vsize: 108416
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 40838 0 0 0 74876 125 0 0 25 0 1 0 429478118 111017984 18048 4294967295 134512640 134672761 3221224576 3218359392 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27104 18048 603 41 0 27063 0
vsize: 108416
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41115 0 0 0 75875 126 0 0 25 0 1 0 429478118 111624192 18242 4294967295 134512640 134672761 3221224576 3219172304 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27252 18242 603 41 0 27211 0
vsize: 109008
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41240 0 0 0 76875 126 0 0 25 0 1 0 429478118 112029696 18367 4294967295 134512640 134672761 3221224576 3220695152 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27351 18367 603 41 0 27310 0
vsize: 109404
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41471 0 0 0 77875 127 0 0 25 0 1 0 429478118 124518400 18398 4294967295 134512640 134672761 3221224576 3218996144 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30400 18398 603 41 0 30359 0
vsize: 121600
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41632 0 0 0 78874 128 0 0 25 0 1 0 429478118 124821504 18517 4294967295 134512640 134672761 3221224576 3220060688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30474 18517 603 41 0 30433 0
vsize: 121896
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41678 0 0 0 79874 128 0 0 25 0 1 0 429478118 124956672 18563 4294967295 134512640 134672761 3221224576 3220633600 134592604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30507 18563 603 41 0 30466 0
vsize: 122028
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41713 0 0 0 80874 128 0 0 25 0 1 0 429478118 125091840 18598 4294967295 134512640 134672761 3221224576 3221049392 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 18598 603 41 0 30499 0
vsize: 122160
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41727 0 0 0 81874 128 0 0 25 0 1 0 429478118 125091840 18612 4294967295 134512640 134672761 3221224576 3219800544 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 18612 603 41 0 30499 0
vsize: 122160
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41727 0 0 0 82874 129 0 0 25 0 1 0 429478118 125091840 18612 4294967295 134512640 134672761 3221224576 3219432864 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 18612 603 41 0 30499 0
vsize: 122160
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41727 0 0 0 83874 129 0 0 25 0 1 0 429478118 125091840 18612 4294967295 134512640 134672761 3221224576 3218980224 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 18612 603 41 0 30499 0
vsize: 122160
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 41727 0 0 0 84874 129 0 0 25 0 1 0 429478118 125091840 18612 4294967295 134512640 134672761 3221224576 3218170656 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30540 18612 603 41 0 30499 0
vsize: 122160
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42058 0 0 0 85873 130 0 0 25 0 1 0 429478118 125833216 18860 4294967295 134512640 134672761 3221224576 3219831152 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30721 18860 603 41 0 30680 0
vsize: 122884
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42149 0 0 0 86874 130 0 0 25 0 1 0 429478118 126103552 18951 4294967295 134512640 134672761 3221224576 3220931120 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30787 18951 603 41 0 30746 0
vsize: 123148
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42416 0 0 0 87873 131 0 0 25 0 1 0 429478118 126062592 19016 4294967295 134512640 134672761 3221224576 3219277136 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30777 19016 603 41 0 30736 0
vsize: 123108
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42567 0 0 0 88873 131 0 0 25 0 1 0 429478118 126500864 19125 4294967295 134512640 134672761 3221224576 3220111856 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30884 19125 603 41 0 30843 0
vsize: 123536
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42610 0 0 0 89872 132 0 0 25 0 1 0 429478118 126500864 19168 4294967295 134512640 134672761 3221224576 3220629488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30884 19168 603 41 0 30843 0
vsize: 123536
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42642 0 0 0 90872 133 0 0 25 0 1 0 429478118 126636032 19200 4294967295 134512640 134672761 3221224576 3221020496 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19200 603 41 0 30876 0
vsize: 123668
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42659 0 0 0 91871 133 0 0 25 0 1 0 429478118 126636032 19217 4294967295 134512640 134672761 3221224576 3219878784 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19217 603 41 0 30876 0
vsize: 123668
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42659 0 0 0 92871 133 0 0 25 0 1 0 429478118 126636032 19217 4294967295 134512640 134672761 3221224576 3219406656 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19217 603 41 0 30876 0
vsize: 123668
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42659 0 0 0 93871 134 0 0 25 0 1 0 429478118 126636032 19217 4294967295 134512640 134672761 3221224576 3219016416 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19217 603 41 0 30876 0
vsize: 123668
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42659 0 0 0 94871 134 0 0 25 0 1 0 429478118 126636032 19217 4294967295 134512640 134672761 3221224576 3218353440 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19217 603 41 0 30876 0
vsize: 123668
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 42659 0 0 0 95871 134 0 0 25 0 1 0 429478118 126636032 19217 4294967295 134512640 134672761 3221224576 3217691616 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 19217 603 41 0 30876 0
vsize: 123668
[startup+970.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43041 0 0 0 96870 136 0 0 25 0 1 0 429478118 127512576 19516 4294967295 134512640 134672761 3221224576 3220325168 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31131 19516 603 41 0 31090 0
vsize: 124524
[startup+980.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43111 0 0 0 97870 136 0 0 25 0 1 0 429478118 127782912 19586 4294967295 134512640 134672761 3221224576 3221131664 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31197 19586 603 41 0 31156 0
vsize: 124788
[startup+990.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43483 0 0 0 98869 137 0 0 25 0 1 0 429478118 128221184 19751 4294967295 134512640 134672761 3221224576 3219085520 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31304 19751 603 41 0 31263 0
vsize: 125216
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43623 0 0 0 99869 137 0 0 25 0 1 0 429478118 128524288 19849 4294967295 134512640 134672761 3221224576 3219782096 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31378 19849 603 41 0 31337 0
vsize: 125512
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43662 0 0 0 100868 138 0 0 25 0 1 0 429478118 128659456 19888 4294967295 134512640 134672761 3221224576 3220253744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31411 19888 603 41 0 31370 0
vsize: 125644
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43692 0 0 0 101867 139 0 0 25 0 1 0 429478118 128659456 19918 4294967295 134512640 134672761 3221224576 3220622384 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31411 19918 603 41 0 31370 0
vsize: 125644
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43717 0 0 0 102867 139 0 0 25 0 1 0 429478118 128794624 19943 4294967295 134512640 134672761 3221224576 3220928048 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31444 19943 603 41 0 31403 0
vsize: 125776
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43739 0 0 0 103867 139 0 0 25 0 1 0 429478118 128794624 19965 4294967295 134512640 134672761 3221224576 3221191376 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31444 19965 603 41 0 31403 0
vsize: 125776
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 104867 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3219256224 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 105868 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3218961216 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 106868 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3218664480 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 107868 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3218316192 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 108867 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3217711008 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 43741 0 0 0 109868 139 0 0 25 0 1 0 429478118 128794624 19967 4294967295 134512640 134672761 3221224576 3217238976 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31444 19967 603 41 0 31403 0
vsize: 125776
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 44124 0 0 0 110867 140 0 0 25 0 1 0 429478118 129671168 20267 4294967295 134512640 134672761 3221224576 3219831632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31658 20267 603 41 0 31617 0
vsize: 126632
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 44208 0 0 0 111867 140 0 0 25 0 1 0 429478118 129941504 20351 4294967295 134512640 134672761 3221224576 3220660880 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31724 20351 603 41 0 31683 0
vsize: 126896
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 44277 0 0 0 112867 141 0 0 25 0 1 0 429478118 130211840 20420 4294967295 134512640 134672761 3221224576 3221214896 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31790 20420 603 41 0 31749 0
vsize: 127160
[startup+1139.74 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 12679
Raw data (stat): 12679 (minisat+) R 12678 32461 32460 0 -1 0 44277 0 0 0 112867 141 0 0 25 0 1 0 429478118 130211840 20420 4294967295 134512640 134672761 3221224576 3221214896 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31790 20420 603 41 0 31749 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1139.74
CPU time (s): 1139.8
CPU user time (s): 1136.62
CPU system time (s): 3.18651
CPU usage (%): 100.005
Max. virtual memory (Kb): 127160
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####