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-f2000.opb
MD5SUM	4675a5d50c7e04c9a0597ae768da1a88
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	4000
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	4000
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	4000
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	4000
Total number of constraints	10500
Number of constraints which are clauses	10500
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	2
Maximum length of a constraint	3
Trace number 4671

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 19:47:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3512 boxname=wulflinc10 idbench=128 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4675a5d50c7e04c9a0597ae768da1a88  /oldhome/oroussel/tmp/wulflinc10/normalized-f2000.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc10/normalized-f2000.opb /oldhome/oroussel/tmp/wulflinc10/normalized-f2000.opb
IDLAUNCH: 3512
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        909884 kB
Buffers:         33708 kB
Cached:          71528 kB
SwapCached:        164 kB
Active:          48744 kB
Inactive:        59544 kB
HighTotal:      131008 kB
HighFree:        55692 kB
LowTotal:       903652 kB
LowFree:        854192 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10952 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:07:06 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 3512 7 1200.14 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 10500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10500    29500 |    3500       0        0     nan |  0.000 % |
c |       101 |   10500    29500 |    3850     101     5214    51.6 |  0.000 % |
c |       254 |   10500    29500 |    4235     254    16768    66.0 |  0.000 % |
c |       480 |   10500    29500 |    4658     480    31254    65.1 |  0.000 % |
c |       818 |   10500    29500 |    5124     818    54667    66.8 |  0.000 % |
c |      1325 |   10500    29500 |    5636    1325    91945    69.4 |  0.000 % |
c |      2085 |   10500    29500 |    6200    2085   147368    70.7 |  0.000 % |
c |      3224 |   10500    29500 |    6820    3224   227442    70.5 |  0.000 % |
c |      4933 |   10500    29500 |    7502    4933   356310    72.2 |  0.000 % |
c |      7498 |   10500    29500 |    8252    7498   558986    74.6 |  0.000 % |
c |     11342 |   10500    29500 |    9078    7035   532667    75.7 |  0.000 % |
c |     17110 |   10500    29500 |    9985    8082   628618    77.8 |  0.000 % |
c |     25760 |   10500    29500 |   10984    6399   501007    78.3 |  0.000 % |
c |     38734 |   10500    29500 |   12082    8099   680844    84.1 |  0.000 % |
c |     58195 |   10500    29500 |   13291    8833   695144    78.7 |  0.000 % |
c |     87387 |   10500    29500 |   14620   10633   872256    82.0 |  0.000 % |
c |    131179 |   10500    29500 |   16082    9098   714655    78.6 |  0.000 % |
c |    196863 |   10500    29500 |   17690    8808   654716    74.3 |  0.000 % |
c |    295391 |   10500    29500 |   19459   16874  1288385    76.4 |  0.000 % |
c |    443181 |   10500    29500 |   21405   15399  1144903    74.3 |  0.000 % |
c |    664864 |   10500    29500 |   23546   18740  1450858    77.4 |  0.000 % |
#### 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.85 0.94 0.69 2/54 27373
Raw data (stat): 27373 (runsolver) R 27372 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420369397 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.0004 s]
Raw data (loadavg): 0.87 0.94 0.70 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 1400 0 0 0 993 3 0 0 25 0 1 0 420369397 7303168 1378 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1783 1378 603 41 0 1742 0
vsize: 7132
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.70 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 1659 0 0 0 1991 4 0 0 25 0 1 0 420369397 8380416 1637 4294967295 134512640 134672761 3221224576 3221223760 134559321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2046 1637 603 41 0 2005 0
vsize: 8184
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.70 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 1823 0 0 0 2990 5 0 0 25 0 1 0 420369397 9052160 1801 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2210 1801 603 41 0 2169 0
vsize: 8840
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.70 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 1910 0 0 0 3990 6 0 0 25 0 1 0 420369397 9457664 1888 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2309 1888 603 41 0 2268 0
vsize: 9236
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.94 0.71 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2012 0 0 0 4990 6 0 0 25 0 1 0 420369397 9859072 1990 4294967295 134512640 134672761 3221224576 3221223744 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 1990 603 41 0 2366 0
vsize: 9628
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.95 0.71 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2038 0 0 0 5990 6 0 0 25 0 1 0 420369397 9859072 2016 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2407 2016 603 41 0 2366 0
vsize: 9628
[startup+70.002 s]
Raw data (loadavg): 0.95 0.95 0.71 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2149 0 0 0 6989 7 0 0 25 0 1 0 420369397 10387456 2127 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2536 2127 603 41 0 2495 0
vsize: 10144
[startup+80.003 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2217 0 0 0 7989 7 0 0 25 0 1 0 420369397 10657792 2195 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2602 2195 603 41 0 2561 0
vsize: 10408
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.95 0.72 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2297 0 0 0 8989 7 0 0 25 0 1 0 420369397 10924032 2275 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2667 2275 603 41 0 2626 0
vsize: 10668
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2309 0 0 0 9989 8 0 0 25 0 1 0 420369397 11059200 2287 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2700 2287 603 41 0 2659 0
vsize: 10800
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2418 0 0 0 10987 8 0 0 25 0 1 0 420369397 11460608 2396 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2798 2396 603 41 0 2757 0
vsize: 11192
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2445 0 0 0 11987 9 0 0 25 0 1 0 420369397 11595776 2423 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2423 603 41 0 2790 0
vsize: 11324
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2482 0 0 0 12987 9 0 0 25 0 1 0 420369397 11730944 2460 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2460 603 41 0 2823 0
vsize: 11456
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2489 0 0 0 13987 9 0 0 25 0 1 0 420369397 11730944 2467 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2467 603 41 0 2823 0
vsize: 11456
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2512 0 0 0 14987 9 0 0 25 0 1 0 420369397 11866112 2490 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2490 603 41 0 2856 0
vsize: 11588
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2531 0 0 0 15987 9 0 0 25 0 1 0 420369397 12001280 2509 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2509 603 41 0 2889 0
vsize: 11720
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2647 0 0 0 16987 9 0 0 25 0 1 0 420369397 12546048 2625 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2647 0 0 0 17988 9 0 0 25 0 1 0 420369397 12546048 2625 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2650 0 0 0 18988 9 0 0 25 0 1 0 420369397 12546048 2628 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2628 603 41 0 3022 0
vsize: 12252
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2657 0 0 0 19988 9 0 0 25 0 1 0 420369397 12546048 2635 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2635 603 41 0 3022 0
vsize: 12252
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2669 0 0 0 20988 9 0 0 25 0 1 0 420369397 12546048 2647 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3063 2647 603 41 0 3022 0
vsize: 12252
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2710 0 0 0 21988 9 0 0 25 0 1 0 420369397 12824576 2688 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2688 603 41 0 3090 0
vsize: 12524
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2714 0 0 0 22988 9 0 0 25 0 1 0 420369397 12824576 2692 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2714 0 0 0 23988 9 0 0 25 0 1 0 420369397 12824576 2692 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2714 0 0 0 24989 9 0 0 25 0 1 0 420369397 12824576 2692 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2750 0 0 0 25989 10 0 0 25 0 1 0 420369397 12959744 2728 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3164 2728 603 41 0 3123 0
vsize: 12656
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2857 0 0 0 26989 10 0 0 25 0 1 0 420369397 13365248 2835 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3263 2835 603 41 0 3222 0
vsize: 13052
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2915 0 0 0 27989 10 0 0 25 0 1 0 420369397 13631488 2893 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3328 2893 603 41 0 3287 0
vsize: 13312
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2954 0 0 0 28989 10 0 0 25 0 1 0 420369397 13766656 2932 4294967295 134512640 134672761 3221224576 3221223744 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3361 2932 603 41 0 3320 0
vsize: 13444
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2968 0 0 0 29989 10 0 0 25 0 1 0 420369397 13766656 2946 4294967295 134512640 134672761 3221224576 3221223744 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3361 2946 603 41 0 3320 0
vsize: 13444
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2968 0 0 0 30989 10 0 0 25 0 1 0 420369397 13766656 2946 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3361 2946 603 41 0 3320 0
vsize: 13444
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2971 0 0 0 31989 10 0 0 25 0 1 0 420369397 13905920 2949 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.77 3/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2971 0 0 0 32990 10 0 0 25 0 1 0 420369397 13905920 2949 4294967295 134512640 134672761 3221224576 3221223700 134566095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2979 0 0 0 33990 10 0 0 25 0 1 0 420369397 13905920 2957 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2957 603 41 0 3354 0
vsize: 13580
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 2988 0 0 0 34990 10 0 0 25 0 1 0 420369397 13905920 2966 4294967295 134512640 134672761 3221224576 3221223740 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3395 2966 603 41 0 3354 0
vsize: 13580
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3008 0 0 0 35990 10 0 0 25 0 1 0 420369397 14041088 2986 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3008 0 0 0 36991 10 0 0 25 0 1 0 420369397 14041088 2986 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3048 0 0 0 37991 10 0 0 25 0 1 0 420369397 14172160 3026 4294967295 134512640 134672761 3221224576 3221223680 134554919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3460 3026 603 41 0 3419 0
vsize: 13840
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3055 0 0 0 38990 11 0 0 25 0 1 0 420369397 14172160 3033 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3460 3033 603 41 0 3419 0
vsize: 13840
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3174 0 0 0 39989 11 0 0 25 0 1 0 420369397 14708736 3152 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3591 3152 603 41 0 3550 0
vsize: 14364
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3179 0 0 0 40988 11 0 0 25 0 1 0 420369397 14708736 3157 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3157 603 41 0 3550 0
vsize: 14364
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3184 0 0 0 41989 11 0 0 25 0 1 0 420369397 14708736 3162 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3162 603 41 0 3550 0
vsize: 14364
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3206 0 0 0 42989 11 0 0 25 0 1 0 420369397 14843904 3184 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3624 3184 603 41 0 3583 0
vsize: 14496
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3220 0 0 0 43989 11 0 0 25 0 1 0 420369397 14843904 3198 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3624 3198 603 41 0 3583 0
vsize: 14496
[startup+450.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3249 0 0 0 44989 12 0 0 25 0 1 0 420369397 14979072 3227 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3227 603 41 0 3616 0
vsize: 14628
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3253 0 0 0 45989 12 0 0 25 0 1 0 420369397 14979072 3231 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3231 603 41 0 3616 0
vsize: 14628
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3255 0 0 0 46989 12 0 0 25 0 1 0 420369397 14979072 3233 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3657 3233 603 41 0 3616 0
vsize: 14628
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3274 0 0 0 47989 12 0 0 25 0 1 0 420369397 15126528 3252 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3252 603 41 0 3652 0
vsize: 14772
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3278 0 0 0 48990 12 0 0 25 0 1 0 420369397 15126528 3256 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3256 603 41 0 3652 0
vsize: 14772
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3280 0 0 0 49990 12 0 0 25 0 1 0 420369397 15126528 3258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3280 0 0 0 50990 12 0 0 25 0 1 0 420369397 15126528 3258 4294967295 134512640 134672761 3221224576 3221223744 134561124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3287 0 0 0 51990 12 0 0 25 0 1 0 420369397 15126528 3265 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3265 603 41 0 3652 0
vsize: 14772
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3287 0 0 0 52990 12 0 0 25 0 1 0 420369397 15126528 3265 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3265 603 41 0 3652 0
vsize: 14772
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3293 0 0 0 53991 12 0 0 25 0 1 0 420369397 15257600 3271 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3271 603 41 0 3684 0
vsize: 14900
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3321 0 0 0 54991 12 0 0 25 0 1 0 420369397 15257600 3299 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3725 3299 603 41 0 3684 0
vsize: 14900
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3332 0 0 0 55991 12 0 0 25 0 1 0 420369397 15392768 3310 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3758 3310 603 41 0 3717 0
vsize: 15032
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3386 0 0 0 56991 12 0 0 25 0 1 0 420369397 15527936 3364 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3791 3364 603 41 0 3750 0
vsize: 15164
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3429 0 0 0 57991 12 0 0 25 0 1 0 420369397 15806464 3407 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3407 603 41 0 3818 0
vsize: 15436
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3435 0 0 0 58991 12 0 0 25 0 1 0 420369397 15806464 3413 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3435 0 0 0 59991 12 0 0 25 0 1 0 420369397 15806464 3413 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3552 0 0 0 60990 13 0 0 25 0 1 0 420369397 16211968 3530 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3958 3530 603 41 0 3917 0
vsize: 15832
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3560 0 0 0 61989 13 0 0 25 0 1 0 420369397 16355328 3538 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3993 3538 603 41 0 3952 0
vsize: 15972
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3656 0 0 0 62989 13 0 0 25 0 1 0 420369397 16777216 3634 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4096 3634 603 41 0 4055 0
vsize: 16384
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3657 0 0 0 63989 13 0 0 25 0 1 0 420369397 16777216 3635 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4096 3635 603 41 0 4055 0
vsize: 16384
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3727 0 0 0 64989 14 0 0 25 0 1 0 420369397 17047552 3705 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3705 603 41 0 4121 0
vsize: 16648
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3737 0 0 0 65989 14 0 0 25 0 1 0 420369397 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+670.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3737 0 0 0 66989 14 0 0 25 0 1 0 420369397 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+680.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3737 0 0 0 67989 14 0 0 25 0 1 0 420369397 17047552 3715 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.83 3/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3737 0 0 0 68990 14 0 0 25 0 1 0 420369397 17047552 3715 4294967295 134512640 134672761 3221224576 3221223760 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3742 0 0 0 69990 14 0 0 25 0 1 0 420369397 17047552 3720 4294967295 134512640 134672761 3221224576 3221223744 134559126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3720 603 41 0 4121 0
vsize: 16648
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3745 0 0 0 70990 14 0 0 25 0 1 0 420369397 17047552 3723 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3723 603 41 0 4121 0
vsize: 16648
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.83 3/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3746 0 0 0 71990 14 0 0 25 0 1 0 420369397 17047552 3724 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4162 3724 603 41 0 4121 0
vsize: 16648
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3751 0 0 0 72990 14 0 0 25 0 1 0 420369397 17190912 3729 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3751 0 0 0 73991 14 0 0 25 0 1 0 420369397 17190912 3729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3785 0 0 0 74991 14 0 0 25 0 1 0 420369397 17326080 3763 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3763 603 41 0 4189 0
vsize: 16920
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3791 0 0 0 75991 14 0 0 25 0 1 0 420369397 17326080 3769 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3769 603 41 0 4189 0
vsize: 16920
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 27373
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3810 0 0 0 76991 14 0 0 25 0 1 0 420369397 17326080 3788 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3788 603 41 0 4189 0
vsize: 16920
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 27374
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3813 0 0 0 77991 14 0 0 25 0 1 0 420369397 17326080 3791 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+790.016 s]
Raw data (loadavg): 1.30 1.04 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3813 0 0 0 78990 14 0 0 25 0 1 0 420369397 17326080 3791 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+800.015 s]
Raw data (loadavg): 1.25 1.03 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3813 0 0 0 79990 14 0 0 25 0 1 0 420369397 17326080 3791 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+810.016 s]
Raw data (loadavg): 1.21 1.03 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3813 0 0 0 80990 15 0 0 25 0 1 0 420369397 17326080 3791 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+820.016 s]
Raw data (loadavg): 1.18 1.03 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3834 0 0 0 81991 15 0 0 25 0 1 0 420369397 17461248 3812 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3812 603 41 0 4222 0
vsize: 17052
[startup+830.016 s]
Raw data (loadavg): 1.15 1.03 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3834 0 0 0 82991 15 0 0 25 0 1 0 420369397 17461248 3812 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3812 603 41 0 4222 0
vsize: 17052
[startup+840.016 s]
Raw data (loadavg): 1.13 1.03 0.86 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3838 0 0 0 83991 15 0 0 25 0 1 0 420369397 17461248 3816 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3816 603 41 0 4222 0
vsize: 17052
[startup+850.016 s]
Raw data (loadavg): 1.11 1.03 0.87 2/54 27426
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3841 0 0 0 84991 15 0 0 25 0 1 0 420369397 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+860.017 s]
Raw data (loadavg): 1.09 1.03 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3841 0 0 0 85991 15 0 0 25 0 1 0 420369397 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+870.016 s]
Raw data (loadavg): 1.08 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3841 0 0 0 86991 15 0 0 25 0 1 0 420369397 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+880.016 s]
Raw data (loadavg): 1.06 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3841 0 0 0 87991 15 0 0 25 0 1 0 420369397 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+890.016 s]
Raw data (loadavg): 1.05 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3841 0 0 0 88992 15 0 0 25 0 1 0 420369397 17461248 3819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+900.016 s]
Raw data (loadavg): 1.04 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3887 0 0 0 89992 15 0 0 25 0 1 0 420369397 17727488 3865 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4328 3865 603 41 0 4287 0
vsize: 17312
[startup+910.016 s]
Raw data (loadavg): 1.04 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3891 0 0 0 90992 15 0 0 25 0 1 0 420369397 17727488 3869 4294967295 134512640 134672761 3221224576 3221223760 134559553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4328 3869 603 41 0 4287 0
vsize: 17312
[startup+920.016 s]
Raw data (loadavg): 1.03 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3931 0 0 0 91992 15 0 0 25 0 1 0 420369397 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+930.016 s]
Raw data (loadavg): 1.03 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3931 0 0 0 92992 15 0 0 25 0 1 0 420369397 17883136 3909 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+940.016 s]
Raw data (loadavg): 1.02 1.02 0.87 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 3931 0 0 0 93992 15 0 0 25 0 1 0 420369397 17883136 3909 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+950.017 s]
Raw data (loadavg): 1.02 1.02 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4015 0 0 0 94992 16 0 0 25 0 1 0 420369397 18284544 3993 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 3993 603 41 0 4423 0
vsize: 17856
[startup+960.016 s]
Raw data (loadavg): 1.01 1.02 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4018 0 0 0 95992 16 0 0 25 0 1 0 420369397 18284544 3996 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 3996 603 41 0 4423 0
vsize: 17856
[startup+970.016 s]
Raw data (loadavg): 1.01 1.02 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4024 0 0 0 96992 16 0 0 25 0 1 0 420369397 18284544 4002 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 4002 603 41 0 4423 0
vsize: 17856
[startup+980.015 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4033 0 0 0 97992 16 0 0 25 0 1 0 420369397 18284544 4011 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 4011 603 41 0 4423 0
vsize: 17856
[startup+990.015 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4038 0 0 0 98992 16 0 0 25 0 1 0 420369397 18415616 4016 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4016 603 41 0 4455 0
vsize: 17984
[startup+1000.01 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4041 0 0 0 99992 16 0 0 25 0 1 0 420369397 18415616 4019 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4019 603 41 0 4455 0
vsize: 17984
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4046 0 0 0 100992 16 0 0 25 0 1 0 420369397 18415616 4024 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4024 603 41 0 4455 0
vsize: 17984
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4047 0 0 0 101993 16 0 0 25 0 1 0 420369397 18415616 4025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4025 603 41 0 4455 0
vsize: 17984
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4051 0 0 0 102993 16 0 0 25 0 1 0 420369397 18415616 4029 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.01 0.88 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4051 0 0 0 103993 16 0 0 25 0 1 0 420369397 18415616 4029 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.01 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4056 0 0 0 104993 16 0 0 25 0 1 0 420369397 18415616 4034 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4034 603 41 0 4455 0
vsize: 17984
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.01 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4060 0 0 0 105993 16 0 0 25 0 1 0 420369397 18415616 4038 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4496 4038 603 41 0 4455 0
vsize: 17984
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.01 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4099 0 0 0 106994 16 0 0 25 0 1 0 420369397 18546688 4077 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4077 603 41 0 4487 0
vsize: 18112
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4103 0 0 0 107994 16 0 0 25 0 1 0 420369397 18685952 4081 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4562 4081 603 41 0 4521 0
vsize: 18248
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4159 0 0 0 108994 16 0 0 25 0 1 0 420369397 18821120 4137 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4595 4137 603 41 0 4554 0
vsize: 18380
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4162 0 0 0 109994 16 0 0 25 0 1 0 420369397 18821120 4140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4595 4140 603 41 0 4554 0
vsize: 18380
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4179 0 0 0 110994 16 0 0 25 0 1 0 420369397 18980864 4157 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4179 0 0 0 111994 16 0 0 25 0 1 0 420369397 18980864 4157 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4184 0 0 0 112994 16 0 0 25 0 1 0 420369397 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27428
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4184 0 0 0 113995 16 0 0 25 0 1 0 420369397 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4184 0 0 0 114995 16 0 0 25 0 1 0 420369397 18980864 4162 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4184 0 0 0 115995 16 0 0 25 0 1 0 420369397 18980864 4162 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4210 0 0 0 116995 16 0 0 25 0 1 0 420369397 19111936 4188 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4188 603 41 0 4625 0
vsize: 18664
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4214 0 0 0 117995 16 0 0 25 0 1 0 420369397 19111936 4192 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4192 603 41 0 4625 0
vsize: 18664
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4214 0 0 0 118995 16 0 0 25 0 1 0 420369397 19111936 4192 4294967295 134512640 134672761 3221224576 3221223760 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4192 603 41 0 4625 0
vsize: 18664
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 27430
Raw data (stat): 27373 (minisat+) R 27372 25347 25346 0 -1 0 4227 0 0 0 119996 16 0 0 25 0 1 0 420369397 19111936 4205 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4666 4205 603 41 0 4625 0
vsize: 18664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.90 1/54 27430
Raw data (stat): 27373 (minisat+) Z 27372 25347 25346 0 -1 12 4229 0 0 0 119996 17 0 0 25 0 1 0 420369397 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.02
CPU time (s): 1200.14
CPU user time (s): 1199.96
CPU system time (s): 0.176973
CPU usage (%): 100.01
Max. virtual memory (Kb): 18664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####