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-1-c.opb
MD5SUM	8c1b8634a2f99e9f8e579ef031d10353
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	2630
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	2630
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	2630
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	2630
Total number of constraints	6569
Number of constraints which are clauses	6569
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 5932

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 02:20:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4339 boxname=wulflinc30 idbench=203 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c1b8634a2f99e9f8e579ef031d10353  /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb
IDLAUNCH: 4339
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        731952 kB
Buffers:         38168 kB
Cached:         223904 kB
SwapCached:          0 kB
Active:          84456 kB
Inactive:       180456 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        731700 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32240 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:40:14 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 4339 7 1200.15 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6569 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 |    6569    18020 |    2189       0        0     nan |  0.000 % |
c |       100 |    6569    18020 |    2407     100     3667    36.7 |  0.004 % |
c |       251 |    6569    18020 |    2648     251     9998    39.8 |  0.000 % |
c |       477 |    6569    18020 |    2913     477    19389    40.6 |  0.000 % |
c |       814 |    6569    18020 |    3204     814    28997    35.6 |  0.000 % |
c |      1320 |    6569    18020 |    3525    1320    43427    32.9 |  0.000 % |
c |      2079 |    6562    18004 |    3877    2077    64872    31.2 |  0.076 % |
c |      3218 |    6562    18004 |    4265    3216    92939    28.9 |  0.076 % |
c |      4927 |    6562    18004 |    4692    2772    64097    23.1 |  0.076 % |
c |      7489 |    6562    18004 |    5161    2951    64576    21.9 |  0.076 % |
c |     11333 |    6562    18004 |    5677    4187    97402    23.3 |  0.076 % |
c |     17099 |    6562    18004 |    6245    4190    93186    22.2 |  0.076 % |
c |     25748 |    6562    18004 |    6870    3311    68434    20.7 |  0.076 % |
c |     38722 |    6562    18004 |    7557    5903   133047    22.5 |  0.076 % |
c |     58183 |    6562    18004 |    8312    6287   144714    23.0 |  0.076 % |
c |     87376 |    6562    18004 |    9143    6021   133526    22.2 |  0.076 % |
c |    131166 |    6562    18004 |   10058    8376   183814    21.9 |  0.076 % |
c |    196850 |    6562    18004 |   11064    8127   172744    21.3 |  0.076 % |
c |    295376 |    6562    18004 |   12170    6300   144154    22.9 |  0.076 % |
c |    443166 |    6562    18004 |   13387    6996   179583    25.7 |  0.076 % |
c |    664849 |    6562    18004 |   14726   13043   279106    21.4 |  0.076 % |
#### 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.65 0.88 0.88 2/54 18249
Raw data (stat): 18249 (runsolver) R 18248 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480940355 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99982 s]
Raw data (loadavg): 0.70 0.88 0.88 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 774 0 0 0 997 2 0 0 25 0 1 0 480940355 4775936 752 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1166 752 603 41 0 1125 0
vsize: 4664
[startup+20.001 s]
Raw data (loadavg): 0.75 0.89 0.88 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 801 0 0 0 1996 2 0 0 25 0 1 0 480940355 4775936 779 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1166 779 603 41 0 1125 0
vsize: 4664
[startup+30.0018 s]
Raw data (loadavg): 0.78 0.89 0.88 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 815 0 0 0 2996 3 0 0 25 0 1 0 480940355 4915200 793 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1200 793 603 41 0 1159 0
vsize: 4800
[startup+40.0012 s]
Raw data (loadavg): 0.82 0.89 0.88 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 835 0 0 0 3995 3 0 0 25 0 1 0 480940355 5054464 813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1234 813 603 41 0 1193 0
vsize: 4936
[startup+50.0024 s]
Raw data (loadavg): 0.84 0.90 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 871 0 0 0 4995 4 0 0 25 0 1 0 480940355 5185536 849 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 849 603 41 0 1225 0
vsize: 5064
[startup+60.0032 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 877 0 0 0 5994 4 0 0 25 0 1 0 480940355 5185536 855 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 855 603 41 0 1225 0
vsize: 5064
[startup+70.0036 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 916 0 0 0 6994 4 0 0 25 0 1 0 480940355 5320704 894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1299 894 603 41 0 1258 0
vsize: 5196
[startup+80.0051 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 920 0 0 0 7994 5 0 0 25 0 1 0 480940355 5459968 898 4294967295 134512640 134672761 3221224560 3221223772 1075346912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+90.0056 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 920 0 0 0 8993 5 0 0 25 0 1 0 480940355 5459968 898 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+100.006 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 924 0 0 0 9993 6 0 0 25 0 1 0 480940355 5459968 902 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 902 603 41 0 1292 0
vsize: 5332
[startup+110.007 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 948 0 0 0 10992 6 0 0 25 0 1 0 480940355 5459968 926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 926 603 41 0 1292 0
vsize: 5332
[startup+120.008 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 950 0 0 0 11992 7 0 0 25 0 1 0 480940355 5459968 928 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+130.008 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 950 0 0 0 12992 7 0 0 25 0 1 0 480940355 5459968 928 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+140.009 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 959 0 0 0 13991 8 0 0 25 0 1 0 480940355 5595136 937 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 937 603 41 0 1325 0
vsize: 5464
[startup+150.009 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 964 0 0 0 14991 8 0 0 25 0 1 0 480940355 5595136 942 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 942 603 41 0 1325 0
vsize: 5464
[startup+160.009 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 989 0 0 0 15990 9 0 0 25 0 1 0 480940355 5730304 967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 967 603 41 0 1358 0
vsize: 5596
[startup+170.01 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1006 0 0 0 16990 9 0 0 25 0 1 0 480940355 5730304 984 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 984 603 41 0 1358 0
vsize: 5596
[startup+180.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1010 0 0 0 17989 10 0 0 25 0 1 0 480940355 5730304 988 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 988 603 41 0 1358 0
vsize: 5596
[startup+190.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1016 0 0 0 18989 11 0 0 25 0 1 0 480940355 5730304 994 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+200.01 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1016 0 0 0 19988 11 0 0 25 0 1 0 480940355 5730304 994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+210.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1016 0 0 0 20988 12 0 0 25 0 1 0 480940355 5730304 994 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+220.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1016 0 0 0 21988 12 0 0 25 0 1 0 480940355 5730304 994 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+230.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1016 0 0 0 22987 12 0 0 25 0 1 0 480940355 5730304 994 4294967295 134512640 134672761 3221224560 3221223664 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+240.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1041 0 0 0 23987 13 0 0 25 0 1 0 480940355 5865472 1019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1019 603 41 0 1391 0
vsize: 5728
[startup+250.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1058 0 0 0 24987 13 0 0 25 0 1 0 480940355 6012928 1036 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1036 603 41 0 1427 0
vsize: 5872
[startup+260.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1063 0 0 0 25986 14 0 0 25 0 1 0 480940355 6012928 1041 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1041 603 41 0 1427 0
vsize: 5872
[startup+270.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1070 0 0 0 26986 14 0 0 25 0 1 0 480940355 6012928 1048 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1048 603 41 0 1427 0
vsize: 5872
[startup+280.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1076 0 0 0 27986 15 0 0 25 0 1 0 480940355 6012928 1054 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1054 603 41 0 1427 0
vsize: 5872
[startup+290.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1094 0 0 0 28985 15 0 0 25 0 1 0 480940355 6148096 1072 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1072 603 41 0 1460 0
vsize: 6004
[startup+300.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1094 0 0 0 29985 15 0 0 25 0 1 0 480940355 6148096 1072 4294967295 134512640 134672761 3221224560 3221223744 134559390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1072 603 41 0 1460 0
vsize: 6004
[startup+310.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1101 0 0 0 30985 15 0 0 25 0 1 0 480940355 6148096 1079 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1079 603 41 0 1460 0
vsize: 6004
[startup+320.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1108 0 0 0 31985 15 0 0 25 0 1 0 480940355 6148096 1086 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1086 603 41 0 1460 0
vsize: 6004
[startup+330.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1114 0 0 0 32985 16 0 0 25 0 1 0 480940355 6291456 1092 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+340.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1114 0 0 0 33985 16 0 0 25 0 1 0 480940355 6291456 1092 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+350.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1114 0 0 0 34986 16 0 0 25 0 1 0 480940355 6291456 1092 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+360.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1118 0 0 0 35986 16 0 0 25 0 1 0 480940355 6291456 1096 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1096 603 41 0 1495 0
vsize: 6144
[startup+370.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1124 0 0 0 36985 16 0 0 25 0 1 0 480940355 6291456 1102 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1102 603 41 0 1495 0
vsize: 6144
[startup+380.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1161 0 0 0 37985 16 0 0 25 0 1 0 480940355 6426624 1139 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1139 603 41 0 1528 0
vsize: 6276
[startup+390.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1173 0 0 0 38985 16 0 0 25 0 1 0 480940355 6426624 1151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+400.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1173 0 0 0 39986 16 0 0 25 0 1 0 480940355 6426624 1151 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+410.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1175 0 0 0 40986 16 0 0 25 0 1 0 480940355 6561792 1153 4294967295 134512640 134672761 3221224560 3221223744 134558394 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+420.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1175 0 0 0 41986 16 0 0 25 0 1 0 480940355 6561792 1153 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+430.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1177 0 0 0 42986 16 0 0 25 0 1 0 480940355 6561792 1155 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1155 603 41 0 1561 0
vsize: 6408
[startup+440.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1179 0 0 0 43986 16 0 0 25 0 1 0 480940355 6561792 1157 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1157 603 41 0 1561 0
vsize: 6408
[startup+450.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1184 0 0 0 44986 16 0 0 25 0 1 0 480940355 6561792 1162 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1162 603 41 0 1561 0
vsize: 6408
[startup+460.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1186 0 0 0 45987 16 0 0 25 0 1 0 480940355 6561792 1164 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1164 603 41 0 1561 0
vsize: 6408
[startup+470.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1196 0 0 0 46987 16 0 0 25 0 1 0 480940355 6561792 1174 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1174 603 41 0 1561 0
vsize: 6408
[startup+480.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1203 0 0 0 47987 16 0 0 25 0 1 0 480940355 6561792 1181 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1181 603 41 0 1561 0
vsize: 6408
[startup+490.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 48987 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 49987 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223664 134554926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 50987 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223664 134555091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 51988 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 52988 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1209 0 0 0 53988 16 0 0 25 0 1 0 480940355 6717440 1187 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1212 0 0 0 54988 16 0 0 25 0 1 0 480940355 6717440 1190 4294967295 134512640 134672761 3221224560 3221223744 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1190 603 41 0 1599 0
vsize: 6560
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1228 0 0 0 55988 16 0 0 25 0 1 0 480940355 6717440 1206 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1206 603 41 0 1599 0
vsize: 6560
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1238 0 0 0 56988 17 0 0 25 0 1 0 480940355 6717440 1216 4294967295 134512640 134672761 3221224560 3221223696 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1216 603 41 0 1599 0
vsize: 6560
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1240 0 0 0 57988 17 0 0 25 0 1 0 480940355 6717440 1218 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1218 603 41 0 1599 0
vsize: 6560
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1247 0 0 0 58988 17 0 0 25 0 1 0 480940355 6868992 1225 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1225 603 41 0 1636 0
vsize: 6708
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1253 0 0 0 59989 17 0 0 25 0 1 0 480940355 6868992 1231 4294967295 134512640 134672761 3221224560 3221223760 134557897 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1231 603 41 0 1636 0
vsize: 6708
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1259 0 0 0 60989 17 0 0 25 0 1 0 480940355 6868992 1237 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1237 603 41 0 1636 0
vsize: 6708
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1260 0 0 0 61989 17 0 0 25 0 1 0 480940355 6868992 1238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1238 603 41 0 1636 0
vsize: 6708
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1261 0 0 0 62989 17 0 0 25 0 1 0 480940355 6868992 1239 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1261 0 0 0 63989 17 0 0 25 0 1 0 480940355 6868992 1239 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1267 0 0 0 64989 17 0 0 25 0 1 0 480940355 6868992 1245 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1245 603 41 0 1636 0
vsize: 6708
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1267 0 0 0 65990 17 0 0 25 0 1 0 480940355 6868992 1245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1245 603 41 0 1636 0
vsize: 6708
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1273 0 0 0 66989 17 0 0 25 0 1 0 480940355 6868992 1251 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1273 0 0 0 67988 18 0 0 25 0 1 0 480940355 6868992 1251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1273 0 0 0 68987 18 0 0 25 0 1 0 480940355 6868992 1251 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1273 0 0 0 69987 18 0 0 25 0 1 0 480940355 6868992 1251 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1277 0 0 0 70987 18 0 0 25 0 1 0 480940355 7004160 1255 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1255 603 41 0 1669 0
vsize: 6840
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1293 0 0 0 71987 18 0 0 25 0 1 0 480940355 7004160 1271 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1271 603 41 0 1669 0
vsize: 6840
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1299 0 0 0 72988 18 0 0 25 0 1 0 480940355 7004160 1277 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1277 603 41 0 1669 0
vsize: 6840
[startup+740.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 73988 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 74988 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 75988 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 76988 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 77989 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 78989 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+800.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1305 0 0 0 79989 18 0 0 25 0 1 0 480940355 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1326 0 0 0 80989 18 0 0 25 0 1 0 480940355 7139328 1304 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1304 603 41 0 1702 0
vsize: 6972
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1355 0 0 0 81989 18 0 0 25 0 1 0 480940355 7270400 1333 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1775 1333 603 41 0 1734 0
vsize: 7100
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1361 0 0 0 82989 18 0 0 25 0 1 0 480940355 7270400 1339 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1775 1339 603 41 0 1734 0
vsize: 7100
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1365 0 0 0 83989 18 0 0 25 0 1 0 480940355 7270400 1343 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1775 1343 603 41 0 1734 0
vsize: 7100
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1367 0 0 0 84989 18 0 0 25 0 1 0 480940355 7270400 1345 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1775 1345 603 41 0 1734 0
vsize: 7100
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1376 0 0 0 85989 18 0 0 25 0 1 0 480940355 7401472 1354 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1354 603 41 0 1766 0
vsize: 7228
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1387 0 0 0 86989 18 0 0 25 0 1 0 480940355 7401472 1365 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1387 0 0 0 87990 18 0 0 25 0 1 0 480940355 7401472 1365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1387 0 0 0 88990 18 0 0 25 0 1 0 480940355 7401472 1365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+900.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1393 0 0 0 89990 18 0 0 25 0 1 0 480940355 7401472 1371 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1393 0 0 0 90990 18 0 0 25 0 1 0 480940355 7401472 1371 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1393 0 0 0 91990 18 0 0 25 0 1 0 480940355 7401472 1371 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1423 0 0 0 92990 18 0 0 25 0 1 0 480940355 7532544 1401 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1839 1401 603 41 0 1798 0
vsize: 7356
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1432 0 0 0 93991 18 0 0 25 0 1 0 480940355 7667712 1410 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1872 1410 603 41 0 1831 0
vsize: 7488
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1432 0 0 0 94991 18 0 0 25 0 1 0 480940355 7663616 1410 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1410 603 41 0 1830 0
vsize: 7484
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1432 0 0 0 95991 19 0 0 25 0 1 0 480940355 7663616 1410 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1410 603 41 0 1830 0
vsize: 7484
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1436 0 0 0 96991 19 0 0 25 0 1 0 480940355 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1436 0 0 0 97991 19 0 0 25 0 1 0 480940355 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1436 0 0 0 98991 19 0 0 25 0 1 0 480940355 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1436 0 0 0 99991 19 0 0 25 0 1 0 480940355 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1436 0 0 0 100992 19 0 0 25 0 1 0 480940355 7663616 1414 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 101992 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 102992 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 103992 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 104992 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 105993 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 106993 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 107993 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 108993 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 109993 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 110994 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 111994 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 112994 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 113994 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1437 0 0 0 114994 19 0 0 25 0 1 0 480940355 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1442 0 0 0 115994 19 0 0 25 0 1 0 480940355 7663616 1420 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1442 0 0 0 116995 19 0 0 25 0 1 0 480940355 7663616 1420 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1442 0 0 0 117995 19 0 0 25 0 1 0 480940355 7663616 1420 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1448 0 0 0 118995 19 0 0 25 0 1 0 480940355 7663616 1426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18249
Raw data (stat): 18249 (minisat+) R 18248 11931 11930 0 -1 0 1448 0 0 0 119995 19 0 0 25 0 1 0 480940355 7663616 1426 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18249
Raw data (stat): 18249 (minisat+) Z 18248 11931 11930 0 -1 12 1450 0 0 0 119995 19 0 0 25 0 1 0 480940355 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.04
CPU time (s): 1200.15
CPU user time (s): 1199.96
CPU system time (s): 0.19597
CPU usage (%): 100.009
Max. virtual memory (Kb): 7488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####