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 5954

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 02:22:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4347 boxname=wulflinc11 idbench=211 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b2d6fc6e4e4b51f8b59d0f4ed12a9f74  /oldhome/oroussel/tmp/wulflinc11/normalized-par32-5-c.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc11/normalized-par32-5-c.opb /oldhome/oroussel/tmp/wulflinc11/normalized-par32-5-c.opb
IDLAUNCH: 4347
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        908796 kB
Buffers:         36128 kB
Cached:          65224 kB
SwapCached:       4932 kB
Active:          57236 kB
Inactive:        51932 kB
HighTotal:      131008 kB
HighFree:        61964 kB
LowTotal:       903652 kB
LowFree:        846832 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11148 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:42:39 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4347 7 1200.2 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.98 0.92 2/54 6514
Raw data (stat): 6514 (runsolver) R 6513 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422733895 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 792 0 0 0 996 2 0 0 25 0 1 0 422733895 4751360 770 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1160 770 603 41 0 1119 0
vsize: 4640
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 826 0 0 0 1995 2 0 0 25 0 1 0 422733895 5017600 804 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1225 804 603 41 0 1184 0
vsize: 4900
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 863 0 0 0 2995 2 0 0 25 0 1 0 422733895 5156864 841 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1259 841 603 41 0 1218 0
vsize: 5036
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 883 0 0 0 3993 3 0 0 25 0 1 0 422733895 5156864 861 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1259 861 603 41 0 1218 0
vsize: 5036
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 909 0 0 0 4993 3 0 0 25 0 1 0 422733895 5287936 887 4294967295 134512640 134672761 3221224560 3221223728 134560813 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.0023 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 915 0 0 0 5993 3 0 0 25 0 1 0 422733895 5287936 893 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1291 893 603 41 0 1250 0
vsize: 5164
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 978 0 0 0 6993 3 0 0 25 0 1 0 422733895 5558272 956 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1357 956 603 41 0 1316 0
vsize: 5428
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 988 0 0 0 7994 3 0 0 25 0 1 0 422733895 5705728 966 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1393 966 603 41 0 1352 0
vsize: 5572
[startup+90.0039 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1020 0 0 0 8993 4 0 0 25 0 1 0 422733895 5836800 998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 998 603 41 0 1384 0
vsize: 5700
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1028 0 0 0 9993 4 0 0 25 0 1 0 422733895 5836800 1006 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1006 603 41 0 1384 0
vsize: 5700
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1033 0 0 0 10994 4 0 0 25 0 1 0 422733895 5836800 1011 4294967295 134512640 134672761 3221224560 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1011 603 41 0 1384 0
vsize: 5700
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1034 0 0 0 11994 4 0 0 25 0 1 0 422733895 5836800 1012 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1034 0 0 0 12994 4 0 0 25 0 1 0 422733895 5836800 1012 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1041 0 0 0 13994 4 0 0 25 0 1 0 422733895 5836800 1019 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1042 0 0 0 14994 4 0 0 25 0 1 0 422733895 5836800 1020 4294967295 134512640 134672761 3221224560 3221223728 134560864 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1046 0 0 0 15994 4 0 0 25 0 1 0 422733895 5836800 1024 4294967295 134512640 134672761 3221224560 3221223728 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.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1074 0 0 0 16994 4 0 0 25 0 1 0 422733895 5971968 1052 4294967295 134512640 134672761 3221224560 3221223664 134560367 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1074 0 0 0 17994 4 0 0 25 0 1 0 422733895 5971968 1052 4294967295 134512640 134672761 3221224560 3221223664 134560070 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1079 0 0 0 18995 4 0 0 25 0 1 0 422733895 6127616 1057 4294967295 134512640 134672761 3221224560 3221223728 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1079 0 0 0 19995 4 0 0 25 0 1 0 422733895 6127616 1057 4294967295 134512640 134672761 3221224560 3221223728 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.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1086 0 0 0 20995 4 0 0 25 0 1 0 422733895 6127616 1064 4294967295 134512640 134672761 3221224560 3221223760 134557800 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1098 0 0 0 21995 4 0 0 25 0 1 0 422733895 6127616 1076 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1109 0 0 0 22995 4 0 0 25 0 1 0 422733895 6262784 1087 4294967295 134512640 134672761 3221224560 3221223728 134561375 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1109 0 0 0 23995 4 0 0 25 0 1 0 422733895 6262784 1087 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 24996 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 25996 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223700 134560556 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.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 26996 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223696 134560683 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 27996 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223664 134554647 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 28996 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1114 0 0 0 29997 4 0 0 25 0 1 0 422733895 6262784 1092 4294967295 134512640 134672761 3221224560 3221223664 134560402 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.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1116 0 0 0 30997 4 0 0 25 0 1 0 422733895 6262784 1094 4294967295 134512640 134672761 3221224560 3221223728 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+320.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1116 0 0 0 31997 4 0 0 25 0 1 0 422733895 6262784 1094 4294967295 134512640 134672761 3221224560 3221223728 134561198 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1136 0 0 0 32997 4 0 0 25 0 1 0 422733895 6262784 1114 4294967295 134512640 134672761 3221224560 3221223728 134561021 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1160 0 0 0 33998 4 0 0 25 0 1 0 422733895 6397952 1138 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1178 0 0 0 34998 4 0 0 25 0 1 0 422733895 6533120 1156 4294967295 134512640 134672761 3221224560 3221223696 134565092 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.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1198 0 0 0 35998 4 0 0 25 0 1 0 422733895 6533120 1176 4294967295 134512640 134672761 3221224560 3221223728 134560942 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.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1204 0 0 0 36998 4 0 0 25 0 1 0 422733895 6668288 1182 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1205 0 0 0 37998 4 0 0 25 0 1 0 422733895 6668288 1183 4294967295 134512640 134672761 3221224560 3221223652 1075351157 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1205 0 0 0 38999 4 0 0 25 0 1 0 422733895 6668288 1183 4294967295 134512640 134672761 3221224560 3221223744 134558662 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.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1205 0 0 0 39999 4 0 0 25 0 1 0 422733895 6668288 1183 4294967295 134512640 134672761 3221224560 3221223708 134560552 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1205 0 0 0 40999 4 0 0 25 0 1 0 422733895 6668288 1183 4294967295 134512640 134672761 3221224560 3221223696 134560673 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 41999 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223656 1075347236 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 42999 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 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+440.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 44000 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560956 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 45000 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 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+460.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 46000 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134561151 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.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1211 0 0 0 47000 4 0 0 25 0 1 0 422733895 6668288 1189 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+480.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1216 0 0 0 48000 4 0 0 25 0 1 0 422733895 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134561151 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1216 0 0 0 49000 4 0 0 25 0 1 0 422733895 6668288 1194 4294967295 134512640 134672761 3221224560 3221223664 134560418 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1216 0 0 0 50001 4 0 0 25 0 1 0 422733895 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1216 0 0 0 51001 4 0 0 25 0 1 0 422733895 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1222 0 0 0 52001 4 0 0 25 0 1 0 422733895 6668288 1200 4294967295 134512640 134672761 3221224560 3221223696 134560706 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1247 0 0 0 53001 4 0 0 25 0 1 0 422733895 6799360 1225 4294967295 134512640 134672761 3221224560 3221223568 1075349729 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1248 0 0 0 54001 4 0 0 25 0 1 0 422733895 6799360 1226 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1252 0 0 0 55001 4 0 0 25 0 1 0 422733895 6799360 1230 4294967295 134512640 134672761 3221224560 3221223744 134559489 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1258 0 0 0 56001 5 0 0 25 0 1 0 422733895 6799360 1236 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1258 0 0 0 57001 5 0 0 25 0 1 0 422733895 6799360 1236 4294967295 134512640 134672761 3221224560 3221223744 134559356 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1260 0 0 0 58001 5 0 0 25 0 1 0 422733895 6799360 1238 4294967295 134512640 134672761 3221224560 3221223744 134558702 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1265 0 0 0 59001 5 0 0 25 0 1 0 422733895 6934528 1243 4294967295 134512640 134672761 3221224560 3221223728 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1265 0 0 0 60002 5 0 0 25 0 1 0 422733895 6934528 1243 4294967295 134512640 134672761 3221224560 3221223728 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+610.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1270 0 0 0 61002 5 0 0 25 0 1 0 422733895 6934528 1248 4294967295 134512640 134672761 3221224560 3221223728 134561151 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1275 0 0 0 62002 5 0 0 25 0 1 0 422733895 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560895 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1275 0 0 0 63002 5 0 0 25 0 1 0 422733895 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 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+640.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1275 0 0 0 64002 5 0 0 25 0 1 0 422733895 6934528 1253 4294967295 134512640 134672761 3221224560 3221223664 134554642 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1281 0 0 0 65003 5 0 0 25 0 1 0 422733895 6934528 1259 4294967295 134512640 134672761 3221224560 3221223760 134557876 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1281 0 0 0 66003 5 0 0 25 0 1 0 422733895 6934528 1259 4294967295 134512640 134672761 3221224560 3221223728 134560920 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1281 0 0 0 67003 5 0 0 25 0 1 0 422733895 6934528 1259 4294967295 134512640 134672761 3221224560 3221223728 134560903 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1286 0 0 0 68003 5 0 0 25 0 1 0 422733895 6934528 1264 4294967295 134512640 134672761 3221224560 3221223728 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1286 0 0 0 69003 5 0 0 25 0 1 0 422733895 6934528 1264 4294967295 134512640 134672761 3221224560 3221223728 134560858 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.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1292 0 0 0 70003 5 0 0 25 0 1 0 422733895 7098368 1270 4294967295 134512640 134672761 3221224560 3221223744 134559190 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1298 0 0 0 71004 5 0 0 25 0 1 0 422733895 7098368 1276 4294967295 134512640 134672761 3221224560 3221223744 134559625 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1304 0 0 0 72004 5 0 0 25 0 1 0 422733895 7098368 1282 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1304 0 0 0 73004 5 0 0 25 0 1 0 422733895 7098368 1282 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1306 0 0 0 74004 5 0 0 25 0 1 0 422733895 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134561001 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1306 0 0 0 75004 5 0 0 25 0 1 0 422733895 7098368 1284 4294967295 134512640 134672761 3221224560 3221223696 134565137 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1306 0 0 0 76005 5 0 0 25 0 1 0 422733895 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1306 0 0 0 77005 5 0 0 25 0 1 0 422733895 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 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+780.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1307 0 0 0 78005 5 0 0 25 0 1 0 422733895 7098368 1285 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1308 0 0 0 79005 5 0 0 25 0 1 0 422733895 7098368 1286 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1308 0 0 0 80005 5 0 0 25 0 1 0 422733895 7098368 1286 4294967295 134512640 134672761 3221224560 3221223696 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1286 603 41 0 1692 0
vsize: 6932
[startup+810.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1310 0 0 0 81005 5 0 0 25 0 1 0 422733895 7098368 1288 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1357 0 0 0 82005 5 0 0 25 0 1 0 422733895 7368704 1335 4294967295 134512640 134672761 3221224560 3221223728 134560876 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 83005 5 0 0 25 0 1 0 422733895 7368704 1339 4294967295 134512640 134672761 3221224560 3221223728 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+840.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 84005 5 0 0 25 0 1 0 422733895 7368704 1339 4294967295 134512640 134672761 3221224560 3221223744 134558324 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 85005 5 0 0 25 0 1 0 422733895 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134560876 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 86005 5 0 0 25 0 1 0 422733895 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 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+870.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 87006 5 0 0 25 0 1 0 422733895 7364608 1339 4294967295 134512640 134672761 3221224560 3221223744 134559581 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1361 0 0 0 88006 5 0 0 25 0 1 0 422733895 7364608 1339 4294967295 134512640 134672761 3221224560 3221223664 134554642 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1362 0 0 0 89006 5 0 0 25 0 1 0 422733895 7364608 1340 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1362 0 0 0 90006 5 0 0 25 0 1 0 422733895 7364608 1340 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1377 0 0 0 91006 5 0 0 25 0 1 0 422733895 7364608 1355 4294967295 134512640 134672761 3221224560 3221223716 134561241 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1377 0 0 0 92007 5 0 0 25 0 1 0 422733895 7364608 1355 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1377 0 0 0 93007 5 0 0 25 0 1 0 422733895 7364608 1355 4294967295 134512640 134672761 3221224560 3221223696 134560596 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1377 0 0 0 94007 5 0 0 25 0 1 0 422733895 7364608 1355 4294967295 134512640 134672761 3221224560 3221223760 134557836 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.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1379 0 0 0 95007 5 0 0 25 0 1 0 422733895 7364608 1357 4294967295 134512640 134672761 3221224560 3221223728 134560956 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.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1380 0 0 0 96008 5 0 0 25 0 1 0 422733895 7364608 1358 4294967295 134512640 134672761 3221224560 3221223712 134565070 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.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1380 0 0 0 97010 5 0 0 25 0 1 0 422733895 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1380 0 0 0 98010 5 0 0 25 0 1 0 422733895 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1380 0 0 0 99010 5 0 0 25 0 1 0 422733895 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1380 0 0 0 100010 5 0 0 25 0 1 0 422733895 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 101010 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223744 134558687 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 102011 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223716 134565154 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 103011 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223696 134560588 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 104011 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223664 134554642 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 105011 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223744 134558648 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 106011 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223744 134559340 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.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1382 0 0 0 107012 5 0 0 25 0 1 0 422733895 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560892 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1383 0 0 0 108012 5 0 0 25 0 1 0 422733895 7364608 1361 4294967295 134512640 134672761 3221224560 3221223704 134560553 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1383 0 0 0 109012 5 0 0 25 0 1 0 422733895 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134561151 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1383 0 0 0 110012 5 0 0 25 0 1 0 422733895 7364608 1361 4294967295 134512640 134672761 3221224560 3221223716 134561241 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1383 0 0 0 111013 5 0 0 25 0 1 0 422733895 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134560892 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1385 0 0 0 112013 5 0 0 25 0 1 0 422733895 7364608 1363 4294967295 134512640 134672761 3221224560 3221223744 134559041 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1386 0 0 0 113013 5 0 0 25 0 1 0 422733895 7364608 1364 4294967295 134512640 134672761 3221224560 3221223744 134558632 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1386 0 0 0 114013 5 0 0 25 0 1 0 422733895 7364608 1364 4294967295 134512640 134672761 3221224560 3221223728 134560830 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1386 0 0 0 115013 5 0 0 25 0 1 0 422733895 7364608 1364 4294967295 134512640 134672761 3221224560 3221223728 134560836 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1387 0 0 0 116013 5 0 0 25 0 1 0 422733895 7364608 1365 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1387 0 0 0 117014 5 0 0 25 0 1 0 422733895 7364608 1365 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1387 0 0 0 118014 5 0 0 25 0 1 0 422733895 7364608 1365 4294967295 134512640 134672761 3221224560 3221223696 134560709 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1391 0 0 0 119014 5 0 0 25 0 1 0 422733895 7364608 1369 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 6514
Raw data (stat): 6514 (minisat+) R 6513 32461 32460 0 -1 0 1391 0 0 0 120014 5 0 0 25 0 1 0 422733895 7364608 1369 4294967295 134512640 134672761 3221224560 3221223664 134559835 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.05 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 6514
Raw data (stat): 6514 (minisat+) Z 6513 32461 32460 0 -1 12 1393 0 0 0 120014 5 0 0 25 0 1 0 422733895 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.05
CPU time (s): 1200.2
CPU user time (s): 1200.15
CPU system time (s): 0.057991
CPU usage (%): 100.013
Max. virtual memory (Kb): 7196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####