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-chnl20_25_pb.cnf.cr.opb
MD5SUM6c328ef6f9d8d5a179eec9bf3550b7fd
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 26
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.027995
Number of variables1000
Total number of constraints90
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint25

Trace number 6087 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 03:21:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4521 boxname=wulflinc22 idbench=9 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6c328ef6f9d8d5a179eec9bf3550b7fd  /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_25_pb.cnf.cr.opb
IDLAUNCH: 4521
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        827880 kB
Buffers:         33240 kB
Cached:         130252 kB
SwapCached:        524 kB
Active:          50364 kB
Inactive:       116524 kB
HighTotal:      131008 kB
HighFree:         7000 kB
LowTotal:       903652 kB
LowFree:        820880 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34252 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:41:35 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4521 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> BDD-cost:   47
c ---[  38]---> BDD-cost:   47
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:   47
c ---[  35]---> BDD-cost:   47
c ---[  34]---> BDD-cost:   47
c ---[  33]---> BDD-cost:   47
c ---[  32]---> BDD-cost:   47
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:   47
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8330    23920 |    2776       0        0     nan |  0.000 % |
c |       101 |    8330    23920 |    3053     101     6919    68.5 |  1.389 % |
c |       251 |    8025    23005 |    3358     115     6957    60.5 |  3.542 % |
c |       477 |    7675    21955 |    3694     192    12671    66.0 |  5.938 % |
c |       814 |    7665    21925 |    4064     525    49843    94.9 |  6.007 % |
c |      1321 |    7570    21640 |    4470     987    94615    95.9 |  6.667 % |
c |      2080 |    7410    21160 |    4917    1678   176408   105.1 |  7.778 % |
c |      3219 |    7345    20965 |    5409    2799   337002   120.4 |  8.229 % |
c |      4927 |    7135    20335 |    5950    4410   521083   118.2 |  9.688 % |
c |      7492 |    6950    19780 |    6545    6885   846383   122.9 | 10.972 % |
c |     11338 |    6470    18340 |    7200    3630   399408   110.0 | 14.306 % |
c |     17105 |    6216    17580 |    7920    5453   887007   162.7 | 16.076 % |
c |     25756 |    6121    17295 |    8712    5459  1012382   185.5 | 16.736 % |
c |     38730 |    5986    16890 |    9583    8728  1595241   182.8 | 17.674 % |
c |     58191 |    5637    15845 |   10541    7112   818611   115.1 | 20.104 % |
c |     87384 |    5248    14680 |   11596    6974   792316   113.6 | 22.813 % |
c |    131174 |    4963    13825 |   12755   11520  1399276   121.5 | 24.792 % |
c |    196858 |    4632    12840 |   14031   13671  2724059   199.3 | 27.118 % |
c |    295386 |    4299    11855 |   15434   13114  2463663   187.9 | 29.479 % |
c |    443177 |    4081    11205 |   16977    9055  1850021   204.3 | 31.007 % |
#### 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.90 0.94 0.90 2/54 31713
Raw data (stat): 31713 (runsolver) R 31712 26298 26297 0 -1 64 1 0 0 0 0 0 0 0 19 0 1 0 481309211 1052672 97 4294967295 134512640 135381576 3221224432 3221219804 135024789 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 1547 0 0 0 995 3 0 0 25 0 1 0 481309211 7884800 1525 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1925 1525 603 41 0 1884 0
vsize: 7700
[startup+20.0013 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 1838 0 0 0 1995 4 0 0 25 0 1 0 481309211 9093120 1816 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2220 1816 603 41 0 2179 0
vsize: 8880
[startup+30.0024 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 2427 0 0 0 2993 5 0 0 25 0 1 0 481309211 11571200 2405 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2825 2405 603 41 0 2784 0
vsize: 11300
[startup+40.0027 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 2645 0 0 0 3992 6 0 0 25 0 1 0 481309211 12369920 2623 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2623 603 41 0 2979 0
vsize: 12080
[startup+50.0025 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 2816 0 0 0 4992 7 0 0 25 0 1 0 481309211 13180928 2794 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3218 2794 603 41 0 3177 0
vsize: 12872
[startup+60.0028 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 2819 0 0 0 5992 7 0 0 25 0 1 0 481309211 13180928 2797 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3218 2797 603 41 0 3177 0
vsize: 12872
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 2836 0 0 0 6992 7 0 0 25 0 1 0 481309211 13180928 2814 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3218 2814 603 41 0 3177 0
vsize: 12872
[startup+80.0036 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3059 0 0 0 7992 7 0 0 25 0 1 0 481309211 14135296 3037 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3451 3037 603 41 0 3410 0
vsize: 13804
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3074 0 0 0 8992 8 0 0 25 0 1 0 481309211 14270464 3052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3052 603 41 0 3443 0
vsize: 13936
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3093 0 0 0 9991 8 0 0 25 0 1 0 481309211 14270464 3071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3071 603 41 0 3443 0
vsize: 13936
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3093 0 0 0 10991 8 0 0 25 0 1 0 481309211 14270464 3071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3071 603 41 0 3443 0
vsize: 13936
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3094 0 0 0 11991 9 0 0 25 0 1 0 481309211 14270464 3072 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3072 603 41 0 3443 0
vsize: 13936
[startup+130.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3095 0 0 0 12991 9 0 0 25 0 1 0 481309211 14270464 3073 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3073 603 41 0 3443 0
vsize: 13936
[startup+140.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3095 0 0 0 13991 9 0 0 25 0 1 0 481309211 14270464 3073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3073 603 41 0 3443 0
vsize: 13936
[startup+150.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3095 0 0 0 14991 10 0 0 25 0 1 0 481309211 14270464 3073 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3073 603 41 0 3443 0
vsize: 13936
[startup+160.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3095 0 0 0 15990 10 0 0 25 0 1 0 481309211 14270464 3073 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3073 603 41 0 3443 0
vsize: 13936
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3096 0 0 0 16990 10 0 0 25 0 1 0 481309211 14270464 3074 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3074 603 41 0 3443 0
vsize: 13936
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3096 0 0 0 17990 11 0 0 25 0 1 0 481309211 14270464 3074 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3484 3074 603 41 0 3443 0
vsize: 13936
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3141 0 0 0 18990 11 0 0 25 0 1 0 481309211 14553088 3119 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3553 3119 603 41 0 3512 0
vsize: 14212
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3159 0 0 0 19989 12 0 0 25 0 1 0 481309211 14700544 3137 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3589 3137 603 41 0 3548 0
vsize: 14356
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3165 0 0 0 20989 12 0 0 25 0 1 0 481309211 14700544 3143 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3589 3143 603 41 0 3548 0
vsize: 14356
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3165 0 0 0 21989 12 0 0 25 0 1 0 481309211 14700544 3143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3589 3143 603 41 0 3548 0
vsize: 14356
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3393 0 0 0 22988 14 0 0 25 0 1 0 481309211 15663104 3371 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3824 3371 603 41 0 3783 0
vsize: 15296
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3431 0 0 0 23988 14 0 0 25 0 1 0 481309211 15798272 3409 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3857 3409 603 41 0 3816 0
vsize: 15428
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3431 0 0 0 24988 14 0 0 25 0 1 0 481309211 15798272 3409 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3857 3409 603 41 0 3816 0
vsize: 15428
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3447 0 0 0 25987 14 0 0 25 0 1 0 481309211 15798272 3425 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3857 3425 603 41 0 3816 0
vsize: 15428
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3557 0 0 0 26987 15 0 0 25 0 1 0 481309211 16379904 3535 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3999 3535 603 41 0 3958 0
vsize: 15996
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3590 0 0 0 27987 15 0 0 25 0 1 0 481309211 16543744 3568 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4039 3568 603 41 0 3998 0
vsize: 16156
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3674 0 0 0 28987 15 0 0 25 0 1 0 481309211 16814080 3652 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4105 3652 603 41 0 4064 0
vsize: 16420
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 3849 0 0 0 29987 16 0 0 25 0 1 0 481309211 17625088 3827 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3827 603 41 0 4262 0
vsize: 17212
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4457 0 0 0 30985 18 0 0 25 0 1 0 481309211 20037632 4435 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4892 4435 603 41 0 4851 0
vsize: 19568
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4457 0 0 0 31985 18 0 0 25 0 1 0 481309211 20037632 4435 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4892 4435 603 41 0 4851 0
vsize: 19568
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4657 0 0 0 32984 19 0 0 25 0 1 0 481309211 20848640 4635 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5090 4635 603 41 0 5049 0
vsize: 20360
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4939 0 0 0 33984 19 0 0 25 0 1 0 481309211 22056960 4917 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5385 4917 603 41 0 5344 0
vsize: 21540
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4939 0 0 0 34984 20 0 0 25 0 1 0 481309211 22056960 4917 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5385 4917 603 41 0 5344 0
vsize: 21540
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 4939 0 0 0 35984 20 0 0 25 0 1 0 481309211 22056960 4917 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5385 4917 603 41 0 5344 0
vsize: 21540
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 36983 20 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 37983 21 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 38983 21 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 39983 21 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 40983 21 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 41983 21 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 42983 22 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 43983 22 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5073 0 0 0 44982 22 0 0 25 0 1 0 481309211 22593536 5051 4294967295 134512640 134672761 3221224544 3221223728 134559509 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5051 603 41 0 5475 0
vsize: 22064
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5100 0 0 0 45982 23 0 0 25 0 1 0 481309211 22757376 5078 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5556 5078 603 41 0 5515 0
vsize: 22224
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5413 0 0 0 46981 24 0 0 25 0 1 0 481309211 23957504 5391 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5849 5391 603 41 0 5808 0
vsize: 23396
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5419 0 0 0 47981 25 0 0 25 0 1 0 481309211 24109056 5397 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5397 603 41 0 5845 0
vsize: 23544
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5424 0 0 0 48981 25 0 0 25 0 1 0 481309211 24109056 5402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5402 603 41 0 5845 0
vsize: 23544
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5442 0 0 0 49980 25 0 0 25 0 1 0 481309211 24109056 5420 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5420 603 41 0 5845 0
vsize: 23544
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5454 0 0 0 50980 25 0 0 25 0 1 0 481309211 24244224 5432 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5432 603 41 0 5878 0
vsize: 23676
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5454 0 0 0 51980 26 0 0 25 0 1 0 481309211 24244224 5432 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5432 603 41 0 5878 0
vsize: 23676
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5455 0 0 0 52981 26 0 0 25 0 1 0 481309211 24244224 5433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5433 603 41 0 5878 0
vsize: 23676
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5455 0 0 0 53980 26 0 0 25 0 1 0 481309211 24244224 5433 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5433 603 41 0 5878 0
vsize: 23676
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5455 0 0 0 54980 26 0 0 25 0 1 0 481309211 24244224 5433 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5433 603 41 0 5878 0
vsize: 23676
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5461 0 0 0 55980 26 0 0 25 0 1 0 481309211 24244224 5439 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5439 603 41 0 5878 0
vsize: 23676
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5484 0 0 0 56980 27 0 0 25 0 1 0 481309211 24379392 5462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5952 5462 603 41 0 5911 0
vsize: 23808
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5513 0 0 0 57980 27 0 0 25 0 1 0 481309211 24518656 5491 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5986 5491 603 41 0 5945 0
vsize: 23944
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5705 0 0 0 58979 28 0 0 25 0 1 0 481309211 25632768 5683 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6258 5683 603 41 0 6217 0
vsize: 25032
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5804 0 0 0 59978 29 0 0 25 0 1 0 481309211 26222592 5782 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6402 5782 603 41 0 6361 0
vsize: 25608
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5820 0 0 0 60978 29 0 0 25 0 1 0 481309211 26222592 5798 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6402 5798 603 41 0 6361 0
vsize: 25608
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5820 0 0 0 61977 30 0 0 25 0 1 0 481309211 26222592 5798 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6402 5798 603 41 0 6361 0
vsize: 25608
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5844 0 0 0 62977 30 0 0 25 0 1 0 481309211 26415104 5822 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6449 5822 603 41 0 6408 0
vsize: 25796
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5856 0 0 0 63977 30 0 0 25 0 1 0 481309211 26415104 5834 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6449 5834 603 41 0 6408 0
vsize: 25796
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5856 0 0 0 64977 30 0 0 25 0 1 0 481309211 26415104 5834 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6449 5834 603 41 0 6408 0
vsize: 25796
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5856 0 0 0 65977 31 0 0 25 0 1 0 481309211 26415104 5834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6449 5834 603 41 0 6408 0
vsize: 25796
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 5911 0 0 0 66976 31 0 0 25 0 1 0 481309211 26685440 5889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6515 5889 603 41 0 6474 0
vsize: 26060
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6139 0 0 0 67976 32 0 0 25 0 1 0 481309211 27631616 6117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6746 6117 603 41 0 6705 0
vsize: 26984
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6155 0 0 0 68976 32 0 0 25 0 1 0 481309211 27787264 6133 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6784 6133 603 41 0 6743 0
vsize: 27136
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6214 0 0 0 69976 32 0 0 25 0 1 0 481309211 27947008 6192 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6823 6192 603 41 0 6782 0
vsize: 27292
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6241 0 0 0 70976 32 0 0 25 0 1 0 481309211 28110848 6219 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6863 6219 603 41 0 6822 0
vsize: 27452
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6241 0 0 0 71976 32 0 0 25 0 1 0 481309211 28110848 6219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6863 6219 603 41 0 6822 0
vsize: 27452
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6241 0 0 0 72976 33 0 0 25 0 1 0 481309211 28110848 6219 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6863 6219 603 41 0 6822 0
vsize: 27452
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6431 0 0 0 73975 34 0 0 25 0 1 0 481309211 28913664 6409 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7059 6409 603 41 0 7018 0
vsize: 28236
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 6749 0 0 0 74973 35 0 0 25 0 1 0 481309211 30265344 6727 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7389 6727 603 41 0 7348 0
vsize: 29556
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7008 0 0 0 75973 36 0 0 25 0 1 0 481309211 31346688 6986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7653 6986 603 41 0 7612 0
vsize: 30612
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7178 0 0 0 76972 37 0 0 25 0 1 0 481309211 32030720 7156 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7820 7156 603 41 0 7779 0
vsize: 31280
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7196 0 0 0 77972 37 0 0 25 0 1 0 481309211 32194560 7174 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7860 7174 603 41 0 7819 0
vsize: 31440
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7226 0 0 0 78972 37 0 0 25 0 1 0 481309211 32358400 7204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7900 7204 603 41 0 7859 0
vsize: 31600
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7252 0 0 0 79972 37 0 0 25 0 1 0 481309211 32522240 7230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7940 7230 603 41 0 7899 0
vsize: 31760
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7381 0 0 0 80971 38 0 0 25 0 1 0 481309211 32927744 7359 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8039 7359 603 41 0 7998 0
vsize: 32156
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7481 0 0 0 81971 39 0 0 25 0 1 0 481309211 33341440 7459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8140 7459 603 41 0 8099 0
vsize: 32560
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7481 0 0 0 82971 39 0 0 25 0 1 0 481309211 33341440 7459 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8140 7459 603 41 0 8099 0
vsize: 32560
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7481 0 0 0 83971 39 0 0 25 0 1 0 481309211 33341440 7459 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8140 7459 603 41 0 8099 0
vsize: 32560
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7482 0 0 0 84971 39 0 0 25 0 1 0 481309211 33341440 7460 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8140 7460 603 41 0 8099 0
vsize: 32560
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7494 0 0 0 85971 40 0 0 25 0 1 0 481309211 33525760 7472 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7472 603 41 0 8144 0
vsize: 32740
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7494 0 0 0 86971 40 0 0 25 0 1 0 481309211 33525760 7472 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7472 603 41 0 8144 0
vsize: 32740
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7494 0 0 0 87971 40 0 0 25 0 1 0 481309211 33525760 7472 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7472 603 41 0 8144 0
vsize: 32740
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7494 0 0 0 88971 40 0 0 25 0 1 0 481309211 33525760 7472 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7472 603 41 0 8144 0
vsize: 32740
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7506 0 0 0 89971 40 0 0 25 0 1 0 481309211 33525760 7484 4294967295 134512640 134672761 3221224544 3221223612 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7484 603 41 0 8144 0
vsize: 32740
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7557 0 0 0 90970 40 0 0 25 0 1 0 481309211 33853440 7535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8265 7535 603 41 0 8224 0
vsize: 33060
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7583 0 0 0 91970 41 0 0 25 0 1 0 481309211 34017280 7561 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8305 7561 603 41 0 8264 0
vsize: 33220
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7588 0 0 0 92970 41 0 0 25 0 1 0 481309211 34017280 7566 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8305 7566 603 41 0 8264 0
vsize: 33220
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7605 0 0 0 93970 42 0 0 25 0 1 0 481309211 34168832 7583 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8342 7583 603 41 0 8301 0
vsize: 33368
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7618 0 0 0 94970 42 0 0 25 0 1 0 481309211 34168832 7596 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8342 7596 603 41 0 8301 0
vsize: 33368
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7630 0 0 0 95970 42 0 0 25 0 1 0 481309211 34328576 7608 4294967295 134512640 134672761 3221224544 3221223500 1075350787 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7608 603 41 0 8340 0
vsize: 33524
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7630 0 0 0 96969 42 0 0 25 0 1 0 481309211 34328576 7608 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7608 603 41 0 8340 0
vsize: 33524
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7630 0 0 0 97969 43 0 0 25 0 1 0 481309211 34328576 7608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7608 603 41 0 8340 0
vsize: 33524
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7636 0 0 0 98969 43 0 0 25 0 1 0 481309211 34328576 7614 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7614 603 41 0 8340 0
vsize: 33524
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7658 0 0 0 99969 43 0 0 25 0 1 0 481309211 34328576 7636 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7636 603 41 0 8340 0
vsize: 33524
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7658 0 0 0 100968 44 0 0 25 0 1 0 481309211 34328576 7636 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8381 7636 603 41 0 8340 0
vsize: 33524
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7668 0 0 0 101968 44 0 0 25 0 1 0 481309211 34476032 7646 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8417 7646 603 41 0 8376 0
vsize: 33668
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7684 0 0 0 102968 45 0 0 25 0 1 0 481309211 34476032 7662 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8417 7662 603 41 0 8376 0
vsize: 33668
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7828 0 0 0 103967 45 0 0 25 0 1 0 481309211 35143680 7806 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8580 7806 603 41 0 8539 0
vsize: 34320
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7831 0 0 0 104967 45 0 0 25 0 1 0 481309211 35143680 7809 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8580 7809 603 41 0 8539 0
vsize: 34320
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7840 0 0 0 105967 46 0 0 25 0 1 0 481309211 35143680 7818 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8580 7818 603 41 0 8539 0
vsize: 34320
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7853 0 0 0 106967 46 0 0 25 0 1 0 481309211 35278848 7831 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8613 7831 603 41 0 8572 0
vsize: 34452
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7866 0 0 0 107966 47 0 0 25 0 1 0 481309211 35278848 7844 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8613 7844 603 41 0 8572 0
vsize: 34452
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 7882 0 0 0 108966 47 0 0 25 0 1 0 481309211 35438592 7860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8652 7860 603 41 0 8611 0
vsize: 34608
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8090 0 0 0 109965 48 0 0 25 0 1 0 481309211 36241408 8068 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8848 8068 603 41 0 8807 0
vsize: 35392
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8098 0 0 0 110965 48 0 0 25 0 1 0 481309211 36241408 8076 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8848 8076 603 41 0 8807 0
vsize: 35392
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8102 0 0 0 111965 48 0 0 25 0 1 0 481309211 36384768 8080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8080 603 41 0 8842 0
vsize: 35532
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8117 0 0 0 112965 48 0 0 25 0 1 0 481309211 36384768 8095 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8095 603 41 0 8842 0
vsize: 35532
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8117 0 0 0 113965 49 0 0 25 0 1 0 481309211 36384768 8095 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8095 603 41 0 8842 0
vsize: 35532
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8117 0 0 0 114965 49 0 0 25 0 1 0 481309211 36384768 8095 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8095 603 41 0 8842 0
vsize: 35532
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8118 0 0 0 115965 49 0 0 25 0 1 0 481309211 36384768 8096 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8096 603 41 0 8842 0
vsize: 35532
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8119 0 0 0 116965 49 0 0 25 0 1 0 481309211 36384768 8097 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8097 603 41 0 8842 0
vsize: 35532
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8140 0 0 0 117965 49 0 0 25 0 1 0 481309211 36548608 8118 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8923 8118 603 41 0 8882 0
vsize: 35692
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8157 0 0 0 118965 49 0 0 25 0 1 0 481309211 36548608 8135 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8923 8135 603 41 0 8882 0
vsize: 35692
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31713
Raw data (stat): 31713 (minisat+) R 31712 26298 26297 0 -1 0 8157 0 0 0 119965 49 0 0 25 0 1 0 481309211 36548608 8135 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8923 8135 603 41 0 8882 0
vsize: 35692
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31713
Raw data (stat): 31713 (minisat+) Z 31712 26298 26297 0 -1 12 8159 0 0 0 119965 51 0 0 25 0 1 0 481309211 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.05
CPU time (s): 1200.17
CPU user time (s): 1199.66
CPU system time (s): 0.515921
CPU usage (%): 100.01
Max. virtual memory (Kb): 35692
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####