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-chnl30_40_pb.cnf.cr.opb
MD5SUM6a0000bd3257094a387dbf208b4df8cf
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.073987
Number of variables2400
Total number of constraints140
Number of constraints which are clauses80
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint40

Trace number 4583 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 19:24:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3397 boxname=wulflinc5 idbench=13 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a0000bd3257094a387dbf208b4df8cf  /oldhome/oroussel/tmp/wulflinc5/normalized-chnl30_40_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-chnl30_40_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc5/normalized-chnl30_40_pb.cnf.cr.opb
IDLAUNCH: 3397
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        926528 kB
Buffers:         32444 kB
Cached:          54568 kB
SwapCached:       2272 kB
Active:          46760 kB
Inactive:        45328 kB
HighTotal:      131008 kB
HighFree:        72548 kB
LowTotal:       903652 kB
LowFree:        853980 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10344 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:44:48 (client local time) WITH STATUS 0 IN 1200.09 SECONDS
stats: 3397 7 1200.09 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................
c ---[  59]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  58]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  57]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  56]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  55]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  54]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  53]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  52]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  51]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  50]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  49]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  48]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  47]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  46]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  45]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  44]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  43]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  42]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  41]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  40]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  39]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  38]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  37]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  36]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  35]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  34]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  33]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  32]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  31]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  30]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  29]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  28]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  27]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  26]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  25]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  24]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  23]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  22]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  21]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  20]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  19]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  18]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  17]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  16]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  15]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  14]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  13]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  12]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  11]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  10]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   9]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   8]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   7]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   6]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   5]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   4]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   3]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   2]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   1]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[   0]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29360   106500 |    9786       0        0     nan |  0.000 % |
c |       100 |   29360   106500 |   10764     100      200     2.0 |  5.882 % |
c |       250 |   29208   105962 |   11841     223      495     2.2 |  6.176 % |
c |       475 |   28760   104407 |   13025     367      857     2.3 |  7.031 % |
c |       812 |   28005   101821 |   14327     554     1666     3.0 |  8.529 % |
c |      1318 |   27570   100361 |   15760     986     3742     3.8 |  9.552 % |
c |      2081 |   26457    96596 |   17336    1583     6796     4.3 | 12.437 % |
c |      3220 |   23220    85477 |   19070    2186    11723     5.4 | 19.944 % |
c |      4928 |   18802    70285 |   20977    3132    21754     6.9 | 30.028 % |
c |      7491 |   17306    65224 |   23074    5459   430847    78.9 | 33.782 % |
c |     11339 |   17306    65224 |   25382    9307  1970480   211.7 | 33.782 % |
c |     17107 |   17274    65116 |   27920   15071  3730741   247.5 | 33.866 % |
c |     25756 |   17274    65116 |   30712   23720  6775496   285.6 | 33.866 % |
c |     38731 |   17251    65037 |   33783   15458  7305793   472.6 | 33.922 % |
c |     58195 |   17251    65037 |   37162   34922 19680139   563.5 | 33.922 % |
c |     87387 |   17242    65008 |   40878   37009 21555409   582.4 | 33.950 % |
#### 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.00 2/54 25660
Raw data (stat): 25660 (runsolver) R 25659 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420228918 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 967 0 1 0 984 2 0 0 25 0 1 0 420228918 5591040 946 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1365 946 603 41 0 1324 0
vsize: 5460
[startup+20.0001 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 1773 0 1 0 1981 4 0 0 25 0 1 0 420228918 8810496 1752 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2151 1752 603 41 0 2110 0
vsize: 8604
[startup+29.9999 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 4116 0 1 0 2975 10 0 0 25 0 1 0 420228918 18493440 4095 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4515 4095 603 41 0 4474 0
vsize: 18060
[startup+39.9997 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 5892 0 1 0 3969 16 0 0 25 0 1 0 420228918 25788416 5871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6296 5871 603 41 0 6255 0
vsize: 25184
[startup+49.9994 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 7293 0 1 0 4963 21 0 0 25 0 1 0 420228918 31555584 7272 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7704 7272 603 41 0 7663 0
vsize: 30816
[startup+60.0001 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 8470 0 1 0 5959 25 0 0 25 0 1 0 420228918 36413440 8449 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8890 8449 603 41 0 8849 0
vsize: 35560
[startup+70.0008 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 9722 0 1 0 6956 28 0 0 25 0 1 0 420228918 41418752 9701 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10112 9701 603 41 0 10071 0
vsize: 40448
[startup+80.001 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 11069 0 1 0 7953 31 0 0 25 0 1 0 420228918 46944256 11048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11461 11048 603 41 0 11420 0
vsize: 45844
[startup+90.0013 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 12234 0 1 0 8949 35 0 0 25 0 1 0 420228918 51810304 12213 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12649 12213 603 41 0 12608 0
vsize: 50596
[startup+100.001 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13761 0 1 0 9945 40 0 0 25 0 1 0 420228918 58159104 13740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14199 13740 603 41 0 14158 0
vsize: 56796
[startup+110.002 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 10945 40 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+120.002 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 11944 41 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+130.001 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 12944 41 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+140.003 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 13944 41 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+150.002 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 14944 41 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+160.001 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 13959 0 1 0 15944 41 0 0 25 0 1 0 420228918 58970112 13938 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14397 13938 603 41 0 14356 0
vsize: 57588
[startup+170.001 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 14216 0 1 0 16944 42 0 0 25 0 1 0 420228918 60051456 14195 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14661 14195 603 41 0 14620 0
vsize: 58644
[startup+180.001 s]
Raw data (loadavg): 1.03 0.46 0.17 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 14855 0 1 0 17942 44 0 0 25 0 1 0 420228918 62631936 14834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15291 14834 603 41 0 15250 0
vsize: 61164
[startup+190.001 s]
Raw data (loadavg): 1.02 0.48 0.18 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 15440 0 1 0 18941 45 0 0 25 0 1 0 420228918 65064960 15419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15885 15419 603 41 0 15844 0
vsize: 63540
[startup+200.001 s]
Raw data (loadavg): 1.02 0.50 0.19 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 16031 0 1 0 19940 46 0 0 25 0 1 0 420228918 67497984 16010 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16479 16010 603 41 0 16438 0
vsize: 65916
[startup+210.001 s]
Raw data (loadavg): 1.02 0.51 0.20 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 16655 0 1 0 20939 48 0 0 25 0 1 0 420228918 70070272 16634 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17107 16634 603 41 0 17066 0
vsize: 68428
[startup+220.001 s]
Raw data (loadavg): 1.01 0.53 0.21 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 17372 0 1 0 21937 49 0 0 25 0 1 0 420228918 73043968 17351 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17833 17351 603 41 0 17792 0
vsize: 71332
[startup+230.001 s]
Raw data (loadavg): 1.01 0.54 0.21 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 17928 0 1 0 22936 51 0 0 25 0 1 0 420228918 75366400 17907 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18400 17907 603 41 0 18359 0
vsize: 73600
[startup+240.001 s]
Raw data (loadavg): 1.01 0.56 0.22 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 18518 0 1 0 23935 52 0 0 25 0 1 0 420228918 77799424 18497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18994 18497 603 41 0 18953 0
vsize: 75976
[startup+250.001 s]
Raw data (loadavg): 1.01 0.57 0.23 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 19152 0 1 0 24934 53 0 0 25 0 1 0 420228918 80396288 19131 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19628 19131 603 41 0 19587 0
vsize: 78512
[startup+260.001 s]
Raw data (loadavg): 1.00 0.59 0.24 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 19497 0 1 0 25933 54 0 0 25 0 1 0 420228918 81747968 19476 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19958 19476 603 41 0 19917 0
vsize: 79832
[startup+270.001 s]
Raw data (loadavg): 1.00 0.60 0.24 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 19969 0 1 0 26932 55 0 0 25 0 1 0 420228918 83783680 19948 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20455 19948 603 41 0 20414 0
vsize: 81820
[startup+280.001 s]
Raw data (loadavg): 1.00 0.61 0.25 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 20195 0 1 0 27931 56 0 0 25 0 1 0 420228918 84729856 20174 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20686 20174 603 41 0 20645 0
vsize: 82744
[startup+290.001 s]
Raw data (loadavg): 1.00 0.62 0.26 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 20502 0 1 0 28931 57 0 0 25 0 1 0 420228918 86085632 20481 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21017 20481 603 41 0 20976 0
vsize: 84068
[startup+300.001 s]
Raw data (loadavg): 1.00 0.64 0.27 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 20813 0 1 0 29930 57 0 0 25 0 1 0 420228918 87351296 20792 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21326 20792 603 41 0 21285 0
vsize: 85304
[startup+310.001 s]
Raw data (loadavg): 1.00 0.65 0.28 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 21214 0 1 0 30929 59 0 0 25 0 1 0 420228918 88973312 21193 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21722 21193 603 41 0 21681 0
vsize: 86888
[startup+320.002 s]
Raw data (loadavg): 1.00 0.66 0.28 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 21563 0 1 0 31929 59 0 0 25 0 1 0 420228918 90460160 21542 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22085 21542 603 41 0 22044 0
vsize: 88340
[startup+330.001 s]
Raw data (loadavg): 1.00 0.67 0.29 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 21918 0 1 0 32928 60 0 0 25 0 1 0 420228918 91947008 21897 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22448 21897 603 41 0 22407 0
vsize: 89792
[startup+340.002 s]
Raw data (loadavg): 1.00 0.68 0.30 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 22231 0 1 0 33927 61 0 0 25 0 1 0 420228918 93163520 22210 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22745 22210 603 41 0 22704 0
vsize: 90980
[startup+350.001 s]
Raw data (loadavg): 1.00 0.69 0.30 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 22614 0 1 0 34926 63 0 0 25 0 1 0 420228918 94785536 22593 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22593 603 41 0 23100 0
vsize: 92564
[startup+360.001 s]
Raw data (loadavg): 1.00 0.70 0.31 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 22933 0 1 0 35925 63 0 0 25 0 1 0 420228918 95997952 22912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23437 22912 603 41 0 23396 0
vsize: 93748
[startup+370.001 s]
Raw data (loadavg): 1.00 0.71 0.32 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 23373 0 1 0 36924 65 0 0 25 0 1 0 420228918 97886208 23352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23898 23352 603 41 0 23857 0
vsize: 95592
[startup+380.001 s]
Raw data (loadavg): 1.00 0.72 0.32 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 23590 0 1 0 37923 66 0 0 25 0 1 0 420228918 98697216 23569 4294967295 134512640 134672761 3221224544 3221223728 134559176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24096 23570 603 41 0 24055 0
vsize: 96384
[startup+390.001 s]
Raw data (loadavg): 1.00 0.73 0.33 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 23848 0 1 0 38923 66 0 0 25 0 1 0 420228918 99790848 23827 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24363 23827 603 41 0 24322 0
vsize: 97452
[startup+400.001 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 24170 0 1 0 39922 67 0 0 25 0 1 0 420228918 101142528 24149 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24693 24149 603 41 0 24652 0
vsize: 98772
[startup+410.002 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 24434 0 1 0 40922 67 0 0 25 0 1 0 420228918 102223872 24413 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24957 24413 603 41 0 24916 0
vsize: 99828
[startup+420.002 s]
Raw data (loadavg): 1.00 0.75 0.35 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 24800 0 1 0 41921 68 0 0 25 0 1 0 420228918 103710720 24779 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25320 24779 603 41 0 25279 0
vsize: 101280
[startup+430.002 s]
Raw data (loadavg): 1.00 0.76 0.36 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25171 0 1 0 42921 69 0 0 25 0 1 0 420228918 105197568 25150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25683 25150 603 41 0 25642 0
vsize: 102732
[startup+440.003 s]
Raw data (loadavg): 1.00 0.77 0.36 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25241 0 1 0 43921 69 0 0 25 0 1 0 420228918 105467904 25220 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25220 603 41 0 25708 0
vsize: 102996
[startup+450.003 s]
Raw data (loadavg): 1.00 0.77 0.37 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 44921 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+460.003 s]
Raw data (loadavg): 1.00 0.78 0.38 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 45921 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+470.002 s]
Raw data (loadavg): 1.00 0.79 0.38 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 46922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+480.002 s]
Raw data (loadavg): 1.00 0.79 0.39 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 47922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+490.002 s]
Raw data (loadavg): 1.00 0.80 0.39 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 48922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+500.002 s]
Raw data (loadavg): 1.00 0.81 0.40 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 49922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+510.002 s]
Raw data (loadavg): 1.00 0.81 0.41 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 50922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+520.002 s]
Raw data (loadavg): 1.00 0.82 0.41 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 51922 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+530.002 s]
Raw data (loadavg): 1.00 0.82 0.42 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 52923 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+540.001 s]
Raw data (loadavg): 1.00 0.83 0.42 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25242 0 1 0 53923 69 0 0 25 0 1 0 420228918 105467904 25221 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25221 603 41 0 25708 0
vsize: 102996
[startup+550.001 s]
Raw data (loadavg): 1.00 0.83 0.43 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25243 0 1 0 54923 69 0 0 25 0 1 0 420228918 105467904 25222 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25222 603 41 0 25708 0
vsize: 102996
[startup+560.002 s]
Raw data (loadavg): 1.00 0.84 0.43 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 55923 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+570.002 s]
Raw data (loadavg): 1.00 0.84 0.44 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 56923 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+580.002 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 57923 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+590.002 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 58924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+600.002 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 59924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+610.002 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 60924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+620.003 s]
Raw data (loadavg): 1.00 0.86 0.47 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 61924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+630.002 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 62924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+640.002 s]
Raw data (loadavg): 1.00 0.87 0.48 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 63924 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+650.001 s]
Raw data (loadavg): 1.00 0.88 0.48 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25244 0 1 0 64925 69 0 0 25 0 1 0 420228918 105467904 25223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25223 603 41 0 25708 0
vsize: 102996
[startup+660.002 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25245 0 1 0 65925 69 0 0 25 0 1 0 420228918 105467904 25224 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25224 603 41 0 25708 0
vsize: 102996
[startup+670.002 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25245 0 1 0 66925 69 0 0 25 0 1 0 420228918 105467904 25224 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25224 603 41 0 25708 0
vsize: 102996
[startup+680.002 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25246 0 1 0 67925 69 0 0 25 0 1 0 420228918 105467904 25225 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25225 603 41 0 25708 0
vsize: 102996
[startup+690.002 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25246 0 1 0 68925 69 0 0 25 0 1 0 420228918 105467904 25225 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25225 603 41 0 25708 0
vsize: 102996
[startup+700.003 s]
Raw data (loadavg): 1.00 0.89 0.51 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 69926 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+710.003 s]
Raw data (loadavg): 1.00 0.90 0.51 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 70926 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+720.003 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 71926 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+730.003 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 72926 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+740.004 s]
Raw data (loadavg): 1.00 0.90 0.53 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 73926 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+750.003 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 74927 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+760.004 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25247 0 1 0 75927 69 0 0 25 0 1 0 420228918 105467904 25226 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25226 603 41 0 25708 0
vsize: 102996
[startup+770.003 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 76927 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+780.003 s]
Raw data (loadavg): 1.00 0.91 0.55 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 77927 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+790.003 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 78927 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+800.004 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 79927 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+810.004 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 80928 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+820.004 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 81928 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+830.004 s]
Raw data (loadavg): 1.00 0.92 0.57 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 82928 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+840.004 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 83928 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+850.004 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 84928 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+860.004 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 85929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+870.005 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 86929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+880.005 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 87929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+890.005 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 88929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+900.005 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 89929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+910.005 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 90929 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+920.005 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 91930 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+930.004 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25248 0 1 0 92930 69 0 0 25 0 1 0 420228918 105467904 25227 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25227 603 41 0 25708 0
vsize: 102996
[startup+940.005 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25251 0 1 0 93930 69 0 0 25 0 1 0 420228918 105467904 25230 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25230 603 41 0 25708 0
vsize: 102996
[startup+950.005 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25254 0 1 0 94930 69 0 0 25 0 1 0 420228918 105467904 25233 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25233 603 41 0 25708 0
vsize: 102996
[startup+960.004 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25254 0 1 0 95930 69 0 0 25 0 1 0 420228918 105467904 25233 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25233 603 41 0 25708 0
vsize: 102996
[startup+970.005 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25255 0 1 0 96931 69 0 0 25 0 1 0 420228918 105467904 25234 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25234 603 41 0 25708 0
vsize: 102996
[startup+980.005 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25255 0 1 0 97931 69 0 0 25 0 1 0 420228918 105467904 25234 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25234 603 41 0 25708 0
vsize: 102996
[startup+990.006 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25255 0 1 0 98931 69 0 0 25 0 1 0 420228918 105467904 25234 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25234 603 41 0 25708 0
vsize: 102996
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25255 0 1 0 99931 69 0 0 25 0 1 0 420228918 105467904 25234 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25234 603 41 0 25708 0
vsize: 102996
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 100931 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 101931 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 102932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 103932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.95 0.65 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 104932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 105932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 106932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 107932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 108933 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 109933 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 110933 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25256 0 1 0 111932 69 0 0 25 0 1 0 420228918 105467904 25235 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25235 603 41 0 25708 0
vsize: 102996
[startup+1130 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 112932 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1140 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 113933 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1150 s]
Raw data (loadavg): 1.00 0.96 0.68 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 114933 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 115933 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1170 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 116933 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1180 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 117933 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223500 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 118934 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 25660
Raw data (stat): 25660 (minisat+) R 25659 24215 24214 0 -1 0 25258 0 1 0 119934 69 0 0 25 0 1 0 420228918 105467904 25237 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25749 25237 603 41 0 25708 0
vsize: 102996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.69 1/54 25660
Raw data (stat): 25660 (minisat+) Z 25659 24215 24214 0 -1 12 25260 0 1 0 119934 74 0 0 25 0 1 0 420228918 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.05
CPU time (s): 1200.09
CPU user time (s): 1199.34
CPU system time (s): 0.744886
CPU usage (%): 100.003
Max. virtual memory (Kb): 102996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####