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-chnl30_35_pb.cnf.cr.opb
MD5SUMb1c5adb5438ceaf1c654cfedb79b695e
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 36
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.06099
Number of variables2100
Total number of constraints130
Number of constraints which are clauses70
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint35

Trace number 4748 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        911488 kB
Buffers:         26052 kB
Cached:          77376 kB
SwapCached:          0 kB
Active:          33648 kB
Inactive:        72680 kB
HighTotal:      131008 kB
HighFree:        49924 kB
LowTotal:       903652 kB
LowFree:        861564 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11180 kB
Committed_AS:    63756 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:30:12 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 104 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 130 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................
c ---[  59]---> BDD-cost:   67
c ---[  58]---> BDD-cost:   67
c ---[  57]---> BDD-cost:   67
c ---[  56]---> BDD-cost:   67
c ---[  55]---> BDD-cost:   67
c ---[  54]---> BDD-cost:   67
c ---[  53]---> BDD-cost:   67
c ---[  52]---> BDD-cost:   67
c ---[  51]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   67
c ---[  49]---> BDD-cost:   67
c ---[  48]---> BDD-cost:   67
c ---[  47]---> BDD-cost:   67
c ---[  46]---> BDD-cost:   67
c ---[  45]---> BDD-cost:   67
c ---[  44]---> BDD-cost:   67
c ---[  43]---> BDD-cost:   67
c ---[  42]---> BDD-cost:   67
c ---[  41]---> BDD-cost:   67
c ---[  40]---> BDD-cost:   67
c ---[  39]---> BDD-cost:   67
c ---[  38]---> BDD-cost:   67
c ---[  37]---> BDD-cost:   67
c ---[  36]---> BDD-cost:   67
c ---[  35]---> BDD-cost:   67
c ---[  34]---> BDD-cost:   67
c ---[  33]---> BDD-cost:   67
c ---[  32]---> BDD-cost:   67
c ---[  31]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   67
c ---[  29]---> BDD-cost:   67
c ---[  28]---> BDD-cost:   67
c ---[  27]---> BDD-cost:   67
c ---[  26]---> BDD-cost:   67
c ---[  25]---> BDD-cost:   67
c ---[  24]---> BDD-cost:   67
c ---[  23]---> BDD-cost:   67
c ---[  22]---> BDD-cost:   67
c ---[  21]---> BDD-cost:   67
c ---[  20]---> BDD-cost:   67
c ---[  19]---> BDD-cost:   67
c ---[  18]---> BDD-cost:   67
c ---[  17]---> BDD-cost:   67
c ---[  16]---> BDD-cost:   67
c ---[  15]---> BDD-cost:   67
c ---[  14]---> BDD-cost:   67
c ---[  13]---> BDD-cost:   67
c ---[  12]---> BDD-cost:   67
c ---[  11]---> BDD-cost:   67
c ---[  10]---> BDD-cost:   67
c ---[   9]---> BDD-cost:   67
c ---[   8]---> BDD-cost:   67
c ---[   7]---> BDD-cost:   67
c ---[   6]---> BDD-cost:   67
c ---[   5]---> BDD-cost:   67
c ---[   4]---> BDD-cost:   67
c ---[   3]---> BDD-cost:   67
c ---[   2]---> BDD-cost:   67
c ---[   1]---> BDD-cost:   67
c ---[   0]---> BDD-cost:   67
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10030    28020 |    3343       0        0     nan |  0.000 % |
c |       105 |   10030    28020 |    3677     105    11655   111.0 |  0.980 % |
c |       257 |   10030    28020 |    4045     257    29832   116.1 |  0.980 % |
c |       483 |   10030    28020 |    4449     483    70240   145.4 |  0.980 % |
c |       822 |   10030    28020 |    4894     822   128798   156.7 |  0.980 % |
c |      1332 |   10030    28020 |    5383    1332   212600   159.6 |  0.980 % |
c |      2091 |   10030    28020 |    5922    2091   359695   172.0 |  0.980 % |
c |      3231 |   10030    28020 |    6514    3231   581665   180.0 |  0.980 % |
c |      4941 |   10030    28020 |    7166    4941  1128031   228.3 |  0.980 % |
c |      7504 |   10030    28020 |    7882    7504  1889344   251.8 |  0.980 % |
c |     11348 |   10030    28020 |    8670    6199  1605192   258.9 |  0.980 % |
c |     17117 |   10030    28020 |    9537    6488  1486146   229.1 |  0.980 % |
c |     25767 |   10030    28020 |   10491    9195  2320409   252.4 |  0.980 % |
c |     38743 |   10030    28020 |   11540    9205  1749321   190.0 |  0.980 % |
c |     58205 |   10030    28020 |   12695    7890  2211413   280.3 |  0.980 % |
c |     87397 |   10030    28020 |   13964    8204  2185785   266.4 |  0.980 % |
c |    131187 |   10030    28020 |   15360   10994  2976111   270.7 |  0.980 % |
c |    196872 |   10030    28020 |   16897   18139  5203446   286.9 |  0.980 % |
c |    295406 |   10030    28020 |   18586   16345  8504574   520.3 |  0.980 % |
#### 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.89 0.93 0.87 2/55 1279
Raw data (stat): 1279 (runsolver) R 1278 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 355985641 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.91 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 3006 0 0 0 992 6 0 0 25 0 1 0 355985641 13910016 2984 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3396 2984 603 41 0 3355 0
vsize: 13584
[startup+20.0007 s]
Raw data (loadavg): 0.92 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 3532 0 0 0 1991 8 0 0 25 0 1 0 355985641 16068608 3510 4294967295 134512640 134672761 3221224624 3221223728 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3923 3510 603 41 0 3882 0
vsize: 15692
[startup+30.0014 s]
Raw data (loadavg): 0.93 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 3772 0 0 0 2991 8 0 0 25 0 1 0 355985641 17145856 3750 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4186 3750 603 41 0 4145 0
vsize: 16744
[startup+40.0011 s]
Raw data (loadavg): 0.94 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 4051 0 0 0 3990 9 0 0 25 0 1 0 355985641 18231296 4029 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4451 4029 603 41 0 4410 0
vsize: 17804
[startup+50.0012 s]
Raw data (loadavg): 0.95 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 4337 0 0 0 4989 10 0 0 25 0 1 0 355985641 19447808 4315 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4748 4315 603 41 0 4707 0
vsize: 18992
[startup+60.0014 s]
Raw data (loadavg): 0.96 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 4338 0 0 0 5989 10 0 0 25 0 1 0 355985641 19447808 4316 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4748 4316 603 41 0 4707 0
vsize: 18992
[startup+70.0011 s]
Raw data (loadavg): 0.96 0.94 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 4338 0 0 0 6989 10 0 0 25 0 1 0 355985641 19447808 4316 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4748 4316 603 41 0 4707 0
vsize: 18992
[startup+80.0018 s]
Raw data (loadavg): 0.97 0.95 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 4400 0 0 0 7989 11 0 0 25 0 1 0 355985641 19718144 4378 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 4378 603 41 0 4773 0
vsize: 19256
[startup+90.0014 s]
Raw data (loadavg): 0.97 0.95 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5241 0 0 0 8987 13 0 0 25 0 1 0 355985641 23093248 5219 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5638 5219 603 41 0 5597 0
vsize: 22552
[startup+100.001 s]
Raw data (loadavg): 0.98 0.95 0.88 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5319 0 0 0 9987 13 0 0 25 0 1 0 355985641 23502848 5297 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5297 603 41 0 5697 0
vsize: 22952
[startup+110.002 s]
Raw data (loadavg): 0.98 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5333 0 0 0 10987 13 0 0 25 0 1 0 355985641 23502848 5311 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5311 603 41 0 5697 0
vsize: 22952
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5614 0 0 0 11985 15 0 0 25 0 1 0 355985641 24723456 5592 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6036 5592 603 41 0 5995 0
vsize: 24144
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5833 0 0 0 12985 15 0 0 25 0 1 0 355985641 25677824 5811 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6269 5811 603 41 0 6228 0
vsize: 25076
[startup+140.003 s]
Raw data (loadavg): 0.99 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5834 0 0 0 13985 15 0 0 25 0 1 0 355985641 25677824 5812 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6269 5812 603 41 0 6228 0
vsize: 25076
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 14985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+160.002 s]
Raw data (loadavg): 0.99 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 15985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+170.002 s]
Raw data (loadavg): 0.99 0.95 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 16985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 17985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 18985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 5942 0 0 0 19985 16 0 0 25 0 1 0 355985641 26079232 5920 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.89 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6407 0 0 0 20984 17 0 0 25 0 1 0 355985641 28172288 6385 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6878 6385 603 41 0 6837 0
vsize: 27512
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6408 0 0 0 21984 18 0 0 25 0 1 0 355985641 28172288 6386 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6878 6386 603 41 0 6837 0
vsize: 27512
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6409 0 0 0 22984 18 0 0 25 0 1 0 355985641 28172288 6387 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6878 6387 603 41 0 6837 0
vsize: 27512
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6471 0 0 0 23983 18 0 0 25 0 1 0 355985641 28442624 6449 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6944 6449 603 41 0 6903 0
vsize: 27776
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6505 0 0 0 24983 18 0 0 25 0 1 0 355985641 28577792 6483 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6977 6483 603 41 0 6936 0
vsize: 27908
[startup+260.003 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6505 0 0 0 25983 19 0 0 25 0 1 0 355985641 28577792 6483 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6977 6483 603 41 0 6936 0
vsize: 27908
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 6715 0 0 0 26983 19 0 0 25 0 1 0 355985641 29388800 6693 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7175 6693 603 41 0 7134 0
vsize: 28700
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7144 0 0 0 27982 20 0 0 25 0 1 0 355985641 31145984 7122 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7604 7122 603 41 0 7563 0
vsize: 30416
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7154 0 0 0 28983 20 0 0 25 0 1 0 355985641 31293440 7132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7154 0 0 0 29982 20 0 0 25 0 1 0 355985641 31293440 7132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7154 0 0 0 30982 20 0 0 25 0 1 0 355985641 31293440 7132 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7157 0 0 0 31982 20 0 0 25 0 1 0 355985641 31293440 7135 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7640 7135 603 41 0 7599 0
vsize: 30560
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7158 0 0 0 32982 20 0 0 25 0 1 0 355985641 31293440 7136 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7640 7136 603 41 0 7599 0
vsize: 30560
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 7792 0 0 0 33980 23 0 0 25 0 1 0 355985641 33849344 7770 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8264 7770 603 41 0 8223 0
vsize: 33056
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8030 0 0 0 34980 23 0 0 25 0 1 0 355985641 34795520 8008 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8030 0 0 0 35980 23 0 0 25 0 1 0 355985641 34795520 8008 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8030 0 0 0 36980 23 0 0 25 0 1 0 355985641 34795520 8008 4294967295 134512640 134672761 3221224624 3221223728 134555096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8204 0 0 0 37979 24 0 0 25 0 1 0 355985641 35471360 8182 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8660 8182 603 41 0 8619 0
vsize: 34640
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8256 0 0 0 38979 24 0 0 25 0 1 0 355985641 35741696 8234 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8726 8234 603 41 0 8685 0
vsize: 34904
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8256 0 0 0 39980 24 0 0 25 0 1 0 355985641 35741696 8234 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8726 8234 603 41 0 8685 0
vsize: 34904
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8266 0 0 0 40980 24 0 0 25 0 1 0 355985641 35741696 8244 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8726 8244 603 41 0 8685 0
vsize: 34904
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8604 0 0 0 41979 26 0 0 25 0 1 0 355985641 37105664 8582 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9059 8582 603 41 0 9018 0
vsize: 36236
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8615 0 0 0 42979 26 0 0 25 0 1 0 355985641 37302272 8593 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8615 0 0 0 43979 26 0 0 25 0 1 0 355985641 37302272 8593 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8615 0 0 0 44979 26 0 0 25 0 1 0 355985641 37302272 8593 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 8775 0 0 0 45979 26 0 0 25 0 1 0 355985641 37834752 8753 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9237 8753 603 41 0 9196 0
vsize: 36948
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9056 0 0 0 46978 27 0 0 25 0 1 0 355985641 39051264 9034 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9534 9034 603 41 0 9493 0
vsize: 38136
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9056 0 0 0 47978 27 0 0 25 0 1 0 355985641 39051264 9034 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9534 9034 603 41 0 9493 0
vsize: 38136
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9056 0 0 0 48978 28 0 0 25 0 1 0 355985641 39051264 9034 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9534 9034 603 41 0 9493 0
vsize: 38136
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9328 0 0 0 49977 28 0 0 25 0 1 0 355985641 40132608 9306 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 9306 603 41 0 9757 0
vsize: 39192
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9329 0 0 0 50977 28 0 0 25 0 1 0 355985641 40132608 9307 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 9307 603 41 0 9757 0
vsize: 39192
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9329 0 0 0 51978 28 0 0 25 0 1 0 355985641 40132608 9307 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 9307 603 41 0 9757 0
vsize: 39192
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9330 0 0 0 52978 28 0 0 25 0 1 0 355985641 40132608 9308 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 9308 603 41 0 9757 0
vsize: 39192
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9330 0 0 0 53978 28 0 0 25 0 1 0 355985641 40132608 9308 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9798 9308 603 41 0 9757 0
vsize: 39192
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9358 0 0 0 54978 29 0 0 25 0 1 0 355985641 40284160 9336 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9358 0 0 0 55978 29 0 0 25 0 1 0 355985641 40284160 9336 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9358 0 0 0 56978 29 0 0 25 0 1 0 355985641 40284160 9336 4294967295 134512640 134672761 3221224624 3221223728 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9358 0 0 0 57978 29 0 0 25 0 1 0 355985641 40284160 9336 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 9358 0 0 0 58978 29 0 0 25 0 1 0 355985641 40284160 9336 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 10222 0 0 0 59976 31 0 0 25 0 1 0 355985641 43925504 10200 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10724 10200 603 41 0 10683 0
vsize: 42896
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 10232 0 0 0 60976 31 0 0 25 0 1 0 355985641 43925504 10210 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10724 10210 603 41 0 10683 0
vsize: 42896
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 10802 0 0 0 61975 33 0 0 25 0 1 0 355985641 46223360 10780 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11285 10780 603 41 0 11244 0
vsize: 45140
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 11850 0 0 0 62973 35 0 0 25 0 1 0 355985641 50548736 11828 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12341 11828 603 41 0 12300 0
vsize: 49364
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12109 0 0 0 63972 35 0 0 25 0 1 0 355985641 51630080 12087 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 12087 603 41 0 12564 0
vsize: 50420
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12110 0 0 0 64972 35 0 0 25 0 1 0 355985641 51630080 12088 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 12088 603 41 0 12564 0
vsize: 50420
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12110 0 0 0 65973 35 0 0 25 0 1 0 355985641 51630080 12088 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 12088 603 41 0 12564 0
vsize: 50420
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12110 0 0 0 66973 35 0 0 25 0 1 0 355985641 51630080 12088 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 12088 603 41 0 12564 0
vsize: 50420
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12110 0 0 0 67973 35 0 0 25 0 1 0 355985641 51630080 12088 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12605 12088 603 41 0 12564 0
vsize: 50420
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 68972 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 69972 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223808 134559482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 70972 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 71973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+730.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 72973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+740.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 73973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 74973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 75973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+770.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 12550 0 0 0 76973 36 0 0 25 0 1 0 355985641 53518336 12528 4294967295 134512640 134672761 3221224624 3221223808 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13066 12528 603 41 0 13025 0
vsize: 52264
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13374 0 0 0 77972 39 0 0 25 0 1 0 355985641 56909824 13352 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13894 13352 603 41 0 13853 0
vsize: 55576
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13598 0 0 0 78971 39 0 0 25 0 1 0 355985641 57720832 13576 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14092 13576 603 41 0 14051 0
vsize: 56368
[startup+800.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13598 0 0 0 79972 39 0 0 25 0 1 0 355985641 57720832 13576 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14092 13576 603 41 0 14051 0
vsize: 56368
[startup+810.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13598 0 0 0 80972 39 0 0 25 0 1 0 355985641 57720832 13576 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14092 13576 603 41 0 14051 0
vsize: 56368
[startup+820.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13599 0 0 0 81972 39 0 0 25 0 1 0 355985641 57720832 13577 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14092 13577 603 41 0 14051 0
vsize: 56368
[startup+830.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 13951 0 0 0 82971 40 0 0 25 0 1 0 355985641 59207680 13929 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14455 13929 603 41 0 14414 0
vsize: 57820
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 83970 41 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+850.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 84970 41 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223808 134559424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 85970 41 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 86970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 87970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 88970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+900.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 89970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+910.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 90970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 91970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 92970 42 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14789 0 0 0 93970 43 0 0 25 0 1 0 355985641 62586880 14767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14767 603 41 0 15239 0
vsize: 61120
[startup+950.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 94970 43 0 0 25 0 1 0 355985641 62586880 14769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14769 603 41 0 15239 0
vsize: 61120
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 95970 43 0 0 25 0 1 0 355985641 62586880 14769 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14769 603 41 0 15239 0
vsize: 61120
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 96970 43 0 0 25 0 1 0 355985641 62586880 14769 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15280 14769 603 41 0 15239 0
vsize: 61120
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 97970 43 0 0 25 0 1 0 355985641 62521344 14755 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15264 14755 603 41 0 15223 0
vsize: 61056
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 98970 43 0 0 25 0 1 0 355985641 62521344 14755 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15264 14755 603 41 0 15223 0
vsize: 61056
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 99970 43 0 0 25 0 1 0 355985641 62521344 14755 4294967295 134512640 134672761 3221224624 3221223728 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15264 14755 603 41 0 15223 0
vsize: 61056
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 100970 43 0 0 25 0 1 0 355985641 62521344 14755 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15264 14755 603 41 0 15223 0
vsize: 61056
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 101970 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 102970 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 103970 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 104970 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 105971 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 106971 43 0 0 25 0 1 0 355985641 62509056 14752 4294967295 134512640 134672761 3221224624 3221223712 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15261 14752 603 41 0 15220 0
vsize: 61044
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 107971 43 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 108971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 109971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 110971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 111971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 112971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14791 0 0 0 113971 44 0 0 25 0 1 0 355985641 62500864 14750 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14750 603 41 0 15218 0
vsize: 61036
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 114971 44 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 115970 44 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 116970 45 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 117971 45 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 118971 45 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1279
Raw data (stat): 1279 (minisat+) R 1278 30927 30926 0 -1 0 14792 0 0 0 119971 45 0 0 25 0 1 0 355985641 62500864 14751 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14751 603 41 0 15218 0
vsize: 61036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 1279
Raw data (stat): 1279 (minisat+) Z 1278 30927 30926 0 -1 12 14794 0 0 0 119971 48 0 0 25 0 1 0 355985641 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.04
CPU time (s): 1200.19
CPU user time (s): 1199.71
CPU system time (s): 0.480926
CPU usage (%): 100.013
Max. virtual memory (Kb): 61120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####