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 5154

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        910720 kB
Buffers:         35244 kB
Cached:          65996 kB
SwapCached:       3276 kB
Active:          68116 kB
Inactive:        39268 kB
HighTotal:      131008 kB
HighFree:        61096 kB
LowTotal:       903652 kB
LowFree:        849624 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11068 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:35:50 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 3595 7 1200.16 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.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (runsolver) R 16578 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421251170 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 792 0 0 0 995 2 0 0 25 0 1 0 421251170 4751360 770 4294967295 134512640 134672761 3221224560 3221223760 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1160 770 603 41 0 1119 0
vsize: 4640
[startup+20.0023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 826 0 0 0 1995 2 0 0 25 0 1 0 421251170 5017600 804 4294967295 134512640 134672761 3221224560 3221223696 134565092 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.0039 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 863 0 0 0 2994 2 0 0 25 0 1 0 421251170 5156864 841 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.0034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 890 0 0 0 3994 2 0 0 25 0 1 0 421251170 5156864 868 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1259 868 603 41 0 1218 0
vsize: 5036
[startup+50.0035 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 909 0 0 0 4994 3 0 0 25 0 1 0 421251170 5287936 887 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1291 887 603 41 0 1250 0
vsize: 5164
[startup+60.0043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 915 0 0 0 5994 3 0 0 25 0 1 0 421251170 5287936 893 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1291 893 603 41 0 1250 0
vsize: 5164
[startup+70.0049 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 978 0 0 0 6994 3 0 0 25 0 1 0 421251170 5558272 956 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1357 956 603 41 0 1316 0
vsize: 5428
[startup+80.0061 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 988 0 0 0 7994 3 0 0 25 0 1 0 421251170 5705728 966 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1393 966 603 41 0 1352 0
vsize: 5572
[startup+90.0059 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1020 0 0 0 8994 3 0 0 25 0 1 0 421251170 5836800 998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 998 603 41 0 1384 0
vsize: 5700
[startup+100.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1028 0 0 0 9994 3 0 0 25 0 1 0 421251170 5836800 1006 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1006 603 41 0 1384 0
vsize: 5700
[startup+110.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1033 0 0 0 10994 3 0 0 25 0 1 0 421251170 5836800 1011 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1011 603 41 0 1384 0
vsize: 5700
[startup+120.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1034 0 0 0 11995 3 0 0 25 0 1 0 421251170 5836800 1012 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+130.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1034 0 0 0 12995 3 0 0 25 0 1 0 421251170 5836800 1012 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1012 603 41 0 1384 0
vsize: 5700
[startup+140.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1041 0 0 0 13995 3 0 0 25 0 1 0 421251170 5836800 1019 4294967295 134512640 134672761 3221224560 3221223628 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1019 603 41 0 1384 0
vsize: 5700
[startup+150.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1042 0 0 0 14995 3 0 0 25 0 1 0 421251170 5836800 1020 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1020 603 41 0 1384 0
vsize: 5700
[startup+160.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1046 0 0 0 15995 3 0 0 25 0 1 0 421251170 5836800 1024 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1024 603 41 0 1384 0
vsize: 5700
[startup+170.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1074 0 0 0 16995 3 0 0 25 0 1 0 421251170 5971968 1052 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1458 1052 603 41 0 1417 0
vsize: 5832
[startup+180.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1074 0 0 0 17995 3 0 0 25 0 1 0 421251170 5971968 1052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1458 1052 603 41 0 1417 0
vsize: 5832
[startup+190.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1079 0 0 0 18996 3 0 0 25 0 1 0 421251170 6127616 1057 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1057 603 41 0 1455 0
vsize: 5984
[startup+200.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1079 0 0 0 19996 3 0 0 25 0 1 0 421251170 6127616 1057 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1057 603 41 0 1455 0
vsize: 5984
[startup+210.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1086 0 0 0 20996 3 0 0 25 0 1 0 421251170 6127616 1064 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1064 603 41 0 1455 0
vsize: 5984
[startup+220.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1098 0 0 0 21996 3 0 0 25 0 1 0 421251170 6127616 1076 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1076 603 41 0 1455 0
vsize: 5984
[startup+230.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1109 0 0 0 22997 3 0 0 25 0 1 0 421251170 6262784 1087 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1087 603 41 0 1488 0
vsize: 6116
[startup+240.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1109 0 0 0 23997 3 0 0 25 0 1 0 421251170 6262784 1087 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1087 603 41 0 1488 0
vsize: 6116
[startup+250.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 24997 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223744 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+260.014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 25997 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+270.014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 26997 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+280.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 27998 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+290.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 28998 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+300.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1114 0 0 0 29998 3 0 0 25 0 1 0 421251170 6262784 1092 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+310.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1116 0 0 0 30998 3 0 0 25 0 1 0 421251170 6262784 1094 4294967295 134512640 134672761 3221224560 3221223632 134553546 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1094 603 41 0 1488 0
vsize: 6116
[startup+320.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1116 0 0 0 31998 3 0 0 25 0 1 0 421251170 6262784 1094 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1094 603 41 0 1488 0
vsize: 6116
[startup+330.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1136 0 0 0 32998 4 0 0 25 0 1 0 421251170 6262784 1114 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1114 603 41 0 1488 0
vsize: 6116
[startup+340.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1160 0 0 0 33998 4 0 0 25 0 1 0 421251170 6397952 1138 4294967295 134512640 134672761 3221224560 3221223616 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1562 1138 603 41 0 1521 0
vsize: 6248
[startup+350.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1178 0 0 0 34998 4 0 0 25 0 1 0 421251170 6533120 1156 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1595 1156 603 41 0 1554 0
vsize: 6380
[startup+360.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1198 0 0 0 35999 4 0 0 25 0 1 0 421251170 6533120 1176 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1595 1176 603 41 0 1554 0
vsize: 6380
[startup+370.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1204 0 0 0 36999 4 0 0 25 0 1 0 421251170 6668288 1182 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1182 603 41 0 1587 0
vsize: 6512
[startup+380.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1205 0 0 0 37999 4 0 0 25 0 1 0 421251170 6668288 1183 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+390.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1205 0 0 0 38999 4 0 0 25 0 1 0 421251170 6668288 1183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+400.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1205 0 0 0 39999 4 0 0 25 0 1 0 421251170 6668288 1183 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+410.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1205 0 0 0 40999 4 0 0 25 0 1 0 421251170 6668288 1183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1183 603 41 0 1587 0
vsize: 6512
[startup+420.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 42000 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+430.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 43000 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+440.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 44000 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+450.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 45000 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+460.02 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 46000 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+470.02 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1211 0 0 0 47001 4 0 0 25 0 1 0 421251170 6668288 1189 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1189 603 41 0 1587 0
vsize: 6512
[startup+480.021 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1216 0 0 0 48001 4 0 0 25 0 1 0 421251170 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+490.02 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1216 0 0 0 49001 4 0 0 25 0 1 0 421251170 6668288 1194 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+500.02 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1216 0 0 0 50001 4 0 0 25 0 1 0 421251170 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+510.021 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1216 0 0 0 51001 4 0 0 25 0 1 0 421251170 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1194 603 41 0 1587 0
vsize: 6512
[startup+520.021 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1222 0 0 0 52001 4 0 0 25 0 1 0 421251170 6668288 1200 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1628 1200 603 41 0 1587 0
vsize: 6512
[startup+530.021 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1247 0 0 0 53001 4 0 0 25 0 1 0 421251170 6799360 1225 4294967295 134512640 134672761 3221224560 3221223744 134558651 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.023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1247 0 0 0 53999 4 0 0 25 0 1 0 421251170 6799360 1225 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1660 1225 603 41 0 1619 0
vsize: 6640
[startup+550.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1252 0 0 0 54999 4 0 0 25 0 1 0 421251170 6799360 1230 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1230 603 41 0 1619 0
vsize: 6640
[startup+560.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1258 0 0 0 55999 4 0 0 25 0 1 0 421251170 6799360 1236 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1236 603 41 0 1619 0
vsize: 6640
[startup+570.023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1258 0 0 0 56999 4 0 0 25 0 1 0 421251170 6799360 1236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1236 603 41 0 1619 0
vsize: 6640
[startup+580.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1260 0 0 0 57999 4 0 0 25 0 1 0 421251170 6799360 1238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1238 603 41 0 1619 0
vsize: 6640
[startup+590.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1265 0 0 0 59000 4 0 0 25 0 1 0 421251170 6934528 1243 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1243 603 41 0 1652 0
vsize: 6772
[startup+600.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1265 0 0 0 60000 4 0 0 25 0 1 0 421251170 6934528 1243 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1243 603 41 0 1652 0
vsize: 6772
[startup+610.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1270 0 0 0 61000 4 0 0 25 0 1 0 421251170 6934528 1248 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1248 603 41 0 1652 0
vsize: 6772
[startup+620.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1275 0 0 0 62000 4 0 0 25 0 1 0 421251170 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+630.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1275 0 0 0 63000 4 0 0 25 0 1 0 421251170 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134564732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+640.026 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1275 0 0 0 64001 4 0 0 25 0 1 0 421251170 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+650.026 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1281 0 0 0 65001 4 0 0 25 0 1 0 421251170 6934528 1259 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+660.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1281 0 0 0 66001 4 0 0 25 0 1 0 421251170 6934528 1259 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+670.026 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1281 0 0 0 67001 4 0 0 25 0 1 0 421251170 6934528 1259 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+680.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1286 0 0 0 68001 4 0 0 25 0 1 0 421251170 6934528 1264 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1264 603 41 0 1652 0
vsize: 6772
[startup+690.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1286 0 0 0 69002 4 0 0 25 0 1 0 421251170 6934528 1264 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1264 603 41 0 1652 0
vsize: 6772
[startup+700.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1292 0 0 0 70002 4 0 0 25 0 1 0 421251170 7098368 1270 4294967295 134512640 134672761 3221224560 3221223744 134558557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1270 603 41 0 1692 0
vsize: 6932
[startup+710.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1298 0 0 0 71002 4 0 0 25 0 1 0 421251170 7098368 1276 4294967295 134512640 134672761 3221224560 3221223744 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1276 603 41 0 1692 0
vsize: 6932
[startup+720.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1304 0 0 0 72002 4 0 0 25 0 1 0 421251170 7098368 1282 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1282 603 41 0 1692 0
vsize: 6932
[startup+730.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1304 0 0 0 73002 4 0 0 25 0 1 0 421251170 7098368 1282 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1282 603 41 0 1692 0
vsize: 6932
[startup+740.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1306 0 0 0 74003 4 0 0 25 0 1 0 421251170 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+750.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1306 0 0 0 75003 4 0 0 25 0 1 0 421251170 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+760.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1306 0 0 0 76003 4 0 0 25 0 1 0 421251170 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+770.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1306 0 0 0 77003 4 0 0 25 0 1 0 421251170 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+780.032 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1307 0 0 0 78003 4 0 0 25 0 1 0 421251170 7098368 1285 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1285 603 41 0 1692 0
vsize: 6932
[startup+790.031 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1308 0 0 0 79004 4 0 0 25 0 1 0 421251170 7098368 1286 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1286 603 41 0 1692 0
vsize: 6932
[startup+800.031 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1308 0 0 0 80004 4 0 0 25 0 1 0 421251170 7098368 1286 4294967295 134512640 134672761 3221224560 3221223728 134560903 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.032 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1310 0 0 0 81002 5 0 0 25 0 1 0 421251170 7098368 1288 4294967295 134512640 134672761 3221224560 3221223696 134565086 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.033 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1357 0 0 0 82002 5 0 0 25 0 1 0 421251170 7368704 1335 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1335 603 41 0 1758 0
vsize: 7196
[startup+830.034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1360 0 0 0 83002 5 0 0 25 0 1 0 421251170 7368704 1338 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1338 603 41 0 1758 0
vsize: 7196
[startup+840.035 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1361 0 0 0 84002 5 0 0 25 0 1 0 421251170 7368704 1339 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1339 603 41 0 1758 0
vsize: 7196
[startup+850.034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1361 0 0 0 85002 5 0 0 25 0 1 0 421251170 7364608 1339 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+860.034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1361 0 0 0 86002 5 0 0 25 0 1 0 421251170 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+870.034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1361 0 0 0 87002 5 0 0 25 0 1 0 421251170 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+880.035 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1361 0 0 0 88003 5 0 0 25 0 1 0 421251170 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+890.036 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1362 0 0 0 89003 5 0 0 25 0 1 0 421251170 7364608 1340 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1340 603 41 0 1757 0
vsize: 7192
[startup+900.036 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1362 0 0 0 90003 5 0 0 25 0 1 0 421251170 7364608 1340 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1340 603 41 0 1757 0
vsize: 7192
[startup+910.036 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1362 0 0 0 91003 5 0 0 25 0 1 0 421251170 7364608 1340 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1340 603 41 0 1757 0
vsize: 7192
[startup+920.036 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1377 0 0 0 92003 5 0 0 25 0 1 0 421251170 7364608 1355 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+930.037 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1377 0 0 0 93004 5 0 0 25 0 1 0 421251170 7364608 1355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+940.038 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1377 0 0 0 94004 5 0 0 25 0 1 0 421251170 7364608 1355 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+950.038 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1379 0 0 0 95004 5 0 0 25 0 1 0 421251170 7364608 1357 4294967295 134512640 134672761 3221224560 3221223728 134561309 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1357 603 41 0 1757 0
vsize: 7192
[startup+960.039 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1380 0 0 0 96004 5 0 0 25 0 1 0 421251170 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+970.038 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1380 0 0 0 97004 5 0 0 25 0 1 0 421251170 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+980.039 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1380 0 0 0 98005 5 0 0 25 0 1 0 421251170 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+990.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1380 0 0 0 99005 5 0 0 25 0 1 0 421251170 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+1000.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1380 0 0 0 100005 5 0 0 25 0 1 0 421251170 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+1010.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 101005 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1020.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 102005 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1030.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 103006 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1040.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 104006 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1050.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 105006 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1060.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 106006 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1070.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 107006 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1080.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1382 0 0 0 108007 5 0 0 25 0 1 0 421251170 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1090.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1383 0 0 0 109007 5 0 0 25 0 1 0 421251170 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1100.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1383 0 0 0 110007 5 0 0 25 0 1 0 421251170 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1110.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1383 0 0 0 111007 5 0 0 25 0 1 0 421251170 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1361 603 41 0 1757 0
vsize: 7192
[startup+1120.04 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1385 0 0 0 112007 5 0 0 25 0 1 0 421251170 7364608 1363 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1363 603 41 0 1757 0
vsize: 7192
[startup+1130.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1386 0 0 0 113008 5 0 0 25 0 1 0 421251170 7364608 1364 4294967295 134512640 134672761 3221224560 3221223556 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1140.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1386 0 0 0 114008 5 0 0 25 0 1 0 421251170 7364608 1364 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1150.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1386 0 0 0 115008 5 0 0 25 0 1 0 421251170 7364608 1364 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1160.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1387 0 0 0 116008 5 0 0 25 0 1 0 421251170 7364608 1365 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1170.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1387 0 0 0 117008 5 0 0 25 0 1 0 421251170 7364608 1365 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1180.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1387 0 0 0 118009 5 0 0 25 0 1 0 421251170 7364608 1365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1190.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1387 0 0 0 119009 5 0 0 25 0 1 0 421251170 7364608 1365 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1365 603 41 0 1757 0
vsize: 7192
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16579
Raw data (stat): 16579 (minisat+) R 16578 10720 10719 0 -1 0 1391 0 0 0 120009 5 0 0 25 0 1 0 421251170 7364608 1369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 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 1.00 0.92 1/54 16579
Raw data (stat): 16579 (minisat+) Z 16578 10720 10719 0 -1 12 1393 0 0 0 120009 5 0 0 25 0 1 0 421251170 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.05
CPU time (s): 1200.16
CPU user time (s): 1200.1
CPU system time (s): 0.05999
CPU usage (%): 100.009
Max. virtual memory (Kb): 7196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####