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_45_sat_pb.cnf.cr.opb
MD5SUM	da4cd22fd601b0d838453ba86be8f9aa
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	6.73997
Number of variables	3038
Total number of constraints	2160
Number of constraints which are clauses	2070
Number of constraints which are cardinality constraints (but not clauses)	90
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 6088

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-14 03:35:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4569 boxname=wulflinc27 idbench=57 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  da4cd22fd601b0d838453ba86be8f9aa  /oldhome/oroussel/tmp/wulflinc27/normalized-fpga45_45_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-fpga45_45_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc27/normalized-fpga45_45_sat_pb.cnf.cr.opb
IDLAUNCH: 4569
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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	: 3
cpu MHz		: 451.169
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:        840896 kB
Buffers:         35172 kB
Cached:         121468 kB
SwapCached:       3160 kB
Active:          70172 kB
Inactive:        92500 kB
HighTotal:      131008 kB
HighFree:         6132 kB
LowTotal:       903652 kB
LowFree:        834764 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25596 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:42:25 (client local time) WITH STATUS 30 IN 406.21 SECONDS
stats: 4569 7 406.21 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  89]---> BDD-cost:   87
c ---[  88]---> BDD-cost:   87
c ---[  87]---> BDD-cost:   87
c ---[  86]---> BDD-cost:   87
c ---[  85]---> BDD-cost:   87
c ---[  84]---> BDD-cost:   87
c ---[  83]---> BDD-cost:   87
c ---[  82]---> BDD-cost:   87
c ---[  81]---> BDD-cost:   87
c ---[  80]---> BDD-cost:   87
c ---[  79]---> BDD-cost:   87
c ---[  78]---> BDD-cost:   87
c ---[  77]---> BDD-cost:   87
c ---[  76]---> BDD-cost:   87
c ---[  75]---> BDD-cost:   87
c ---[  74]---> BDD-cost:   87
c ---[  73]---> BDD-cost:   87
c ---[  72]---> BDD-cost:   87
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:   87
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   41
c ---[  43]---> BDD-cost:   41
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:   43
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 |   27792   120905 |    9264       0        0     nan |  0.000 % |
c |       101 |   27593   120310 |   10190      26      130     5.0 |  1.481 % |
c |       251 |   27248   119275 |   11209      29      194     6.7 |  2.250 % |
c |       476 |   26873   118150 |   12330      97      432     4.5 |  3.098 % |
c |       813 |   26053   115690 |   13563     108      430     4.0 |  4.953 % |
c |      1319 |   25468   113935 |   14919     442    84733   191.7 |  6.275 % |
c |      2078 |   25108   112855 |   16411    1067   287096   269.1 |  7.090 % |
c |      3219 |   24284   110385 |   18052    1924   518994   269.7 |  8.955 % |
c |      4929 |   23779   108870 |   19858    3409   969730   284.5 | 10.097 % |
c |      7491 |   23634   108435 |   21844    5901  1323611   224.3 | 10.425 % |
c |     11336 |   21305   101450 |   24028    8861  2246917   253.6 | 15.694 % |
c |     17102 |   19318    95495 |   26431   13887  3530363   254.2 | 20.206 % |
c |     25751 |   17478    89975 |   29074   21902  6325312   288.8 | 24.356 % |
c |     38726 |   17273    89360 |   31981   34808 11051138   317.5 | 24.819 % |
c |     58189 |   16378    86675 |   35180   31138 12107597   388.8 | 26.843 % |
c ==============================================================================
c [1mSATISFIABLE: No goal function specified.[0m
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 15
c conflicts             : 61872          (152 /sec)
c decisions             : 808166         (1992 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 405.735 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.77 0.90 0.90 2/54 24792
Raw data (stat): 24792 (runsolver) R 24791 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481393299 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.0007 s]
Raw data (loadavg): 0.81 0.90 0.90 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 1547 0 0 0 994 4 0 0 25 0 1 0 481393299 8175616 1524 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1996 1524 603 41 0 1955 0
vsize: 7984
[startup+20.0011 s]
Raw data (loadavg): 0.83 0.91 0.90 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 2339 0 0 0 1991 6 0 0 25 0 1 0 481393299 11407360 2316 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2785 2316 603 41 0 2744 0
vsize: 11140
[startup+30.0022 s]
Raw data (loadavg): 0.86 0.91 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 2890 0 0 0 2991 7 0 0 25 0 1 0 481393299 13705216 2867 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3346 2867 603 41 0 3305 0
vsize: 13384
[startup+40.002 s]
Raw data (loadavg): 0.88 0.91 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 3146 0 0 0 3990 8 0 0 25 0 1 0 481393299 14782464 3123 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3609 3123 603 41 0 3568 0
vsize: 14436
[startup+50.0025 s]
Raw data (loadavg): 0.90 0.91 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 3372 0 0 0 4990 8 0 0 25 0 1 0 481393299 15728640 3349 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3840 3349 603 41 0 3799 0
vsize: 15360
[startup+60.0028 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 3641 0 0 0 5990 9 0 0 25 0 1 0 481393299 16809984 3618 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4104 3618 603 41 0 4063 0
vsize: 16416
[startup+70.0035 s]
Raw data (loadavg): 0.93 0.92 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 4013 0 0 0 6988 10 0 0 25 0 1 0 481393299 18296832 3990 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4467 3990 603 41 0 4426 0
vsize: 17868
[startup+80.004 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 4221 0 0 0 7988 10 0 0 25 0 1 0 481393299 19107840 4198 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4665 4198 603 41 0 4624 0
vsize: 18660
[startup+90.0041 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 4756 0 0 0 8986 12 0 0 25 0 1 0 481393299 21401600 4733 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5225 4733 603 41 0 5184 0
vsize: 20900
[startup+100.005 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 5072 0 0 0 9986 13 0 0 25 0 1 0 481393299 22614016 5049 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5521 5049 603 41 0 5480 0
vsize: 22084
[startup+110.005 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 5095 0 0 0 10986 13 0 0 25 0 1 0 481393299 22749184 5072 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5554 5072 603 41 0 5513 0
vsize: 22216
[startup+120.006 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 5868 0 0 0 11985 14 0 0 25 0 1 0 481393299 25845760 5845 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6310 5845 603 41 0 6269 0
vsize: 25240
[startup+130.007 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 6006 0 0 0 12985 15 0 0 25 0 1 0 481393299 26521600 5983 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6475 5983 603 41 0 6434 0
vsize: 25900
[startup+140.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 6124 0 0 0 13984 15 0 0 25 0 1 0 481393299 27054080 6101 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6605 6101 603 41 0 6564 0
vsize: 26420
[startup+150.007 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 6603 0 0 0 14983 16 0 0 25 0 1 0 481393299 28946432 6580 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7067 6580 603 41 0 7026 0
vsize: 28268
[startup+160.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 6830 0 0 0 15983 17 0 0 25 0 1 0 481393299 29892608 6807 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7298 6807 603 41 0 7257 0
vsize: 29192
[startup+170.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 7435 0 0 0 16981 18 0 0 25 0 1 0 481393299 32317440 7412 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7890 7412 603 41 0 7849 0
vsize: 31560
[startup+180.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 7916 0 0 0 17980 20 0 0 25 0 1 0 481393299 34344960 7893 4294967295 134512640 134672761 3221224528 3221223700 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8385 7893 603 41 0 8344 0
vsize: 33540
[startup+190.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 8022 0 0 0 18980 20 0 0 25 0 1 0 481393299 34750464 7999 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8484 7999 603 41 0 8443 0
vsize: 33936
[startup+200.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 8212 0 0 0 19980 21 0 0 25 0 1 0 481393299 35561472 8189 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8682 8189 603 41 0 8641 0
vsize: 34728
[startup+210.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 8987 0 0 0 20978 23 0 0 25 0 1 0 481393299 38666240 8964 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9440 8964 603 41 0 9399 0
vsize: 37760
[startup+220.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 10326 0 0 0 21974 27 0 0 25 0 1 0 481393299 44236800 10303 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10800 10303 603 41 0 10759 0
vsize: 43200
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 11855 0 0 0 22969 32 0 0 25 0 1 0 481393299 50634752 11832 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12362 11832 603 41 0 12321 0
vsize: 49448
[startup+240.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 23966 35 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 24966 35 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 25966 35 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+270.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 26966 35 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+280.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 27967 35 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 28967 36 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+300.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 29967 36 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+310.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13179 0 0 0 30967 36 0 0 25 0 1 0 481393299 56033280 13156 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13680 13156 603 41 0 13639 0
vsize: 54720
[startup+320.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13737 0 0 0 31966 37 0 0 25 0 1 0 481393299 58327040 13714 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14240 13714 603 41 0 14199 0
vsize: 56960
[startup+330.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 13890 0 0 0 32965 38 0 0 25 0 1 0 481393299 59011072 13867 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14407 13867 603 41 0 14366 0
vsize: 57628
[startup+340.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 14150 0 0 0 33965 39 0 0 25 0 1 0 481393299 60088320 14127 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14670 14127 603 41 0 14629 0
vsize: 58680
[startup+350.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 14246 0 0 0 34965 39 0 0 25 0 1 0 481393299 60358656 14223 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14736 14223 603 41 0 14695 0
vsize: 58944
[startup+360.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 14527 0 0 0 35965 39 0 0 25 0 1 0 481393299 61579264 14504 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15034 14504 603 41 0 14993 0
vsize: 60136
[startup+370.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 14872 0 0 0 36963 40 0 0 25 0 1 0 481393299 62935040 14849 4294967295 134512640 134672761 3221224528 3221223700 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15365 14849 603 41 0 15324 0
vsize: 61460
[startup+380.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 15151 0 0 0 37963 41 0 0 25 0 1 0 481393299 64155648 15128 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15663 15128 603 41 0 15622 0
vsize: 62652
[startup+390.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 15394 0 0 0 38962 42 0 0 25 0 1 0 481393299 65101824 15371 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15894 15371 603 41 0 15853 0
vsize: 63576
[startup+400.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 15598 0 0 0 39962 42 0 0 25 0 1 0 481393299 65912832 15575 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16092 15575 603 41 0 16051 0
vsize: 64368
[startup+406.175 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 24792
Raw data (stat): 24792 (minisat+) R 24791 18865 18864 0 -1 0 15598 0 0 0 39962 42 0 0 25 0 1 0 481393299 65912832 15575 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16092 15575 603 41 0 16051 0
vsize: 0

Child status: 30
Real time (s): 406.175
CPU time (s): 406.21
CPU user time (s): 405.737
CPU system time (s): 0.472928
CPU usage (%): 100.009
Max. virtual memory (Kb): 64368
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####