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_30_pb.cnf.cr.opb
MD5SUMafcc4289aafaea265ed2d465965a3342
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 31
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.036993
Number of variables1200
Total number of constraints100
Number of constraints which are clauses60
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 constraint30

Trace number 4580 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-13 19:24:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3394 boxname=wulflinc25 idbench=10 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  afcc4289aafaea265ed2d465965a3342  /oldhome/oroussel/tmp/wulflinc25/normalized-chnl20_30_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc25/normalized-chnl20_30_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc25/normalized-chnl20_30_pb.cnf.cr.opb
IDLAUNCH: 3394
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907972 kB
Buffers:         32372 kB
Cached:          60208 kB
SwapCached:         36 kB
Active:          42472 kB
Inactive:        52984 kB
HighTotal:      131008 kB
HighFree:        67088 kB
LowTotal:       903652 kB
LowFree:        840884 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            25636 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:44:22 (client local time) WITH STATUS 0 IN 1200.05 SECONDS
stats: 3394 7 1200.05 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................
c ---[  39]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  38]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  37]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  36]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  35]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  34]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  33]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  32]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  31]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  30]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  29]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  28]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  27]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  26]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  25]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  24]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  23]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  22]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  21]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  20]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  19]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  18]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  17]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  16]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  15]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  14]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  13]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  12]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  11]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[  10]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   9]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   8]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   7]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   6]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   5]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   4]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   3]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   2]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   1]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ---[   0]---> Adder-cost: 52   maxlim: 28   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   13700    49680 |    4566       0        0     nan |  0.000 % |
c |       101 |   13123    47643 |    5022      23      154     6.7 |  9.324 % |
c |       251 |   12893    46881 |    5524     143      709     5.0 | 10.588 % |
c |       477 |   12453    45401 |    6077     311     1438     4.6 | 13.029 % |
c |       814 |   11472    42049 |    6685     508     2581     5.1 | 17.971 % |
c |      1320 |    9932    36763 |    7353     796     4634     5.8 | 26.000 % |
c |      2079 |    8036    30283 |    8088    1265     9860     7.8 | 35.824 % |
c |      3222 |    7749    29295 |    8897    2356   184476    78.3 | 37.265 % |
c |      4934 |    7749    29295 |    9787    4068   558556   137.3 | 37.265 % |
c |      7496 |    7668    29016 |   10766    6616  1016433   153.6 | 37.676 % |
c |     11340 |    7662    28996 |   11843   10458  1805603   172.7 | 37.706 % |
c |     17107 |    7640    28921 |   13027    9445  1925043   203.8 | 37.824 % |
c |     25758 |    7640    28921 |   14330   10749  2335875   217.3 | 37.824 % |
c |     38734 |    7624    28869 |   15763   15725  3711996   236.1 | 37.912 % |
c |     58195 |    7624    28869 |   17339    9014  2119342   235.1 | 37.912 % |
c |     87387 |    7615    28840 |   19073    9647  2228585   231.0 | 37.971 % |
c |    131176 |    7615    28840 |   20980   11895  2869761   241.3 | 37.971 % |
c |    196861 |    7609    28820 |   23078   20838  4923653   236.3 | 38.000 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.00 0.00 0.04 1/54 29393
Raw data (stat): 29393 (runsolver) R 29392 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478457009 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0011 s]
Raw data (loadavg): 0.15 0.03 0.05 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 2123 0 1 0 983 4 0 0 25 0 1 0 478457009 10203136 2102 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2491 2102 603 41 0 2450 0
vsize: 9964
[startup+20.0014 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 3377 0 1 0 1979 8 0 0 25 0 1 0 478457009 15339520 3356 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3356 603 41 0 3704 0
vsize: 14980
[startup+30.0019 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 3377 0 1 0 2979 8 0 0 25 0 1 0 478457009 15339520 3356 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3745 3356 603 41 0 3704 0
vsize: 14980
[startup+40.0019 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4102 0 1 0 3977 10 0 0 25 0 1 0 478457009 18309120 4081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4470 4081 603 41 0 4429 0
vsize: 17880
[startup+50.0012 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4102 0 1 0 4977 10 0 0 25 0 1 0 478457009 18309120 4081 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4470 4081 603 41 0 4429 0
vsize: 17880
[startup+60.0018 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4200 0 1 0 5976 11 0 0 25 0 1 0 478457009 18710528 4179 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4568 4179 603 41 0 4527 0
vsize: 18272
[startup+70.0017 s]
Raw data (loadavg): 0.69 0.21 0.11 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4705 0 1 0 6975 12 0 0 25 0 1 0 478457009 20893696 4684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5101 4684 603 41 0 5060 0
vsize: 20404
[startup+80.0019 s]
Raw data (loadavg): 0.73 0.23 0.12 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4730 0 1 0 7975 12 0 0 25 0 1 0 478457009 21028864 4709 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4709 603 41 0 5093 0
vsize: 20536
[startup+90.0015 s]
Raw data (loadavg): 0.77 0.26 0.13 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4730 0 1 0 8976 12 0 0 25 0 1 0 478457009 21028864 4709 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4709 603 41 0 5093 0
vsize: 20536
[startup+100.001 s]
Raw data (loadavg): 0.81 0.28 0.13 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4731 0 1 0 9976 12 0 0 25 0 1 0 478457009 21028864 4710 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4710 603 41 0 5093 0
vsize: 20536
[startup+110.002 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 4846 0 1 0 10975 12 0 0 25 0 1 0 478457009 21434368 4825 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5233 4825 603 41 0 5192 0
vsize: 20932
[startup+120.002 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5139 0 1 0 11975 13 0 0 25 0 1 0 478457009 22769664 5118 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5559 5118 603 41 0 5518 0
vsize: 22236
[startup+130.002 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5359 0 1 0 12974 14 0 0 25 0 1 0 478457009 23580672 5338 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5757 5338 603 41 0 5716 0
vsize: 23028
[startup+140.002 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5359 0 1 0 13975 14 0 0 25 0 1 0 478457009 23580672 5338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5757 5338 603 41 0 5716 0
vsize: 23028
[startup+150.001 s]
Raw data (loadavg): 0.92 0.39 0.18 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5359 0 1 0 14975 14 0 0 25 0 1 0 478457009 23580672 5338 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5757 5338 603 41 0 5716 0
vsize: 23028
[startup+160.001 s]
Raw data (loadavg): 0.93 0.41 0.19 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5359 0 1 0 15975 14 0 0 25 0 1 0 478457009 23580672 5338 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5757 5338 603 41 0 5716 0
vsize: 23028
[startup+170 s]
Raw data (loadavg): 0.94 0.43 0.19 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5507 0 1 0 16975 14 0 0 25 0 1 0 478457009 24252416 5486 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5921 5486 603 41 0 5880 0
vsize: 23684
[startup+180.001 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5507 0 1 0 17975 14 0 0 25 0 1 0 478457009 24252416 5486 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5921 5486 603 41 0 5880 0
vsize: 23684
[startup+190.002 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5551 0 1 0 18975 14 0 0 25 0 1 0 478457009 24387584 5530 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5530 603 41 0 5913 0
vsize: 23816
[startup+200.001 s]
Raw data (loadavg): 0.96 0.48 0.22 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5551 0 1 0 19975 14 0 0 25 0 1 0 478457009 24387584 5530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5530 603 41 0 5913 0
vsize: 23816
[startup+210.001 s]
Raw data (loadavg): 0.97 0.50 0.23 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5551 0 1 0 20975 14 0 0 25 0 1 0 478457009 24387584 5530 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5530 603 41 0 5913 0
vsize: 23816
[startup+220.001 s]
Raw data (loadavg): 0.97 0.51 0.23 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5551 0 1 0 21975 14 0 0 25 0 1 0 478457009 24387584 5530 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5530 603 41 0 5913 0
vsize: 23816
[startup+230 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5563 0 1 0 22976 14 0 0 25 0 1 0 478457009 24543232 5542 4294967295 134512640 134672761 3221224544 3221223456 1075352303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5992 5542 603 41 0 5951 0
vsize: 23968
[startup+240 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 5797 0 1 0 23975 15 0 0 25 0 1 0 478457009 25509888 5776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6228 5776 603 41 0 6187 0
vsize: 24912
[startup+250 s]
Raw data (loadavg): 0.98 0.56 0.26 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6041 0 1 0 24975 15 0 0 25 0 1 0 478457009 26456064 6020 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6020 603 41 0 6418 0
vsize: 25836
[startup+260.001 s]
Raw data (loadavg): 0.98 0.57 0.27 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6041 0 1 0 25976 15 0 0 25 0 1 0 478457009 26456064 6020 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6020 603 41 0 6418 0
vsize: 25836
[startup+270 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6041 0 1 0 26976 15 0 0 25 0 1 0 478457009 26456064 6020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6020 603 41 0 6418 0
vsize: 25836
[startup+280 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6045 0 1 0 27976 15 0 0 25 0 1 0 478457009 26456064 6024 4294967295 134512640 134672761 3221224544 3221223728 134558857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6024 603 41 0 6418 0
vsize: 25836
[startup+289.999 s]
Raw data (loadavg): 0.99 0.61 0.29 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6045 0 1 0 28976 15 0 0 25 0 1 0 478457009 26456064 6024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6024 603 41 0 6418 0
vsize: 25836
[startup+299.999 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6045 0 1 0 29976 15 0 0 25 0 1 0 478457009 26456064 6024 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6024 603 41 0 6418 0
vsize: 25836
[startup+310 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6045 0 1 0 30976 15 0 0 25 0 1 0 478457009 26456064 6024 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6024 603 41 0 6418 0
vsize: 25836
[startup+319.999 s]
Raw data (loadavg): 0.99 0.65 0.31 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6045 0 1 0 31977 15 0 0 25 0 1 0 478457009 26456064 6024 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 6024 603 41 0 6418 0
vsize: 25836
[startup+329.999 s]
Raw data (loadavg): 0.99 0.66 0.31 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 32976 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+340 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 33976 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+349.999 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 34976 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+359.999 s]
Raw data (loadavg): 0.99 0.69 0.33 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 35976 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+370 s]
Raw data (loadavg): 0.99 0.70 0.34 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 36977 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+379.999 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 37977 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+389.998 s]
Raw data (loadavg): 0.99 0.72 0.35 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 38977 15 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+399.999 s]
Raw data (loadavg): 0.99 0.73 0.36 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6088 0 1 0 39976 16 0 0 25 0 1 0 478457009 26726400 6067 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6525 6067 603 41 0 6484 0
vsize: 26100
[startup+409.999 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6313 0 1 0 40976 16 0 0 25 0 1 0 478457009 27668480 6292 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6755 6292 603 41 0 6714 0
vsize: 27020
[startup+419.999 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6568 0 1 0 41975 17 0 0 25 0 1 0 478457009 28614656 6547 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6547 603 41 0 6945 0
vsize: 27944
[startup+429.998 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6570 0 1 0 42976 17 0 0 25 0 1 0 478457009 28614656 6549 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6986 6549 603 41 0 6945 0
vsize: 27944
[startup+439.998 s]
Raw data (loadavg): 0.99 0.76 0.39 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6580 0 1 0 43976 17 0 0 25 0 1 0 478457009 28811264 6559 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7034 6559 603 41 0 6993 0
vsize: 28136
[startup+449.998 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6608 0 1 0 44976 17 0 0 25 0 1 0 478457009 29007872 6587 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7082 6587 603 41 0 7041 0
vsize: 28328
[startup+459.998 s]
Raw data (loadavg): 0.99 0.77 0.40 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6609 0 1 0 45976 17 0 0 25 0 1 0 478457009 29007872 6588 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7082 6588 603 41 0 7041 0
vsize: 28328
[startup+469.997 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6710 0 1 0 46976 17 0 0 25 0 1 0 478457009 29413376 6689 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6689 603 41 0 7140 0
vsize: 28724
[startup+479.997 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6711 0 1 0 47976 17 0 0 25 0 1 0 478457009 29413376 6690 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6690 603 41 0 7140 0
vsize: 28724
[startup+489.997 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6711 0 1 0 48976 17 0 0 25 0 1 0 478457009 29413376 6690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7181 6690 603 41 0 7140 0
vsize: 28724
[startup+499.997 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6780 0 1 0 49976 17 0 0 25 0 1 0 478457009 29683712 6759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6759 603 41 0 7206 0
vsize: 28988
[startup+509.997 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6780 0 1 0 50976 17 0 0 25 0 1 0 478457009 29683712 6759 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6759 603 41 0 7206 0
vsize: 28988
[startup+519.996 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6780 0 1 0 51977 17 0 0 25 0 1 0 478457009 29683712 6759 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6759 603 41 0 7206 0
vsize: 28988
[startup+529.996 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6780 0 1 0 52977 17 0 0 25 0 1 0 478457009 29683712 6759 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6759 603 41 0 7206 0
vsize: 28988
[startup+539.997 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6780 0 1 0 53977 17 0 0 25 0 1 0 478457009 29683712 6759 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6759 603 41 0 7206 0
vsize: 28988
[startup+549.996 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 54976 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+559.996 s]
Raw data (loadavg): 0.99 0.83 0.46 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 55976 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+569.995 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 56976 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+579.995 s]
Raw data (loadavg): 0.99 0.84 0.47 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 57976 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+589.994 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 58977 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+599.994 s]
Raw data (loadavg): 0.99 0.85 0.48 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 6807 0 1 0 59977 18 0 0 25 0 1 0 478457009 29683712 6786 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7247 6786 603 41 0 7206 0
vsize: 28988
[startup+609.995 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7305 0 1 0 60975 19 0 0 25 0 1 0 478457009 31846400 7284 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7775 7284 603 41 0 7734 0
vsize: 31100
[startup+619.994 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7373 0 1 0 61975 19 0 0 25 0 1 0 478457009 32116736 7352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7352 603 41 0 7800 0
vsize: 31364
[startup+629.994 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7373 0 1 0 62975 19 0 0 25 0 1 0 478457009 32116736 7352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7352 603 41 0 7800 0
vsize: 31364
[startup+639.994 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7373 0 1 0 63976 19 0 0 25 0 1 0 478457009 32116736 7352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7352 603 41 0 7800 0
vsize: 31364
[startup+649.994 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7387 0 1 0 64976 19 0 0 25 0 1 0 478457009 32116736 7366 4294967295 134512640 134672761 3221224544 3221223544 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7366 603 41 0 7800 0
vsize: 31364
[startup+659.994 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7387 0 1 0 65976 19 0 0 25 0 1 0 478457009 32116736 7366 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7366 603 41 0 7800 0
vsize: 31364
[startup+669.994 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 66976 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+679.994 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 67976 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+689.993 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 68977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+699.993 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 69977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+709.992 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 70977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+719.992 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 71977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+729.992 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 72977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+739.992 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 73977 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+749.992 s]
Raw data (loadavg): 0.99 0.90 0.55 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7388 0 1 0 74978 19 0 0 25 0 1 0 478457009 32116736 7367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7367 603 41 0 7800 0
vsize: 31364
[startup+759.991 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 75978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+769.991 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 76978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+779.991 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 77978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+789.991 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 78978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+799.991 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 79978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+809.991 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 80978 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+819.991 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 81979 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+829.991 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7390 0 1 0 82979 20 0 0 25 0 1 0 478457009 32116736 7369 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7841 7369 603 41 0 7800 0
vsize: 31364
[startup+839.992 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7399 0 1 0 83978 20 0 0 25 0 1 0 478457009 32116736 7378 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7841 7378 603 41 0 7800 0
vsize: 31364
[startup+849.991 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7410 0 1 0 84977 20 0 0 25 0 1 0 478457009 32280576 7389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7881 7389 603 41 0 7840 0
vsize: 31524
[startup+859.991 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7423 0 1 0 85977 20 0 0 25 0 1 0 478457009 32280576 7402 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7881 7402 603 41 0 7840 0
vsize: 31524
[startup+869.991 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7532 0 1 0 86977 21 0 0 25 0 1 0 478457009 32686080 7511 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7980 7511 603 41 0 7939 0
vsize: 31920
[startup+879.991 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7701 0 1 0 87976 21 0 0 25 0 1 0 478457009 33361920 7680 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8145 7680 603 41 0 8104 0
vsize: 32580
[startup+889.99 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7872 0 1 0 88976 22 0 0 25 0 1 0 478457009 34226176 7851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8356 7851 603 41 0 8315 0
vsize: 33424
[startup+899.99 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 89976 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+909.99 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 90976 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+919.99 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 91976 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+929.99 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 92977 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+939.989 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 93977 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+949.989 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 94977 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+959.989 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7906 0 1 0 95977 22 0 0 25 0 1 0 478457009 34361344 7885 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8389 7885 603 41 0 8348 0
vsize: 33556
[startup+969.988 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 96977 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+979.988 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 97977 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+989.987 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 98977 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+999.987 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 99978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 100978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 101978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 102978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 103978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 104978 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 105979 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1069.98 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7931 0 1 0 106979 22 0 0 25 0 1 0 478457009 34516992 7910 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7910 603 41 0 8386 0
vsize: 33708
[startup+1079.98 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7947 0 1 0 107979 22 0 0 25 0 1 0 478457009 34516992 7926 4294967295 134512640 134672761 3221224544 3221223728 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8427 7926 603 41 0 8386 0
vsize: 33708
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7980 0 1 0 108979 22 0 0 25 0 1 0 478457009 34713600 7959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8475 7959 603 41 0 8434 0
vsize: 33900
[startup+1099.98 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7991 0 1 0 109979 22 0 0 25 0 1 0 478457009 34713600 7970 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8475 7970 603 41 0 8434 0
vsize: 33900
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 7993 0 1 0 110979 22 0 0 25 0 1 0 478457009 34713600 7972 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8475 7972 603 41 0 8434 0
vsize: 33900
[startup+1119.98 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8005 0 1 0 111979 22 0 0 25 0 1 0 478457009 34877440 7984 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7984 603 41 0 8474 0
vsize: 34060
[startup+1129.98 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8007 0 1 0 112980 22 0 0 25 0 1 0 478457009 34877440 7986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7986 603 41 0 8474 0
vsize: 34060
[startup+1139.98 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8026 0 1 0 113980 22 0 0 25 0 1 0 478457009 35041280 8005 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8005 603 41 0 8514 0
vsize: 34220
[startup+1149.98 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8039 0 1 0 114980 22 0 0 25 0 1 0 478457009 35041280 8018 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8018 603 41 0 8514 0
vsize: 34220
[startup+1159.98 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8040 0 1 0 115980 22 0 0 25 0 1 0 478457009 35041280 8019 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8019 603 41 0 8514 0
vsize: 34220
[startup+1169.98 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8040 0 1 0 116980 22 0 0 25 0 1 0 478457009 35041280 8019 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8019 603 41 0 8514 0
vsize: 34220
[startup+1179.98 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8040 0 1 0 117980 22 0 0 25 0 1 0 478457009 35041280 8019 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8555 8019 603 41 0 8514 0
vsize: 34220
[startup+1189.98 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8068 0 1 0 118981 22 0 0 25 0 1 0 478457009 35237888 8047 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8603 8047 603 41 0 8562 0
vsize: 34412
[startup+1199.98 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 29393
Raw data (stat): 29393 (minisat+) R 29392 28099 28098 0 -1 0 8068 0 1 0 119981 22 0 0 25 0 1 0 478457009 35237888 8047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8603 8047 603 41 0 8562 0
vsize: 34412
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 29393
Raw data (stat): 29393 (minisat+) Z 29392 28099 28098 0 -1 12 8070 0 1 0 119981 23 0 0 25 0 1 0 478457009 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
CPU time (s): 1200.05
CPU user time (s): 1199.81
CPU system time (s): 0.238963
CPU usage (%): 100.004
Max. virtual memory (Kb): 34412
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####