PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-par32-5-c.opb
MD5SUM	b2d6fc6e4e4b51f8b59d0f4ed12a9f74
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	2678
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	2678
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	2678
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	2678
Total number of constraints	6689
Number of constraints which are clauses	6689
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 4981

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 21:04:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1895 boxname=wulflinc6 idbench=211 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b2d6fc6e4e4b51f8b59d0f4ed12a9f74  /oldhome/oroussel/tmp/wulflinc6/normalized-par32-5-c.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc6/normalized-par32-5-c.opb
IDLAUNCH: 1895
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        920980 kB
Buffers:         34480 kB
Cached:          57396 kB
SwapCached:       2644 kB
Active:          50520 kB
Inactive:        46900 kB
HighTotal:      131008 kB
HighFree:        69692 kB
LowTotal:       903652 kB
LowFree:        851288 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10748 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:24:28 (client local time) WITH STATUS 0 IN 1200.37 SECONDS
stats: 1895 7 1200.37 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6689 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 |    6689    18356 |    2229       0        0     nan |  0.000 % |
c |       100 |    6689    18356 |    2451     100     2632    26.3 |  0.003 % |
c |       250 |    6689    18356 |    2697     250     5006    20.0 |  0.000 % |
c |       476 |    6689    18356 |    2966     476    10796    22.7 |  0.000 % |
c |       814 |    6689    18356 |    3263     814    16392    20.1 |  0.000 % |
c |      1321 |    6689    18356 |    3589    1321    31673    24.0 |  0.000 % |
c |      2081 |    6689    18356 |    3948    2081    43067    20.7 |  0.000 % |
c |      3222 |    6689    18356 |    4343    3222    88584    27.5 |  0.000 % |
c |      4930 |    6689    18356 |    4778    2659    86619    32.6 |  0.000 % |
c |      7492 |    6689    18356 |    5255    2771    76580    27.6 |  0.000 % |
c |     11336 |    6689    18356 |    5781    3945   104842    26.6 |  0.000 % |
c |     17104 |    6682    18340 |    6359    3858    86419    22.4 |  0.075 % |
c |     25753 |    6682    18340 |    6995    6099   138880    22.8 |  0.075 % |
c |     38728 |    6682    18340 |    7695    4938   110361    22.3 |  0.075 % |
c |     58189 |    6682    18340 |    8464    4995   107208    21.5 |  0.075 % |
c |     87383 |    6682    18340 |    9311    8509   228522    26.9 |  0.075 % |
c |    131173 |    6682    18340 |   10242    5370   108555    20.2 |  0.075 % |
c |    196858 |    6682    18340 |   11266    9087   200061    22.0 |  0.075 % |
c |    295385 |    6682    18340 |   12393   11274   240260    21.3 |  0.075 % |
c |    443174 |    6682    18340 |   13632    9238   225489    24.4 |  0.075 % |
c |    664857 |    6682    18340 |   14995   11547   233366    20.2 |  0.075 % |
#### 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.91 0.95 0.90 2/54 31909
Raw data (stat): 31909 (runsolver) R 31908 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420826182 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0007 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 31909
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 792 0 0 0 996 2 0 0 25 0 1 0 420826182 4751360 770 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1160 770 603 41 0 1119 0
vsize: 4640
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 31909
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 826 0 0 0 1995 2 0 0 25 0 1 0 420826182 5017600 804 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1225 804 603 41 0 1184 0
vsize: 4900
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31909
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 865 0 0 0 2995 2 0 0 25 0 1 0 420826182 5156864 843 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1259 843 603 41 0 1218 0
vsize: 5036
[startup+40.0032 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 31909
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 901 0 0 0 3996 2 0 0 25 0 1 0 420826182 5287936 879 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1291 879 603 41 0 1250 0
vsize: 5164
[startup+50.004 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 31909
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 909 0 0 0 4996 2 0 0 25 0 1 0 420826182 5287936 887 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1291 887 603 41 0 1250 0
vsize: 5164
[startup+60.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 915 0 0 0 5996 2 0 0 25 0 1 0 420826182 5287936 893 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1291 893 603 41 0 1250 0
vsize: 5164
[startup+70.0059 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 981 0 0 0 6995 3 0 0 25 0 1 0 420826182 5705728 959 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1393 959 603 41 0 1352 0
vsize: 5572
[startup+80.0066 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 988 0 0 0 7995 4 0 0 25 0 1 0 420826182 5705728 966 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1393 966 603 41 0 1352 0
vsize: 5572
[startup+90.0068 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1020 0 0 0 8995 4 0 0 25 0 1 0 420826182 5836800 998 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 998 603 41 0 1384 0
vsize: 5700
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1028 0 0 0 9995 4 0 0 25 0 1 0 420826182 5836800 1006 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1006 603 41 0 1384 0
vsize: 5700
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1033 0 0 0 10995 4 0 0 25 0 1 0 420826182 5836800 1011 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1011 603 41 0 1384 0
vsize: 5700
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1034 0 0 0 11995 5 0 0 25 0 1 0 420826182 5836800 1012 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1034 0 0 0 12995 5 0 0 25 0 1 0 420826182 5836800 1012 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1041 0 0 0 13995 5 0 0 25 0 1 0 420826182 5836800 1019 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1019 603 41 0 1384 0
vsize: 5700
[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1042 0 0 0 14995 5 0 0 25 0 1 0 420826182 5836800 1020 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1020 603 41 0 1384 0
vsize: 5700
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1046 0 0 0 15996 5 0 0 25 0 1 0 420826182 5836800 1024 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1024 603 41 0 1384 0
vsize: 5700
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1074 0 0 0 16996 5 0 0 25 0 1 0 420826182 5971968 1052 4294967295 134512640 134672761 3221224640 3221223744 134555126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1458 1052 603 41 0 1417 0
vsize: 5832
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1074 0 0 0 17996 5 0 0 25 0 1 0 420826182 5971968 1052 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1458 1052 603 41 0 1417 0
vsize: 5832
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1079 0 0 0 18996 5 0 0 25 0 1 0 420826182 6127616 1057 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1496 1057 603 41 0 1455 0
vsize: 5984
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1079 0 0 0 19997 5 0 0 25 0 1 0 420826182 6127616 1057 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1496 1057 603 41 0 1455 0
vsize: 5984
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1086 0 0 0 20997 5 0 0 25 0 1 0 420826182 6127616 1064 4294967295 134512640 134672761 3221224640 3221223796 134565028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1496 1064 603 41 0 1455 0
vsize: 5984
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1098 0 0 0 21997 5 0 0 25 0 1 0 420826182 6127616 1076 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1496 1076 603 41 0 1455 0
vsize: 5984
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1109 0 0 0 22998 5 0 0 25 0 1 0 420826182 6262784 1087 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1087 603 41 0 1488 0
vsize: 6116
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1109 0 0 0 23998 5 0 0 25 0 1 0 420826182 6262784 1087 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1087 603 41 0 1488 0
vsize: 6116
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 24998 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 25999 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 26999 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 27999 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 29000 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1114 0 0 0 30000 5 0 0 25 0 1 0 420826182 6262784 1092 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1116 0 0 0 31001 5 0 0 25 0 1 0 420826182 6262784 1094 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1094 603 41 0 1488 0
vsize: 6116
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1116 0 0 0 32001 5 0 0 25 0 1 0 420826182 6262784 1094 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1094 603 41 0 1488 0
vsize: 6116
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1136 0 0 0 33001 6 0 0 25 0 1 0 420826182 6262784 1114 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1114 603 41 0 1488 0
vsize: 6116
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1160 0 0 0 34001 6 0 0 25 0 1 0 420826182 6397952 1138 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1562 1138 603 41 0 1521 0
vsize: 6248
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1178 0 0 0 35001 6 0 0 25 0 1 0 420826182 6533120 1156 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1595 1156 603 41 0 1554 0
vsize: 6380
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1198 0 0 0 36002 6 0 0 25 0 1 0 420826182 6533120 1176 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1595 1176 603 41 0 1554 0
vsize: 6380
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1204 0 0 0 37002 6 0 0 25 0 1 0 420826182 6668288 1182 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1182 603 41 0 1587 0
vsize: 6512
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1205 0 0 0 38002 6 0 0 25 0 1 0 420826182 6668288 1183 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1205 0 0 0 39003 6 0 0 25 0 1 0 420826182 6668288 1183 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1205 0 0 0 40003 6 0 0 25 0 1 0 420826182 6668288 1183 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1205 0 0 0 41003 6 0 0 25 0 1 0 420826182 6668288 1183 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1211 0 0 0 42003 6 0 0 25 0 1 0 420826182 6668288 1189 4294967295 134512640 134672761 3221224640 3221223824 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1211 0 0 0 43004 6 0 0 25 0 1 0 420826182 6668288 1189 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1211 0 0 0 44004 6 0 0 25 0 1 0 420826182 6668288 1189 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1211 0 0 0 45005 6 0 0 25 0 1 0 420826182 6668288 1189 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1211 0 0 0 46005 6 0 0 25 0 1 0 420826182 6668288 1189 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1213 0 0 0 47005 6 0 0 25 0 1 0 420826182 6668288 1191 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1191 603 41 0 1587 0
vsize: 6512
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1216 0 0 0 48006 6 0 0 25 0 1 0 420826182 6668288 1194 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1216 0 0 0 49006 6 0 0 25 0 1 0 420826182 6668288 1194 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+500.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1216 0 0 0 50006 6 0 0 25 0 1 0 420826182 6668288 1194 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1216 0 0 0 51007 6 0 0 25 0 1 0 420826182 6668288 1194 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1222 0 0 0 52007 6 0 0 25 0 1 0 420826182 6668288 1200 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1200 603 41 0 1587 0
vsize: 6512
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1247 0 0 0 53007 6 0 0 25 0 1 0 420826182 6799360 1225 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1225 603 41 0 1619 0
vsize: 6640
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1248 0 0 0 54007 6 0 0 25 0 1 0 420826182 6799360 1226 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1226 603 41 0 1619 0
vsize: 6640
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1252 0 0 0 55008 6 0 0 25 0 1 0 420826182 6799360 1230 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1230 603 41 0 1619 0
vsize: 6640
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1258 0 0 0 56008 6 0 0 25 0 1 0 420826182 6799360 1236 4294967295 134512640 134672761 3221224640 3221223800 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1236 603 41 0 1619 0
vsize: 6640
[startup+570.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1258 0 0 0 57008 6 0 0 25 0 1 0 420826182 6799360 1236 4294967295 134512640 134672761 3221224640 3221223808 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1236 603 41 0 1619 0
vsize: 6640
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1260 0 0 0 58009 6 0 0 25 0 1 0 420826182 6799360 1238 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1238 603 41 0 1619 0
vsize: 6640
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1265 0 0 0 59009 6 0 0 25 0 1 0 420826182 6934528 1243 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1243 603 41 0 1652 0
vsize: 6772
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1265 0 0 0 60009 6 0 0 25 0 1 0 420826182 6934528 1243 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1243 603 41 0 1652 0
vsize: 6772
[startup+610.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1270 0 0 0 61010 6 0 0 25 0 1 0 420826182 6934528 1248 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1248 603 41 0 1652 0
vsize: 6772
[startup+620.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1275 0 0 0 62010 6 0 0 25 0 1 0 420826182 6934528 1253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+630.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1275 0 0 0 63010 6 0 0 25 0 1 0 420826182 6934528 1253 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1275 0 0 0 64011 6 0 0 25 0 1 0 420826182 6934528 1253 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1281 0 0 0 65011 6 0 0 25 0 1 0 420826182 6934528 1259 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1281 0 0 0 66012 6 0 0 25 0 1 0 420826182 6934528 1259 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1281 0 0 0 67012 6 0 0 25 0 1 0 420826182 6934528 1259 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1286 0 0 0 68012 6 0 0 25 0 1 0 420826182 6934528 1264 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1264 603 41 0 1652 0
vsize: 6772
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1286 0 0 0 69013 6 0 0 25 0 1 0 420826182 6934528 1264 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1693 1264 603 41 0 1652 0
vsize: 6772
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1292 0 0 0 70013 6 0 0 25 0 1 0 420826182 7098368 1270 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1270 603 41 0 1692 0
vsize: 6932
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1298 0 0 0 71013 6 0 0 25 0 1 0 420826182 7098368 1276 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1276 603 41 0 1692 0
vsize: 6932
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1304 0 0 0 72014 6 0 0 25 0 1 0 420826182 7098368 1282 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1282 603 41 0 1692 0
vsize: 6932
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1304 0 0 0 73014 6 0 0 25 0 1 0 420826182 7098368 1282 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1282 603 41 0 1692 0
vsize: 6932
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1306 0 0 0 74014 6 0 0 25 0 1 0 420826182 7098368 1284 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1306 0 0 0 75015 6 0 0 25 0 1 0 420826182 7098368 1284 4294967295 134512640 134672761 3221224640 3221223776 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1306 0 0 0 76015 6 0 0 25 0 1 0 420826182 7098368 1284 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1306 0 0 0 77016 6 0 0 25 0 1 0 420826182 7098368 1284 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1307 0 0 0 78016 7 0 0 25 0 1 0 420826182 7098368 1285 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1285 603 41 0 1692 0
vsize: 6932
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1308 0 0 0 79016 7 0 0 25 0 1 0 420826182 7098368 1286 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1286 603 41 0 1692 0
vsize: 6932
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1308 0 0 0 80016 7 0 0 25 0 1 0 420826182 7098368 1286 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1286 603 41 0 1692 0
vsize: 6932
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1310 0 0 0 81016 7 0 0 25 0 1 0 420826182 7098368 1288 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1288 603 41 0 1692 0
vsize: 6932
[startup+820.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1357 0 0 0 82017 7 0 0 25 0 1 0 420826182 7368704 1335 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1335 603 41 0 1758 0
vsize: 7196
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 83017 7 0 0 25 0 1 0 420826182 7368704 1339 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1339 603 41 0 1758 0
vsize: 7196
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 84017 7 0 0 25 0 1 0 420826182 7368704 1339 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1339 603 41 0 1758 0
vsize: 7196
[startup+850.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 85018 7 0 0 25 0 1 0 420826182 7364608 1339 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 86018 7 0 0 25 0 1 0 420826182 7364608 1339 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 87018 7 0 0 25 0 1 0 420826182 7364608 1339 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1361 0 0 0 88019 7 0 0 25 0 1 0 420826182 7364608 1339 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1362 0 0 0 89019 7 0 0 25 0 1 0 420826182 7364608 1340 4294967295 134512640 134672761 3221224640 3221223840 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1340 603 41 0 1757 0
vsize: 7192
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1362 0 0 0 90019 7 0 0 25 0 1 0 420826182 7364608 1340 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1340 603 41 0 1757 0
vsize: 7192
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1377 0 0 0 91019 7 0 0 25 0 1 0 420826182 7364608 1355 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1377 0 0 0 92020 7 0 0 25 0 1 0 420826182 7364608 1355 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+930.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1377 0 0 0 93020 7 0 0 25 0 1 0 420826182 7364608 1355 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+940.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1377 0 0 0 94020 7 0 0 25 0 1 0 420826182 7364608 1355 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1379 0 0 0 95021 7 0 0 25 0 1 0 420826182 7364608 1357 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1357 603 41 0 1757 0
vsize: 7192
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1380 0 0 0 96021 7 0 0 25 0 1 0 420826182 7364608 1358 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1380 0 0 0 97021 7 0 0 25 0 1 0 420826182 7364608 1358 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1380 0 0 0 98021 7 0 0 25 0 1 0 420826182 7364608 1358 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+990.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1380 0 0 0 99022 7 0 0 25 0 1 0 420826182 7364608 1358 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1380 0 0 0 100022 7 0 0 25 0 1 0 420826182 7364608 1358 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 101022 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 102022 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 103023 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 104023 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 105023 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 106024 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1382 0 0 0 107024 7 0 0 25 0 1 0 420826182 7364608 1360 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1383 0 0 0 108024 7 0 0 25 0 1 0 420826182 7364608 1361 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1383 0 0 0 109025 7 0 0 25 0 1 0 420826182 7364608 1361 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1383 0 0 0 110025 7 0 0 25 0 1 0 420826182 7364608 1361 4294967295 134512640 134672761 3221224640 3221223792 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1383 0 0 0 111025 7 0 0 25 0 1 0 420826182 7364608 1361 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1385 0 0 0 112026 7 0 0 25 0 1 0 420826182 7364608 1363 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1363 603 41 0 1757 0
vsize: 7192
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1386 0 0 0 113026 7 0 0 25 0 1 0 420826182 7364608 1364 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1386 0 0 0 114026 7 0 0 25 0 1 0 420826182 7364608 1364 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1386 0 0 0 115027 7 0 0 25 0 1 0 420826182 7364608 1364 4294967295 134512640 134672761 3221224640 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1387 0 0 0 116027 7 0 0 25 0 1 0 420826182 7364608 1365 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1387 0 0 0 117027 7 0 0 25 0 1 0 420826182 7364608 1365 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1387 0 0 0 118028 7 0 0 25 0 1 0 420826182 7364608 1365 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1391 0 0 0 119028 7 0 0 25 0 1 0 420826182 7364608 1369 4294967295 134512640 134672761 3221224640 3221223808 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1369 603 41 0 1757 0
vsize: 7192
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31911
Raw data (stat): 31909 (minisat+) R 31908 29653 29652 0 -1 0 1391 0 0 0 120028 7 0 0 25 0 1 0 420826182 7364608 1369 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1798 1369 603 41 0 1757 0
vsize: 7192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31911
Raw data (stat): 31909 (minisat+) Z 31908 29653 29652 0 -1 12 1393 0 0 0 120028 8 0 0 23 0 1 0 420826182 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.37
CPU user time (s): 1200.29
CPU system time (s): 0.081987
CPU usage (%): 100.026
Max. virtual memory (Kb): 7196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####