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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-f1000.opb
MD5SUM3b740c03d309134e8e181ea08fc4a1e3
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
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 2000
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 2000
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2000
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2000
Total number of constraints5250
Number of constraints which are clauses5250
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 4670 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-13 19:47:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3511 boxname=wulflinc30 idbench=127 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b740c03d309134e8e181ea08fc4a1e3  /oldhome/oroussel/tmp/wulflinc30/normalized-f1000.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc30/normalized-f1000.opb /oldhome/oroussel/tmp/wulflinc30/normalized-f1000.opb
IDLAUNCH: 3511
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        746896 kB
Buffers:         37080 kB
Cached:         210100 kB
SwapCached:          0 kB
Active:          79060 kB
Inactive:       170952 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        746644 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32176 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:07:04 (client local time) WITH STATUS 0 IN 1200.11 SECONDS
stats: 3511 7 1200.11 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5250 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 |    5250    14750 |    1750       0        0     nan |  0.000 % |
c |       100 |    5250    14750 |    1925     100     3875    38.8 |  0.000 % |
c |       250 |    5250    14750 |    2117     250    10126    40.5 |  0.000 % |
c |       475 |    5250    14750 |    2329     475    18401    38.7 |  0.000 % |
c |       813 |    5250    14750 |    2562     813    31625    38.9 |  0.000 % |
c |      1319 |    5250    14750 |    2818    1319    51895    39.3 |  0.000 % |
c |      2079 |    5250    14750 |    3100    2079    83376    40.1 |  0.000 % |
c |      3219 |    5250    14750 |    3410    3219   133390    41.4 |  0.000 % |
c |      4927 |    5250    14750 |    3751    3134   136512    43.6 |  0.000 % |
c |      7489 |    5250    14750 |    4126    3713   163080    43.9 |  0.000 % |
c |     11335 |    5250    14750 |    4539    3280   139769    42.6 |  0.000 % |
c |     17102 |    5250    14750 |    4992    4323   194018    44.9 |  0.000 % |
c |     25751 |    5250    14750 |    5492    2626   104281    39.7 |  0.000 % |
c |     38725 |    5250    14750 |    6041    4250   177931    41.9 |  0.000 % |
c |     58186 |    5250    14750 |    6645    5028   218270    43.4 |  0.000 % |
c |     87378 |    5250    14750 |    7310    3492   135818    38.9 |  0.000 % |
c |    131170 |    5250    14750 |    8041    6015   241026    40.1 |  0.000 % |
c |    196855 |    5250    14750 |    8845    5979   238890    40.0 |  0.000 % |
c |    295382 |    5250    14750 |    9729    5160   195623    37.9 |  0.000 % |
c |    443172 |    5250    14750 |   10702    9137   375254    41.1 |  0.000 % |
c |    664860 |    5250    14750 |   11773    8065   328188    40.7 |  0.000 % |
c |    997386 |    5250    14750 |   12950    6081   232085    38.2 |  0.000 % |
c |   1496176 |    5250    14750 |   14245   12487   501590    40.2 |  0.000 % |
#### 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.68 0.89 0.68 2/54 13683
Raw data (stat): 13683 (runsolver) R 13682 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478580958 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+9.99955 s]
Raw data (loadavg): 0.73 0.90 0.68 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 821 0 0 0 995 2 0 0 25 0 1 0 478580958 4943872 799 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1207 799 603 41 0 1166 0
vsize: 4828
[startup+20.0065 s]
Raw data (loadavg): 0.77 0.90 0.68 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 906 0 0 0 1995 3 0 0 25 0 1 0 478580958 5214208 884 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1273 884 603 41 0 1232 0
vsize: 5092
[startup+30.0077 s]
Raw data (loadavg): 0.80 0.90 0.69 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 981 0 0 0 2995 4 0 0 25 0 1 0 478580958 5488640 959 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1340 959 603 41 0 1299 0
vsize: 5360
[startup+40.0071 s]
Raw data (loadavg): 0.83 0.90 0.69 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1049 0 0 0 3994 4 0 0 25 0 1 0 478580958 5758976 1027 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1406 1027 603 41 0 1365 0
vsize: 5624
[startup+50.0079 s]
Raw data (loadavg): 0.86 0.91 0.69 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1098 0 0 0 4993 5 0 0 25 0 1 0 478580958 6033408 1076 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1473 1076 603 41 0 1432 0
vsize: 5892
[startup+60.0081 s]
Raw data (loadavg): 0.88 0.91 0.69 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1138 0 0 0 5993 5 0 0 25 0 1 0 478580958 6168576 1116 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1506 1116 603 41 0 1465 0
vsize: 6024
[startup+70.0089 s]
Raw data (loadavg): 0.90 0.91 0.70 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1144 0 0 0 6992 5 0 0 25 0 1 0 478580958 6168576 1122 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1506 1122 603 41 0 1465 0
vsize: 6024
[startup+80.0092 s]
Raw data (loadavg): 0.91 0.91 0.70 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1203 0 0 0 7992 6 0 0 25 0 1 0 478580958 6438912 1181 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1572 1181 603 41 0 1531 0
vsize: 6288
[startup+90.0094 s]
Raw data (loadavg): 0.93 0.92 0.70 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1234 0 0 0 8992 6 0 0 25 0 1 0 478580958 6574080 1212 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1605 1212 603 41 0 1564 0
vsize: 6420
[startup+100.01 s]
Raw data (loadavg): 0.94 0.92 0.71 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1272 0 0 0 9991 7 0 0 25 0 1 0 478580958 6709248 1250 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1638 1250 603 41 0 1597 0
vsize: 6552
[startup+110.011 s]
Raw data (loadavg): 0.95 0.92 0.71 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1278 0 0 0 10991 7 0 0 25 0 1 0 478580958 6844416 1256 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1671 1256 603 41 0 1630 0
vsize: 6684
[startup+120.012 s]
Raw data (loadavg): 0.95 0.92 0.71 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1337 0 0 0 11990 7 0 0 25 0 1 0 478580958 6975488 1315 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1703 1315 603 41 0 1662 0
vsize: 6812
[startup+130.013 s]
Raw data (loadavg): 0.96 0.92 0.71 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1376 0 0 0 12990 8 0 0 25 0 1 0 478580958 7245824 1354 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1769 1354 603 41 0 1728 0
vsize: 7076
[startup+140.012 s]
Raw data (loadavg): 0.97 0.93 0.72 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1392 0 0 0 13989 9 0 0 25 0 1 0 478580958 7245824 1370 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1769 1370 603 41 0 1728 0
vsize: 7076
[startup+150.013 s]
Raw data (loadavg): 0.97 0.93 0.72 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1414 0 0 0 14989 9 0 0 25 0 1 0 478580958 7393280 1392 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1392 603 41 0 1764 0
vsize: 7220
[startup+160.014 s]
Raw data (loadavg): 0.98 0.93 0.72 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1423 0 0 0 15988 9 0 0 25 0 1 0 478580958 7393280 1401 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1805 1401 603 41 0 1764 0
vsize: 7220
[startup+170.014 s]
Raw data (loadavg): 0.98 0.93 0.73 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1438 0 0 0 16988 10 0 0 25 0 1 0 478580958 7536640 1416 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1840 1416 603 41 0 1799 0
vsize: 7360
[startup+180.015 s]
Raw data (loadavg): 0.98 0.93 0.73 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1442 0 0 0 17988 10 0 0 25 0 1 0 478580958 7536640 1420 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1840 1420 603 41 0 1799 0
vsize: 7360
[startup+190.015 s]
Raw data (loadavg): 0.98 0.94 0.73 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1509 0 0 0 18987 11 0 0 25 0 1 0 478580958 7806976 1487 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1906 1487 603 41 0 1865 0
vsize: 7624
[startup+200.016 s]
Raw data (loadavg): 0.99 0.94 0.73 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1546 0 0 0 19986 11 0 0 25 0 1 0 478580958 7942144 1524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1524 603 41 0 1898 0
vsize: 7756
[startup+210.016 s]
Raw data (loadavg): 0.99 0.94 0.73 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1567 0 0 0 20986 12 0 0 25 0 1 0 478580958 7942144 1545 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1939 1545 603 41 0 1898 0
vsize: 7756
[startup+220.016 s]
Raw data (loadavg): 0.99 0.94 0.74 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1577 0 0 0 21986 12 0 0 25 0 1 0 478580958 8081408 1555 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1555 603 41 0 1932 0
vsize: 7892
[startup+230.016 s]
Raw data (loadavg): 0.99 0.94 0.74 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1585 0 0 0 22985 12 0 0 25 0 1 0 478580958 8081408 1563 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1563 603 41 0 1932 0
vsize: 7892
[startup+240.016 s]
Raw data (loadavg): 0.99 0.94 0.74 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1590 0 0 0 23985 12 0 0 25 0 1 0 478580958 8081408 1568 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1973 1568 603 41 0 1932 0
vsize: 7892
[startup+250.017 s]
Raw data (loadavg): 0.99 0.94 0.74 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1601 0 0 0 24985 13 0 0 25 0 1 0 478580958 8220672 1579 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1579 603 41 0 1966 0
vsize: 8028
[startup+260.018 s]
Raw data (loadavg): 0.99 0.95 0.74 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1611 0 0 0 25984 13 0 0 25 0 1 0 478580958 8220672 1589 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1589 603 41 0 1966 0
vsize: 8028
[startup+270.019 s]
Raw data (loadavg): 0.99 0.95 0.75 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1629 0 0 0 26983 14 0 0 25 0 1 0 478580958 8220672 1607 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2007 1607 603 41 0 1966 0
vsize: 8028
[startup+280.019 s]
Raw data (loadavg): 0.99 0.95 0.75 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1654 0 0 0 27983 14 0 0 25 0 1 0 478580958 8355840 1632 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2040 1632 603 41 0 1999 0
vsize: 8160
[startup+290.019 s]
Raw data (loadavg): 0.99 0.95 0.75 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1699 0 0 0 28982 15 0 0 25 0 1 0 478580958 8626176 1677 4294967295 134512640 134672761 3221224576 3221223760 134559286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1677 603 41 0 2065 0
vsize: 8424
[startup+300.02 s]
Raw data (loadavg): 0.99 0.95 0.75 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1729 0 0 0 29982 15 0 0 25 0 1 0 478580958 8769536 1707 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1707 603 41 0 2100 0
vsize: 8564
[startup+310.021 s]
Raw data (loadavg): 0.99 0.95 0.75 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1757 0 0 0 30982 15 0 0 25 0 1 0 478580958 8769536 1735 4294967295 134512640 134672761 3221224576 3221223728 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1735 603 41 0 2100 0
vsize: 8564
[startup+320.022 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1761 0 0 0 31981 15 0 0 25 0 1 0 478580958 8904704 1739 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1739 603 41 0 2133 0
vsize: 8696
[startup+330.022 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1772 0 0 0 32981 16 0 0 25 0 1 0 478580958 8904704 1750 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1750 603 41 0 2133 0
vsize: 8696
[startup+340.022 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1775 0 0 0 33981 16 0 0 25 0 1 0 478580958 8904704 1753 4294967295 134512640 134672761 3221224576 3221223760 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1753 603 41 0 2133 0
vsize: 8696
[startup+350.023 s]
Raw data (loadavg): 0.99 0.95 0.76 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1784 0 0 0 34980 16 0 0 25 0 1 0 478580958 8904704 1762 4294967295 134512640 134672761 3221224576 3221223680 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2174 1762 603 41 0 2133 0
vsize: 8696
[startup+360.024 s]
Raw data (loadavg): 0.99 0.96 0.76 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1801 0 0 0 35980 17 0 0 25 0 1 0 478580958 9039872 1779 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2207 1779 603 41 0 2166 0
vsize: 8828
[startup+370.025 s]
Raw data (loadavg): 0.99 0.96 0.77 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1829 0 0 0 36979 17 0 0 25 0 1 0 478580958 9175040 1807 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1807 603 41 0 2199 0
vsize: 8960
[startup+380.025 s]
Raw data (loadavg): 0.99 0.96 0.77 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1831 0 0 0 37979 17 0 0 25 0 1 0 478580958 9175040 1809 4294967295 134512640 134672761 3221224576 3221223824 134562677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1809 603 41 0 2199 0
vsize: 8960
[startup+390.025 s]
Raw data (loadavg): 0.99 0.96 0.77 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1838 0 0 0 38979 18 0 0 25 0 1 0 478580958 9175040 1816 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2240 1816 603 41 0 2199 0
vsize: 8960
[startup+400.026 s]
Raw data (loadavg): 0.99 0.96 0.77 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1860 0 0 0 39978 18 0 0 25 0 1 0 478580958 9306112 1838 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1838 603 41 0 2231 0
vsize: 9088
[startup+410.026 s]
Raw data (loadavg): 0.99 0.96 0.77 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1866 0 0 0 40978 19 0 0 25 0 1 0 478580958 9306112 1844 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1844 603 41 0 2231 0
vsize: 9088
[startup+420.027 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1870 0 0 0 41977 19 0 0 25 0 1 0 478580958 9306112 1848 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2272 1848 603 41 0 2231 0
vsize: 9088
[startup+430.027 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1884 0 0 0 42977 19 0 0 25 0 1 0 478580958 9441280 1862 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+440.027 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1884 0 0 0 43977 20 0 0 25 0 1 0 478580958 9441280 1862 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1862 603 41 0 2264 0
vsize: 9220
[startup+450.028 s]
Raw data (loadavg): 0.99 0.96 0.78 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1892 0 0 0 44976 20 0 0 25 0 1 0 478580958 9441280 1870 4294967295 134512640 134672761 3221224576 3221223584 1075349729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2305 1870 603 41 0 2264 0
vsize: 9220
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1951 0 0 0 45975 21 0 0 25 0 1 0 478580958 9723904 1929 4294967295 134512640 134672761 3221224576 3221223760 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2374 1929 603 41 0 2333 0
vsize: 9496
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1959 0 0 0 46975 21 0 0 25 0 1 0 478580958 9723904 1937 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2374 1937 603 41 0 2333 0
vsize: 9496
[startup+480.03 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1990 0 0 0 47975 22 0 0 25 0 1 0 478580958 9863168 1968 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1968 603 41 0 2367 0
vsize: 9632
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 1997 0 0 0 48974 22 0 0 25 0 1 0 478580958 9863168 1975 4294967295 134512640 134672761 3221224576 3221223752 134559124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1975 603 41 0 2367 0
vsize: 9632
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2001 0 0 0 49974 22 0 0 25 0 1 0 478580958 9863168 1979 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1979 603 41 0 2367 0
vsize: 9632
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2011 0 0 0 50974 22 0 0 25 0 1 0 478580958 9863168 1989 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2408 1989 603 41 0 2367 0
vsize: 9632
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2021 0 0 0 51974 22 0 0 25 0 1 0 478580958 10002432 1999 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 1999 603 41 0 2401 0
vsize: 9768
[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2032 0 0 0 52974 22 0 0 25 0 1 0 478580958 10002432 2010 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2010 603 41 0 2401 0
vsize: 9768
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2038 0 0 0 53975 22 0 0 25 0 1 0 478580958 10002432 2016 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2016 603 41 0 2401 0
vsize: 9768
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2046 0 0 0 54975 22 0 0 25 0 1 0 478580958 10002432 2024 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2442 2024 603 41 0 2401 0
vsize: 9768
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2053 0 0 0 55975 22 0 0 25 0 1 0 478580958 10137600 2031 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+570.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2053 0 0 0 56975 22 0 0 25 0 1 0 478580958 10137600 2031 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2031 603 41 0 2434 0
vsize: 9900
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2059 0 0 0 57975 22 0 0 25 0 1 0 478580958 10137600 2037 4294967295 134512640 134672761 3221224576 3221223712 134565134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2037 603 41 0 2434 0
vsize: 9900
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2080 0 0 0 58975 23 0 0 25 0 1 0 478580958 10137600 2058 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2475 2058 603 41 0 2434 0
vsize: 9900
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2088 0 0 0 59975 23 0 0 25 0 1 0 478580958 10268672 2066 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2066 603 41 0 2466 0
vsize: 10028
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2098 0 0 0 60976 23 0 0 25 0 1 0 478580958 10268672 2076 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2076 603 41 0 2466 0
vsize: 10028
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2102 0 0 0 61976 23 0 0 25 0 1 0 478580958 10268672 2080 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2102 0 0 0 62976 23 0 0 25 0 1 0 478580958 10268672 2080 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2080 603 41 0 2466 0
vsize: 10028
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2105 0 0 0 63976 23 0 0 25 0 1 0 478580958 10268672 2083 4294967295 134512640 134672761 3221224576 3221222688 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2507 2083 603 41 0 2466 0
vsize: 10028
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2116 0 0 0 64976 23 0 0 25 0 1 0 478580958 10412032 2094 4294967295 134512640 134672761 3221224576 3221223744 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2094 603 41 0 2501 0
vsize: 10168
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2120 0 0 0 65976 23 0 0 25 0 1 0 478580958 10412032 2098 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2098 603 41 0 2501 0
vsize: 10168
[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2123 0 0 0 66976 23 0 0 25 0 1 0 478580958 10412032 2101 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2101 603 41 0 2501 0
vsize: 10168
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2134 0 0 0 67976 23 0 0 25 0 1 0 478580958 10412032 2112 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2112 603 41 0 2501 0
vsize: 10168
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2137 0 0 0 68977 23 0 0 25 0 1 0 478580958 10412032 2115 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2542 2115 603 41 0 2501 0
vsize: 10168
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2140 0 0 0 69977 23 0 0 25 0 1 0 478580958 10551296 2118 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2576 2118 603 41 0 2535 0
vsize: 10304
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2144 0 0 0 70977 23 0 0 25 0 1 0 478580958 10551296 2122 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2576 2122 603 41 0 2535 0
vsize: 10304
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2212 0 0 0 71976 23 0 0 25 0 1 0 478580958 10821632 2190 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2190 603 41 0 2601 0
vsize: 10568
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2217 0 0 0 72976 23 0 0 25 0 1 0 478580958 10821632 2195 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2195 603 41 0 2601 0
vsize: 10568
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2231 0 0 0 73976 23 0 0 25 0 1 0 478580958 10821632 2209 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2209 603 41 0 2601 0
vsize: 10568
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2237 0 0 0 74977 23 0 0 25 0 1 0 478580958 10821632 2215 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2642 2215 603 41 0 2601 0
vsize: 10568
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2278 0 0 0 75977 23 0 0 25 0 1 0 478580958 11091968 2256 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2256 603 41 0 2667 0
vsize: 10832
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2284 0 0 0 76977 24 0 0 25 0 1 0 478580958 11091968 2262 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2262 603 41 0 2667 0
vsize: 10832
[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 13683
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2287 0 0 0 77980 24 0 0 25 0 1 0 478580958 11091968 2265 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+790.069 s]
Raw data (loadavg): 1.07 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2287 0 0 0 78981 24 0 0 25 0 1 0 478580958 11091968 2265 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2265 603 41 0 2667 0
vsize: 10832
[startup+800.07 s]
Raw data (loadavg): 1.06 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2289 0 0 0 79981 24 0 0 25 0 1 0 478580958 11091968 2267 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2708 2267 603 41 0 2667 0
vsize: 10832
[startup+810.071 s]
Raw data (loadavg): 1.05 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2297 0 0 0 80981 24 0 0 25 0 1 0 478580958 11227136 2275 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2275 603 41 0 2700 0
vsize: 10964
[startup+820.072 s]
Raw data (loadavg): 1.04 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2298 0 0 0 81981 24 0 0 25 0 1 0 478580958 11227136 2276 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2276 603 41 0 2700 0
vsize: 10964
[startup+830.072 s]
Raw data (loadavg): 1.04 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2301 0 0 0 82981 24 0 0 25 0 1 0 478580958 11227136 2279 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2279 603 41 0 2700 0
vsize: 10964
[startup+840.072 s]
Raw data (loadavg): 1.03 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2308 0 0 0 83981 24 0 0 25 0 1 0 478580958 11227136 2286 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2286 603 41 0 2700 0
vsize: 10964
[startup+850.072 s]
Raw data (loadavg): 1.03 0.99 0.84 2/54 13736
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2312 0 0 0 84982 24 0 0 25 0 1 0 478580958 11227136 2290 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2290 603 41 0 2700 0
vsize: 10964
[startup+860.072 s]
Raw data (loadavg): 1.02 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2316 0 0 0 85982 24 0 0 25 0 1 0 478580958 11227136 2294 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2294 603 41 0 2700 0
vsize: 10964
[startup+870.073 s]
Raw data (loadavg): 1.02 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2323 0 0 0 86982 24 0 0 25 0 1 0 478580958 11227136 2301 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2301 603 41 0 2700 0
vsize: 10964
[startup+880.072 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2324 0 0 0 87982 24 0 0 25 0 1 0 478580958 11227136 2302 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+890.072 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2324 0 0 0 88982 24 0 0 25 0 1 0 478580958 11227136 2302 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2741 2302 603 41 0 2700 0
vsize: 10964
[startup+900.072 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2337 0 0 0 89983 24 0 0 25 0 1 0 478580958 11370496 2315 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2315 603 41 0 2735 0
vsize: 11104
[startup+910.073 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2343 0 0 0 90983 24 0 0 25 0 1 0 478580958 11370496 2321 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2776 2321 603 41 0 2735 0
vsize: 11104
[startup+920.073 s]
Raw data (loadavg): 1.01 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2364 0 0 0 91983 24 0 0 25 0 1 0 478580958 11505664 2342 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2342 603 41 0 2768 0
vsize: 11236
[startup+930.073 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2365 0 0 0 92983 24 0 0 25 0 1 0 478580958 11505664 2343 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2343 603 41 0 2768 0
vsize: 11236
[startup+940.072 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2369 0 0 0 93983 24 0 0 25 0 1 0 478580958 11505664 2347 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+950.072 s]
Raw data (loadavg): 1.00 0.99 0.85 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2369 0 0 0 94983 24 0 0 25 0 1 0 478580958 11505664 2347 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2347 603 41 0 2768 0
vsize: 11236
[startup+960.072 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2373 0 0 0 95984 24 0 0 25 0 1 0 478580958 11505664 2351 4294967295 134512640 134672761 3221224576 3221223532 1075350817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2351 603 41 0 2768 0
vsize: 11236
[startup+970.073 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2376 0 0 0 96984 24 0 0 25 0 1 0 478580958 11505664 2354 4294967295 134512640 134672761 3221224576 3221223680 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2809 2354 603 41 0 2768 0
vsize: 11236
[startup+980.073 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2397 0 0 0 97984 24 0 0 25 0 1 0 478580958 11640832 2375 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+990.073 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2397 0 0 0 98984 24 0 0 25 0 1 0 478580958 11640832 2375 4294967295 134512640 134672761 3221224576 3221223744 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2375 603 41 0 2801 0
vsize: 11368
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2400 0 0 0 99984 24 0 0 25 0 1 0 478580958 11640832 2378 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2378 603 41 0 2801 0
vsize: 11368
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2420 0 0 0 100984 24 0 0 25 0 1 0 478580958 11640832 2398 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2398 603 41 0 2801 0
vsize: 11368
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2441 0 0 0 101984 24 0 0 25 0 1 0 478580958 11776000 2419 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2419 603 41 0 2834 0
vsize: 11500
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2445 0 0 0 102985 24 0 0 25 0 1 0 478580958 11776000 2423 4294967295 134512640 134672761 3221224576 3221223760 134559193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2423 603 41 0 2834 0
vsize: 11500
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2449 0 0 0 103985 24 0 0 25 0 1 0 478580958 11776000 2427 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.86 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2449 0 0 0 104985 24 0 0 25 0 1 0 478580958 11776000 2427 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2427 603 41 0 2834 0
vsize: 11500
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2450 0 0 0 105985 24 0 0 25 0 1 0 478580958 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2450 0 0 0 106985 24 0 0 25 0 1 0 478580958 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2450 0 0 0 107986 24 0 0 25 0 1 0 478580958 11776000 2428 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2428 603 41 0 2834 0
vsize: 11500
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2452 0 0 0 108986 24 0 0 25 0 1 0 478580958 11776000 2430 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2430 603 41 0 2834 0
vsize: 11500
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2461 0 0 0 109986 24 0 0 25 0 1 0 478580958 11915264 2439 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2439 603 41 0 2868 0
vsize: 11636
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2465 0 0 0 110986 24 0 0 25 0 1 0 478580958 11915264 2443 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2443 603 41 0 2868 0
vsize: 11636
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2473 0 0 0 111986 24 0 0 25 0 1 0 478580958 11915264 2451 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2451 603 41 0 2868 0
vsize: 11636
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13738
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2497 0 0 0 112986 24 0 0 25 0 1 0 478580958 12050432 2475 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2475 603 41 0 2901 0
vsize: 11768
[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2504 0 0 0 113985 25 0 0 25 0 1 0 478580958 12050432 2482 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2482 603 41 0 2901 0
vsize: 11768
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2511 0 0 0 114984 25 0 0 25 0 1 0 478580958 12050432 2489 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2489 603 41 0 2901 0
vsize: 11768
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.87 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2515 0 0 0 115984 25 0 0 25 0 1 0 478580958 12050432 2493 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2493 603 41 0 2901 0
vsize: 11768
[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2519 0 0 0 116984 26 0 0 25 0 1 0 478580958 12050432 2497 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2519 0 0 0 117983 26 0 0 25 0 1 0 478580958 12050432 2497 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2942 2497 603 41 0 2901 0
vsize: 11768
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2522 0 0 0 118983 26 0 0 25 0 1 0 478580958 12189696 2500 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2500 603 41 0 2935 0
vsize: 11904
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.88 2/54 13740
Raw data (stat): 13683 (minisat+) R 13682 11931 11930 0 -1 0 2536 0 0 0 119983 27 0 0 25 0 1 0 478580958 12189696 2514 4294967295 134512640 134672761 3221224576 3221223680 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2976 2514 603 41 0 2935 0
vsize: 11904
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.88 1/54 13740
Raw data (stat): 13683 (minisat+) Z 13682 11931 11930 0 -1 12 2538 0 0 0 119983 27 0 0 25 0 1 0 478580958 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.09
CPU time (s): 1200.11
CPU user time (s): 1199.83
CPU system time (s): 0.279957
CPU usage (%): 100.002
Max. virtual memory (Kb): 11904
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####