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_40_pb.cnf.cr.opb
MD5SUM85d4e2fa5fd7a61a85d3ecb1e311bddb
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 41
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.083986
Number of variables2800
Total number of constraints150
Number of constraints which are clauses80
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 constraint40

Trace number 6147 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 03:30:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4527 boxname=wulflinc7 idbench=15 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  85d4e2fa5fd7a61a85d3ecb1e311bddb  /oldhome/oroussel/tmp/wulflinc7/normalized-chnl35_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-chnl35_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc7/normalized-chnl35_40_pb.cnf.cr.opb
IDLAUNCH: 4527
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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		: 451.050
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:        874840 kB
Buffers:         38084 kB
Cached:         102268 kB
SwapCached:          0 kB
Active:          73104 kB
Inactive:        70156 kB
HighTotal:      131008 kB
HighFree:        24836 kB
LowTotal:       903652 kB
LowFree:        850004 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10956 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:50:38 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 4527 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 150 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  69]---> BDD-cost:   77
c ---[  68]---> BDD-cost:   77
c ---[  67]---> BDD-cost:   77
c ---[  66]---> BDD-cost:   77
c ---[  65]---> BDD-cost:   77
c ---[  64]---> BDD-cost:   77
c ---[  63]---> BDD-cost:   77
c ---[  62]---> BDD-cost:   77
c ---[  61]---> BDD-cost:   77
c ---[  60]---> BDD-cost:   77
c ---[  59]---> BDD-cost:   77
c ---[  58]---> BDD-cost:   77
c ---[  57]---> BDD-cost:   77
c ---[  56]---> BDD-cost:   77
c ---[  55]---> BDD-cost:   77
c ---[  54]---> BDD-cost:   77
c ---[  53]---> BDD-cost:   77
c ---[  52]---> BDD-cost:   77
c ---[  51]---> BDD-cost:   77
c ---[  50]---> BDD-cost:   77
c ---[  49]---> BDD-cost:   77
c ---[  48]---> BDD-cost:   77
c ---[  47]---> BDD-cost:   77
c ---[  46]---> BDD-cost:   77
c ---[  45]---> BDD-cost:   77
c ---[  44]---> BDD-cost:   77
c ---[  43]---> BDD-cost:   77
c ---[  42]---> BDD-cost:   77
c ---[  41]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:   77
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   77
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   77
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:   77
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   5]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   3]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   1]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   24020    69160 |    8006       0        0     nan |  0.000 % |
c |       100 |   23910    68830 |    8806      57     4229    74.2 |  1.123 % |
c |       250 |   23590    67870 |    9687      67     4255    63.5 |  1.905 % |
c |       477 |   23150    66550 |   10655     125     4533    36.3 |  2.979 % |
c |       819 |   22541    64725 |   11721     222    16844    75.9 |  4.469 % |
c |      1326 |   22391    64275 |   12893     660   100281   151.9 |  4.835 % |
c |      2085 |   22081    63345 |   14183    1307   248952   190.5 |  5.592 % |
c |      3224 |   22046    63240 |   15601    2425   495994   204.5 |  5.678 % |
c |      4933 |   21851    62655 |   17161    4064   927046   228.1 |  6.154 % |
c |      7496 |   21251    60855 |   18877    6390  1481071   231.8 |  7.619 % |
c |     11340 |   20021    57165 |   20765    9758  2605523   267.0 | 10.623 % |
c |     17111 |   18012    51140 |   22842   14765  3772413   255.5 | 15.531 % |
c |     25765 |   16202    45710 |   25126   22797  5955250   261.2 | 19.951 % |
c |     38739 |   14891    41785 |   27638   19726  5415582   274.5 | 23.162 % |
c |     58202 |   14111    39445 |   30402   19702  6272130   318.3 | 25.067 % |
c |     87394 |   13594    37900 |   33443   27983  8045979   287.5 | 26.337 % |
c |    131183 |   13240    36850 |   36787   23722  7676033   323.6 | 27.216 % |
c |    196871 |   12644    35070 |   40466   31055 10723649   345.3 | 28.681 % |
c |    295402 |   12146    33580 |   44512   30617 10287438   336.0 | 29.902 % |
#### 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.91 0.95 0.90 2/54 28831
Raw data (stat): 28831 (runsolver) R 28830 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423148338 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 2031 0 0 0 993 5 0 0 25 0 1 0 423148338 10260480 2005 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2505 2005 603 41 0 2464 0
vsize: 10020
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 2866 0 0 0 1990 7 0 0 25 0 1 0 423148338 13635584 2840 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3329 2840 603 41 0 3288 0
vsize: 13316
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 3002 0 0 0 2990 8 0 0 25 0 1 0 423148338 14176256 2976 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3461 2976 603 41 0 3420 0
vsize: 13844
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 3789 0 0 0 3988 9 0 0 25 0 1 0 423148338 17424384 3763 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4254 3763 603 41 0 4213 0
vsize: 17016
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 4096 0 0 0 4988 10 0 0 25 0 1 0 423148338 18767872 4070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4582 4070 603 41 0 4541 0
vsize: 18328
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 4490 0 0 0 5987 11 0 0 25 0 1 0 423148338 20389888 4464 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4978 4464 603 41 0 4937 0
vsize: 19912
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 4644 0 0 0 6987 11 0 0 25 0 1 0 423148338 20930560 4618 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5110 4618 603 41 0 5069 0
vsize: 20440
[startup+80.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 4826 0 0 0 7987 12 0 0 25 0 1 0 423148338 21737472 4800 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5307 4800 603 41 0 5266 0
vsize: 21228
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 5099 0 0 0 8986 13 0 0 25 0 1 0 423148338 22810624 5073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5073 603 41 0 5528 0
vsize: 22276
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 5316 0 0 0 9985 13 0 0 25 0 1 0 423148338 23752704 5290 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5799 5290 603 41 0 5758 0
vsize: 23196
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 5544 0 0 0 10984 15 0 0 25 0 1 0 423148338 24559616 5518 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5996 5518 603 41 0 5955 0
vsize: 23984
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 5600 0 0 0 11983 15 0 0 25 0 1 0 423148338 24829952 5574 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6062 5574 603 41 0 6021 0
vsize: 24248
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 6192 0 0 0 12982 16 0 0 25 0 1 0 423148338 27324416 6166 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6671 6166 603 41 0 6630 0
vsize: 26684
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 6513 0 0 0 13981 17 0 0 25 0 1 0 423148338 28667904 6487 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6999 6487 603 41 0 6958 0
vsize: 27996
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 6879 0 0 0 14980 18 0 0 25 0 1 0 423148338 30150656 6853 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7361 6853 603 41 0 7320 0
vsize: 29444
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 7135 0 0 0 15980 19 0 0 25 0 1 0 423148338 31232000 7109 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7625 7109 603 41 0 7584 0
vsize: 30500
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 7814 0 0 0 16978 20 0 0 25 0 1 0 423148338 33923072 7788 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8282 7788 603 41 0 8241 0
vsize: 33128
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 8191 0 0 0 17977 21 0 0 25 0 1 0 423148338 35545088 8165 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8678 8165 603 41 0 8637 0
vsize: 34712
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 8961 0 0 0 18976 23 0 0 25 0 1 0 423148338 38633472 8935 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9432 8935 603 41 0 9391 0
vsize: 37728
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9067 0 0 0 19976 23 0 0 25 0 1 0 423148338 39038976 9041 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9531 9041 603 41 0 9490 0
vsize: 38124
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 20976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 21976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 22976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 23976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 24976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9167 0 0 0 25976 23 0 0 25 0 1 0 423148338 39444480 9141 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9630 9141 603 41 0 9589 0
vsize: 38520
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 9761 0 0 0 26975 25 0 0 25 0 1 0 423148338 41865216 9735 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10221 9735 603 41 0 10180 0
vsize: 40884
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 10300 0 0 0 27974 26 0 0 25 0 1 0 423148338 44163072 10274 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10782 10274 603 41 0 10741 0
vsize: 43128
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11267 0 0 0 28973 28 0 0 25 0 1 0 423148338 48078848 11241 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11738 11241 603 41 0 11697 0
vsize: 46952
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 29973 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 30973 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 31973 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 32973 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 33973 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11433 0 0 0 34974 28 0 0 25 0 1 0 423148338 48750592 11407 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11902 11407 603 41 0 11861 0
vsize: 47608
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 11814 0 0 0 35973 29 0 0 25 0 1 0 423148338 50368512 11788 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12297 11788 603 41 0 12256 0
vsize: 49188
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12296 0 0 0 36972 30 0 0 25 0 1 0 423148338 52264960 12270 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 12270 603 41 0 12719 0
vsize: 51040
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 37972 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 38972 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 39973 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 40973 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 41973 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 42973 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 12348 0 0 0 43974 30 0 0 25 0 1 0 423148338 52535296 12322 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12826 12322 603 41 0 12785 0
vsize: 51304
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 44972 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223392 134565745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 45972 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 46972 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 47973 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 48973 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13129 0 0 0 49973 32 0 0 25 0 1 0 423148338 55762944 13103 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 13103 603 41 0 13573 0
vsize: 54456
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 13342 0 0 0 50973 32 0 0 25 0 1 0 423148338 56573952 13316 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13812 13317 603 41 0 13771 0
vsize: 55248
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14330 0 0 0 51970 35 0 0 25 0 1 0 423148338 60633088 14304 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14803 14304 603 41 0 14762 0
vsize: 59212
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 52970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 53970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 54971 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 55971 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 56970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 57970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223648 134560028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 58970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14531 0 0 0 59970 35 0 0 25 0 1 0 423148338 61444096 14505 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 14505 603 41 0 14960 0
vsize: 60004
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 14845 0 0 0 60970 36 0 0 25 0 1 0 423148338 62791680 14819 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15330 14819 603 41 0 15289 0
vsize: 61320
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 15532 0 0 0 61968 37 0 0 25 0 1 0 423148338 65609728 15506 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 15506 603 41 0 15977 0
vsize: 64072
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16254 0 0 0 62967 40 0 0 25 0 1 0 423148338 68546560 16228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16735 16228 603 41 0 16694 0
vsize: 66940
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 63965 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 64965 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 65966 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 66966 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 67966 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 68966 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 69966 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16679 0 0 0 70967 41 0 0 25 0 1 0 423148338 70299648 16653 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16653 603 41 0 17122 0
vsize: 68652
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 16913 0 0 0 71966 42 0 0 25 0 1 0 423148338 71245824 16887 4294967295 134512640 134672761 3221224544 3221223648 134560171 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17394 16887 603 41 0 17353 0
vsize: 69576
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 17804 0 0 0 72965 44 0 0 25 0 1 0 423148338 74903552 17778 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18287 17778 603 41 0 18246 0
vsize: 73148
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18232 0 0 0 73963 45 0 0 25 0 1 0 423148338 76664832 18206 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18206 603 41 0 18676 0
vsize: 74868
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 74964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223648 134559993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 75964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 76964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 77964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 78964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 79965 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+810.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 80965 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+820.015 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 81965 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+830.015 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 82964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+840.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 83964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+850.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18233 0 0 0 84964 45 0 0 25 0 1 0 423148338 76664832 18207 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18717 18207 603 41 0 18676 0
vsize: 74868
[startup+860.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18628 0 0 0 85964 46 0 0 25 0 1 0 423148338 78270464 18602 4294967295 134512640 134672761 3221224544 3221223600 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19109 18602 603 41 0 19068 0
vsize: 76436
[startup+870.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 86964 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+880.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 87964 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+890.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 88964 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+900.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 89964 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+910.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 90965 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+920.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 91965 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+930.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 92965 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+940.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 93965 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+950.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 94965 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+960.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18647 0 0 0 95966 46 0 0 25 0 1 0 423148338 78405632 18621 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19142 18621 603 41 0 19101 0
vsize: 76568
[startup+970.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 18838 0 0 0 96965 47 0 0 25 0 1 0 423148338 79208448 18812 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19338 18812 603 41 0 19297 0
vsize: 77352
[startup+980.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19252 0 0 0 97964 48 0 0 25 0 1 0 423148338 80814080 19226 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19730 19226 603 41 0 19689 0
vsize: 78920
[startup+990.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 98964 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 99964 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 100965 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 101965 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 102965 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 103965 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 104965 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 105966 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 106966 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19284 0 0 0 107966 48 0 0 25 0 1 0 423148338 80949248 19258 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19258 603 41 0 19722 0
vsize: 79052
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 19839 0 0 0 108964 50 0 0 25 0 1 0 423148338 83263488 19813 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20328 19813 603 41 0 20287 0
vsize: 81312
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 20630 0 0 0 109964 51 0 0 25 0 1 0 423148338 86511616 20604 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21121 20604 603 41 0 21080 0
vsize: 84484
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 21516 0 0 0 110962 53 0 0 25 0 1 0 423148338 90173440 21490 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22015 21490 603 41 0 21974 0
vsize: 88060
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 111961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 112961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 113961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 114961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 115962 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 116961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 117961 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 118962 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28831
Raw data (stat): 28831 (minisat+) R 28830 22932 22931 0 -1 0 22035 0 0 0 119962 54 0 0 25 0 1 0 423148338 92307456 22009 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 22009 603 41 0 22495 0
vsize: 90144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28831
Raw data (stat): 28831 (minisat+) Z 28830 22932 22931 0 -1 12 22037 0 0 0 119962 58 0 0 25 0 1 0 423148338 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.62
CPU system time (s): 0.58691
CPU usage (%): 100.012
Max. virtual memory (Kb): 90144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####