PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga45_43_sat_pb.cnf.cr.opb
MD5SUM	f711bed5ebfe5c735a8c12d953afb97c
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	9.61454
Number of variables	2903
Total number of constraints	2066
Number of constraints which are clauses	1978
Number of constraints which are cardinality constraints (but not clauses)	88
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 6100

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-14 03:35:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4567 boxname=wulflinc10 idbench=55 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f711bed5ebfe5c735a8c12d953afb97c  /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_43_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_43_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_43_sat_pb.cnf.cr.opb
IDLAUNCH: 4567
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        861520 kB
Buffers:         35480 kB
Cached:         117764 kB
SwapCached:        164 kB
Active:          55184 kB
Inactive:       101144 kB
HighTotal:      131008 kB
HighFree:         9520 kB
LowTotal:       903652 kB
LowFree:        852000 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11248 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:46:18 (client local time) WITH STATUS 30 IN 654.073 SECONDS
stats: 4567 7 654.073 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2066 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  87]---> BDD-cost:   83
c ---[  86]---> BDD-cost:   83
c ---[  85]---> BDD-cost:   83
c ---[  84]---> BDD-cost:   83
c ---[  83]---> BDD-cost:   83
c ---[  82]---> BDD-cost:   83
c ---[  81]---> BDD-cost:   83
c ---[  80]---> BDD-cost:   83
c ---[  79]---> BDD-cost:   83
c ---[  78]---> BDD-cost:   83
c ---[  77]---> BDD-cost:   83
c ---[  76]---> BDD-cost:   83
c ---[  75]---> BDD-cost:   83
c ---[  74]---> BDD-cost:   83
c ---[  73]---> BDD-cost:   83
c ---[  72]---> BDD-cost:   83
c ---[  71]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   83
c ---[  69]---> BDD-cost:   83
c ---[  68]---> BDD-cost:   83
c ---[  67]---> BDD-cost:   83
c ---[  66]---> BDD-cost:   83
c ---[  65]---> BDD-cost:   83
c ---[  64]---> BDD-cost:   83
c ---[  63]---> BDD-cost:   83
c ---[  62]---> BDD-cost:   83
c ---[  61]---> BDD-cost:   83
c ---[  60]---> BDD-cost:   83
c ---[  59]---> BDD-cost:   83
c ---[  58]---> BDD-cost:   83
c ---[  57]---> BDD-cost:   83
c ---[  56]---> BDD-cost:   83
c ---[  55]---> BDD-cost:   83
c ---[  54]---> BDD-cost:   83
c ---[  53]---> BDD-cost:   83
c ---[  52]---> BDD-cost:   83
c ---[  51]---> BDD-cost:   83
c ---[  50]---> BDD-cost:   83
c ---[  49]---> BDD-cost:   83
c ---[  48]---> BDD-cost:   83
c ---[  47]---> BDD-cost:   83
c ---[  46]---> BDD-cost:   83
c ---[  45]---> BDD-cost:   83
c ---[  44]---> BDD-cost:   83
c ---[  43]---> BDD-cost:   83
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26521   113493 |    8840       0        0     nan |  0.000 % |
c |       100 |   26331   112923 |    9724      11      147    13.4 |  1.504 % |
c |       250 |   26011   111963 |   10696      24      191     8.0 |  2.262 % |
c |       477 |   25526   110508 |   11766      65      322     5.0 |  3.399 % |
c |       819 |   25521   110493 |   12942     403    34244    85.0 |  3.410 % |
c |      1327 |   25471   110343 |   14236     887    78171    88.1 |  3.529 % |
c |      2089 |   24982   108878 |   15660    1455   233387   160.4 |  4.689 % |
c |      3230 |   24402   107138 |   17226    2358   503794   213.7 |  6.063 % |
c |      4939 |   23197   103523 |   18949    3580   876561   244.8 |  8.917 % |
c |      7507 |   22093   100213 |   20844    5679  1527140   268.9 | 11.533 % |
c |     11351 |   20038    94048 |   22928    8693  2261799   260.2 | 16.400 % |
c |     17120 |   19083    91183 |   25221   14110  3310383   234.6 | 18.662 % |
c |     25771 |   17569    86643 |   27743   22197  5200902   234.3 | 22.250 % |
c |     38745 |   16729    84123 |   30518   16302  4890777   300.0 | 24.239 % |
c |     58208 |   16150    82388 |   33569   35589  9407470   264.3 | 25.613 % |
c |     87404 |   15191    79513 |   36926   16055  5548702   345.6 | 27.886 % |
c |    131196 |   14823    78413 |   40619   28507 12618157   442.6 | 28.763 % |
c ==============================================================================
c [1mSATISFIABLE: No goal function specified.[0m
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 17
c conflicts             : 137623         (211 /sec)
c decisions             : 986180         (1509 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 653.616 s
c _______________________________________________________________________________
#### 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.67 0.84 0.87 2/54 32725
Raw data (stat): 32725 (runsolver) R 32724 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423179854 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.0002 s]
Raw data (loadavg): 0.72 0.84 0.87 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 1652 0 0 0 993 4 0 0 25 0 1 0 423179854 8663040 1629 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2115 1629 603 41 0 2074 0
vsize: 8460
[startup+20.0002 s]
Raw data (loadavg): 0.76 0.85 0.87 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 2064 0 0 0 1993 5 0 0 25 0 1 0 423179854 10420224 2041 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 2041 603 41 0 2503 0
vsize: 10176
[startup+30.0005 s]
Raw data (loadavg): 0.80 0.85 0.87 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 2575 0 0 0 2991 6 0 0 25 0 1 0 423179854 12439552 2552 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3037 2552 603 41 0 2996 0
vsize: 12148
[startup+39.9998 s]
Raw data (loadavg): 0.83 0.86 0.87 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 2940 0 0 0 3990 7 0 0 25 0 1 0 423179854 13922304 2917 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2917 603 41 0 3358 0
vsize: 13596
[startup+49.9997 s]
Raw data (loadavg): 0.85 0.86 0.87 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 3285 0 0 0 4990 8 0 0 25 0 1 0 423179854 15400960 3262 4294967295 134512640 134672761 3221224528 3221223700 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3760 3262 603 41 0 3719 0
vsize: 15040
[startup+60 s]
Raw data (loadavg): 0.88 0.87 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 3376 0 0 0 5990 8 0 0 25 0 1 0 423179854 15802368 3353 4294967295 134512640 134672761 3221224528 3221223744 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3858 3353 603 41 0 3817 0
vsize: 15432
[startup+69.9996 s]
Raw data (loadavg): 0.89 0.87 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 3621 0 0 0 6988 9 0 0 25 0 1 0 423179854 16752640 3598 4294967295 134512640 134672761 3221224528 3221223716 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3598 603 41 0 4049 0
vsize: 16360
[startup+80.0005 s]
Raw data (loadavg): 0.91 0.87 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 4017 0 0 0 7988 10 0 0 25 0 1 0 423179854 18374656 3994 4294967295 134512640 134672761 3221224528 3221223652 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4486 3994 603 41 0 4445 0
vsize: 17944
[startup+90.001 s]
Raw data (loadavg): 0.92 0.88 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 4377 0 0 0 8987 11 0 0 25 0 1 0 423179854 19857408 4354 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4848 4354 603 41 0 4807 0
vsize: 19392
[startup+100 s]
Raw data (loadavg): 0.93 0.88 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 4905 0 0 0 9986 11 0 0 25 0 1 0 423179854 22016000 4882 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5375 4882 603 41 0 5334 0
vsize: 21500
[startup+110.001 s]
Raw data (loadavg): 0.94 0.88 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 5432 0 0 0 10985 13 0 0 25 0 1 0 423179854 24199168 5409 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5908 5409 603 41 0 5867 0
vsize: 23632
[startup+120.001 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 5690 0 0 0 11985 13 0 0 25 0 1 0 423179854 25280512 5667 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6172 5667 603 41 0 6131 0
vsize: 24688
[startup+130.002 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 6082 0 0 0 12984 14 0 0 25 0 1 0 423179854 26902528 6059 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6568 6059 603 41 0 6527 0
vsize: 26272
[startup+140.002 s]
Raw data (loadavg): 0.97 0.89 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 6597 0 0 0 13983 15 0 0 25 0 1 0 423179854 28921856 6574 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7061 6574 603 41 0 7020 0
vsize: 28244
[startup+150.001 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 6754 0 0 0 14983 16 0 0 25 0 1 0 423179854 29597696 6731 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7226 6731 603 41 0 7185 0
vsize: 28904
[startup+160.002 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 7249 0 0 0 15983 16 0 0 25 0 1 0 423179854 31625216 7226 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7721 7226 603 41 0 7680 0
vsize: 30884
[startup+170.001 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 8791 0 0 0 16980 19 0 0 25 0 1 0 423179854 37974016 8768 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9271 8768 603 41 0 9230 0
vsize: 37084
[startup+180.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9112 0 0 0 17979 20 0 0 25 0 1 0 423179854 39317504 9089 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9599 9089 603 41 0 9558 0
vsize: 38396
[startup+190.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9465 0 0 0 18979 21 0 0 25 0 1 0 423179854 40665088 9442 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9928 9442 603 41 0 9887 0
vsize: 39712
[startup+200.002 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9513 0 0 0 19979 21 0 0 25 0 1 0 423179854 40935424 9490 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9994 9490 603 41 0 9953 0
vsize: 39976
[startup+210.003 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9513 0 0 0 20979 21 0 0 25 0 1 0 423179854 40935424 9490 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9994 9490 603 41 0 9953 0
vsize: 39976
[startup+220.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9513 0 0 0 21979 21 0 0 25 0 1 0 423179854 40935424 9490 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9994 9490 603 41 0 9953 0
vsize: 39976
[startup+230.004 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9513 0 0 0 22979 21 0 0 25 0 1 0 423179854 40935424 9490 4294967295 134512640 134672761 3221224528 3221223712 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9994 9490 603 41 0 9953 0
vsize: 39976
[startup+240.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9513 0 0 0 23980 21 0 0 25 0 1 0 423179854 40935424 9490 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9994 9490 603 41 0 9953 0
vsize: 39976
[startup+250.003 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 9945 0 0 0 24979 22 0 0 25 0 1 0 423179854 42684416 9922 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10421 9922 603 41 0 10380 0
vsize: 41684
[startup+260.004 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 10873 0 0 0 25977 24 0 0 25 0 1 0 423179854 46465024 10850 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11344 10851 603 41 0 11303 0
vsize: 45376
[startup+270.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11684 0 0 0 26975 26 0 0 25 0 1 0 423179854 49975296 11661 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12201 11661 603 41 0 12160 0
vsize: 48804
[startup+280.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 27975 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223696 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+290.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 28976 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+300.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 29976 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+310.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 30976 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+320.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 31976 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+330.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 11744 0 0 0 32976 26 0 0 25 0 1 0 423179854 50110464 11721 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12234 11721 603 41 0 12193 0
vsize: 48936
[startup+340.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 12133 0 0 0 33975 27 0 0 25 0 1 0 423179854 51732480 12110 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12630 12110 603 41 0 12589 0
vsize: 50520
[startup+350.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 12311 0 0 0 34975 27 0 0 25 0 1 0 423179854 52543488 12288 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12828 12288 603 41 0 12787 0
vsize: 51312
[startup+360.003 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 12946 0 0 0 35974 29 0 0 25 0 1 0 423179854 55115776 12923 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13456 12923 603 41 0 13415 0
vsize: 53824
[startup+370.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13259 0 0 0 36973 30 0 0 25 0 1 0 423179854 56328192 13236 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13752 13236 603 41 0 13711 0
vsize: 55008
[startup+380.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 37973 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+390.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 38973 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223664 134565058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+400.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 39973 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+410.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 40973 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+420.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 41974 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+430.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13357 0 0 0 42974 30 0 0 25 0 1 0 423179854 56729600 13334 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13850 13334 603 41 0 13809 0
vsize: 55400
[startup+440.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 13857 0 0 0 43974 30 0 0 25 0 1 0 423179854 58892288 13834 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13834 603 41 0 14337 0
vsize: 57512
[startup+450.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 14929 0 0 0 44972 32 0 0 25 0 1 0 423179854 63213568 14906 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15433 14906 603 41 0 15392 0
vsize: 61732
[startup+460.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 15747 0 0 0 45971 34 0 0 25 0 1 0 423179854 66588672 15724 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16257 15724 603 41 0 16216 0
vsize: 65028
[startup+470.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 16535 0 0 0 46968 36 0 0 25 0 1 0 423179854 69840896 16512 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17051 16512 603 41 0 17010 0
vsize: 68204
[startup+480.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17302 0 0 0 47967 38 0 0 25 0 1 0 423179854 72982528 17279 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17818 17279 603 41 0 17777 0
vsize: 71272
[startup+490.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17897 0 0 0 48966 39 0 0 25 0 1 0 423179854 75550720 17874 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17874 603 41 0 18404 0
vsize: 73780
[startup+500.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17899 0 0 0 49966 39 0 0 25 0 1 0 423179854 75550720 17876 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17876 603 41 0 18404 0
vsize: 73780
[startup+510.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17902 0 0 0 50966 39 0 0 25 0 1 0 423179854 75550720 17879 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17879 603 41 0 18404 0
vsize: 73780
[startup+520.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17902 0 0 0 51966 39 0 0 25 0 1 0 423179854 75550720 17879 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17879 603 41 0 18404 0
vsize: 73780
[startup+530.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17902 0 0 0 52967 39 0 0 25 0 1 0 423179854 75550720 17879 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17879 603 41 0 18404 0
vsize: 73780
[startup+540.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17906 0 0 0 53967 39 0 0 25 0 1 0 423179854 75550720 17883 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17883 603 41 0 18404 0
vsize: 73780
[startup+550.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17909 0 0 0 54967 39 0 0 25 0 1 0 423179854 75550720 17886 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17886 603 41 0 18404 0
vsize: 73780
[startup+560.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17913 0 0 0 55967 39 0 0 25 0 1 0 423179854 75550720 17890 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17890 603 41 0 18404 0
vsize: 73780
[startup+570.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17914 0 0 0 56967 39 0 0 25 0 1 0 423179854 75550720 17891 4294967295 134512640 134672761 3221224528 3221223632 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17891 603 41 0 18404 0
vsize: 73780
[startup+580.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17915 0 0 0 57967 39 0 0 25 0 1 0 423179854 75550720 17892 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17892 603 41 0 18404 0
vsize: 73780
[startup+590.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17917 0 0 0 58968 39 0 0 25 0 1 0 423179854 75550720 17894 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17894 603 41 0 18404 0
vsize: 73780
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17917 0 0 0 59968 39 0 0 25 0 1 0 423179854 75550720 17894 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17894 603 41 0 18404 0
vsize: 73780
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17918 0 0 0 60968 39 0 0 25 0 1 0 423179854 75550720 17895 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17895 603 41 0 18404 0
vsize: 73780
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17918 0 0 0 61968 39 0 0 25 0 1 0 423179854 75550720 17895 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17895 603 41 0 18404 0
vsize: 73780
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17920 0 0 0 62968 39 0 0 25 0 1 0 423179854 75550720 17897 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17897 603 41 0 18404 0
vsize: 73780
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 17921 0 0 0 63968 39 0 0 25 0 1 0 423179854 75550720 17898 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18445 17898 603 41 0 18404 0
vsize: 73780
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 18643 0 0 0 64967 41 0 0 25 0 1 0 423179854 78536704 18620 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19174 18620 603 41 0 19133 0
vsize: 76696
[startup+653.992 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 32725
Raw data (stat): 32725 (minisat+) R 32724 25347 25346 0 -1 0 18643 0 0 0 64967 41 0 0 25 0 1 0 423179854 78536704 18620 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19174 18620 603 41 0 19133 0
vsize: 0

Child status: 30
Real time (s): 653.991
CPU time (s): 654.073
CPU user time (s): 653.618
CPU system time (s): 0.45493
CPU usage (%): 100.012
Max. virtual memory (Kb): 76696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####