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-chnl10_15_pb.cnf.cr.opb
MD5SUMba9cd165dfff9daff67f98334a7b589e
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 16
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.009997
Number of variables300
Total number of constraints50
Number of constraints which are clauses30
Number of constraints which are cardinality constraints (but not clauses)20
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint10
Maximum length of a constraint15

Trace number 4572 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-13 19:21:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3387 boxname=wulflinc28 idbench=3 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba9cd165dfff9daff67f98334a7b589e  /oldhome/oroussel/tmp/wulflinc28/normalized-chnl10_15_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-chnl10_15_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc28/normalized-chnl10_15_pb.cnf.cr.opb
IDLAUNCH: 3387
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        914228 kB
Buffers:         33796 kB
Cached:          51132 kB
SwapCached:          4 kB
Active:          46260 kB
Inactive:        41496 kB
HighTotal:      131008 kB
HighFree:        76300 kB
LowTotal:       903652 kB
LowFree:        837928 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27156 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:32:19 (client local time) WITH STATUS 20 IN 641.921 SECONDS
stats: 3387 7 641.921 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 50 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................
c ---[  19]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  18]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  17]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  16]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  15]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  14]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  13]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  12]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  11]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[  10]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   9]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   8]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   7]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   6]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   5]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   4]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   3]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   2]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   1]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   0]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2730     9840 |     910       0        0     nan |  0.000 % |
c |       100 |    2527     9157 |    1001      69      437     6.3 | 17.106 % |
c |       251 |    2275     8291 |    1101     184     1288     7.0 | 23.290 % |
c |       479 |    2222     8116 |    1211     405    12356    30.5 | 24.737 % |
c |       817 |    2140     7834 |    1332     728    30723    42.2 | 26.579 % |
c |      1325 |    2051     7545 |    1465    1216    60296    49.6 | 28.816 % |
c |      2084 |    2051     7545 |    1612    1090    50414    46.3 | 28.816 % |
c |      3224 |    2042     7516 |    1773    1271    56802    44.7 | 29.079 % |
c |      4933 |    2017     7435 |    1950    1932    93764    48.5 | 29.737 % |
c |      7498 |    2001     7383 |    2145    2233   107249    48.0 | 30.132 % |
c |     11344 |    2001     7383 |    2360    2385   116982    49.0 | 30.132 % |
c |     17112 |    2001     7383 |    2596    1452    64684    44.5 | 30.132 % |
c |     25763 |    2001     7383 |    2855    2790   130340    46.7 | 30.132 % |
c |     38739 |    2001     7383 |    3141    3023   144353    47.8 | 30.132 % |
c |     58200 |    2001     7383 |    3455    3420   149410    43.7 | 30.132 % |
c |     87392 |    1985     7331 |    3801    2307   105407    45.7 | 30.526 % |
c |    131185 |    1985     7331 |    4181    2761    99508    36.0 | 30.526 % |
c |    196870 |    1969     7279 |    4599    3063   138867    45.3 | 30.921 % |
c |    295397 |    1969     7279 |    5059    3058   118488    38.7 | 30.921 % |
c |    443189 |    1969     7279 |    5565    2813   105717    37.6 | 30.921 % |
c |    664872 |    1969     7279 |    6122    3516   144600    41.1 | 30.921 % |
c |    997397 |    1969     7279 |    6734    4152   186826    45.0 | 30.921 % |
c |   1496185 |    1969     7279 |    7407    5263   157190    29.9 | 30.921 % |
c ==============================================================================
c UNSATISFIABLE
s UNKNOWN
c _______________________________________________________________________________
c 
c restarts              : 23
c conflicts             : 1581496        (2464 /sec)
c decisions             : 1766760        (2753 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 641.731 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.00 0.00 0.04 2/54 11902
Raw data (stat): 11902 (runsolver) D 11901 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478435442 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 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.15 0.03 0.05 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 647 0 1 0 985 2 0 0 25 0 1 0 478435442 4153344 626 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1014 626 603 41 0 973 0
vsize: 4056
[startup+20.0013 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 731 0 1 0 1985 2 0 0 25 0 1 0 478435442 4562944 710 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1114 710 603 41 0 1073 0
vsize: 4456
[startup+30.0015 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 802 0 1 0 2984 2 0 0 25 0 1 0 478435442 4833280 781 4294967295 134512640 134672761 3221224544 3221223680 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1180 781 603 41 0 1139 0
vsize: 4720
[startup+40.0012 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 822 0 1 0 3984 3 0 0 25 0 1 0 478435442 4976640 801 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1215 801 603 41 0 1174 0
vsize: 4860
[startup+50.0023 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 899 0 1 0 4983 3 0 0 25 0 1 0 478435442 5246976 878 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1281 878 603 41 0 1240 0
vsize: 5124
[startup+60.0025 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 933 0 1 0 5983 3 0 0 25 0 1 0 478435442 5394432 912 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1317 912 603 41 0 1276 0
vsize: 5268
[startup+70.0032 s]
Raw data (loadavg): 0.69 0.21 0.11 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 977 0 1 0 6982 4 0 0 25 0 1 0 478435442 5677056 956 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1386 956 603 41 0 1345 0
vsize: 5544
[startup+80.0039 s]
Raw data (loadavg): 0.73 0.23 0.12 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 989 0 1 0 7982 4 0 0 25 0 1 0 478435442 5677056 968 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1386 968 603 41 0 1345 0
vsize: 5544
[startup+90.0036 s]
Raw data (loadavg): 0.77 0.26 0.12 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 999 0 1 0 8982 4 0 0 25 0 1 0 478435442 5677056 978 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1386 978 603 41 0 1345 0
vsize: 5544
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.13 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1006 0 1 0 9982 5 0 0 25 0 1 0 478435442 5824512 985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1422 985 603 41 0 1381 0
vsize: 5688
[startup+110.005 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1030 0 1 0 10981 5 0 0 25 0 1 0 478435442 5824512 1009 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1422 1009 603 41 0 1381 0
vsize: 5688
[startup+120.006 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1049 0 1 0 11981 5 0 0 25 0 1 0 478435442 5971968 1028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1458 1028 603 41 0 1417 0
vsize: 5832
[startup+130.006 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1054 0 1 0 12980 6 0 0 25 0 1 0 478435442 5971968 1033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1458 1033 603 41 0 1417 0
vsize: 5832
[startup+140.005 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1072 0 1 0 13980 6 0 0 25 0 1 0 478435442 6115328 1051 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1493 1051 603 41 0 1452 0
vsize: 5972
[startup+150.006 s]
Raw data (loadavg): 0.92 0.39 0.18 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1073 0 1 0 14980 6 0 0 25 0 1 0 478435442 6115328 1052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1493 1052 603 41 0 1452 0
vsize: 5972
[startup+160.006 s]
Raw data (loadavg): 0.93 0.41 0.19 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1085 0 1 0 15979 7 0 0 25 0 1 0 478435442 6115328 1064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1493 1064 603 41 0 1452 0
vsize: 5972
[startup+170.007 s]
Raw data (loadavg): 0.94 0.43 0.19 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1113 0 1 0 16979 7 0 0 25 0 1 0 478435442 6262784 1092 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1529 1092 603 41 0 1488 0
vsize: 6116
[startup+180.007 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1142 0 1 0 17979 7 0 0 25 0 1 0 478435442 6410240 1121 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1121 603 41 0 1524 0
vsize: 6260
[startup+190.008 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1145 0 1 0 18978 8 0 0 25 0 1 0 478435442 6410240 1124 4294967295 134512640 134672761 3221224544 3221223544 1075350371 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1124 603 41 0 1524 0
vsize: 6260
[startup+200.008 s]
Raw data (loadavg): 0.96 0.48 0.22 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1166 0 1 0 19978 8 0 0 25 0 1 0 478435442 6410240 1145 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1145 603 41 0 1524 0
vsize: 6260
[startup+210.008 s]
Raw data (loadavg): 0.97 0.50 0.22 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1168 0 1 0 20977 9 0 0 25 0 1 0 478435442 6410240 1147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1147 603 41 0 1524 0
vsize: 6260
[startup+220.009 s]
Raw data (loadavg): 0.97 0.51 0.23 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1169 0 1 0 21977 9 0 0 25 0 1 0 478435442 6410240 1148 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1148 603 41 0 1524 0
vsize: 6260
[startup+230.009 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1169 0 1 0 22977 9 0 0 25 0 1 0 478435442 6410240 1148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1148 603 41 0 1524 0
vsize: 6260
[startup+240.009 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1177 0 1 0 23977 10 0 0 25 0 1 0 478435442 6410240 1156 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1565 1156 603 41 0 1524 0
vsize: 6260
[startup+250.01 s]
Raw data (loadavg): 0.98 0.56 0.26 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1186 0 1 0 24976 10 0 0 25 0 1 0 478435442 6553600 1165 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1600 1165 603 41 0 1559 0
vsize: 6400
[startup+260.01 s]
Raw data (loadavg): 0.98 0.57 0.26 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1205 0 1 0 25975 11 0 0 25 0 1 0 478435442 6553600 1184 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1600 1184 603 41 0 1559 0
vsize: 6400
[startup+270.01 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1211 0 1 0 26975 11 0 0 25 0 1 0 478435442 6553600 1190 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1600 1190 603 41 0 1559 0
vsize: 6400
[startup+280.01 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1226 0 1 0 27975 11 0 0 25 0 1 0 478435442 6696960 1205 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1635 1205 603 41 0 1594 0
vsize: 6540
[startup+290.01 s]
Raw data (loadavg): 0.99 0.61 0.29 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1236 0 1 0 28974 12 0 0 25 0 1 0 478435442 6696960 1215 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1635 1215 603 41 0 1594 0
vsize: 6540
[startup+300.011 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1242 0 1 0 29974 12 0 0 25 0 1 0 478435442 6696960 1221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1635 1221 603 41 0 1594 0
vsize: 6540
[startup+310.011 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1254 0 1 0 30973 13 0 0 25 0 1 0 478435442 6860800 1233 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1233 603 41 0 1634 0
vsize: 6700
[startup+320.01 s]
Raw data (loadavg): 0.99 0.65 0.31 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1254 0 1 0 31973 13 0 0 25 0 1 0 478435442 6860800 1233 4294967295 134512640 134672761 3221224544 3221223728 134559379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1233 603 41 0 1634 0
vsize: 6700
[startup+330.011 s]
Raw data (loadavg): 0.99 0.66 0.31 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1267 0 1 0 32972 13 0 0 25 0 1 0 478435442 6860800 1246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1246 603 41 0 1634 0
vsize: 6700
[startup+340.011 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1274 0 1 0 33972 14 0 0 25 0 1 0 478435442 6860800 1253 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1675 1253 603 41 0 1634 0
vsize: 6700
[startup+350.011 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1278 0 1 0 34972 14 0 0 25 0 1 0 478435442 7008256 1257 4294967295 134512640 134672761 3221224544 3221223648 134555197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1711 1257 603 41 0 1670 0
vsize: 6844
[startup+360.012 s]
Raw data (loadavg): 0.99 0.69 0.33 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1308 0 1 0 35971 14 0 0 25 0 1 0 478435442 7155712 1287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1747 1287 603 41 0 1706 0
vsize: 6988
[startup+370.012 s]
Raw data (loadavg): 0.99 0.70 0.34 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1324 0 1 0 36971 15 0 0 25 0 1 0 478435442 7155712 1303 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1747 1303 603 41 0 1706 0
vsize: 6988
[startup+380.012 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1339 0 1 0 37971 15 0 0 25 0 1 0 478435442 7319552 1318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1787 1318 603 41 0 1746 0
vsize: 7148
[startup+390.012 s]
Raw data (loadavg): 0.99 0.72 0.35 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1340 0 1 0 38971 15 0 0 25 0 1 0 478435442 7319552 1319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1787 1319 603 41 0 1746 0
vsize: 7148
[startup+400.013 s]
Raw data (loadavg): 0.99 0.73 0.36 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1355 0 1 0 39970 16 0 0 25 0 1 0 478435442 7319552 1334 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1787 1334 603 41 0 1746 0
vsize: 7148
[startup+410.013 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1362 0 1 0 40970 16 0 0 25 0 1 0 478435442 7483392 1341 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1827 1341 603 41 0 1786 0
vsize: 7308
[startup+420.013 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1372 0 1 0 41970 16 0 0 25 0 1 0 478435442 7483392 1351 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1827 1351 603 41 0 1786 0
vsize: 7308
[startup+430.014 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1382 0 1 0 42969 16 0 0 25 0 1 0 478435442 7483392 1361 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1827 1361 603 41 0 1786 0
vsize: 7308
[startup+440.013 s]
Raw data (loadavg): 0.99 0.76 0.39 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1382 0 1 0 43969 17 0 0 25 0 1 0 478435442 7483392 1361 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1827 1361 603 41 0 1786 0
vsize: 7308
[startup+450.014 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1387 0 1 0 44969 17 0 0 25 0 1 0 478435442 7647232 1366 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1867 1366 603 41 0 1826 0
vsize: 7468
[startup+460.014 s]
Raw data (loadavg): 0.99 0.77 0.40 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1388 0 1 0 45968 18 0 0 25 0 1 0 478435442 7647232 1367 4294967295 134512640 134672761 3221224544 3221223736 134554697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1867 1367 603 41 0 1826 0
vsize: 7468
[startup+470.014 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1393 0 1 0 46968 18 0 0 25 0 1 0 478435442 7647232 1372 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1867 1372 603 41 0 1826 0
vsize: 7468
[startup+480.014 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1405 0 1 0 47968 18 0 0 25 0 1 0 478435442 7647232 1384 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1867 1384 603 41 0 1826 0
vsize: 7468
[startup+490.014 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1416 0 1 0 48968 18 0 0 25 0 1 0 478435442 7811072 1395 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1395 603 41 0 1866 0
vsize: 7628
[startup+500.014 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1416 0 1 0 49969 18 0 0 25 0 1 0 478435442 7811072 1395 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1395 603 41 0 1866 0
vsize: 7628
[startup+510.014 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1426 0 1 0 50969 18 0 0 25 0 1 0 478435442 7811072 1405 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1907 1405 603 41 0 1866 0
vsize: 7628
[startup+520.014 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1451 0 1 0 51968 18 0 0 25 0 1 0 478435442 7974912 1430 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1947 1430 603 41 0 1906 0
vsize: 7788
[startup+530.014 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1463 0 1 0 52969 18 0 0 25 0 1 0 478435442 7974912 1442 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1947 1442 603 41 0 1906 0
vsize: 7788
[startup+540.014 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1475 0 1 0 53969 18 0 0 25 0 1 0 478435442 8138752 1454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1454 603 41 0 1946 0
vsize: 7948
[startup+550.014 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1480 0 1 0 54969 18 0 0 25 0 1 0 478435442 8138752 1459 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1459 603 41 0 1946 0
vsize: 7948
[startup+560.013 s]
Raw data (loadavg): 0.99 0.83 0.46 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1486 0 1 0 55969 18 0 0 25 0 1 0 478435442 8138752 1465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1465 603 41 0 1946 0
vsize: 7948
[startup+570.013 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1492 0 1 0 56969 18 0 0 25 0 1 0 478435442 8138752 1471 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1987 1471 603 41 0 1946 0
vsize: 7948
[startup+580.013 s]
Raw data (loadavg): 0.99 0.84 0.47 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1504 0 1 0 57969 18 0 0 25 0 1 0 478435442 8302592 1483 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2027 1483 603 41 0 1986 0
vsize: 8108
[startup+590.012 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1504 0 1 0 58970 18 0 0 25 0 1 0 478435442 8302592 1483 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2027 1483 603 41 0 1986 0
vsize: 8108
[startup+600.013 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1509 0 1 0 59970 18 0 0 25 0 1 0 478435442 8302592 1488 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2027 1488 603 41 0 1986 0
vsize: 8108
[startup+610.013 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1516 0 1 0 60970 18 0 0 25 0 1 0 478435442 8302592 1495 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2027 1495 603 41 0 1986 0
vsize: 8108
[startup+620.012 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1516 0 1 0 61970 18 0 0 25 0 1 0 478435442 8302592 1495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2027 1495 603 41 0 1986 0
vsize: 8108
[startup+630.013 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1529 0 1 0 62970 18 0 0 25 0 1 0 478435442 8462336 1508 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2066 1508 603 41 0 2025 0
vsize: 8264
[startup+640.013 s]
Raw data (loadavg): 0.99 0.87 0.49 2/54 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1534 0 1 0 63970 18 0 0 25 0 1 0 478435442 8462336 1513 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2066 1513 603 41 0 2025 0
vsize: 8264
[startup+642.046 s]
Raw data (loadavg): 0.99 0.87 0.49 1/53 11902
Raw data (stat): 11902 (minisat+) R 11901 10614 10613 0 -1 0 1534 0 1 0 63970 18 0 0 25 0 1 0 478435442 8462336 1513 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2066 1513 603 41 0 2025 0
vsize: 0

Child status: 20
Real time (s): 642.045
CPU time (s): 641.921
CPU user time (s): 641.731
CPU system time (s): 0.189971
CPU usage (%): 99.9807
Max. virtual memory (Kb): 8264
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####