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-chnl50_55_pb.cnf.cr.opb
MD5SUM88aaed929c30a489c8806c3852596de3
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 56
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.173973
Number of variables5500
Total number of constraints210
Number of constraints which are clauses110
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint55

Trace number 5373 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-13 23:36:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3781 boxname=wulflinc22 idbench=21 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  88aaed929c30a489c8806c3852596de3  /oldhome/oroussel/tmp/wulflinc22/normalized-chnl50_55_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc22/normalized-chnl50_55_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc22/normalized-chnl50_55_pb.cnf.cr.opb
IDLAUNCH: 3781
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        855404 kB
Buffers:         31700 kB
Cached:         104388 kB
SwapCached:        524 kB
Active:          46928 kB
Inactive:        92588 kB
HighTotal:      131008 kB
HighFree:        22876 kB
LowTotal:       903652 kB
LowFree:        832528 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34152 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:56:39 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3781 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> BDD-cost:  107
c ---[  98]---> BDD-cost:  107
c ---[  97]---> BDD-cost:  107
c ---[  96]---> BDD-cost:  107
c ---[  95]---> BDD-cost:  107
c ---[  94]---> BDD-cost:  107
c ---[  93]---> BDD-cost:  107
c ---[  92]---> BDD-cost:  107
c ---[  91]---> BDD-cost:  107
c ---[  90]---> BDD-cost:  107
c ---[  89]---> BDD-cost:  107
c ---[  88]---> BDD-cost:  107
c ---[  87]---> BDD-cost:  107
c ---[  86]---> BDD-cost:  107
c ---[  85]---> BDD-cost:  107
c ---[  84]---> BDD-cost:  107
c ---[  83]---> BDD-cost:  107
c ---[  82]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  107
c ---[  80]---> BDD-cost:  107
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  107
c ---[  76]---> BDD-cost:  107
c ---[  75]---> BDD-cost:  107
c ---[  74]---> BDD-cost:  107
c ---[  73]---> BDD-cost:  107
c ---[  72]---> BDD-cost:  107
c ---[  71]---> BDD-cost:  107
c ---[  70]---> BDD-cost:  107
c ---[  69]---> BDD-cost:  107
c ---[  68]---> BDD-cost:  107
c ---[  67]---> BDD-cost:  107
c ---[  66]---> BDD-cost:  107
c ---[  65]---> BDD-cost:  107
c ---[  64]---> BDD-cost:  107
c ---[  63]---> BDD-cost:  107
c ---[  62]---> BDD-cost:  107
c ---[  61]---> BDD-cost:  107
c ---[  60]---> BDD-cost:  107
c ---[  59]---> BDD-cost:  107
c ---[  58]---> BDD-cost:  107
c ---[  57]---> BDD-cost:  107
c ---[  56]---> BDD-cost:  107
c ---[  55]---> BDD-cost:  107
c ---[  54]---> BDD-cost:  107
c ---[  53]---> BDD-cost:  107
c ---[  52]---> BDD-cost:  107
c ---[  51]---> BDD-cost:  107
c ---[  50]---> BDD-cost:  107
c ---[  49]---> BDD-cost:  107
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  107
c ---[  46]---> BDD-cost:  107
c ---[  45]---> BDD-cost:  107
c ---[  44]---> BDD-cost:  107
c ---[  43]---> BDD-cost:  107
c ---[  42]---> BDD-cost:  107
c ---[  41]---> BDD-cost:  107
c ---[  40]---> BDD-cost:  107
c ---[  39]---> BDD-cost:  107
c ---[  38]---> BDD-cost:  107
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  107
c ---[  35]---> BDD-cost:  107
c ---[  34]---> BDD-cost:  107
c ---[  33]---> BDD-cost:  107
c ---[  32]---> BDD-cost:  107
c ---[  31]---> BDD-cost:  107
c ---[  30]---> BDD-cost:  107
c ---[  29]---> BDD-cost:  107
c ---[  28]---> BDD-cost:  107
c ---[  27]---> BDD-cost:  107
c ---[  26]---> BDD-cost:  107
c ---[  25]---> BDD-cost:  107
c ---[  24]---> BDD-cost:  107
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   26710    74700 |    8012       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16100          
c   -- var.elim.:  2000/16100          
c   -- var.elim.:  3000/16100          
c   -- var.elim.:  4000/16100          
c   -- var.elim.:  5000/16100          
c   -- var.elim.:  6000/16100          
c   -- var.elim.:  7000/16100          
c   -- var.elim.:  8000/16100          
c   -- var.elim.:  9000/16100          
c   -- var.elim.:  10000/16100          
c   -- var.elim.:  11000/16100          
c   -- var.elim.:  12000/16100          
c   -- var.elim.:  13000/16100          
c   -- var.elim.:  14000/16100          
c   -- var.elim.:  15000/16100          
c   -- var.elim.:  16000/16100          
c   -- var.elim.:  16100/16100          
c   -- var.elim.:  1000/5930          
c   -- var.elim.:  2000/5930          
c   -- var.elim.:  3000/5930          
c   -- var.elim.:  4000/5930          
c   -- var.elim.:  5000/5930          
c   -- var.elim.:  5930/5930          
c   -- var.elim.:  206/206          
c   -- subsuming                       
c   -- var.elim.:  1000/3288          
c   -- var.elim.:  2000/3288          
c   -- var.elim.:  3000/3288          
c   -- var.elim.:  3288/3288          
c   -- var.elim.:  982/982          
c   -- var.elim.:  124/124          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  122/122          
c   -- var.elim.:  124/124          
c   -- var.elim.:  126/126          
c   -- var.elim.:  128/128          
c   -- var.elim.:  130/130          
c   -- var.elim.:  132/132          
c   -- var.elim.:  134/134          
c   -- var.elim.:  136/136          
c   -- var.elim.:  138/138          
c   -- var.elim.:  140/140          
c   -- var.elim.:  142/142          
c   -- var.elim.:  144/144          
c   -- var.elim.:  146/146          
c   -- var.elim.:  148/148          
c   -- var.elim.:  150/150          
c   -- var.elim.:  152/152          
c   -- var.elim.:  154/154          
c   -- var.elim.:  156/156          
c   -- var.elim.:  158/158          
c   -- var.elim.:  160/160          
c   -- var.elim.:  162/162          
c   -- var.elim.:  164/164          
c   -- var.elim.:  166/166          
c   -- var.elim.:  168/168          
c   -- var.elim.:  170/170          
c   -- var.elim.:  172/172          
c   -- var.elim.:  174/174          
c   -- var.elim.:  176/176          
c   -- var.elim.:  178/178          
c   -- var.elim.:  180/180          
c   -- var.elim.:  182/182          
c   -- var.elim.:  184/184          
c   -- var.elim.:  186/186          
c   -- var.elim.:  188/188          
c   -- var.elim.:  190/190          
c   -- var.elim.:  192/192          
c   -- var.elim.:  194/194          
c   -- var.elim.:  196/196          
c   -- var.elim.:  198/198          
c   -- var.elim.:  200/200          
c   -- var.elim.:  202/202          
c   -- var.elim.:  204/204          
c   -- var.elim.:  206/206          
c   -- var.elim.:  208/208          
c   -- var.elim.:  494/494          
c   -- subsuming                       
c   -- var.elim.:  1000/5820          
c   -- var.elim.:  2000/5820          
c   -- var.elim.:  3000/5820          
c   -- var.elim.:  4000/5820          
c   -- var.elim.:  5000/5820          
c   -- var.elim.:  5820/5820          
c   -- var.elim.:  1000/5578          
c   -- var.elim.:  2000/5578          
c   -- var.elim.:  3000/5578          
c   -- var.elim.:  4000/5578          
c   -- var.elim.:  5000/5578          
c   -- var.elim.:  5578/5578          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  574/574          
c |         0 |   25478    93006 |      --       0       --      -- |     --   | -1232/18606
c |         0 |   25478    93006 |   10191       0        0     nan |  0.000 % |
c |       102 |   25478    93006 |   11210     102    19645   192.6 |  0.655 % |
c |       252 |   25478    93006 |   12331     252    51521   204.4 |  0.655 % |
c |       477 |   25478    93006 |   13564     477   105132   220.4 |  0.655 % |
c |       814 |   25478    93006 |   14920     814   187082   229.8 |  0.655 % |
c |      1320 |   25478    93006 |   16413    1320   357224   270.6 |  0.655 % |
c |      2082 |   25478    93006 |   18054    2082   545596   262.1 |  0.655 % |
c |      3224 |   25478    93006 |   19859    3224   979151  #### 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.94 0.90 2/54 29949
Raw data (stat): 29949 (runsolver) R 29948 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479959432 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 4389 0 0 0 987 11 0 0 25 0 1 0 479959432 19218432 4234 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4692 4234 603 41 0 4651 0
vsize: 18768
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 6558 0 0 0 1981 17 0 0 25 0 1 0 479959432 28045312 6403 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6847 6403 603 41 0 6806 0
vsize: 27388
[startup+30.0023 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 8260 0 0 0 2976 22 0 0 25 0 1 0 479959432 35049472 8105 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8557 8105 603 41 0 8516 0
vsize: 34228
[startup+40.002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 9898 0 0 0 3972 26 0 0 25 0 1 0 479959432 41775104 9743 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10199 9743 603 41 0 10158 0
vsize: 40796
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 11220 0 0 0 4969 29 0 0 25 0 1 0 479959432 47194112 11065 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11522 11065 603 41 0 11481 0
vsize: 46088
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 12579 0 0 0 5966 32 0 0 25 0 1 0 479959432 52744192 12424 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12877 12424 603 41 0 12836 0
vsize: 51508
[startup+70.0022 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 14295 0 0 0 6963 36 0 0 25 0 1 0 479959432 59731968 14140 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14583 14140 603 41 0 14542 0
vsize: 58332
[startup+80.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 15586 0 0 0 7960 39 0 0 25 0 1 0 479959432 65036288 15431 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15878 15431 603 41 0 15837 0
vsize: 63512
[startup+90.0025 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 16517 0 0 0 8958 41 0 0 25 0 1 0 479959432 68870144 16362 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16814 16362 603 41 0 16773 0
vsize: 67256
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 17426 0 0 0 9955 44 0 0 25 0 1 0 479959432 72691712 17271 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17747 17271 603 41 0 17706 0
vsize: 70988
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 18286 0 0 0 10953 47 0 0 25 0 1 0 479959432 76242944 18131 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18614 18131 603 41 0 18573 0
vsize: 74456
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 18911 0 0 0 11950 49 0 0 25 0 1 0 479959432 78737408 18756 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19223 18756 603 41 0 19182 0
vsize: 76892
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 19556 0 0 0 12949 51 0 0 25 0 1 0 479959432 81399808 19401 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19873 19401 603 41 0 19832 0
vsize: 79492
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20190 0 0 0 13947 53 0 0 25 0 1 0 479959432 84033536 20035 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20516 20035 603 41 0 20475 0
vsize: 82064
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 14947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 15947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 16947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 17947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 18947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 19947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 20947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 21947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 20514 0 0 0 22947 54 0 0 25 0 1 0 479959432 85266432 20352 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20817 20352 603 41 0 20776 0
vsize: 83268
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 21297 0 0 0 23945 57 0 0 25 0 1 0 479959432 88588288 21135 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21628 21135 603 41 0 21587 0
vsize: 86512
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 22458 0 0 0 24943 59 0 0 25 0 1 0 479959432 93356032 22296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22792 22296 603 41 0 22751 0
vsize: 91168
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 23533 0 0 0 25940 62 0 0 25 0 1 0 479959432 97730560 23371 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23860 23371 603 41 0 23819 0
vsize: 95440
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 24349 0 0 0 26938 64 0 0 25 0 1 0 479959432 101072896 24187 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24676 24187 603 41 0 24635 0
vsize: 98704
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 25267 0 0 0 27936 66 0 0 25 0 1 0 479959432 104820736 25105 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25591 25105 603 41 0 25550 0
vsize: 102364
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26133 0 0 0 28935 68 0 0 25 0 1 0 479959432 108417024 25971 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26469 25971 603 41 0 26428 0
vsize: 105876
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26819 0 0 0 29933 70 0 0 25 0 1 0 479959432 111099904 26642 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26642 603 41 0 27083 0
vsize: 108496
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26821 0 0 0 30933 70 0 0 25 0 1 0 479959432 111099904 26644 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26644 603 41 0 27083 0
vsize: 108496
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26822 0 0 0 31933 70 0 0 25 0 1 0 479959432 111099904 26645 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26645 603 41 0 27083 0
vsize: 108496
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26822 0 0 0 32933 70 0 0 25 0 1 0 479959432 111099904 26645 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26645 603 41 0 27083 0
vsize: 108496
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26822 0 0 0 33933 70 0 0 25 0 1 0 479959432 111099904 26645 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26645 603 41 0 27083 0
vsize: 108496
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26823 0 0 0 34933 70 0 0 25 0 1 0 479959432 111099904 26646 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26646 603 41 0 27083 0
vsize: 108496
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26823 0 0 0 35933 70 0 0 25 0 1 0 479959432 111099904 26646 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26646 603 41 0 27083 0
vsize: 108496
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26823 0 0 0 36934 70 0 0 25 0 1 0 479959432 111099904 26646 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26646 603 41 0 27083 0
vsize: 108496
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26824 0 0 0 37934 71 0 0 25 0 1 0 479959432 111099904 26647 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26647 603 41 0 27083 0
vsize: 108496
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26824 0 0 0 38934 71 0 0 25 0 1 0 479959432 111099904 26647 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26647 603 41 0 27083 0
vsize: 108496
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26824 0 0 0 39934 71 0 0 25 0 1 0 479959432 111099904 26647 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26647 603 41 0 27083 0
vsize: 108496
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26824 0 0 0 40934 71 0 0 25 0 1 0 479959432 111099904 26647 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26647 603 41 0 27083 0
vsize: 108496
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26825 0 0 0 41934 71 0 0 25 0 1 0 479959432 111099904 26648 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26648 603 41 0 27083 0
vsize: 108496
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26825 0 0 0 42934 71 0 0 25 0 1 0 479959432 111099904 26648 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26648 603 41 0 27083 0
vsize: 108496
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26825 0 0 0 43934 71 0 0 25 0 1 0 479959432 111099904 26648 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26648 603 41 0 27083 0
vsize: 108496
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26825 0 0 0 44934 71 0 0 25 0 1 0 479959432 111099904 26648 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26648 603 41 0 27083 0
vsize: 108496
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 45935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 46935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 47935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+490.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 48935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 49935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 50935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 51935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 26826 0 0 0 52935 71 0 0 25 0 1 0 479959432 111099904 26649 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 26649 603 41 0 27083 0
vsize: 108496
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 27130 0 0 0 53935 72 0 0 25 0 1 0 479959432 112431104 26953 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27449 26953 603 41 0 27408 0
vsize: 109796
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 28026 0 0 0 54932 75 0 0 25 0 1 0 479959432 116117504 27849 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28349 27849 603 41 0 28308 0
vsize: 113396
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 28873 0 0 0 55931 77 0 0 25 0 1 0 479959432 119558144 28696 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29189 28696 603 41 0 29148 0
vsize: 116756
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 29541 0 0 0 56929 79 0 0 25 0 1 0 479959432 122347520 29364 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29870 29364 603 41 0 29829 0
vsize: 119480
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30395 0 0 0 57927 81 0 0 25 0 1 0 479959432 125501440 30166 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30166 603 41 0 30599 0
vsize: 122560
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30395 0 0 0 58927 81 0 0 25 0 1 0 479959432 125501440 30166 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30166 603 41 0 30599 0
vsize: 122560
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 59927 81 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 60927 81 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 61927 81 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 62927 81 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 63927 82 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223680 134614503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30396 0 0 0 64928 82 0 0 25 0 1 0 479959432 125501440 30167 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30167 603 41 0 30599 0
vsize: 122560
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30397 0 0 0 65928 82 0 0 25 0 1 0 479959432 125501440 30168 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30168 603 41 0 30599 0
vsize: 122560
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30397 0 0 0 66928 82 0 0 25 0 1 0 479959432 125501440 30168 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30168 603 41 0 30599 0
vsize: 122560
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 67928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 68928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 69928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 70928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 71928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223584 134603552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 72928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 73928 82 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 74928 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 75928 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 76928 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 77928 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 78929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 79929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 80929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 81929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 82929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 83929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30398 0 0 0 84929 83 0 0 25 0 1 0 479959432 125501440 30169 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30640 30169 603 41 0 30599 0
vsize: 122560
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 30614 0 0 0 85929 84 0 0 25 0 1 0 479959432 126427136 30385 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30866 30385 603 41 0 30825 0
vsize: 123464
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 31200 0 0 0 86928 85 0 0 25 0 1 0 479959432 128974848 30971 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31488 30971 603 41 0 31447 0
vsize: 125952
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 31478 0 0 0 87927 86 0 0 25 0 1 0 479959432 130117632 31249 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31767 31249 603 41 0 31726 0
vsize: 127068
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 31858 0 0 0 88927 87 0 0 25 0 1 0 479959432 131575808 31629 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32123 31629 603 41 0 32082 0
vsize: 128492
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 32332 0 0 0 89925 88 0 0 25 0 1 0 479959432 133550080 32103 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32605 32103 603 41 0 32564 0
vsize: 130420
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 32594 0 0 0 90924 89 0 0 25 0 1 0 479959432 134766592 32365 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32902 32365 603 41 0 32861 0
vsize: 131608
[startup+920.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 32945 0 0 0 91924 90 0 0 25 0 1 0 479959432 136212480 32716 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33255 32716 603 41 0 33214 0
vsize: 133020
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33227 0 0 0 92923 91 0 0 25 0 1 0 479959432 137138176 32974 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32974 603 41 0 33440 0
vsize: 133924
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33228 0 0 0 93923 91 0 0 25 0 1 0 479959432 137138176 32975 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32975 603 41 0 33440 0
vsize: 133924
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33228 0 0 0 94923 91 0 0 25 0 1 0 479959432 137138176 32975 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32975 603 41 0 33440 0
vsize: 133924
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 95923 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+970.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 96923 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+980.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 97924 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+990.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 98924 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 99924 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 100924 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33229 0 0 0 101924 91 0 0 25 0 1 0 479959432 137138176 32976 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32976 603 41 0 33440 0
vsize: 133924
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33231 0 0 0 102924 91 0 0 25 0 1 0 479959432 137138176 32978 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32978 603 41 0 33440 0
vsize: 133924
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33231 0 0 0 103924 92 0 0 25 0 1 0 479959432 137138176 32978 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32978 603 41 0 33440 0
vsize: 133924
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33231 0 0 0 104925 92 0 0 25 0 1 0 479959432 137138176 32978 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32978 603 41 0 33440 0
vsize: 133924
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33234 0 0 0 105925 92 0 0 25 0 1 0 479959432 137138176 32981 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32981 603 41 0 33440 0
vsize: 133924
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33235 0 0 0 106925 92 0 0 25 0 1 0 479959432 137138176 32982 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32982 603 41 0 33440 0
vsize: 133924
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33235 0 0 0 107925 92 0 0 25 0 1 0 479959432 137138176 32982 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32982 603 41 0 33440 0
vsize: 133924
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 108925 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 109925 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 110926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 111926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 112926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 113926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 114926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 115926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 116926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 117927 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 118926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29949
Raw data (stat): 29949 (minisat+) R 29948 26298 26297 0 -1 0 33237 0 0 0 119926 92 0 0 25 0 1 0 479959432 137138176 32984 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33481 32984 603 41 0 33440 0
vsize: 133924
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29949
Raw data (stat): 29949 (minisat+) Z 29948 26298 26297 0 -1 12 33237 0 0 0 119927 99 0 0 25 0 1 0 479959432 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.26
CPU user time (s): 1199.27
CPU system time (s): 0.990849
CPU usage (%): 100.016
Max. virtual memory (Kb): 133924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####