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-chnl35_45_pb.cnf.cr.opb
MD5SUM1f5fb3c191c2c77719f10f35e4f5f992
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 46
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.094985
Number of variables3150
Total number of constraints160
Number of constraints which are clauses90
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint45

Trace number 4695 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 20:12:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=140 boxname=wulflinc32 idbench=16 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  1f5fb3c191c2c77719f10f35e4f5f992  /oldhome/oroussel/tmp/wulflinc32/normalized-chnl35_45_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc32/normalized-chnl35_45_pb.cnf.cr.opb
IDLAUNCH: 140
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        753612 kB
Buffers:         33748 kB
Cached:         135924 kB
SwapCached:       1212 kB
Active:         138268 kB
Inactive:       111720 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        753356 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25216 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:21:55 (client local time) WITH STATUS 0 IN 545.701 SECONDS
stats: 140 7 545.701 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
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:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15210    42490 |    5070       0        0     nan |  0.000 % |
c |       101 |   15210    42490 |    5577     101    13595   134.6 |  0.758 % |
c |       253 |   15210    42490 |    6134     253    41155   162.7 |  0.758 % |
c |       480 |   15210    42490 |    6748     480    87737   182.8 |  0.758 % |
c |       819 |   15210    42490 |    7422     819   152105   185.7 |  0.758 % |
c |      1328 |   15210    42490 |    8165    1328   233504   175.8 |  0.758 % |
c |      2088 |   15210    42490 |    8981    2088   381775   182.8 |  0.758 % |
c |      3227 |   15210    42490 |    9879    3227   722388   223.9 |  0.758 % |
c |      4937 |   15210    42490 |   10867    4937  1190498   241.1 |  0.758 % |
c |      7499 |   15210    42490 |   11954    7499  1875349   250.1 |  0.758 % |
c |     11348 |   15210    42490 |   13150   11348  2998324   264.2 |  0.758 % |
c |     17114 |   15210    42490 |   14465    8729  2872831   329.1 |  0.758 % |
c |     25764 |   15210    42490 |   15911   17379  5578930   321.0 |  0.758 % |
c |     38739 |   15210    42490 |   17503   11971  5497632   459.2 |  0.758 % |
c |     58200 |   15210    42490 |   19253   10805  3533507   327.0 |  0.758 % |
c |     87395 |   15210    42490 |   21178   25607  7805831   304.8 |  0.758 % |
#### 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.93 0.98 0.90 2/53 10941
Raw data (stat): 10941 (runsolver) R 10940 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478733775 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.94 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 2937 0 0 0 992 6 0 0 25 0 1 0 478733775 13795328 2912 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3368 2912 603 41 0 3327 0
vsize: 13472
[startup+20.0031 s]
Raw data (loadavg): 0.95 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 4831 0 0 0 1988 10 0 0 25 0 1 0 478733775 21622784 4806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5279 4806 603 41 0 5238 0
vsize: 21116
[startup+30.0036 s]
Raw data (loadavg): 0.95 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 6168 0 0 0 2985 14 0 0 25 0 1 0 478733775 27222016 6143 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6646 6143 603 41 0 6605 0
vsize: 26584
[startup+40.0049 s]
Raw data (loadavg): 0.96 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 6277 0 0 0 3984 14 0 0 25 0 1 0 478733775 27627520 6252 4294967295 134512640 134672761 3221224624 3221223840 134558115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6745 6252 603 41 0 6704 0
vsize: 26980
[startup+50.0054 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 6277 0 0 0 4984 15 0 0 25 0 1 0 478733775 27627520 6252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6745 6252 603 41 0 6704 0
vsize: 26980
[startup+60.0059 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 7003 0 0 0 5981 17 0 0 25 0 1 0 478733775 30605312 6978 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7472 6978 603 41 0 7431 0
vsize: 29888
[startup+70.0069 s]
Raw data (loadavg): 0.97 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 7003 0 0 0 6982 17 0 0 25 0 1 0 478733775 30605312 6978 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7472 6978 603 41 0 7431 0
vsize: 29888
[startup+80.0077 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 7520 0 0 0 7981 18 0 0 25 0 1 0 478733775 32772096 7495 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8001 7495 603 41 0 7960 0
vsize: 32004
[startup+90.0081 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 8540 0 0 0 8979 20 0 0 25 0 1 0 478733775 36966400 8515 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9025 8515 603 41 0 8984 0
vsize: 36100
[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 8815 0 0 0 9978 21 0 0 25 0 1 0 478733775 38043648 8790 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9288 8790 603 41 0 9247 0
vsize: 37152
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 8815 0 0 0 10978 21 0 0 25 0 1 0 478733775 38043648 8790 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8790 603 41 0 9247 0
vsize: 37152
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 9121 0 0 0 11976 23 0 0 25 0 1 0 478733775 39260160 9096 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9585 9096 603 41 0 9544 0
vsize: 38340
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10077 0 0 0 12974 25 0 0 25 0 1 0 478733775 43180032 10052 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10542 10052 603 41 0 10501 0
vsize: 42168
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10355 0 0 0 13974 26 0 0 25 0 1 0 478733775 44396544 10330 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10330 603 41 0 10798 0
vsize: 43356
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10355 0 0 0 14974 26 0 0 25 0 1 0 478733775 44396544 10330 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10330 603 41 0 10798 0
vsize: 43356
[startup+160.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10356 0 0 0 15974 26 0 0 25 0 1 0 478733775 44396544 10331 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+170.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10356 0 0 0 16975 26 0 0 25 0 1 0 478733775 44396544 10331 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10356 0 0 0 17975 26 0 0 25 0 1 0 478733775 44396544 10331 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+190.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10356 0 0 0 18975 26 0 0 25 0 1 0 478733775 44396544 10331 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+200.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10357 0 0 0 19975 26 0 0 25 0 1 0 478733775 44396544 10332 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10332 603 41 0 10798 0
vsize: 43356
[startup+210.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10359 0 0 0 20975 26 0 0 25 0 1 0 478733775 44396544 10334 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10334 603 41 0 10798 0
vsize: 43356
[startup+220.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 21975 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+230.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 22976 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+240.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 23976 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+250.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 24976 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223728 134555114 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+260.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 25976 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+270.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 26976 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+280.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 27977 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+290.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10360 0 0 0 28977 26 0 0 25 0 1 0 478733775 44396544 10335 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+300.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10401 0 0 0 29976 26 0 0 25 0 1 0 478733775 44531712 10376 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10872 10376 603 41 0 10831 0
vsize: 43488
[startup+310.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10401 0 0 0 30977 26 0 0 25 0 1 0 478733775 44531712 10376 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10872 10376 603 41 0 10831 0
vsize: 43488
[startup+320.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10401 0 0 0 31977 26 0 0 25 0 1 0 478733775 44531712 10376 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10872 10376 603 41 0 10831 0
vsize: 43488
[startup+330.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10689 0 0 0 32976 27 0 0 25 0 1 0 478733775 45744128 10664 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 10664 603 41 0 11127 0
vsize: 44672
[startup+340.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10689 0 0 0 33977 27 0 0 25 0 1 0 478733775 45744128 10664 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 10664 603 41 0 11127 0
vsize: 44672
[startup+350.026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10689 0 0 0 34977 27 0 0 25 0 1 0 478733775 45744128 10664 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 10664 603 41 0 11127 0
vsize: 44672
[startup+360.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10689 0 0 0 35977 27 0 0 25 0 1 0 478733775 45744128 10664 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 10664 603 41 0 11127 0
vsize: 44672
[startup+370.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 10689 0 0 0 36977 27 0 0 25 0 1 0 478733775 45744128 10664 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 10664 603 41 0 11127 0
vsize: 44672
[startup+380.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 11028 0 0 0 37977 28 0 0 25 0 1 0 478733775 47091712 11003 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11497 11003 603 41 0 11456 0
vsize: 45988
[startup+390.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 11574 0 0 0 38976 29 0 0 25 0 1 0 478733775 49381376 11549 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12056 11549 603 41 0 12015 0
vsize: 48224
[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 12207 0 0 0 39974 30 0 0 25 0 1 0 478733775 51945472 12182 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12682 12182 603 41 0 12641 0
vsize: 50728
[startup+410.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 12852 0 0 0 40973 32 0 0 25 0 1 0 478733775 54640640 12827 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13340 12827 603 41 0 13299 0
vsize: 53360
[startup+420.031 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 13396 0 0 0 41972 33 0 0 25 0 1 0 478733775 56832000 13371 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13875 13371 603 41 0 13834 0
vsize: 55500
[startup+430.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14003 0 0 0 42970 35 0 0 25 0 1 0 478733775 59400192 13978 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14502 13978 603 41 0 14461 0
vsize: 58008
[startup+440.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14436 0 0 0 43969 37 0 0 25 0 1 0 478733775 61210624 14411 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14411 603 41 0 14903 0
vsize: 59776
[startup+450.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14436 0 0 0 44969 37 0 0 25 0 1 0 478733775 61210624 14411 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14411 603 41 0 14903 0
vsize: 59776
[startup+460.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14437 0 0 0 45970 37 0 0 25 0 1 0 478733775 61210624 14412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14412 603 41 0 14903 0
vsize: 59776
[startup+470.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14437 0 0 0 46970 37 0 0 25 0 1 0 478733775 61210624 14412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14412 603 41 0 14903 0
vsize: 59776
[startup+480.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14437 0 0 0 47970 37 0 0 25 0 1 0 478733775 61210624 14412 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14412 603 41 0 14903 0
vsize: 59776
[startup+490.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14438 0 0 0 48970 37 0 0 25 0 1 0 478733775 61210624 14413 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14413 603 41 0 14903 0
vsize: 59776
[startup+500.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14452 0 0 0 49971 37 0 0 25 0 1 0 478733775 61210624 14427 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14944 14427 603 41 0 14903 0
vsize: 59776
[startup+510.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14463 0 0 0 50971 37 0 0 25 0 1 0 478733775 61370368 14438 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14983 14438 603 41 0 14942 0
vsize: 59932
[startup+520.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 14478 0 0 0 51971 37 0 0 25 0 1 0 478733775 61370368 14453 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14983 14453 603 41 0 14942 0
vsize: 59932
[startup+530.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 15090 0 0 0 52970 38 0 0 25 0 1 0 478733775 63946752 15065 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15612 15065 603 41 0 15571 0
vsize: 62448
[startup+540.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/53 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 15543 0 0 0 53970 39 0 0 25 0 1 0 478733775 65703936 15518 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16041 15518 603 41 0 16000 0
vsize: 64164
[startup+545.653 s]
Raw data (loadavg): 0.99 0.98 0.91 1/52 10941
Raw data (stat): 10941 (minisat+) R 10940 7987 7986 0 -1 0 15543 0 0 0 53970 39 0 0 25 0 1 0 478733775 65703936 15518 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16041 15518 603 41 0 16000 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 545.652
CPU time (s): 545.701
CPU user time (s): 545.271
CPU system time (s): 0.429934
CPU usage (%): 100.009
Max. virtual memory (Kb): 64164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####