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_31_pb.cnf.cr.opb
MD5SUM79bafd08ddd684356ab9abc8fabf88a7
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 32
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.05399
Number of variables1860
Total number of constraints122
Number of constraints which are clauses62
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 constraint31

Trace number 6101 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 03:26:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4523 boxname=wulflinc12 idbench=11 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  79bafd08ddd684356ab9abc8fabf88a7  /oldhome/oroussel/tmp/wulflinc12/normalized-chnl30_31_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc12/normalized-chnl30_31_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc12/normalized-chnl30_31_pb.cnf.cr.opb
IDLAUNCH: 4523
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        901804 kB
Buffers:         35872 kB
Cached:          77672 kB
SwapCached:         16 kB
Active:          61768 kB
Inactive:        54628 kB
HighTotal:      131008 kB
HighFree:        49420 kB
LowTotal:       903652 kB
LowFree:        852384 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10932 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:46:21 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 4523 7 1200.14 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 122 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................
c ---[  59]---> BDD-cost:   59
c ---[  58]---> BDD-cost:   59
c ---[  57]---> BDD-cost:   59
c ---[  56]---> BDD-cost:   59
c ---[  55]---> BDD-cost:   59
c ---[  54]---> BDD-cost:   59
c ---[  53]---> BDD-cost:   59
c ---[  52]---> BDD-cost:   59
c ---[  51]---> BDD-cost:   59
c ---[  50]---> BDD-cost:   59
c ---[  49]---> BDD-cost:   59
c ---[  48]---> BDD-cost:   59
c ---[  47]---> BDD-cost:   59
c ---[  46]---> BDD-cost:   59
c ---[  45]---> BDD-cost:   59
c ---[  44]---> BDD-cost:   59
c ---[  43]---> BDD-cost:   59
c ---[  42]---> BDD-cost:   59
c ---[  41]---> BDD-cost:   59
c ---[  40]---> BDD-cost:   59
c ---[  39]---> BDD-cost:   59
c ---[  38]---> BDD-cost:   59
c ---[  37]---> BDD-cost:   59
c ---[  36]---> BDD-cost:   59
c ---[  35]---> BDD-cost:   59
c ---[  34]---> BDD-cost:   59
c ---[  33]---> BDD-cost:   59
c ---[  32]---> BDD-cost:   59
c ---[  31]---> BDD-cost:   59
c ---[  30]---> BDD-cost:   59
c ---[  29]---> BDD-cost:   59
c ---[  28]---> BDD-cost:   59
c ---[  27]---> BDD-cost:   59
c ---[  26]---> BDD-cost:   59
c ---[  25]---> BDD-cost:   59
c ---[  24]---> BDD-cost:   59
c ---[  23]---> BDD-cost:   59
c ---[  22]---> BDD-cost:   59
c ---[  21]---> BDD-cost:   59
c ---[  20]---> BDD-cost:   59
c ---[  19]---> BDD-cost:   59
c ---[  18]---> BDD-cost:   59
c ---[  17]---> BDD-cost:   59
c ---[  16]---> BDD-cost:   59
c ---[  15]---> BDD-cost:   59
c ---[  14]---> BDD-cost:   59
c ---[  13]---> BDD-cost:   59
c ---[  12]---> BDD-cost:   59
c ---[  11]---> BDD-cost:   59
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   59
c ---[   8]---> BDD-cost:   59
c ---[   7]---> BDD-cost:   59
c ---[   6]---> BDD-cost:   59
c ---[   5]---> BDD-cost:   59
c ---[   4]---> BDD-cost:   59
c ---[   3]---> BDD-cost:   59
c ---[   2]---> BDD-cost:   59
c ---[   1]---> BDD-cost:   59
c ---[   0]---> BDD-cost:   59
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15722    45240 |    5240       0        0     nan |  0.000 % |
c |       101 |   15707    45195 |    5764      95     9893   104.1 |  1.167 % |
c |       251 |   15507    44595 |    6340     139    10415    74.9 |  1.944 % |
c |       476 |   14977    43005 |    6974     137    10409    76.0 |  3.889 % |
c |       813 |   14782    42420 |    7671     385    42592   110.6 |  4.593 % |
c |      1319 |   14687    42135 |    8439     851   114513   134.6 |  4.944 % |
c |      2080 |   14617    41925 |    9282    1589   365540   230.0 |  5.204 % |
c |      3220 |   14117    40425 |   10211    2527   527755   208.8 |  7.056 % |
c |      4929 |   13462    38460 |   11232    3983   797261   200.2 |  9.481 % |
c |      7492 |   13112    37410 |   12355    6387  1348803   211.2 | 10.778 % |
c |     11336 |   12069    34285 |   13591    9792  2074414   211.8 | 14.648 % |
c |     17105 |   11035    31185 |   14950    7849  1726005   219.9 | 18.481 % |
c |     25754 |   10675    30105 |   16445   16377  3740443   228.4 | 19.815 % |
c |     38733 |   10242    28810 |   18089   10590  2384473   225.2 | 21.426 % |
c |     58195 |    9918    27840 |   19898   19385  5320750   274.5 | 22.630 % |
c |     87390 |    9237    25805 |   21888   15078  3636234   241.2 | 25.167 % |
c |    131180 |    8566    23800 |   24077   20158  4918789   244.0 | 27.667 % |
c |    196866 |    8127    22485 |   26485   25127  9722466   386.9 | 29.296 % |
c |    295392 |    7745    21345 |   29133   17059  5330027   312.4 | 30.722 % |
#### 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.84 0.95 0.93 2/54 30947
Raw data (stat): 30947 (runsolver) R 30946 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423115294 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0008 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 1633 0 0 0 994 4 0 0 25 0 1 0 423115294 8351744 1611 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1611 603 41 0 1998 0
vsize: 8156
[startup+20.001 s]
Raw data (loadavg): 0.89 0.95 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 2604 0 0 0 1992 7 0 0 25 0 1 0 423115294 12283904 2582 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2999 2582 603 41 0 2958 0
vsize: 11996
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.95 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 3047 0 0 0 2990 8 0 0 25 0 1 0 423115294 14077952 3025 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3437 3025 603 41 0 3396 0
vsize: 13748
[startup+40.0013 s]
Raw data (loadavg): 0.92 0.95 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 3677 0 0 0 3989 10 0 0 25 0 1 0 423115294 16769024 3655 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4094 3655 603 41 0 4053 0
vsize: 16376
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 4108 0 0 0 4988 11 0 0 25 0 1 0 423115294 18522112 4086 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4522 4086 603 41 0 4481 0
vsize: 18088
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 4422 0 0 0 5987 12 0 0 25 0 1 0 423115294 19734528 4400 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4400 603 41 0 4777 0
vsize: 19272
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 4422 0 0 0 6987 12 0 0 25 0 1 0 423115294 19734528 4400 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4818 4400 603 41 0 4777 0
vsize: 19272
[startup+80.0051 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 5120 0 0 0 7985 14 0 0 25 0 1 0 423115294 22601728 5098 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5518 5098 603 41 0 5477 0
vsize: 22072
[startup+90.005 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 5994 0 0 0 8982 16 0 0 25 0 1 0 423115294 26238976 5972 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6406 5972 603 41 0 6365 0
vsize: 25624
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 5994 0 0 0 9982 17 0 0 25 0 1 0 423115294 26238976 5972 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6406 5972 603 41 0 6365 0
vsize: 25624
[startup+110.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 6050 0 0 0 10981 18 0 0 25 0 1 0 423115294 26509312 6028 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6472 6028 603 41 0 6431 0
vsize: 25888
[startup+120.007 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 6050 0 0 0 11981 18 0 0 25 0 1 0 423115294 26509312 6028 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6472 6028 603 41 0 6431 0
vsize: 25888
[startup+130.008 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 6423 0 0 0 12980 20 0 0 25 0 1 0 423115294 27996160 6401 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6835 6401 603 41 0 6794 0
vsize: 27340
[startup+140.008 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 6883 0 0 0 13978 21 0 0 25 0 1 0 423115294 29876224 6861 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7294 6861 603 41 0 7253 0
vsize: 29176
[startup+150.009 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 6883 0 0 0 14978 21 0 0 25 0 1 0 423115294 29876224 6861 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7294 6861 603 41 0 7253 0
vsize: 29176
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 7293 0 0 0 15977 22 0 0 25 0 1 0 423115294 31612928 7271 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7718 7271 603 41 0 7677 0
vsize: 30872
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8062 0 0 0 16974 25 0 0 25 0 1 0 423115294 34713600 8040 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8475 8040 603 41 0 8434 0
vsize: 33900
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8062 0 0 0 17974 25 0 0 25 0 1 0 423115294 34713600 8040 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8475 8040 603 41 0 8434 0
vsize: 33900
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8067 0 0 0 18974 26 0 0 25 0 1 0 423115294 34713600 8045 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8475 8045 603 41 0 8434 0
vsize: 33900
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 19973 27 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 20972 27 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 21972 27 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 22972 28 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 23971 28 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223728 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+250.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 24971 28 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+260.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 25971 28 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 26971 28 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8528 0 0 0 27971 29 0 0 25 0 1 0 423115294 36605952 8506 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8506 603 41 0 8896 0
vsize: 35748
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 28970 29 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 29970 29 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223560 1075352675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 30970 29 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 31970 30 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 32970 30 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 8530 0 0 0 33969 30 0 0 25 0 1 0 423115294 36605952 8508 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8508 603 41 0 8896 0
vsize: 35748
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 9321 0 0 0 34967 33 0 0 25 0 1 0 423115294 39841792 9299 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9727 9299 603 41 0 9686 0
vsize: 38908
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 9995 0 0 0 35964 35 0 0 25 0 1 0 423115294 42672128 9973 4294967295 134512640 134672761 3221224544 3221223728 134558553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10418 9973 603 41 0 10377 0
vsize: 41672
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 9995 0 0 0 36963 36 0 0 25 0 1 0 423115294 42672128 9973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10418 9973 603 41 0 10377 0
vsize: 41672
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 9995 0 0 0 37963 36 0 0 25 0 1 0 423115294 42672128 9973 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10418 9973 603 41 0 10377 0
vsize: 41672
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 10410 0 0 0 38962 38 0 0 25 0 1 0 423115294 44294144 10388 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10814 10388 603 41 0 10773 0
vsize: 43256
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 11303 0 0 0 39959 40 0 0 25 0 1 0 423115294 47919104 11281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11699 11281 603 41 0 11658 0
vsize: 46796
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12050 0 0 0 40957 42 0 0 25 0 1 0 423115294 51023872 12028 4294967295 134512640 134672761 3221224544 3221223376 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12028 603 41 0 12416 0
vsize: 49828
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 41957 43 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 42956 43 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 43955 44 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 44955 44 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 45955 45 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 46955 45 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223728 134558901 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12052 0 0 0 47955 45 0 0 25 0 1 0 423115294 51023872 12030 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12457 12030 603 41 0 12416 0
vsize: 49828
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12339 0 0 0 48954 46 0 0 25 0 1 0 423115294 52232192 12317 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12752 12317 603 41 0 12711 0
vsize: 51008
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 12668 0 0 0 49952 48 0 0 25 0 1 0 423115294 53567488 12646 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13078 12646 603 41 0 13037 0
vsize: 52312
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 50950 50 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 51950 50 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 52950 51 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 53950 51 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 54949 51 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 55949 52 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 56949 52 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+580.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13438 0 0 0 57949 52 0 0 25 0 1 0 423115294 56799232 13416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13867 13416 603 41 0 13826 0
vsize: 55468
[startup+590.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 13795 0 0 0 58948 53 0 0 25 0 1 0 423115294 58150912 13773 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14197 13773 603 41 0 14156 0
vsize: 56788
[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 14472 0 0 0 59946 54 0 0 25 0 1 0 423115294 60989440 14450 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14890 14450 603 41 0 14849 0
vsize: 59560
[startup+610.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15312 0 0 0 60944 57 0 0 25 0 1 0 423115294 64495616 15290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 15290 603 41 0 15705 0
vsize: 62984
[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15312 0 0 0 61944 57 0 0 25 0 1 0 423115294 64495616 15290 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 15290 603 41 0 15705 0
vsize: 62984
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15312 0 0 0 62944 57 0 0 25 0 1 0 423115294 64495616 15290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 15290 603 41 0 15705 0
vsize: 62984
[startup+640.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15312 0 0 0 63943 58 0 0 25 0 1 0 423115294 64495616 15290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 15290 603 41 0 15705 0
vsize: 62984
[startup+650.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15312 0 0 0 64943 58 0 0 25 0 1 0 423115294 64495616 15290 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15746 15290 603 41 0 15705 0
vsize: 62984
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15314 0 0 0 65943 58 0 0 25 0 1 0 423115294 64479232 15292 4294967295 134512640 134672761 3221224544 3221223728 134558768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15742 15292 603 41 0 15701 0
vsize: 62968
[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15314 0 0 0 66942 59 0 0 25 0 1 0 423115294 64479232 15292 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15742 15292 603 41 0 15701 0
vsize: 62968
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15314 0 0 0 67942 59 0 0 25 0 1 0 423115294 64479232 15292 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15742 15292 603 41 0 15701 0
vsize: 62968
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15314 0 0 0 68941 59 0 0 25 0 1 0 423115294 64479232 15292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15292 603 41 0 15701 0
vsize: 62968
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15314 0 0 0 69942 59 0 0 25 0 1 0 423115294 64479232 15292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15292 603 41 0 15701 0
vsize: 62968
[startup+710.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 70942 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+720.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 71942 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+730.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 72942 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+740.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 73943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 74943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 75943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+770.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 76943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 77943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 78943 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 79944 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+810.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 80944 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 81944 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15315 0 0 0 82944 59 0 0 25 0 1 0 423115294 64479232 15293 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15293 603 41 0 15701 0
vsize: 62968
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15316 0 0 0 83944 59 0 0 25 0 1 0 423115294 64479232 15294 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15294 603 41 0 15701 0
vsize: 62968
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15316 0 0 0 84945 59 0 0 25 0 1 0 423115294 64479232 15294 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15742 15294 603 41 0 15701 0
vsize: 62968
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 85944 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 86944 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 87945 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+890.045 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 88945 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 89945 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 90945 60 0 0 25 0 1 0 423115294 65695744 15589 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16039 15589 603 41 0 15998 0
vsize: 64156
[startup+920.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 91945 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+930.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 92945 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 93946 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 94946 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+960.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 95946 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+970.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 96946 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+980.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 97947 60 0 0 25 0 1 0 423115294 65568768 15586 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16008 15586 603 41 0 15967 0
vsize: 64032
[startup+990.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 98947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223728 134558885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 99947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 100947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 101947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1030.05 s]
Raw data (loadavg): 1.07 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 102947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1040.05 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 103947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1050.05 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 104947 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1060.05 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 105948 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1070.05 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15611 0 0 0 106948 60 0 0 25 0 1 0 423115294 64552960 15338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 15338 603 41 0 15719 0
vsize: 63040
[startup+1080.05 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 107947 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1090.05 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 108948 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1100.05 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 109947 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1110.05 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 110947 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1120.05 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 111947 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1130.05 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 112948 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223728 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1140.05 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 15685 0 0 0 113948 61 0 0 25 0 1 0 423115294 64958464 15412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15859 15412 603 41 0 15818 0
vsize: 63436
[startup+1150.05 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 114946 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
[startup+1160.05 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 115947 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 116947 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 117947 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 118947 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 30947
Raw data (stat): 30947 (minisat+) R 30946 25285 25284 0 -1 0 16383 0 0 0 119947 63 0 0 25 0 1 0 423115294 67792896 16110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16551 16110 603 41 0 16510 0
vsize: 66204
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 30947
Raw data (stat): 30947 (minisat+) Z 30946 25285 25284 0 -1 12 16385 0 0 0 119947 66 0 0 25 0 1 0 423115294 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.14
CPU user time (s): 1199.48
CPU system time (s): 0.660899
CPU usage (%): 100.004
Max. virtual memory (Kb): 66204
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####