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 6319

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        817120 kB
Buffers:         36800 kB
Cached:         143116 kB
SwapCached:         12 kB
Active:          65248 kB
Inactive:       117564 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        816868 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            28980 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:31:46 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4723 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.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (runsolver) R 1724 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481609403 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.0004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 792 0 0 0 996 1 0 0 25 0 1 0 481609403 4751360 770 4294967295 134512640 134672761 3221224560 3221223744 134559503 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 826 0 0 0 1996 1 0 0 25 0 1 0 481609403 5017600 804 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1225 804 603 41 0 1184 0
vsize: 4900
[startup+30.0011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 865 0 0 0 2995 2 0 0 25 0 1 0 481609403 5156864 843 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1259 843 603 41 0 1218 0
vsize: 5036
[startup+40.0015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 889 0 0 0 3995 2 0 0 25 0 1 0 481609403 5156864 867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1259 867 603 41 0 1218 0
vsize: 5036
[startup+50.0013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 909 0 0 0 4995 2 0 0 25 0 1 0 481609403 5287936 887 4294967295 134512640 134672761 3221224560 3221223728 134560917 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.0014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 915 0 0 0 5995 2 0 0 25 0 1 0 481609403 5287936 893 4294967295 134512640 134672761 3221224560 3221223744 134559489 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.0019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 978 0 0 0 6996 2 0 0 25 0 1 0 481609403 5558272 956 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.0017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 988 0 0 0 7996 2 0 0 25 0 1 0 481609403 5705728 966 4294967295 134512640 134672761 3221224560 3221223728 134561385 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.0017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1016 0 0 0 8996 2 0 0 25 0 1 0 481609403 5836800 994 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 994 603 41 0 1384 0
vsize: 5700
[startup+100.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1028 0 0 0 9996 2 0 0 25 0 1 0 481609403 5836800 1006 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1006 603 41 0 1384 0
vsize: 5700
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1033 0 0 0 10996 2 0 0 25 0 1 0 481609403 5836800 1011 4294967295 134512640 134672761 3221224560 3221223728 134560882 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1034 0 0 0 11996 2 0 0 25 0 1 0 481609403 5836800 1012 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1034 0 0 0 12996 2 0 0 25 0 1 0 481609403 5836800 1012 4294967295 134512640 134672761 3221224560 3221223728 134560909 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1041 0 0 0 13997 2 0 0 25 0 1 0 481609403 5836800 1019 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1042 0 0 0 14997 2 0 0 25 0 1 0 481609403 5836800 1020 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1042 0 0 0 15997 2 0 0 25 0 1 0 481609403 5836800 1020 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1425 1020 603 41 0 1384 0
vsize: 5700
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1074 0 0 0 16997 2 0 0 25 0 1 0 481609403 5971968 1052 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1074 0 0 0 17997 2 0 0 25 0 1 0 481609403 5971968 1052 4294967295 134512640 134672761 3221224560 3221223696 134560577 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1074 0 0 0 18997 2 0 0 25 0 1 0 481609403 5971968 1052 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1458 1052 603 41 0 1417 0
vsize: 5832
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1079 0 0 0 19997 2 0 0 25 0 1 0 481609403 6127616 1057 4294967295 134512640 134672761 3221224560 3221223728 134561220 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1085 0 0 0 20998 2 0 0 25 0 1 0 481609403 6127616 1063 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1063 603 41 0 1455 0
vsize: 5984
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1094 0 0 0 21998 2 0 0 25 0 1 0 481609403 6127616 1072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1496 1072 603 41 0 1455 0
vsize: 5984
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1109 0 0 0 22998 2 0 0 25 0 1 0 481609403 6262784 1087 4294967295 134512640 134672761 3221224560 3221223728 134561205 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1109 0 0 0 23998 2 0 0 25 0 1 0 481609403 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 24998 2 0 0 25 0 1 0 481609403 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+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 25998 2 0 0 25 0 1 0 481609403 6262784 1092 4294967295 134512640 134672761 3221224560 3221223720 134561029 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 26999 2 0 0 25 0 1 0 481609403 6262784 1092 4294967295 134512640 134672761 3221224560 3221223724 134561235 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 27999 2 0 0 25 0 1 0 481609403 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134561005 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 28999 2 0 0 25 0 1 0 481609403 6262784 1092 4294967295 134512640 134672761 3221224560 3221223684 134566098 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1114 0 0 0 29999 2 0 0 25 0 1 0 481609403 6262784 1092 4294967295 134512640 134672761 3221224560 3221223728 134560892 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1116 0 0 0 30999 2 0 0 25 0 1 0 481609403 6262784 1094 4294967295 134512640 134672761 3221224560 3221223744 134558700 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1116 0 0 0 32000 2 0 0 25 0 1 0 481609403 6262784 1094 4294967295 134512640 134672761 3221224560 3221223696 134565086 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1134 0 0 0 32998 2 0 0 25 0 1 0 481609403 6262784 1112 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1529 1112 603 41 0 1488 0
vsize: 6116
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1156 0 0 0 33997 3 0 0 25 0 1 0 481609403 6397952 1134 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1562 1134 603 41 0 1521 0
vsize: 6248
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1178 0 0 0 34997 3 0 0 25 0 1 0 481609403 6533120 1156 4294967295 134512640 134672761 3221224560 3221223728 134560912 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1198 0 0 0 35997 3 0 0 25 0 1 0 481609403 6533120 1176 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1204 0 0 0 36998 3 0 0 25 0 1 0 481609403 6668288 1182 4294967295 134512640 134672761 3221224560 3221223728 134561218 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1205 0 0 0 37998 3 0 0 25 0 1 0 481609403 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+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1205 0 0 0 38998 3 0 0 25 0 1 0 481609403 6668288 1183 4294967295 134512640 134672761 3221224560 3221223728 134561218 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1205 0 0 0 39998 3 0 0 25 0 1 0 481609403 6668288 1183 4294967295 134512640 134672761 3221224560 3221223760 134557849 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1205 0 0 0 40998 3 0 0 25 0 1 0 481609403 6668288 1183 4294967295 134512640 134672761 3221224560 3221223728 134560828 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 41999 3 0 0 25 0 1 0 481609403 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 42999 3 0 0 25 0 1 0 481609403 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134561385 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 43999 3 0 0 25 0 1 0 481609403 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+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 44999 3 0 0 25 0 1 0 481609403 6668288 1189 4294967295 134512640 134672761 3221224560 3221223724 134561235 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 45999 3 0 0 25 0 1 0 481609403 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1211 0 0 0 46999 3 0 0 25 0 1 0 481609403 6668288 1189 4294967295 134512640 134672761 3221224560 3221223728 134560867 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1216 0 0 0 47999 3 0 0 25 0 1 0 481609403 6668288 1194 4294967295 134512640 134672761 3221224560 3221223744 134559514 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1216 0 0 0 49000 3 0 0 25 0 1 0 481609403 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+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1216 0 0 0 50000 3 0 0 25 0 1 0 481609403 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1216 0 0 0 51000 3 0 0 25 0 1 0 481609403 6668288 1194 4294967295 134512640 134672761 3221224560 3221223728 134561193 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1216 0 0 0 52000 3 0 0 25 0 1 0 481609403 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+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1222 0 0 0 53000 3 0 0 25 0 1 0 481609403 6668288 1200 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1628 1200 603 41 0 1587 0
vsize: 6512
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1247 0 0 0 53999 3 0 0 25 0 1 0 481609403 6799360 1225 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1225 603 41 0 1619 0
vsize: 6640
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1252 0 0 0 54999 3 0 0 25 0 1 0 481609403 6799360 1230 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1252 0 0 0 56000 3 0 0 25 0 1 0 481609403 6799360 1230 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1230 603 41 0 1619 0
vsize: 6640
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1258 0 0 0 57000 3 0 0 25 0 1 0 481609403 6799360 1236 4294967295 134512640 134672761 3221224560 3221223728 134561198 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1258 0 0 0 58000 3 0 0 25 0 1 0 481609403 6799360 1236 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1660 1236 603 41 0 1619 0
vsize: 6640
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1260 0 0 0 59000 3 0 0 25 0 1 0 481609403 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+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1265 0 0 0 60000 3 0 0 25 0 1 0 481609403 6934528 1243 4294967295 134512640 134672761 3221224560 3221223728 134561008 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1265 0 0 0 61001 3 0 0 25 0 1 0 481609403 6934528 1243 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1243 603 41 0 1652 0
vsize: 6772
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1275 0 0 0 62001 3 0 0 25 0 1 0 481609403 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1275 0 0 0 63001 3 0 0 25 0 1 0 481609403 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1275 0 0 0 64001 3 0 0 25 0 1 0 481609403 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1275 0 0 0 65001 3 0 0 25 0 1 0 481609403 6934528 1253 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1253 603 41 0 1652 0
vsize: 6772
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1281 0 0 0 66001 3 0 0 25 0 1 0 481609403 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+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1281 0 0 0 67001 3 0 0 25 0 1 0 481609403 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1281 0 0 0 68001 3 0 0 25 0 1 0 481609403 6934528 1259 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1259 603 41 0 1652 0
vsize: 6772
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1286 0 0 0 69002 3 0 0 25 0 1 0 481609403 6934528 1264 4294967295 134512640 134672761 3221224560 3221223744 134558341 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1286 0 0 0 70002 3 0 0 25 0 1 0 481609403 6934528 1264 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1693 1264 603 41 0 1652 0
vsize: 6772
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1292 0 0 0 71002 3 0 0 25 0 1 0 481609403 7098368 1270 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1270 603 41 0 1692 0
vsize: 6932
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1298 0 0 0 72002 3 0 0 25 0 1 0 481609403 7098368 1276 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1276 603 41 0 1692 0
vsize: 6932
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1304 0 0 0 73002 3 0 0 25 0 1 0 481609403 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.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1305 0 0 0 74008 3 0 0 25 0 1 0 481609403 7098368 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1283 603 41 0 1692 0
vsize: 6932
[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1306 0 0 0 75008 3 0 0 25 0 1 0 481609403 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1306 0 0 0 76008 3 0 0 25 0 1 0 481609403 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560979 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1306 0 0 0 77008 3 0 0 25 0 1 0 481609403 7098368 1284 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1306 0 0 0 78008 3 0 0 25 0 1 0 481609403 7098368 1284 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1284 603 41 0 1692 0
vsize: 6932
[startup+790.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1307 0 0 0 79008 3 0 0 25 0 1 0 481609403 7098368 1285 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1733 1285 603 41 0 1692 0
vsize: 6932
[startup+800.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1308 0 0 0 80009 3 0 0 25 0 1 0 481609403 7098368 1286 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1308 0 0 0 81009 3 0 0 25 0 1 0 481609403 7098368 1286 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1286 603 41 0 1692 0
vsize: 6932
[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1310 0 0 0 82008 4 0 0 25 0 1 0 481609403 7098368 1288 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1733 1288 603 41 0 1692 0
vsize: 6932
[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1357 0 0 0 83007 4 0 0 25 0 1 0 481609403 7368704 1335 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1799 1335 603 41 0 1758 0
vsize: 7196
[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 84007 4 0 0 25 0 1 0 481609403 7368704 1339 4294967295 134512640 134672761 3221224560 3221223696 134560604 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 85007 4 0 0 25 0 1 0 481609403 7368704 1339 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1799 1339 603 41 0 1758 0
vsize: 7196
[startup+860.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 86007 4 0 0 25 0 1 0 481609403 7364608 1339 4294967295 134512640 134672761 3221224560 3221223744 134558654 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 87007 4 0 0 25 0 1 0 481609403 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134560895 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 88007 4 0 0 25 0 1 0 481609403 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134561229 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.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1361 0 0 0 89007 4 0 0 25 0 1 0 481609403 7364608 1339 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1339 603 41 0 1757 0
vsize: 7192
[startup+900.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1362 0 0 0 90008 4 0 0 25 0 1 0 481609403 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1362 0 0 0 91008 4 0 0 25 0 1 0 481609403 7364608 1340 4294967295 134512640 134672761 3221224560 3221223712 134565153 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1377 0 0 0 92008 4 0 0 25 0 1 0 481609403 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+930.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1377 0 0 0 93008 4 0 0 25 0 1 0 481609403 7364608 1355 4294967295 134512640 134672761 3221224560 3221223728 134560892 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1377 0 0 0 94009 4 0 0 25 0 1 0 481609403 7364608 1355 4294967295 134512640 134672761 3221224560 3221223620 1075346687 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.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1377 0 0 0 95009 4 0 0 25 0 1 0 481609403 7364608 1355 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1355 603 41 0 1757 0
vsize: 7192
[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1379 0 0 0 96009 4 0 0 25 0 1 0 481609403 7364608 1357 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1357 603 41 0 1757 0
vsize: 7192
[startup+970.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1380 0 0 0 97009 4 0 0 25 0 1 0 481609403 7364608 1358 4294967295 134512640 134672761 3221224560 3221223696 134560688 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.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1380 0 0 0 98009 4 0 0 25 0 1 0 481609403 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+990.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1380 0 0 0 99010 4 0 0 25 0 1 0 481609403 7364608 1358 4294967295 134512640 134672761 3221224560 3221223696 134565039 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1380 0 0 0 100010 4 0 0 25 0 1 0 481609403 7364608 1358 4294967295 134512640 134672761 3221224560 3221223728 134560869 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1380 0 0 0 101010 4 0 0 25 0 1 0 481609403 7364608 1358 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1358 603 41 0 1757 0
vsize: 7192
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 102010 4 0 0 25 0 1 0 481609403 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560858 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 103011 4 0 0 25 0 1 0 481609403 7364608 1360 4294967295 134512640 134672761 3221224560 3221223744 134559498 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 104011 4 0 0 25 0 1 0 481609403 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 105011 4 0 0 25 0 1 0 481609403 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+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 106011 4 0 0 25 0 1 0 481609403 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 107012 4 0 0 25 0 1 0 481609403 7364608 1360 4294967295 134512640 134672761 3221224560 3221223744 134558629 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 108012 4 0 0 25 0 1 0 481609403 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+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1382 0 0 0 109012 4 0 0 25 0 1 0 481609403 7364608 1360 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1360 603 41 0 1757 0
vsize: 7192
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1383 0 0 0 110012 4 0 0 25 0 1 0 481609403 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134561021 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1383 0 0 0 111013 4 0 0 25 0 1 0 481609403 7364608 1361 4294967295 134512640 134672761 3221224560 3221223728 134560858 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1383 0 0 0 112013 4 0 0 25 0 1 0 481609403 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+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1385 0 0 0 113013 4 0 0 25 0 1 0 481609403 7364608 1363 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1363 603 41 0 1757 0
vsize: 7192
[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1386 0 0 0 114013 4 0 0 25 0 1 0 481609403 7364608 1364 4294967295 134512640 134672761 3221224560 3221223664 134554665 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1386 0 0 0 115013 4 0 0 25 0 1 0 481609403 7364608 1364 4294967295 134512640 134672761 3221224560 3221223728 134560898 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1386 0 0 0 116013 4 0 0 25 0 1 0 481609403 7364608 1364 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1798 1364 603 41 0 1757 0
vsize: 7192
[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1387 0 0 0 117014 4 0 0 25 0 1 0 481609403 7364608 1365 4294967295 134512640 134672761 3221224560 3221223728 134561118 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1387 0 0 0 118014 4 0 0 25 0 1 0 481609403 7364608 1365 4294967295 134512640 134672761 3221224560 3221223728 134560983 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.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1387 0 0 0 119014 4 0 0 25 0 1 0 481609403 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+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1725
Raw data (stat): 1725 (minisat+) R 1724 27222 27221 0 -1 0 1387 0 0 0 120015 4 0 0 25 0 1 0 481609403 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1725
Raw data (stat): 1725 (minisat+) Z 1724 27222 27221 0 -1 12 1389 0 0 0 120015 4 0 0 23 0 1 0 481609403 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.11
CPU time (s): 1200.2
CPU user time (s): 1200.16
CPU system time (s): 0.047992
CPU usage (%): 100.007
Max. virtual memory (Kb): 7196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####