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 4740 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 20:08:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=41 boxname=wulflinc9 idbench=5 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3f8902c4e8af50006f671e2bddb3e9aa  /oldhome/oroussel/tmp/wulflinc9/normalized-chnl15_16_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-chnl15_16_pb.cnf.cr.opb
IDLAUNCH: 41
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        914692 kB
Buffers:         33812 kB
Cached:          66400 kB
SwapCached:        564 kB
Active:          48916 kB
Inactive:        54692 kB
HighTotal:      131008 kB
HighFree:        60732 kB
LowTotal:       903652 kB
LowFree:        853960 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10768 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:28:32 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 41 7 1200.18 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.99 0.99 0.88 2/54 32502
Raw data (stat): 32502 (runsolver) R 32501 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420491194 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.99949 s]
Raw data (loadavg): 0.99 0.99 0.88 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 812 0 0 0 995 2 0 0 25 0 1 0 420491194 4845568 790 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1183 790 603 41 0 1142 0
vsize: 4732
[startup+20.0007 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 882 0 0 0 1995 2 0 0 25 0 1 0 420491194 5115904 860 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1249 860 603 41 0 1208 0
vsize: 4996
[startup+30.0015 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 947 0 0 0 2994 3 0 0 25 0 1 0 420491194 5386240 925 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1315 925 603 41 0 1274 0
vsize: 5260
[startup+40.0018 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 989 0 0 0 3994 3 0 0 25 0 1 0 420491194 5521408 967 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1348 967 603 41 0 1307 0
vsize: 5392
[startup+50.003 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1022 0 0 0 4994 4 0 0 25 0 1 0 420491194 5656576 1000 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1381 1000 603 41 0 1340 0
vsize: 5524
[startup+60.0027 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1037 0 0 0 5993 4 0 0 25 0 1 0 420491194 5791744 1015 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1414 1015 603 41 0 1373 0
vsize: 5656
[startup+70.0029 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1037 0 0 0 6993 4 0 0 25 0 1 0 420491194 5787648 1015 4294967295 134512640 134672761 3221224624 3221223792 134560929 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.003 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1127 0 0 0 7993 4 0 0 25 0 1 0 420491194 6193152 1105 4294967295 134512640 134672761 3221224624 3221223808 134558925 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.0037 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1145 0 0 0 8993 4 0 0 25 0 1 0 420491194 6193152 1123 4294967295 134512640 134672761 3221224624 3221223792 134560996 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.003 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1152 0 0 0 9993 4 0 0 25 0 1 0 420491194 6193152 1130 4294967295 134512640 134672761 3221224624 3221223792 134560858 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.003 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1153 0 0 0 10994 4 0 0 25 0 1 0 420491194 6193152 1131 4294967295 134512640 134672761 3221224624 3221223728 134560054 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.004 s]
Raw data (loadavg): 0.99 0.99 0.89 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1191 0 0 0 11994 4 0 0 25 0 1 0 420491194 6463488 1169 4294967295 134512640 134672761 3221224624 3221223760 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1578 1169 603 41 0 1537 0
vsize: 6312
[startup+130.004 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1229 0 0 0 12994 4 0 0 25 0 1 0 420491194 6598656 1207 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1611 1207 603 41 0 1570 0
vsize: 6444
[startup+140.005 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1245 0 0 0 13994 4 0 0 25 0 1 0 420491194 6598656 1223 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.005 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1294 0 0 0 14994 4 0 0 25 0 1 0 420491194 6864896 1272 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1676 1272 603 41 0 1635 0
vsize: 6704
[startup+160.005 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1322 0 0 0 15994 4 0 0 25 0 1 0 420491194 7000064 1300 4294967295 134512640 134672761 3221224624 3221223792 134559675 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.005 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1347 0 0 0 16994 4 0 0 25 0 1 0 420491194 7135232 1325 4294967295 134512640 134672761 3221224624 3221223672 1075349627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1742 1325 603 41 0 1701 0
vsize: 6968
[startup+180.006 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1427 0 0 0 17994 5 0 0 25 0 1 0 420491194 7405568 1405 4294967295 134512640 134672761 3221224624 3221223748 134566100 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.007 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1427 0 0 0 18994 5 0 0 25 0 1 0 420491194 7405568 1405 4294967295 134512640 134672761 3221224624 3221223728 134560405 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.007 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1443 0 0 0 19994 5 0 0 25 0 1 0 420491194 7553024 1421 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.007 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1459 0 0 0 20994 5 0 0 25 0 1 0 420491194 7553024 1437 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1437 603 41 0 1803 0
vsize: 7376
[startup+220.007 s]
Raw data (loadavg): 0.99 0.99 0.90 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1466 0 0 0 21994 5 0 0 25 0 1 0 420491194 7553024 1444 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1444 603 41 0 1803 0
vsize: 7376
[startup+230.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1467 0 0 0 22995 5 0 0 25 0 1 0 420491194 7553024 1445 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1844 1445 603 41 0 1803 0
vsize: 7376
[startup+240.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1478 0 0 0 23995 5 0 0 25 0 1 0 420491194 7684096 1456 4294967295 134512640 134672761 3221224624 3221223808 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1876 1456 603 41 0 1835 0
vsize: 7504
[startup+250.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1487 0 0 0 24995 5 0 0 25 0 1 0 420491194 7684096 1465 4294967295 134512640 134672761 3221224624 3221223768 134560553 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1576 0 0 0 25995 5 0 0 25 0 1 0 420491194 8093696 1554 4294967295 134512640 134672761 3221224624 3221223808 134559594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1976 1554 603 41 0 1935 0
vsize: 7904
[startup+270.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1579 0 0 0 26995 5 0 0 25 0 1 0 420491194 8093696 1557 4294967295 134512640 134672761 3221224624 3221223792 134561014 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1583 0 0 0 27995 5 0 0 25 0 1 0 420491194 8093696 1561 4294967295 134512640 134672761 3221224624 3221223728 134554642 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1627 0 0 0 28995 5 0 0 25 0 1 0 420491194 8228864 1605 4294967295 134512640 134672761 3221224624 3221223792 134561198 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1651 0 0 0 29995 5 0 0 25 0 1 0 420491194 8364032 1629 4294967295 134512640 134672761 3221224624 3221223808 134559324 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1657 0 0 0 30995 5 0 0 25 0 1 0 420491194 8499200 1635 4294967295 134512640 134672761 3221224624 3221223792 134561375 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.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1657 0 0 0 31996 5 0 0 25 0 1 0 420491194 8499200 1635 4294967295 134512640 134672761 3221224624 3221223792 134561156 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1657 0 0 0 32996 5 0 0 25 0 1 0 420491194 8499200 1635 4294967295 134512640 134672761 3221224624 3221223792 134561218 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.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1666 0 0 0 33996 5 0 0 25 0 1 0 420491194 8499200 1644 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2075 1644 603 41 0 2034 0
vsize: 8300
[startup+350.011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1689 0 0 0 34996 5 0 0 25 0 1 0 420491194 8646656 1667 4294967295 134512640 134672761 3221224624 3221223792 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.011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1698 0 0 0 35996 5 0 0 25 0 1 0 420491194 8646656 1676 4294967295 134512640 134672761 3221224624 3221223776 134565212 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.011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1712 0 0 0 36996 6 0 0 25 0 1 0 420491194 8646656 1690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2111 1690 603 41 0 2070 0
vsize: 8444
[startup+380.011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1739 0 0 0 37996 6 0 0 25 0 1 0 420491194 8781824 1717 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2144 1717 603 41 0 2103 0
vsize: 8576
[startup+390.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1757 0 0 0 38995 6 0 0 25 0 1 0 420491194 8921088 1735 4294967295 134512640 134672761 3221224624 3221223776 134561244 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.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1783 0 0 0 39996 6 0 0 25 0 1 0 420491194 9056256 1761 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2211 1761 603 41 0 2170 0
vsize: 8844
[startup+410.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1811 0 0 0 40995 6 0 0 25 0 1 0 420491194 9179136 1789 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1789 603 41 0 2200 0
vsize: 8964
[startup+420.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1815 0 0 0 41996 6 0 0 25 0 1 0 420491194 9179136 1793 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1793 603 41 0 2200 0
vsize: 8964
[startup+430.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1815 0 0 0 42996 6 0 0 25 0 1 0 420491194 9179136 1793 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1793 603 41 0 2200 0
vsize: 8964
[startup+440.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1822 0 0 0 43996 6 0 0 25 0 1 0 420491194 9179136 1800 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2241 1800 603 41 0 2200 0
vsize: 8964
[startup+450.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1841 0 0 0 44996 6 0 0 25 0 1 0 420491194 9314304 1819 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2274 1819 603 41 0 2233 0
vsize: 9096
[startup+460.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1841 0 0 0 45997 6 0 0 25 0 1 0 420491194 9285632 1819 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2267 1819 603 41 0 2226 0
vsize: 9068
[startup+470.015 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1856 0 0 0 46997 6 0 0 25 0 1 0 420491194 9285632 1834 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2267 1834 603 41 0 2226 0
vsize: 9068
[startup+480.015 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1866 0 0 0 47997 6 0 0 25 0 1 0 420491194 9428992 1844 4294967295 134512640 134672761 3221224624 3221223792 134561001 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.015 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1874 0 0 0 48997 6 0 0 25 0 1 0 420491194 9428992 1852 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1852 603 41 0 2261 0
vsize: 9208
[startup+500.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1879 0 0 0 49997 6 0 0 25 0 1 0 420491194 9428992 1857 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1857 603 41 0 2261 0
vsize: 9208
[startup+510.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1879 0 0 0 50997 6 0 0 25 0 1 0 420491194 9428992 1857 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1857 603 41 0 2261 0
vsize: 9208
[startup+520.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1887 0 0 0 51998 6 0 0 25 0 1 0 420491194 9428992 1865 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1865 603 41 0 2261 0
vsize: 9208
[startup+530.016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1888 0 0 0 52998 6 0 0 25 0 1 0 420491194 9428992 1866 4294967295 134512640 134672761 3221224624 3221223776 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1866 603 41 0 2261 0
vsize: 9208
[startup+540.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1899 0 0 0 53998 6 0 0 25 0 1 0 420491194 9428992 1877 4294967295 134512640 134672761 3221224624 3221223728 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1877 603 41 0 2261 0
vsize: 9208
[startup+550.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1900 0 0 0 54998 6 0 0 25 0 1 0 420491194 9428992 1878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2302 1878 603 41 0 2261 0
vsize: 9208
[startup+560.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1914 0 0 0 55998 6 0 0 25 0 1 0 420491194 9564160 1892 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2335 1892 603 41 0 2294 0
vsize: 9340
[startup+570.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1928 0 0 0 56999 6 0 0 25 0 1 0 420491194 9555968 1906 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2333 1906 603 41 0 2292 0
vsize: 9332
[startup+580.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1930 0 0 0 57999 6 0 0 25 0 1 0 420491194 9555968 1908 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2333 1908 603 41 0 2292 0
vsize: 9332
[startup+590.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 1966 0 0 0 58999 7 0 0 25 0 1 0 420491194 9691136 1944 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2366 1944 603 41 0 2325 0
vsize: 9464
[startup+600.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2004 0 0 0 59998 7 0 0 25 0 1 0 420491194 9826304 1982 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2399 1982 603 41 0 2358 0
vsize: 9596
[startup+610.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2004 0 0 0 60998 7 0 0 25 0 1 0 420491194 9826304 1982 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2399 1982 603 41 0 2358 0
vsize: 9596
[startup+620.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2016 0 0 0 61998 7 0 0 25 0 1 0 420491194 9961472 1994 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2432 1994 603 41 0 2391 0
vsize: 9728
[startup+630.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2021 0 0 0 62998 7 0 0 25 0 1 0 420491194 9961472 1999 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2432 1999 603 41 0 2391 0
vsize: 9728
[startup+640.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2021 0 0 0 63998 7 0 0 25 0 1 0 420491194 9961472 1999 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2432 1999 603 41 0 2391 0
vsize: 9728
[startup+650.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2024 0 0 0 64999 7 0 0 25 0 1 0 420491194 9961472 2002 4294967295 134512640 134672761 3221224624 3221223728 134555105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2432 2002 603 41 0 2391 0
vsize: 9728
[startup+660.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2037 0 0 0 65999 7 0 0 25 0 1 0 420491194 10104832 2015 4294967295 134512640 134672761 3221224624 3221223808 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2015 603 41 0 2426 0
vsize: 9868
[startup+670.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2039 0 0 0 66999 7 0 0 25 0 1 0 420491194 10104832 2017 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2017 603 41 0 2426 0
vsize: 9868
[startup+680.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2041 0 0 0 67999 7 0 0 25 0 1 0 420491194 10104832 2019 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2019 603 41 0 2426 0
vsize: 9868
[startup+690.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2047 0 0 0 68999 7 0 0 25 0 1 0 420491194 10104832 2025 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2025 603 41 0 2426 0
vsize: 9868
[startup+700.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2052 0 0 0 69999 7 0 0 25 0 1 0 420491194 10104832 2030 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2030 603 41 0 2426 0
vsize: 9868
[startup+710.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2056 0 0 0 71000 7 0 0 25 0 1 0 420491194 10104832 2034 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2034 603 41 0 2426 0
vsize: 9868
[startup+720.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2059 0 0 0 72000 7 0 0 25 0 1 0 420491194 10104832 2037 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2037 603 41 0 2426 0
vsize: 9868
[startup+730.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2063 0 0 0 73000 7 0 0 25 0 1 0 420491194 10104832 2041 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2041 603 41 0 2426 0
vsize: 9868
[startup+740.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2064 0 0 0 74000 7 0 0 25 0 1 0 420491194 10104832 2042 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2042 603 41 0 2426 0
vsize: 9868
[startup+750.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2064 0 0 0 75000 7 0 0 25 0 1 0 420491194 10104832 2042 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2467 2042 603 41 0 2426 0
vsize: 9868
[startup+760.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2109 0 0 0 76001 7 0 0 25 0 1 0 420491194 10375168 2087 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2533 2087 603 41 0 2492 0
vsize: 10132
[startup+770.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2109 0 0 0 77001 7 0 0 25 0 1 0 420491194 10354688 2087 4294967295 134512640 134672761 3221224624 3221223808 134558684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2528 2087 603 41 0 2487 0
vsize: 10112
[startup+780.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2110 0 0 0 78001 7 0 0 25 0 1 0 420491194 10293248 2088 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2513 2088 603 41 0 2472 0
vsize: 10052
[startup+790.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2110 0 0 0 79001 7 0 0 25 0 1 0 420491194 10244096 2082 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2501 2082 603 41 0 2460 0
vsize: 10004
[startup+800.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2119 0 0 0 80001 7 0 0 25 0 1 0 420491194 10379264 2091 4294967295 134512640 134672761 3221224624 3221223728 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2091 603 41 0 2493 0
vsize: 10136
[startup+810.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2122 0 0 0 81001 7 0 0 25 0 1 0 420491194 10379264 2094 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2094 603 41 0 2493 0
vsize: 10136
[startup+820.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2124 0 0 0 82002 7 0 0 25 0 1 0 420491194 10379264 2096 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2096 603 41 0 2493 0
vsize: 10136
[startup+830.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2125 0 0 0 83002 7 0 0 25 0 1 0 420491194 10379264 2097 4294967295 134512640 134672761 3221224624 3221223808 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2097 603 41 0 2493 0
vsize: 10136
[startup+840.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2128 0 0 0 84002 7 0 0 25 0 1 0 420491194 10379264 2100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2100 603 41 0 2493 0
vsize: 10136
[startup+850.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2129 0 0 0 85002 7 0 0 25 0 1 0 420491194 10379264 2101 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2101 603 41 0 2493 0
vsize: 10136
[startup+860.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2138 0 0 0 86002 7 0 0 25 0 1 0 420491194 10379264 2110 4294967295 134512640 134672761 3221224624 3221223728 134555592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2110 603 41 0 2493 0
vsize: 10136
[startup+870.025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2140 0 0 0 87003 7 0 0 25 0 1 0 420491194 10379264 2112 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2112 603 41 0 2493 0
vsize: 10136
[startup+880.025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2140 0 0 0 88003 7 0 0 25 0 1 0 420491194 10379264 2112 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2112 603 41 0 2493 0
vsize: 10136
[startup+890.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2142 0 0 0 89003 7 0 0 25 0 1 0 420491194 10379264 2114 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2114 603 41 0 2493 0
vsize: 10136
[startup+900.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2143 0 0 0 90003 7 0 0 25 0 1 0 420491194 10379264 2115 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2534 2115 603 41 0 2493 0
vsize: 10136
[startup+910.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2169 0 0 0 91003 7 0 0 25 0 1 0 420491194 10514432 2141 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2567 2141 603 41 0 2526 0
vsize: 10268
[startup+920.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2248 0 0 0 92002 8 0 0 25 0 1 0 420491194 10784768 2220 4294967295 134512640 134672761 3221224624 3221223808 134558433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2633 2220 603 41 0 2592 0
vsize: 10532
[startup+930.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2284 0 0 0 93003 8 0 0 25 0 1 0 420491194 10919936 2256 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2256 603 41 0 2625 0
vsize: 10664
[startup+940.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2288 0 0 0 94003 8 0 0 25 0 1 0 420491194 10919936 2260 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2260 603 41 0 2625 0
vsize: 10664
[startup+950.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2288 0 0 0 95003 8 0 0 25 0 1 0 420491194 10919936 2260 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2260 603 41 0 2625 0
vsize: 10664
[startup+960.029 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2289 0 0 0 96003 8 0 0 25 0 1 0 420491194 10919936 2261 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2261 603 41 0 2625 0
vsize: 10664
[startup+970.029 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2290 0 0 0 97003 8 0 0 25 0 1 0 420491194 10919936 2262 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+980.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2290 0 0 0 98004 8 0 0 25 0 1 0 420491194 10919936 2262 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+990.031 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2290 0 0 0 99004 8 0 0 25 0 1 0 420491194 10919936 2262 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2262 603 41 0 2625 0
vsize: 10664
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 100004 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 101004 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 102005 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 103005 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 104005 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223808 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 105005 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223792 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2291 0 0 0 106005 8 0 0 25 0 1 0 420491194 10919936 2263 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2263 603 41 0 2625 0
vsize: 10664
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2292 0 0 0 107006 8 0 0 25 0 1 0 420491194 10919936 2264 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2264 603 41 0 2625 0
vsize: 10664
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2297 0 0 0 108006 8 0 0 25 0 1 0 420491194 11067392 2269 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2269 603 41 0 2661 0
vsize: 10808
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2303 0 0 0 109006 8 0 0 25 0 1 0 420491194 11067392 2275 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2275 603 41 0 2661 0
vsize: 10808
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2308 0 0 0 110006 8 0 0 25 0 1 0 420491194 11067392 2280 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2308 0 0 0 111006 8 0 0 25 0 1 0 420491194 11067392 2280 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2308 0 0 0 112007 8 0 0 25 0 1 0 420491194 11067392 2280 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2308 0 0 0 113007 8 0 0 25 0 1 0 420491194 11067392 2280 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2308 0 0 0 114007 8 0 0 25 0 1 0 420491194 11067392 2280 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2280 603 41 0 2661 0
vsize: 10808
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 115007 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 116007 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 117008 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223728 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 118008 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 119008 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 32502
Raw data (stat): 32502 (minisat+) R 32501 30854 30853 0 -1 0 2318 0 0 0 120008 8 0 0 25 0 1 0 420491194 11067392 2290 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2702 2290 603 41 0 2661 0
vsize: 10808
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.99 0.91 1/54 32502
Raw data (stat): 32502 (minisat+) Z 32501 30854 30853 0 -1 12 2320 0 0 0 120008 8 0 0 25 0 1 0 420491194 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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