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/manquinho/primes-dimacs-cnf/normalized-par32-5.opb
MD5SUM	9b244c88702eddacf15d45f12fda5eb0
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	6352
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13501
Number of constraints which are clauses	13501
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	3
Trace number 5564

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 00:27:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3972 boxname=wulflinc27 idbench=212 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b244c88702eddacf15d45f12fda5eb0  /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb /oldhome/oroussel/tmp/wulflinc27/normalized-par32-5.opb
IDLAUNCH: 3972
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        850916 kB
Buffers:         34240 kB
Cached:         112540 kB
SwapCached:       3160 kB
Active:          51304 kB
Inactive:       101464 kB
HighTotal:      131008 kB
HighFree:        15064 kB
LowTotal:       903652 kB
LowFree:        835852 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25484 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:47:11 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 3972 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13094 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9705    24266 |    2911       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4770          
c   -- var.elim.:  2000/4770          
c   -- var.elim.:  3000/4770          
c   -- var.elim.:  4000/4770          
c   -- var.elim.:  4770/4770          
c |         0 |    9705    24266 |    3882       0        0     nan |  0.000 % |
c |       101 |    9705    24266 |    4270     101     1013    10.0 | 24.906 % |
c |       252 |    9705    24266 |    4697     252     5642    22.4 | 24.906 % |
c |       477 |    9705    24266 |    5166     477    12834    26.9 | 24.906 % |
c |       #### 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.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (runsolver) R 23082 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480262172 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1559 0 0 0 993 5 0 0 25 0 1 0 480262172 7942144 1499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1939 1499 603 41 0 1898 0
vsize: 7756
[startup+20.0003 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1559 0 0 0 1993 5 0 0 25 0 1 0 480262172 7942144 1499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1499 603 41 0 1898 0
vsize: 7756
[startup+30.0003 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1744 0 0 0 2992 6 0 0 25 0 1 0 480262172 8753152 1684 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2137 1684 603 41 0 2096 0
vsize: 8548
[startup+40.0012 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1847 0 0 0 3992 6 0 0 25 0 1 0 480262172 9125888 1787 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2228 1787 603 41 0 2187 0
vsize: 8912
[startup+50.0017 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1935 0 0 0 4992 6 0 0 25 0 1 0 480262172 9527296 1875 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2326 1875 603 41 0 2285 0
vsize: 9304
[startup+60.0018 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 1999 0 0 0 5992 6 0 0 25 0 1 0 480262172 9748480 1939 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2380 1939 603 41 0 2339 0
vsize: 9520
[startup+70.0026 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2170 0 0 0 6992 7 0 0 25 0 1 0 480262172 10424320 2110 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2545 2110 603 41 0 2504 0
vsize: 10180
[startup+80.0032 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2240 0 0 0 7991 7 0 0 25 0 1 0 480262172 10686464 2180 4294967295 134512640 134672761 3221224560 3221223744 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2609 2180 603 41 0 2568 0
vsize: 10436
[startup+90.0043 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2303 0 0 0 8992 8 0 0 25 0 1 0 480262172 10981376 2243 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2681 2243 603 41 0 2640 0
vsize: 10724
[startup+100.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2422 0 0 0 9991 8 0 0 25 0 1 0 480262172 11476992 2362 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2802 2362 603 41 0 2761 0
vsize: 11208
[startup+110.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2488 0 0 0 10991 9 0 0 25 0 1 0 480262172 11739136 2428 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2866 2428 603 41 0 2825 0
vsize: 11464
[startup+120.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2548 0 0 0 11991 9 0 0 25 0 1 0 480262172 11988992 2488 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2927 2488 603 41 0 2886 0
vsize: 11708
[startup+130.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2548 0 0 0 12991 9 0 0 25 0 1 0 480262172 11988992 2488 4294967295 134512640 134672761 3221224560 3221223744 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2927 2488 603 41 0 2886 0
vsize: 11708
[startup+140.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2548 0 0 0 13990 9 0 0 25 0 1 0 480262172 11988992 2488 4294967295 134512640 134672761 3221224560 3221223744 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2927 2488 603 41 0 2886 0
vsize: 11708
[startup+150.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2616 0 0 0 14990 10 0 0 25 0 1 0 480262172 12320768 2555 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3008 2555 603 41 0 2967 0
vsize: 12032
[startup+160.004 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2640 0 0 0 15990 10 0 0 25 0 1 0 480262172 12419072 2579 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3032 2579 603 41 0 2991 0
vsize: 12128
[startup+170.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2691 0 0 0 16990 10 0 0 25 0 1 0 480262172 12619776 2629 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3081 2629 603 41 0 3040 0
vsize: 12324
[startup+180.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2721 0 0 0 17990 10 0 0 25 0 1 0 480262172 12754944 2659 4294967295 134512640 134672761 3221224560 3221223616 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3114 2659 603 41 0 3073 0
vsize: 12456
[startup+190.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2721 0 0 0 18990 10 0 0 25 0 1 0 480262172 12738560 2659 4294967295 134512640 134672761 3221224560 3221223744 134615529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3110 2659 603 41 0 3069 0
vsize: 12440
[startup+200.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2721 0 0 0 19990 10 0 0 25 0 1 0 480262172 12738560 2659 4294967295 134512640 134672761 3221224560 3221223760 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3110 2659 603 41 0 3069 0
vsize: 12440
[startup+210.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2724 0 0 0 20990 10 0 0 25 0 1 0 480262172 12730368 2661 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3108 2661 603 41 0 3067 0
vsize: 12432
[startup+220.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2725 0 0 0 21991 10 0 0 25 0 1 0 480262172 12730368 2662 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3108 2662 603 41 0 3067 0
vsize: 12432
[startup+230.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2734 0 0 0 22991 10 0 0 25 0 1 0 480262172 12763136 2670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2670 603 41 0 3075 0
vsize: 12464
[startup+240.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2734 0 0 0 23991 10 0 0 25 0 1 0 480262172 12763136 2670 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2670 603 41 0 3075 0
vsize: 12464
[startup+250.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2734 0 0 0 24991 11 0 0 25 0 1 0 480262172 12763136 2670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3116 2670 603 41 0 3075 0
vsize: 12464
[startup+260.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2744 0 0 0 25991 11 0 0 25 0 1 0 480262172 12795904 2679 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3124 2679 603 41 0 3083 0
vsize: 12496
[startup+270.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2847 0 0 0 26991 11 0 0 25 0 1 0 480262172 13217792 2781 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3227 2781 603 41 0 3186 0
vsize: 12908
[startup+280.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2847 0 0 0 27991 11 0 0 25 0 1 0 480262172 13217792 2781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3227 2781 603 41 0 3186 0
vsize: 12908
[startup+290.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2864 0 0 0 28991 12 0 0 25 0 1 0 480262172 13283328 2797 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3243 2797 603 41 0 3202 0
vsize: 12972
[startup+300.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2903 0 0 0 29991 12 0 0 25 0 1 0 480262172 13438976 2835 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3281 2835 603 41 0 3240 0
vsize: 13124
[startup+310.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 2916 0 0 0 30991 12 0 0 25 0 1 0 480262172 13438976 2848 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3281 2848 603 41 0 3240 0
vsize: 13124
[startup+320.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3016 0 0 0 31991 12 0 0 25 0 1 0 480262172 13885440 2947 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3390 2947 603 41 0 3349 0
vsize: 13560
[startup+330.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3022 0 0 0 32991 12 0 0 25 0 1 0 480262172 13901824 2952 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2952 603 41 0 3353 0
vsize: 13576
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3022 0 0 0 33991 12 0 0 25 0 1 0 480262172 13901824 2952 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3394 2952 603 41 0 3353 0
vsize: 13576
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 34991 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+360.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 35991 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+370.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 36991 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+380.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 37991 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+390.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 38992 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+400.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 39992 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+410.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 40992 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+420.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 41992 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+430.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3028 0 0 0 42992 13 0 0 25 0 1 0 480262172 13918208 2957 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3398 2957 603 41 0 3357 0
vsize: 13592
[startup+440.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3038 0 0 0 43992 13 0 0 25 0 1 0 480262172 13950976 2966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 2966 603 41 0 3365 0
vsize: 13624
[startup+450.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3039 0 0 0 44992 13 0 0 25 0 1 0 480262172 13950976 2967 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 2967 603 41 0 3365 0
vsize: 13624
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3039 0 0 0 45992 13 0 0 25 0 1 0 480262172 13950976 2967 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3406 2967 603 41 0 3365 0
vsize: 13624
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3108 0 0 0 46992 14 0 0 25 0 1 0 480262172 14352384 3036 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 3036 603 41 0 3463 0
vsize: 14016
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3116 0 0 0 47992 14 0 0 25 0 1 0 480262172 14352384 3044 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 3044 603 41 0 3463 0
vsize: 14016
[startup+490.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3116 0 0 0 48992 14 0 0 25 0 1 0 480262172 14352384 3044 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3504 3044 603 41 0 3463 0
vsize: 14016
[startup+500.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3149 0 0 0 49992 14 0 0 25 0 1 0 480262172 14417920 3077 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3520 3077 603 41 0 3479 0
vsize: 14080
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3149 0 0 0 50992 14 0 0 25 0 1 0 480262172 14417920 3077 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3520 3077 603 41 0 3479 0
vsize: 14080
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3155 0 0 0 51992 14 0 0 25 0 1 0 480262172 14434304 3082 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3524 3082 603 41 0 3483 0
vsize: 14096
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3155 0 0 0 52993 14 0 0 25 0 1 0 480262172 14434304 3082 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3524 3082 603 41 0 3483 0
vsize: 14096
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3155 0 0 0 53993 14 0 0 25 0 1 0 480262172 14434304 3082 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3524 3082 603 41 0 3483 0
vsize: 14096
[startup+550.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3155 0 0 0 54993 14 0 0 25 0 1 0 480262172 14434304 3082 4294967295 134512640 134672761 3221224560 3221223600 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3524 3082 603 41 0 3483 0
vsize: 14096
[startup+560.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3164 0 0 0 55993 14 0 0 25 0 1 0 480262172 14467072 3090 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 3090 603 41 0 3491 0
vsize: 14128
[startup+570.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3164 0 0 0 56993 14 0 0 25 0 1 0 480262172 14467072 3090 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3532 3090 603 41 0 3491 0
vsize: 14128
[startup+580.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3175 0 0 0 57994 14 0 0 25 0 1 0 480262172 14508032 3100 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3542 3100 603 41 0 3501 0
vsize: 14168
[startup+590.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3175 0 0 0 58994 14 0 0 25 0 1 0 480262172 14508032 3100 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3542 3100 603 41 0 3501 0
vsize: 14168
[startup+600.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 59994 14 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+610.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 60994 14 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+620.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 61994 14 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+630.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 62994 14 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+640.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 63995 15 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+650.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3226 0 0 0 64995 15 0 0 25 0 1 0 480262172 14725120 3151 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3151 603 41 0 3554 0
vsize: 14380
[startup+660.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3235 0 0 0 65995 15 0 0 25 0 1 0 480262172 14757888 3159 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3603 3159 603 41 0 3562 0
vsize: 14412
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3235 0 0 0 66995 15 0 0 25 0 1 0 480262172 14757888 3159 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3603 3159 603 41 0 3562 0
vsize: 14412
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3256 0 0 0 67995 15 0 0 25 0 1 0 480262172 14856192 3180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3627 3180 603 41 0 3586 0
vsize: 14508
[startup+690.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3256 0 0 0 68995 15 0 0 25 0 1 0 480262172 14856192 3180 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3627 3180 603 41 0 3586 0
vsize: 14508
[startup+700.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3263 0 0 0 69995 15 0 0 25 0 1 0 480262172 14856192 3187 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3627 3187 603 41 0 3586 0
vsize: 14508
[startup+710.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3319 0 0 0 70995 15 0 0 25 0 1 0 480262172 15093760 3243 4294967295 134512640 134672761 3221224560 3221223684 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3685 3243 603 41 0 3644 0
vsize: 14740
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3319 0 0 0 71995 15 0 0 25 0 1 0 480262172 15093760 3243 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3685 3243 603 41 0 3644 0
vsize: 14740
[startup+730.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3337 0 0 0 72996 15 0 0 25 0 1 0 480262172 15159296 3260 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3701 3260 603 41 0 3660 0
vsize: 14804
[startup+740.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3337 0 0 0 73996 15 0 0 25 0 1 0 480262172 15159296 3260 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3701 3260 603 41 0 3660 0
vsize: 14804
[startup+750.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3337 0 0 0 74996 15 0 0 25 0 1 0 480262172 15159296 3260 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3701 3260 603 41 0 3660 0
vsize: 14804
[startup+760.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3354 0 0 0 75996 16 0 0 25 0 1 0 480262172 15224832 3276 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3276 603 41 0 3676 0
vsize: 14868
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3354 0 0 0 76996 16 0 0 25 0 1 0 480262172 15224832 3276 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3276 603 41 0 3676 0
vsize: 14868
[startup+780.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3354 0 0 0 77996 16 0 0 25 0 1 0 480262172 15224832 3276 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3717 3276 603 41 0 3676 0
vsize: 14868
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3373 0 0 0 78996 16 0 0 25 0 1 0 480262172 15302656 3295 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3736 3295 603 41 0 3695 0
vsize: 14944
[startup+800.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3373 0 0 0 79996 16 0 0 25 0 1 0 480262172 15302656 3295 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3736 3295 603 41 0 3695 0
vsize: 14944
[startup+810.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3373 0 0 0 80996 16 0 0 25 0 1 0 480262172 15302656 3295 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3736 3295 603 41 0 3695 0
vsize: 14944
[startup+820.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 81997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+830.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 82997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+840.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 83997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+850.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 84997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+860.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 85997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+870.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3411 0 0 0 86997 16 0 0 25 0 1 0 480262172 15454208 3332 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3773 3332 603 41 0 3732 0
vsize: 15092
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3428 0 0 0 87997 17 0 0 25 0 1 0 480262172 15519744 3348 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3348 603 41 0 3748 0
vsize: 15156
[startup+890.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3428 0 0 0 88997 17 0 0 25 0 1 0 480262172 15519744 3348 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3348 603 41 0 3748 0
vsize: 15156
[startup+900.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3438 0 0 0 89997 17 0 0 25 0 1 0 480262172 15552512 3357 4294967295 134512640 134672761 3221224560 3221223372 1075349917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3797 3357 603 41 0 3756 0
vsize: 15188
[startup+910.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3438 0 0 0 90997 17 0 0 25 0 1 0 480262172 15552512 3357 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3797 3357 603 41 0 3756 0
vsize: 15188
[startup+920.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3438 0 0 0 91998 17 0 0 25 0 1 0 480262172 15552512 3357 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3797 3357 603 41 0 3756 0
vsize: 15188
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3438 0 0 0 92998 17 0 0 25 0 1 0 480262172 15552512 3357 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3797 3357 603 41 0 3756 0
vsize: 15188
[startup+940.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 93998 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+950.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 94998 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+960.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 95998 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+970.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 96998 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+980.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 97999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 98999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 99999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 100999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 101999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 102999 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1040.03 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 104000 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1050.03 s]
Raw data (loadavg): 1.06 1.02 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3454 0 0 0 105000 17 0 0 25 0 1 0 480262172 15618048 3372 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3372 603 41 0 3772 0
vsize: 15252
[startup+1060.03 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3471 0 0 0 106000 17 0 0 25 0 1 0 480262172 15683584 3388 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3388 603 41 0 3788 0
vsize: 15316
[startup+1070.03 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3471 0 0 0 107000 17 0 0 25 0 1 0 480262172 15683584 3388 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3388 603 41 0 3788 0
vsize: 15316
[startup+1080.03 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3471 0 0 0 108000 17 0 0 25 0 1 0 480262172 15683584 3388 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3388 603 41 0 3788 0
vsize: 15316
[startup+1090.04 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3473 0 0 0 109001 17 0 0 25 0 1 0 480262172 15683584 3390 4294967295 134512640 134672761 3221224560 3221223744 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3390 603 41 0 3788 0
vsize: 15316
[startup+1100.04 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3473 0 0 0 110001 18 0 0 25 0 1 0 480262172 15683584 3390 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3390 603 41 0 3788 0
vsize: 15316
[startup+1110.04 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3473 0 0 0 111001 18 0 0 25 0 1 0 480262172 15683584 3390 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3390 603 41 0 3788 0
vsize: 15316
[startup+1120.04 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 112002 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1130.04 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 113002 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1140.04 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 114002 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1150.04 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 115002 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223552 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 116001 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 117000 18 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 118000 19 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 119000 19 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 23083
Raw data (stat): 23083 (minisat+) R 23082 18865 18864 0 -1 0 3478 0 0 0 120000 19 0 0 25 0 1 0 480262172 15683584 3395 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3829 3395 603 41 0 3788 0
vsize: 15316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 23083
Raw data (stat): 23083 (minisat+) Z 23082 18865 18864 0 -1 12 3478 0 0 0 120000 19 0 0 25 0 1 0 480262172 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1200.01
CPU system time (s): 0.199969
CPU usage (%): 100.013
Max. virtual memory (Kb): 15316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####