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-2-c.opb
MD5SUM	40e47c460002545cc2670ca84fd53082
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	2606
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	2606
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	2606
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	2606
Total number of constraints	6509
Number of constraints which are clauses	6509
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 4942

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 20:57:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1841 boxname=wulflinc32 idbench=205 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  40e47c460002545cc2670ca84fd53082  /oldhome/oroussel/tmp/wulflinc32/normalized-par32-2-c.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc32/normalized-par32-2-c.opb
IDLAUNCH: 1841
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        747052 kB
Buffers:         33940 kB
Cached:         142056 kB
SwapCached:       1212 kB
Active:         139644 kB
Inactive:       116768 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        746796 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25352 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:17:47 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 1841 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6509 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 |    6509    17852 |    2169       0        0     nan |  0.000 % |
c |       101 |    6509    17852 |    2385     101     2462    24.4 |  0.004 % |
c |       254 |    6509    17852 |    2624     254     6700    26.4 |  0.000 % |
c |       479 |    6509    17852 |    2886     479     9646    20.1 |  0.000 % |
c |       818 |    6509    17852 |    3175     818    18135    22.2 |  0.000 % |
c |      1324 |    6509    17852 |    3493    1324    25947    19.6 |  0.000 % |
c |      2083 |    6509    17852 |    3842    2083    49373    23.7 |  0.000 % |
c |      3223 |    6509    17852 |    4226    3223    66840    20.7 |  0.000 % |
c |      4935 |    6509    17852 |    4649    4935   113629    23.0 |  0.000 % |
c |      7497 |    6509    17852 |    5114    2609    59930    23.0 |  0.000 % |
c |     11341 |    6509    17852 |    5625    3849   103222    26.8 |  0.000 % |
c |     17107 |    6502    17836 |    6188    3798    98704    26.0 |  0.077 % |
c |     25756 |    6502    17836 |    6807    6122   147878    24.2 |  0.077 % |
c |     38730 |    6502    17836 |    7487    5300   120700    22.8 |  0.077 % |
c |     58191 |    6502    17836 |    8236    5807   133966    23.1 |  0.077 % |
c |     87384 |    6502    17836 |    9060    5797   134404    23.2 |  0.077 % |
c |    131173 |    6502    17836 |    9966    8389   195763    23.3 |  0.077 % |
c |    196859 |    6502    17836 |   10963    8687   237112    27.3 |  0.077 % |
c |    295385 |    6502    17836 |   12059    7459   201642    27.0 |  0.077 % |
c |    443174 |    6502    17836 |   13265    9518   210422    22.1 |  0.077 % |
c |    664857 |    6502    17836 |   14591   10972   229363    20.9 |  0.077 % |
#### 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.86 0.94 0.90 2/53 11304
Raw data (stat): 11304 (runsolver) R 11303 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479003355 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.88 0.94 0.90 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 766 0 0 0 996 1 0 0 25 0 1 0 479003355 4767744 744 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1164 744 603 41 0 1123 0
vsize: 4656
[startup+20.0032 s]
Raw data (loadavg): 0.90 0.94 0.90 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 826 0 0 0 1995 2 0 0 25 0 1 0 479003355 4898816 804 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1196 804 603 41 0 1155 0
vsize: 4784
[startup+30.005 s]
Raw data (loadavg): 0.91 0.94 0.90 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 849 0 0 0 2995 2 0 0 25 0 1 0 479003355 5038080 827 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1230 827 603 41 0 1189 0
vsize: 4920
[startup+40.0058 s]
Raw data (loadavg): 0.93 0.94 0.90 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 864 0 0 0 3995 3 0 0 25 0 1 0 479003355 5185536 842 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 842 603 41 0 1225 0
vsize: 5064
[startup+50.0075 s]
Raw data (loadavg): 0.94 0.95 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 890 0 0 0 4994 3 0 0 25 0 1 0 479003355 5185536 868 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 868 603 41 0 1225 0
vsize: 5064
[startup+60.0083 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 902 0 0 0 5994 3 0 0 25 0 1 0 479003355 5332992 880 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1302 880 603 41 0 1261 0
vsize: 5208
[startup+70.01 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 934 0 0 0 6994 4 0 0 25 0 1 0 479003355 5492736 912 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1341 912 603 41 0 1300 0
vsize: 5364
[startup+80.0118 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 941 0 0 0 7994 5 0 0 25 0 1 0 479003355 5492736 919 4294967295 134512640 134672761 3221224640 3221223776 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1341 919 603 41 0 1300 0
vsize: 5364
[startup+90.0126 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 941 0 0 0 8994 5 0 0 25 0 1 0 479003355 5492736 919 4294967295 134512640 134672761 3221224640 3221223832 134554697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1341 919 603 41 0 1300 0
vsize: 5364
[startup+100.013 s]
Raw data (loadavg): 1.05 0.97 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 977 0 0 0 9994 5 0 0 25 0 1 0 479003355 5623808 955 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1373 955 603 41 0 1332 0
vsize: 5492
[startup+110.014 s]
Raw data (loadavg): 1.04 0.97 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 984 0 0 0 10994 5 0 0 25 0 1 0 479003355 5623808 962 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1373 962 603 41 0 1332 0
vsize: 5492
[startup+120.015 s]
Raw data (loadavg): 1.04 0.97 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 984 0 0 0 11994 5 0 0 25 0 1 0 479003355 5623808 962 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1373 962 603 41 0 1332 0
vsize: 5492
[startup+130.015 s]
Raw data (loadavg): 1.03 0.97 0.91 2/53 11304
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 992 0 0 0 12995 5 0 0 25 0 1 0 479003355 5623808 970 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1373 970 603 41 0 1332 0
vsize: 5492
[startup+140.015 s]
Raw data (loadavg): 1.02 0.97 0.91 3/56 11340
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1000 0 0 0 13994 5 0 0 25 0 1 0 479003355 5763072 978 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1407 978 603 41 0 1366 0
vsize: 5628
[startup+150.016 s]
Raw data (loadavg): 1.02 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1057 0 0 0 14994 5 0 0 25 0 1 0 479003355 5898240 1035 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1440 1035 603 41 0 1399 0
vsize: 5760
[startup+160.017 s]
Raw data (loadavg): 1.02 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1071 0 0 0 15995 5 0 0 25 0 1 0 479003355 6033408 1049 4294967295 134512640 134672761 3221224640 3221223808 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1049 603 41 0 1432 0
vsize: 5892
[startup+170.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1075 0 0 0 16995 5 0 0 25 0 1 0 479003355 6033408 1053 4294967295 134512640 134672761 3221224640 3221223808 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1053 603 41 0 1432 0
vsize: 5892
[startup+180.018 s]
Raw data (loadavg): 1.01 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1075 0 0 0 17995 5 0 0 25 0 1 0 479003355 6033408 1053 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1053 603 41 0 1432 0
vsize: 5892
[startup+190.019 s]
Raw data (loadavg): 1.01 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1075 0 0 0 18995 5 0 0 25 0 1 0 479003355 6033408 1053 4294967295 134512640 134672761 3221224640 3221223824 134558435 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1053 603 41 0 1432 0
vsize: 5892
[startup+200.02 s]
Raw data (loadavg): 1.01 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1075 0 0 0 19996 5 0 0 25 0 1 0 479003355 6033408 1053 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1053 603 41 0 1432 0
vsize: 5892
[startup+210.02 s]
Raw data (loadavg): 1.01 0.97 0.91 2/53 11357
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1075 0 0 0 20996 5 0 0 25 0 1 0 479003355 6033408 1053 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1473 1053 603 41 0 1432 0
vsize: 5892
[startup+220.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1097 0 0 0 21996 5 0 0 25 0 1 0 479003355 6168576 1075 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1506 1075 603 41 0 1465 0
vsize: 6024
[startup+230.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1118 0 0 0 22995 5 0 0 25 0 1 0 479003355 6168576 1096 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1096 603 41 0 1465 0
vsize: 6024
[startup+240.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1118 0 0 0 23996 5 0 0 25 0 1 0 479003355 6168576 1096 4294967295 134512640 134672761 3221224640 3221223776 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1096 603 41 0 1465 0
vsize: 6024
[startup+250.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1123 0 0 0 24996 5 0 0 25 0 1 0 479003355 6168576 1101 4294967295 134512640 134672761 3221224640 3221223764 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1101 603 41 0 1465 0
vsize: 6024
[startup+260.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1127 0 0 0 25996 5 0 0 25 0 1 0 479003355 6168576 1105 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1506 1105 603 41 0 1465 0
vsize: 6024
[startup+270.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1131 0 0 0 26996 5 0 0 25 0 1 0 479003355 6303744 1109 4294967295 134512640 134672761 3221224640 3221223776 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1109 603 41 0 1498 0
vsize: 6156
[startup+280.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1142 0 0 0 27997 5 0 0 25 0 1 0 479003355 6303744 1120 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1120 603 41 0 1498 0
vsize: 6156
[startup+290.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1143 0 0 0 28997 5 0 0 25 0 1 0 479003355 6303744 1121 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1121 603 41 0 1498 0
vsize: 6156
[startup+300.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1150 0 0 0 29997 6 0 0 25 0 1 0 479003355 6303744 1128 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1128 603 41 0 1498 0
vsize: 6156
[startup+310.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1150 0 0 0 30997 6 0 0 25 0 1 0 479003355 6303744 1128 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1128 603 41 0 1498 0
vsize: 6156
[startup+320.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1150 0 0 0 31997 6 0 0 25 0 1 0 479003355 6303744 1128 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1128 603 41 0 1498 0
vsize: 6156
[startup+330.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1153 0 0 0 32998 6 0 0 25 0 1 0 479003355 6303744 1131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1131 603 41 0 1498 0
vsize: 6156
[startup+340.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1153 0 0 0 33998 6 0 0 25 0 1 0 479003355 6303744 1131 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1539 1131 603 41 0 1498 0
vsize: 6156
[startup+350.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1153 0 0 0 34997 6 0 0 25 0 1 0 479003355 6303744 1131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1539 1131 603 41 0 1498 0
vsize: 6156
[startup+360.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1180 0 0 0 35997 6 0 0 25 0 1 0 479003355 6438912 1158 4294967295 134512640 134672761 3221224640 3221223824 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1572 1158 603 41 0 1531 0
vsize: 6288
[startup+370.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1183 0 0 0 36998 6 0 0 25 0 1 0 479003355 6438912 1161 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1572 1161 603 41 0 1531 0
vsize: 6288
[startup+380.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1190 0 0 0 37998 6 0 0 25 0 1 0 479003355 6590464 1168 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1168 603 41 0 1568 0
vsize: 6436
[startup+390.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1196 0 0 0 38998 6 0 0 25 0 1 0 479003355 6590464 1174 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1174 603 41 0 1568 0
vsize: 6436
[startup+400.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1196 0 0 0 39998 6 0 0 25 0 1 0 479003355 6590464 1174 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1174 603 41 0 1568 0
vsize: 6436
[startup+410.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1196 0 0 0 40998 6 0 0 25 0 1 0 479003355 6590464 1174 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1174 603 41 0 1568 0
vsize: 6436
[startup+420.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1208 0 0 0 41999 6 0 0 25 0 1 0 479003355 6590464 1186 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1186 603 41 0 1568 0
vsize: 6436
[startup+430.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1213 0 0 0 42999 6 0 0 25 0 1 0 479003355 6590464 1191 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1609 1191 603 41 0 1568 0
vsize: 6436
[startup+440.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1224 0 0 0 43999 6 0 0 25 0 1 0 479003355 6754304 1202 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1202 603 41 0 1608 0
vsize: 6596
[startup+450.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1225 0 0 0 44999 6 0 0 25 0 1 0 479003355 6754304 1203 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1203 603 41 0 1608 0
vsize: 6596
[startup+460.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1226 0 0 0 46000 6 0 0 25 0 1 0 479003355 6754304 1204 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1204 603 41 0 1608 0
vsize: 6596
[startup+470.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1228 0 0 0 47000 6 0 0 25 0 1 0 479003355 6754304 1206 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1206 603 41 0 1608 0
vsize: 6596
[startup+480.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1228 0 0 0 48000 6 0 0 25 0 1 0 479003355 6754304 1206 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1206 603 41 0 1608 0
vsize: 6596
[startup+490.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1238 0 0 0 49000 6 0 0 25 0 1 0 479003355 6754304 1216 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1216 603 41 0 1608 0
vsize: 6596
[startup+500.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11359
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1238 0 0 0 50000 6 0 0 25 0 1 0 479003355 6754304 1216 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1216 603 41 0 1608 0
vsize: 6596
[startup+510.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1238 0 0 0 51001 6 0 0 25 0 1 0 479003355 6754304 1216 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1216 603 41 0 1608 0
vsize: 6596
[startup+520.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1238 0 0 0 52001 6 0 0 25 0 1 0 479003355 6754304 1216 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1649 1216 603 41 0 1608 0
vsize: 6596
[startup+530.043 s]
Raw data (loadavg): 1.08 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1245 0 0 0 53001 7 0 0 25 0 1 0 479003355 6754304 1223 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1649 1223 603 41 0 1608 0
vsize: 6596
[startup+540.044 s]
Raw data (loadavg): 1.07 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1251 0 0 0 54000 7 0 0 25 0 1 0 479003355 6914048 1229 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1229 603 41 0 1647 0
vsize: 6752
[startup+550.044 s]
Raw data (loadavg): 1.06 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1254 0 0 0 55000 7 0 0 25 0 1 0 479003355 6914048 1232 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1232 603 41 0 1647 0
vsize: 6752
[startup+560.044 s]
Raw data (loadavg): 1.05 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1258 0 0 0 56000 7 0 0 25 0 1 0 479003355 6914048 1236 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1236 603 41 0 1647 0
vsize: 6752
[startup+570.045 s]
Raw data (loadavg): 1.04 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1258 0 0 0 57001 7 0 0 25 0 1 0 479003355 6914048 1236 4294967295 134512640 134672761 3221224640 3221223848 1075346913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1236 603 41 0 1647 0
vsize: 6752
[startup+580.045 s]
Raw data (loadavg): 1.03 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1265 0 0 0 58001 7 0 0 25 0 1 0 479003355 6914048 1243 4294967295 134512640 134672761 3221224640 3221223744 134555133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1243 603 41 0 1647 0
vsize: 6752
[startup+590.045 s]
Raw data (loadavg): 1.03 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1266 0 0 0 59001 7 0 0 25 0 1 0 479003355 6914048 1244 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1244 603 41 0 1647 0
vsize: 6752
[startup+600.051 s]
Raw data (loadavg): 1.02 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1272 0 0 0 60002 7 0 0 25 0 1 0 479003355 6914048 1250 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1250 603 41 0 1647 0
vsize: 6752
[startup+610.052 s]
Raw data (loadavg): 1.02 0.99 0.92 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1272 0 0 0 61002 7 0 0 25 0 1 0 479003355 6914048 1250 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1250 603 41 0 1647 0
vsize: 6752
[startup+620.053 s]
Raw data (loadavg): 1.10 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1272 0 0 0 62002 7 0 0 25 0 1 0 479003355 6914048 1250 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1250 603 41 0 1647 0
vsize: 6752
[startup+630.053 s]
Raw data (loadavg): 1.08 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1278 0 0 0 63003 7 0 0 25 0 1 0 479003355 6914048 1256 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1688 1256 603 41 0 1647 0
vsize: 6752
[startup+640.054 s]
Raw data (loadavg): 1.07 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1285 0 0 0 64003 7 0 0 25 0 1 0 479003355 7077888 1263 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1263 603 41 0 1687 0
vsize: 6912
[startup+650.055 s]
Raw data (loadavg): 1.14 1.02 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1285 0 0 0 65003 7 0 0 25 0 1 0 479003355 7077888 1263 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1263 603 41 0 1687 0
vsize: 6912
[startup+660.056 s]
Raw data (loadavg): 1.11 1.02 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1292 0 0 0 66003 7 0 0 25 0 1 0 479003355 7077888 1270 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1270 603 41 0 1687 0
vsize: 6912
[startup+670.057 s]
Raw data (loadavg): 1.10 1.02 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1292 0 0 0 67004 7 0 0 25 0 1 0 479003355 7077888 1270 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1270 603 41 0 1687 0
vsize: 6912
[startup+680.058 s]
Raw data (loadavg): 1.08 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1292 0 0 0 68004 7 0 0 25 0 1 0 479003355 7077888 1270 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1270 603 41 0 1687 0
vsize: 6912
[startup+690.059 s]
Raw data (loadavg): 1.07 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1292 0 0 0 69004 7 0 0 25 0 1 0 479003355 7077888 1270 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1270 603 41 0 1687 0
vsize: 6912
[startup+700.059 s]
Raw data (loadavg): 1.06 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1292 0 0 0 70004 7 0 0 25 0 1 0 479003355 7077888 1270 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1270 603 41 0 1687 0
vsize: 6912
[startup+710.059 s]
Raw data (loadavg): 1.05 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1303 0 0 0 71005 7 0 0 25 0 1 0 479003355 7077888 1281 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1281 603 41 0 1687 0
vsize: 6912
[startup+720.06 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1309 0 0 0 72005 7 0 0 25 0 1 0 479003355 7077888 1287 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1728 1287 603 41 0 1687 0
vsize: 6912
[startup+730.061 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1315 0 0 0 73005 7 0 0 25 0 1 0 479003355 7241728 1293 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1293 603 41 0 1727 0
vsize: 7072
[startup+740.061 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1315 0 0 0 74005 7 0 0 25 0 1 0 479003355 7241728 1293 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1293 603 41 0 1727 0
vsize: 7072
[startup+750.062 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1315 0 0 0 75005 7 0 0 25 0 1 0 479003355 7241728 1293 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1293 603 41 0 1727 0
vsize: 7072
[startup+760.062 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1315 0 0 0 76006 7 0 0 25 0 1 0 479003355 7241728 1293 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1293 603 41 0 1727 0
vsize: 7072
[startup+770.063 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1315 0 0 0 77006 7 0 0 25 0 1 0 479003355 7241728 1293 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1293 603 41 0 1727 0
vsize: 7072
[startup+780.064 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1316 0 0 0 78006 7 0 0 25 0 1 0 479003355 7241728 1294 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1294 603 41 0 1727 0
vsize: 7072
[startup+790.064 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1318 0 0 0 79006 7 0 0 25 0 1 0 479003355 7241728 1296 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1296 603 41 0 1727 0
vsize: 7072
[startup+800.065 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1318 0 0 0 80007 7 0 0 25 0 1 0 479003355 7241728 1296 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1296 603 41 0 1727 0
vsize: 7072
[startup+810.066 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1322 0 0 0 81006 7 0 0 25 0 1 0 479003355 7241728 1300 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1300 603 41 0 1727 0
vsize: 7072
[startup+820.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1345 0 0 0 82007 7 0 0 25 0 1 0 479003355 7241728 1323 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1768 1323 603 41 0 1727 0
vsize: 7072
[startup+830.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1359 0 0 0 83007 7 0 0 25 0 1 0 479003355 7405568 1337 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1337 603 41 0 1767 0
vsize: 7232
[startup+840.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1369 0 0 0 84007 7 0 0 25 0 1 0 479003355 7405568 1347 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1347 603 41 0 1767 0
vsize: 7232
[startup+850.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1375 0 0 0 85007 7 0 0 25 0 1 0 479003355 7405568 1353 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1353 603 41 0 1767 0
vsize: 7232
[startup+860.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1382 0 0 0 86008 7 0 0 25 0 1 0 479003355 7405568 1360 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1360 603 41 0 1767 0
vsize: 7232
[startup+870.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1395 0 0 0 87008 7 0 0 25 0 1 0 479003355 7565312 1373 4294967295 134512640 134672761 3221224640 3221223824 134559665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1373 603 41 0 1806 0
vsize: 7388
[startup+880.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1401 0 0 0 88008 7 0 0 25 0 1 0 479003355 7565312 1379 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1379 603 41 0 1806 0
vsize: 7388
[startup+890.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1404 0 0 0 89008 7 0 0 25 0 1 0 479003355 7565312 1382 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1382 603 41 0 1806 0
vsize: 7388
[startup+900.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 90009 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+910.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 91009 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+920.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 92009 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+930.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 93009 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+940.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 94010 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+950.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 95010 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223744 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+960.076 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1416 0 0 0 96010 7 0 0 25 0 1 0 479003355 7565312 1394 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1847 1394 603 41 0 1806 0
vsize: 7388
[startup+970.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1424 0 0 0 97010 7 0 0 25 0 1 0 479003355 7729152 1402 4294967295 134512640 134672761 3221224640 3221223776 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1402 603 41 0 1846 0
vsize: 7548
[startup+980.078 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1427 0 0 0 98011 7 0 0 25 0 1 0 479003355 7729152 1405 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1405 603 41 0 1846 0
vsize: 7548
[startup+990.079 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1427 0 0 0 99011 7 0 0 25 0 1 0 479003355 7729152 1405 4294967295 134512640 134672761 3221224640 3221223696 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1405 603 41 0 1846 0
vsize: 7548
[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 100011 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223776 134565066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 101011 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 102012 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 103012 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 104012 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1428 0 0 0 105012 7 0 0 25 0 1 0 479003355 7729152 1406 4294967295 134512640 134672761 3221224640 3221223824 134558497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1406 603 41 0 1846 0
vsize: 7548
[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1430 0 0 0 106012 7 0 0 25 0 1 0 479003355 7729152 1408 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1408 603 41 0 1846 0
vsize: 7548
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1430 0 0 0 107013 7 0 0 25 0 1 0 479003355 7729152 1408 4294967295 134512640 134672761 3221224640 3221223744 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1408 603 41 0 1846 0
vsize: 7548
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1440 0 0 0 108013 7 0 0 25 0 1 0 479003355 7729152 1418 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1418 603 41 0 1846 0
vsize: 7548
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1440 0 0 0 109013 7 0 0 25 0 1 0 479003355 7729152 1418 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1418 603 41 0 1846 0
vsize: 7548
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1441 0 0 0 110013 7 0 0 25 0 1 0 479003355 7729152 1419 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1419 603 41 0 1846 0
vsize: 7548
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1442 0 0 0 111014 7 0 0 25 0 1 0 479003355 7729152 1420 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1420 603 41 0 1846 0
vsize: 7548
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 112014 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 113014 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 114014 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 115015 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 116015 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 117015 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 118015 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 119016 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 11361
Raw data (stat): 11304 (minisat+) R 11303 7987 7986 0 -1 0 1448 0 0 0 120016 7 0 0 25 0 1 0 479003355 7729152 1426 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1887 1426 603 41 0 1846 0
vsize: 7548
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 11361
Raw data (stat): 11304 (minisat+) Z 11303 7987 7986 0 -1 12 1450 0 0 0 120016 7 0 0 25 0 1 0 479003355 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.1
CPU time (s): 1200.24
CPU user time (s): 1200.16
CPU system time (s): 0.079987
CPU usage (%): 100.012
Max. virtual memory (Kb): 7548
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####