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/aloul/FPGA_SAT05/normalized-chnl15_16_pb.cnf.cr.opb
MD5SUM3f8902c4e8af50006f671e2bddb3e9aa
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 17
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.013997
Number of variables480
Total number of constraints62
Number of constraints which are clauses32
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint16

Trace number 5702 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        899368 kB
Buffers:         34288 kB
Cached:          79380 kB
SwapCached:       2272 kB
Active:          53952 kB
Inactive:        64820 kB
HighTotal:      131008 kB
HighFree:        47740 kB
LowTotal:       903652 kB
LowFree:        851628 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10868 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:50:05 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 4141 7 1200.09 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 62 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................
c ---[  29]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  27]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  25]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  19]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  17]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  15]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   29
c ---[  12]---> BDD-cost:   29
c ---[  11]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   8]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   6]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   4]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost:   29
c ---[   1]---> BDD-cost:   29
c ---[   0]---> BDD-cost:   29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2162     6030 |     720       0        0     nan |  0.000 % |
c |       102 |    2162     6030 |     792     102     5686    55.7 |  2.222 % |
c |       252 |    2162     6030 |     871     252    14004    55.6 |  2.222 % |
c |       478 |    2162     6030 |     958     478    28490    59.6 |  2.222 % |
c |       815 |    2162     6030 |    1054     815    57080    70.0 |  2.222 % |
c |      1322 |    2162     6030 |    1159    1322   104342    78.9 |  2.222 % |
c |      2084 |    2162     6030 |    1275    1423   130456    91.7 |  2.222 % |
c |      3226 |    2162     6030 |    1403    1038    95866    92.4 |  2.222 % |
c |      4934 |    2162     6030 |    1543    1033   102989    99.7 |  2.222 % |
c |      7499 |    2162     6030 |    1697    1732   186615   107.7 |  2.222 % |
c |     11345 |    2162     6030 |    1867    1717   162221    94.5 |  2.222 % |
c |     17111 |    2162     6030 |    2054    1970   199253   101.1 |  2.222 % |
c |     25760 |    2162     6030 |    2259    2320   271642   117.1 |  2.222 % |
c |     38735 |    2162     6030 |    2485    2566   270521   105.4 |  2.222 % |
c |     58199 |    2162     6030 |    2734    2477   258968   104.5 |  2.222 % |
c |     87394 |    2162     6030 |    3007    2810   295638   105.2 |  2.222 % |
c |    131184 |    2162     6030 |    3308    1846   187402   101.5 |  2.222 % |
c |    196869 |    2162     6030 |    3639    3043   323650   106.4 |  2.222 % |
c |    295396 |    2162     6030 |    4003    3086   314350   101.9 |  2.222 % |
c |    443187 |    2162     6030 |    4403    2851   287482   100.8 |  2.222 % |
c |    664871 |    2162     6030 |    4843    3470   330999    95.4 |  2.222 % |
c |    997401 |    2162     6030 |    5328    4395   477257   108.6 |  2.222 % |
c |   1496194 |    2162     6030 |    5860    4647   485933   104.6 |  2.222 % |
#### 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.85 0.97 0.91 2/54 28351
Raw data (stat): 28351 (runsolver) R 28350 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422420896 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 812 0 0 0 995 2 0 0 25 0 1 0 422420896 4845568 790 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1183 790 603 41 0 1142 0
vsize: 4732
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 882 0 0 0 1995 3 0 0 25 0 1 0 422420896 5115904 860 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1249 860 603 41 0 1208 0
vsize: 4996
[startup+30.0028 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 947 0 0 0 2994 3 0 0 25 0 1 0 422420896 5386240 925 4294967295 134512640 134672761 3221224544 3221223728 134559569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1315 925 603 41 0 1274 0
vsize: 5260
[startup+40.0035 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 989 0 0 0 3994 3 0 0 25 0 1 0 422420896 5521408 967 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1348 967 603 41 0 1307 0
vsize: 5392
[startup+50.0038 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1024 0 0 0 4993 4 0 0 25 0 1 0 422420896 5656576 1002 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1381 1002 603 41 0 1340 0
vsize: 5524
[startup+60.005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1037 0 0 0 5993 5 0 0 25 0 1 0 422420896 5791744 1015 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1414 1015 603 41 0 1373 0
vsize: 5656
[startup+70.0058 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1037 0 0 0 6992 5 0 0 25 0 1 0 422420896 5787648 1015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1413 1015 603 41 0 1372 0
vsize: 5652
[startup+80.0071 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1127 0 0 0 7992 5 0 0 25 0 1 0 422420896 6193152 1105 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1512 1105 603 41 0 1471 0
vsize: 6048
[startup+90.0072 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1145 0 0 0 8991 6 0 0 25 0 1 0 422420896 6193152 1123 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1512 1123 603 41 0 1471 0
vsize: 6048
[startup+100.007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1152 0 0 0 9991 6 0 0 25 0 1 0 422420896 6193152 1130 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1512 1130 603 41 0 1471 0
vsize: 6048
[startup+110.007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1153 0 0 0 10991 6 0 0 25 0 1 0 422420896 6193152 1131 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1512 1131 603 41 0 1471 0
vsize: 6048
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1203 0 0 0 11990 7 0 0 25 0 1 0 422420896 6463488 1181 4294967295 134512640 134672761 3221224544 3221223696 134565029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1181 603 41 0 1537 0
vsize: 6312
[startup+130.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1228 0 0 0 12990 7 0 0 25 0 1 0 422420896 6598656 1206 4294967295 134512640 134672761 3221224544 3221223752 1075346913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1611 1206 603 41 0 1570 0
vsize: 6444
[startup+140.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1245 0 0 0 13989 7 0 0 25 0 1 0 422420896 6598656 1223 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1611 1223 603 41 0 1570 0
vsize: 6444
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1303 0 0 0 14989 8 0 0 25 0 1 0 422420896 6864896 1281 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1676 1281 603 41 0 1635 0
vsize: 6704
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1322 0 0 0 15988 8 0 0 25 0 1 0 422420896 7000064 1300 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1709 1300 603 41 0 1668 0
vsize: 6836
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1368 0 0 0 16987 9 0 0 25 0 1 0 422420896 7135232 1346 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1742 1346 603 41 0 1701 0
vsize: 6968
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1427 0 0 0 17987 9 0 0 25 0 1 0 422420896 7405568 1405 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1405 603 41 0 1767 0
vsize: 7232
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1427 0 0 0 18987 9 0 0 25 0 1 0 422420896 7405568 1405 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1808 1405 603 41 0 1767 0
vsize: 7232
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1443 0 0 0 19986 10 0 0 25 0 1 0 422420896 7553024 1421 4294967295 134512640 134672761 3221224544 3221223728 134559611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1421 603 41 0 1803 0
vsize: 7376
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1462 0 0 0 20986 10 0 0 25 0 1 0 422420896 7553024 1440 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1440 603 41 0 1803 0
vsize: 7376
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1467 0 0 0 21985 11 0 0 25 0 1 0 422420896 7553024 1445 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1445 603 41 0 1803 0
vsize: 7376
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1474 0 0 0 22985 11 0 0 25 0 1 0 422420896 7684096 1452 4294967295 134512640 134672761 3221224544 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1876 1452 603 41 0 1835 0
vsize: 7504
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1479 0 0 0 23985 11 0 0 25 0 1 0 422420896 7684096 1457 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1876 1457 603 41 0 1835 0
vsize: 7504
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1487 0 0 0 24985 11 0 0 25 0 1 0 422420896 7684096 1465 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1876 1465 603 41 0 1835 0
vsize: 7504
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1579 0 0 0 25984 12 0 0 25 0 1 0 422420896 8093696 1557 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1976 1557 603 41 0 1935 0
vsize: 7904
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1579 0 0 0 26984 12 0 0 25 0 1 0 422420896 8093696 1557 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1976 1557 603 41 0 1935 0
vsize: 7904
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1583 0 0 0 27984 12 0 0 25 0 1 0 422420896 8093696 1561 4294967295 134512640 134672761 3221224544 3221223776 134541821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1976 1561 603 41 0 1935 0
vsize: 7904
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1627 0 0 0 28983 12 0 0 25 0 1 0 422420896 8228864 1605 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2009 1605 603 41 0 1968 0
vsize: 8036
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1651 0 0 0 29983 12 0 0 25 0 1 0 422420896 8364032 1629 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2042 1629 603 41 0 2001 0
vsize: 8168
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1657 0 0 0 30983 13 0 0 25 0 1 0 422420896 8499200 1635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1635 603 41 0 2034 0
vsize: 8300
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1657 0 0 0 31982 13 0 0 25 0 1 0 422420896 8499200 1635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1635 603 41 0 2034 0
vsize: 8300
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1657 0 0 0 32982 14 0 0 25 0 1 0 422420896 8499200 1635 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1635 603 41 0 2034 0
vsize: 8300
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1669 0 0 0 33981 14 0 0 25 0 1 0 422420896 8499200 1647 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1647 603 41 0 2034 0
vsize: 8300
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1689 0 0 0 34981 14 0 0 25 0 1 0 422420896 8646656 1667 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1667 603 41 0 2070 0
vsize: 8444
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1698 0 0 0 35981 15 0 0 25 0 1 0 422420896 8646656 1676 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1676 603 41 0 2070 0
vsize: 8444
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1711 0 0 0 36980 15 0 0 25 0 1 0 422420896 8646656 1689 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1689 603 41 0 2070 0
vsize: 8444
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1741 0 0 0 37980 15 0 0 25 0 1 0 422420896 8781824 1719 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2144 1719 603 41 0 2103 0
vsize: 8576
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1757 0 0 0 38980 15 0 0 25 0 1 0 422420896 8921088 1735 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1735 603 41 0 2137 0
vsize: 8712
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1782 0 0 0 39979 16 0 0 25 0 1 0 422420896 9056256 1760 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2211 1760 603 41 0 2170 0
vsize: 8844
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1810 0 0 0 40979 16 0 0 25 0 1 0 422420896 9179136 1788 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1788 603 41 0 2200 0
vsize: 8964
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1814 0 0 0 41978 16 0 0 25 0 1 0 422420896 9179136 1792 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1792 603 41 0 2200 0
vsize: 8964
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1814 0 0 0 42978 17 0 0 25 0 1 0 422420896 9179136 1792 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1792 603 41 0 2200 0
vsize: 8964
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1821 0 0 0 43978 17 0 0 25 0 1 0 422420896 9179136 1799 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1799 603 41 0 2200 0
vsize: 8964
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1840 0 0 0 44977 17 0 0 25 0 1 0 422420896 9314304 1818 4294967295 134512640 134672761 3221224544 3221223668 134556415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2274 1818 603 41 0 2233 0
vsize: 9096
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1843 0 0 0 45977 18 0 0 25 0 1 0 422420896 9285632 1821 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2267 1821 603 41 0 2226 0
vsize: 9068
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1855 0 0 0 46976 18 0 0 25 0 1 0 422420896 9285632 1833 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2267 1833 603 41 0 2226 0
vsize: 9068
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1866 0 0 0 47976 18 0 0 25 0 1 0 422420896 9428992 1844 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1844 603 41 0 2261 0
vsize: 9208
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1876 0 0 0 48976 19 0 0 25 0 1 0 422420896 9428992 1854 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1854 603 41 0 2261 0
vsize: 9208
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1878 0 0 0 49976 19 0 0 25 0 1 0 422420896 9428992 1856 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1856 603 41 0 2261 0
vsize: 9208
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1878 0 0 0 50976 19 0 0 25 0 1 0 422420896 9428992 1856 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1856 603 41 0 2261 0
vsize: 9208
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1886 0 0 0 51976 19 0 0 25 0 1 0 422420896 9428992 1864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1864 603 41 0 2261 0
vsize: 9208
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1887 0 0 0 52977 19 0 0 25 0 1 0 422420896 9428992 1865 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1865 603 41 0 2261 0
vsize: 9208
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1898 0 0 0 53977 19 0 0 25 0 1 0 422420896 9428992 1876 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1876 603 41 0 2261 0
vsize: 9208
[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1899 0 0 0 54977 19 0 0 25 0 1 0 422420896 9428992 1877 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2302 1877 603 41 0 2261 0
vsize: 9208
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1913 0 0 0 55977 19 0 0 25 0 1 0 422420896 9564160 1891 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2335 1891 603 41 0 2294 0
vsize: 9340
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1927 0 0 0 56977 19 0 0 25 0 1 0 422420896 9555968 1905 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2333 1905 603 41 0 2292 0
vsize: 9332
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1929 0 0 0 57977 19 0 0 25 0 1 0 422420896 9555968 1907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2333 1907 603 41 0 2292 0
vsize: 9332
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 1952 0 0 0 58977 19 0 0 25 0 1 0 422420896 9691136 1930 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2366 1930 603 41 0 2325 0
vsize: 9464
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2003 0 0 0 59976 19 0 0 25 0 1 0 422420896 9826304 1981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2399 1981 603 41 0 2358 0
vsize: 9596
[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2003 0 0 0 60976 19 0 0 25 0 1 0 422420896 9826304 1981 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2399 1981 603 41 0 2358 0
vsize: 9596
[startup+620.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2015 0 0 0 61977 19 0 0 25 0 1 0 422420896 9961472 1993 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2432 1993 603 41 0 2391 0
vsize: 9728
[startup+630.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2020 0 0 0 62977 19 0 0 25 0 1 0 422420896 9961472 1998 4294967295 134512640 134672761 3221224544 3221223728 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2432 1998 603 41 0 2391 0
vsize: 9728
[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2020 0 0 0 63977 19 0 0 25 0 1 0 422420896 9961472 1998 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2432 1998 603 41 0 2391 0
vsize: 9728
[startup+650.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2024 0 0 0 64977 19 0 0 25 0 1 0 422420896 9961472 2002 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2432 2002 603 41 0 2391 0
vsize: 9728
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2037 0 0 0 65977 19 0 0 25 0 1 0 422420896 10104832 2015 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2015 603 41 0 2426 0
vsize: 9868
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2038 0 0 0 66978 19 0 0 25 0 1 0 422420896 10104832 2016 4294967295 134512640 134672761 3221224544 3221223728 134558943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2016 603 41 0 2426 0
vsize: 9868
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2041 0 0 0 67978 19 0 0 25 0 1 0 422420896 10104832 2019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2019 603 41 0 2426 0
vsize: 9868
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2047 0 0 0 68978 19 0 0 25 0 1 0 422420896 10104832 2025 4294967295 134512640 134672761 3221224544 3221223536 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2025 603 41 0 2426 0
vsize: 9868
[startup+700.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2050 0 0 0 69978 19 0 0 25 0 1 0 422420896 10104832 2028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2028 603 41 0 2426 0
vsize: 9868
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2053 0 0 0 70978 19 0 0 25 0 1 0 422420896 10104832 2031 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2031 603 41 0 2426 0
vsize: 9868
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2059 0 0 0 71978 19 0 0 25 0 1 0 422420896 10104832 2037 4294967295 134512640 134672761 3221224544 3221223648 134554907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2037 603 41 0 2426 0
vsize: 9868
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2063 0 0 0 72979 19 0 0 25 0 1 0 422420896 10104832 2041 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2041 603 41 0 2426 0
vsize: 9868
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2064 0 0 0 73979 19 0 0 25 0 1 0 422420896 10104832 2042 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2042 603 41 0 2426 0
vsize: 9868
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2064 0 0 0 74979 19 0 0 25 0 1 0 422420896 10104832 2042 4294967295 134512640 134672761 3221224544 3221223728 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2467 2042 603 41 0 2426 0
vsize: 9868
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2109 0 0 0 75979 20 0 0 25 0 1 0 422420896 10375168 2087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2533 2087 603 41 0 2492 0
vsize: 10132
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2109 0 0 0 76979 20 0 0 25 0 1 0 422420896 10358784 2087 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2529 2087 603 41 0 2488 0
vsize: 10116
[startup+780.038 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2110 0 0 0 77980 20 0 0 25 0 1 0 422420896 10338304 2088 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2088 603 41 0 2483 0
vsize: 10096
[startup+790.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2110 0 0 0 78980 20 0 0 25 0 1 0 422420896 10244096 2082 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2501 2082 603 41 0 2460 0
vsize: 10004
[startup+800.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2119 0 0 0 79980 20 0 0 25 0 1 0 422420896 10379264 2091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2091 603 41 0 2493 0
vsize: 10136
[startup+810.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2120 0 0 0 80980 20 0 0 25 0 1 0 422420896 10379264 2092 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2092 603 41 0 2493 0
vsize: 10136
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2124 0 0 0 81980 20 0 0 25 0 1 0 422420896 10379264 2096 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2096 603 41 0 2493 0
vsize: 10136
[startup+830.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2125 0 0 0 82980 20 0 0 25 0 1 0 422420896 10379264 2097 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2097 603 41 0 2493 0
vsize: 10136
[startup+840.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2125 0 0 0 83981 20 0 0 25 0 1 0 422420896 10379264 2097 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2097 603 41 0 2493 0
vsize: 10136
[startup+850.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2128 0 0 0 84981 20 0 0 25 0 1 0 422420896 10379264 2100 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2100 603 41 0 2493 0
vsize: 10136
[startup+860.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2130 0 0 0 85981 20 0 0 25 0 1 0 422420896 10379264 2102 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2102 603 41 0 2493 0
vsize: 10136
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2140 0 0 0 86981 20 0 0 25 0 1 0 422420896 10379264 2112 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2112 603 41 0 2493 0
vsize: 10136
[startup+880.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2140 0 0 0 87982 20 0 0 25 0 1 0 422420896 10379264 2112 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2112 603 41 0 2493 0
vsize: 10136
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2141 0 0 0 88982 20 0 0 25 0 1 0 422420896 10379264 2113 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2113 603 41 0 2493 0
vsize: 10136
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2142 0 0 0 89982 20 0 0 25 0 1 0 422420896 10379264 2114 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2114 603 41 0 2493 0
vsize: 10136
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2147 0 0 0 90982 20 0 0 25 0 1 0 422420896 10379264 2119 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2534 2119 603 41 0 2493 0
vsize: 10136
[startup+920.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2243 0 0 0 91982 20 0 0 25 0 1 0 422420896 10784768 2215 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2215 603 41 0 2592 0
vsize: 10532
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2256 0 0 0 92982 20 0 0 25 0 1 0 422420896 10784768 2228 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2633 2228 603 41 0 2592 0
vsize: 10532
[startup+940.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2288 0 0 0 93982 20 0 0 25 0 1 0 422420896 10919936 2260 4294967295 134512640 134672761 3221224544 3221223264 134565745 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2260 603 41 0 2625 0
vsize: 10664
[startup+950.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2288 0 0 0 94982 20 0 0 25 0 1 0 422420896 10919936 2260 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2260 603 41 0 2625 0
vsize: 10664
[startup+960.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2288 0 0 0 95982 20 0 0 25 0 1 0 422420896 10919936 2260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2260 603 41 0 2625 0
vsize: 10664
[startup+970.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2289 0 0 0 96982 20 0 0 25 0 1 0 422420896 10919936 2261 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2261 603 41 0 2625 0
vsize: 10664
[startup+980.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2290 0 0 0 97983 20 0 0 25 0 1 0 422420896 10919936 2262 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2290 0 0 0 98983 20 0 0 25 0 1 0 422420896 10919936 2262 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2290 0 0 0 99983 20 0 0 25 0 1 0 422420896 10919936 2262 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 100983 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 101983 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 102984 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 103984 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 104984 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 105984 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2291 0 0 0 106985 20 0 0 25 0 1 0 422420896 10919936 2263 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2292 0 0 0 107985 20 0 0 25 0 1 0 422420896 10919936 2264 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2666 2264 603 41 0 2625 0
vsize: 10664
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2303 0 0 0 108985 20 0 0 25 0 1 0 422420896 11067392 2275 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2275 603 41 0 2661 0
vsize: 10808
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 109985 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 110985 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 111985 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223500 1075349878 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 112986 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 113986 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2308 0 0 0 114986 20 0 0 25 0 1 0 422420896 11067392 2280 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2318 0 0 0 115986 20 0 0 25 0 1 0 422420896 11067392 2290 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2318 0 0 0 116986 20 0 0 25 0 1 0 422420896 11067392 2290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2318 0 0 0 117987 20 0 0 25 0 1 0 422420896 11067392 2290 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2318 0 0 0 118987 20 0 0 25 0 1 0 422420896 11067392 2290 4294967295 134512640 134672761 3221224544 3221223680 134565058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28351
Raw data (stat): 28351 (minisat+) R 28350 24215 24214 0 -1 0 2318 0 0 0 119987 20 0 0 25 0 1 0 422420896 11067392 2290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28351
Raw data (stat): 28351 (minisat+) Z 28350 24215 24214 0 -1 12 2320 0 0 0 119987 21 0 0 25 0 1 0 422420896 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.09
CPU user time (s): 1199.87
CPU system time (s): 0.211967
CPU usage (%): 100.003
Max. virtual memory (Kb): 10808
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####