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-fpga45_44_sat_pb.cnf.cr.opb
MD5SUMc501a04dd091dbe678ec2743021adc30
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 46
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark15.2037
Number of variables2970
Total number of constraints2113
Number of constraints which are clauses2024
Number of constraints which are cardinality constraints (but not clauses)89
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint22
Maximum length of a constraint45

Trace number 4821 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-13 20:27:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=500 boxname=wulflinc30 idbench=56 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c501a04dd091dbe678ec2743021adc30  /oldhome/oroussel/tmp/wulflinc30/normalized-fpga45_44_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-fpga45_44_sat_pb.cnf.cr.opb
IDLAUNCH: 500
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        745824 kB
Buffers:         37112 kB
Cached:         211088 kB
SwapCached:          0 kB
Active:          79356 kB
Inactive:       171668 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        745572 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32200 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:47:22 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 500 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  88]---> BDD-cost:   85
c ---[  87]---> BDD-cost:   85
c ---[  86]---> BDD-cost:   85
c ---[  85]---> BDD-cost:   85
c ---[  84]---> BDD-cost:   85
c ---[  83]---> BDD-cost:   85
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:   85
c ---[  79]---> BDD-cost:   85
c ---[  78]---> BDD-cost:   85
c ---[  77]---> BDD-cost:   85
c ---[  76]---> BDD-cost:   85
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:   85
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:   85
c ---[  71]---> BDD-cost:   85
c ---[  70]---> BDD-cost:   85
c ---[  69]---> BDD-cost:   85
c ---[  68]---> BDD-cost:   85
c ---[  67]---> BDD-cost:   85
c ---[  66]---> BDD-cost:   85
c ---[  65]---> BDD-cost:   85
c ---[  64]---> BDD-cost:   85
c ---[  63]---> BDD-cost:   85
c ---[  62]---> BDD-cost:   85
c ---[  61]---> BDD-cost:   85
c ---[  60]---> BDD-cost:   85
c ---[  59]---> BDD-cost:   85
c ---[  58]---> BDD-cost:   85
c ---[  57]---> BDD-cost:   85
c ---[  56]---> BDD-cost:   85
c ---[  55]---> BDD-cost:   85
c ---[  54]---> BDD-cost:   85
c ---[  53]---> BDD-cost:   85
c ---[  52]---> BDD-cost:   85
c ---[  51]---> BDD-cost:   85
c ---[  50]---> BDD-cost:   85
c ---[  49]---> BDD-cost:   85
c ---[  48]---> BDD-cost:   85
c ---[  47]---> BDD-cost:   85
c ---[  46]---> BDD-cost:   85
c ---[  45]---> BDD-cost:   85
c ---[  44]---> BDD-cost:   85
c ---[  43]---> BDD-cost:   41
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:   41
c ---[  24]---> BDD-cost:   41
c ---[  23]---> BDD-cost:   41
c ---[  22]---> BDD-cost:   41
c ---[  21]---> BDD-cost:   43
c ---[  20]---> BDD-cost:   43
c ---[  19]---> BDD-cost:   43
c ---[  18]---> BDD-cost:   43
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:   43
c ---[  15]---> BDD-cost:   43
c ---[  14]---> BDD-cost:   43
c ---[  13]---> BDD-cost:   43
c ---[  12]---> BDD-cost:   43
c ---[  11]---> BDD-cost:   43
c ---[  10]---> BDD-cost:   43
c ---[   9]---> BDD-cost:   43
c ---[   8]---> BDD-cost:   43
c ---[   7]---> BDD-cost:   43
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:   43
c ---[   4]---> BDD-cost:   43
c ---[   3]---> BDD-cost:   43
c ---[   2]---> BDD-cost:   43
c ---[   1]---> BDD-cost:   43
c ---[   0]---> BDD-cost:   43
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16073    84083 |    5357       0        0     nan |  0.000 % |
c |       101 |   16073    84083 |    5892     101    25615   253.6 |  1.030 % |
c |       252 |   16073    84083 |    6481     252    61496   244.0 |  1.030 % |
c |       477 |   16073    84083 |    7130     477   112639   236.1 |  1.030 % |
c |       816 |   16073    84083 |    7843     816   210746   258.3 |  1.030 % |
c |      1323 |   16073    84083 |    8627    1323   346348   261.8 |  1.030 % |
c |      2083 |   16073    84083 |    9490    2083   564649   271.1 |  1.030 % |
c |      3223 |   16073    84083 |   10439    3223   718568   223.0 |  1.030 % |
c |      4931 |   16073    84083 |   11483    4931  1368853   277.6 |  1.030 % |
c |      7493 |   16073    84083 |   12631    7493  2490469   332.4 |  1.030 % |
c |     11338 |   16073    84083 |   13894   11338  3675913   324.2 |  1.030 % |
c |     17111 |   16073    84083 |   15284   17111  5830865   340.8 |  1.030 % |
c |     25761 |   16073    84083 |   16812   17206  6458966   375.4 |  1.030 % |
c |     38737 |   16073    84083 |   18493   11018  2215373   201.1 |  1.030 % |
c |     58201 |   16073    84083 |   20343   17865  7499448   419.8 |  1.030 % |
c |     87396 |   16073    84083 |   22377   17045  3155458   185.1 |  1.030 % |
c |    131187 |   16073    84083 |   24615   16857  8064521   478.4 |  1.030 % |
c |    196875 |   16073    84083 |   27076   16816  7876802   468.4 |  1.030 % |
#### 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.92 0.98 0.91 1/54 13920
Raw data (stat): 13920 (runsolver) R 13919 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478822846 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 3079 0 0 0 991 6 0 0 25 0 1 0 478822846 14536704 3056 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3056 603 41 0 3508 0
vsize: 14196
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 4736 0 0 0 1987 11 0 0 25 0 1 0 478822846 21278720 4713 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5195 4713 603 41 0 5154 0
vsize: 20780
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 6198 0 0 0 2984 14 0 0 25 0 1 0 478822846 27226112 6175 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6175 603 41 0 6606 0
vsize: 26588
[startup+40.003 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7195 0 0 0 3981 17 0 0 25 0 1 0 478822846 31461376 7172 4294967295 134512640 134672761 3221224624 3221223728 134555197 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7172 603 41 0 7640 0
vsize: 30724
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7195 0 0 0 4981 18 0 0 25 0 1 0 478822846 31461376 7172 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7172 603 41 0 7640 0
vsize: 30724
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7199 0 0 0 5980 18 0 0 25 0 1 0 478822846 31461376 7176 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 7176 603 41 0 7640 0
vsize: 30724
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7982 0 0 0 6977 22 0 0 25 0 1 0 478822846 34689024 7959 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8469 7959 603 41 0 8428 0
vsize: 33876
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7986 0 0 0 7977 22 0 0 25 0 1 0 478822846 34689024 7963 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8469 7963 603 41 0 8428 0
vsize: 33876
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7986 0 0 0 8977 22 0 0 25 0 1 0 478822846 34689024 7963 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8469 7963 603 41 0 8428 0
vsize: 33876
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7986 0 0 0 9977 22 0 0 25 0 1 0 478822846 34689024 7963 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8469 7963 603 41 0 8428 0
vsize: 33876
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 7986 0 0 0 10977 23 0 0 25 0 1 0 478822846 34689024 7963 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8469 7963 603 41 0 8428 0
vsize: 33876
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 8465 0 0 0 11975 25 0 0 25 0 1 0 478822846 36601856 8442 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8936 8442 603 41 0 8895 0
vsize: 35744
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 8936 0 0 0 12973 27 0 0 25 0 1 0 478822846 38498304 8913 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9399 8913 603 41 0 9358 0
vsize: 37596
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9545 0 0 0 13971 29 0 0 25 0 1 0 478822846 41062400 9522 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10025 9522 603 41 0 9984 0
vsize: 40100
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9888 0 0 0 14970 29 0 0 25 0 1 0 478822846 42442752 9865 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10362 9865 603 41 0 10321 0
vsize: 41448
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9889 0 0 0 15970 30 0 0 25 0 1 0 478822846 42442752 9866 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10362 9866 603 41 0 10321 0
vsize: 41448
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9889 0 0 0 16970 30 0 0 25 0 1 0 478822846 42442752 9866 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10362 9866 603 41 0 10321 0
vsize: 41448
[startup+180.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9889 0 0 0 17970 31 0 0 25 0 1 0 478822846 42442752 9866 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10362 9866 603 41 0 10321 0
vsize: 41448
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 9941 0 0 0 18969 31 0 0 25 0 1 0 478822846 42713088 9918 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10428 9918 603 41 0 10387 0
vsize: 41712
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 11838 0 0 0 19964 36 0 0 25 0 1 0 478822846 50409472 11815 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12307 11815 603 41 0 12266 0
vsize: 49228
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12177 0 0 0 20964 37 0 0 25 0 1 0 478822846 51896320 12154 4294967295 134512640 134672761 3221224624 3221223808 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12670 12154 603 41 0 12629 0
vsize: 50680
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12177 0 0 0 21963 37 0 0 25 0 1 0 478822846 51896320 12154 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12670 12154 603 41 0 12629 0
vsize: 50680
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12177 0 0 0 22963 38 0 0 25 0 1 0 478822846 51896320 12154 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12670 12154 603 41 0 12629 0
vsize: 50680
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 23963 38 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 24962 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223728 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 25962 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223808 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+270.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 26963 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 27963 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+290.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 28963 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+300.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 29963 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+310.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 30963 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+320.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 31964 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 32964 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 33964 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223720 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+350.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 34964 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+360.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 35965 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+370.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 36965 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+380.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 37965 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+390.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12179 0 0 0 38965 39 0 0 25 0 1 0 478822846 51896320 12156 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12670 12156 603 41 0 12629 0
vsize: 50680
[startup+400.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 12896 0 0 0 39964 40 0 0 25 0 1 0 478822846 54857728 12873 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13393 12873 603 41 0 13352 0
vsize: 53572
[startup+410.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 13553 0 0 0 40962 42 0 0 25 0 1 0 478822846 57569280 13530 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14055 13530 603 41 0 14014 0
vsize: 56220
[startup+420.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 13731 0 0 0 41962 43 0 0 25 0 1 0 478822846 58245120 13708 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14220 13708 603 41 0 14179 0
vsize: 56880
[startup+430.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 13954 0 0 0 42961 43 0 0 25 0 1 0 478822846 59301888 13931 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14478 13931 603 41 0 14437 0
vsize: 57912
[startup+440.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14348 0 0 0 43960 45 0 0 25 0 1 0 478822846 60821504 14325 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14849 14325 603 41 0 14808 0
vsize: 59396
[startup+450.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14832 0 0 0 44959 46 0 0 25 0 1 0 478822846 62840832 14809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15342 14809 603 41 0 15301 0
vsize: 61368
[startup+460.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 45959 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+470.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 46959 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+480.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 47959 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+490.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 48959 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+500.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 49959 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+510.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14898 0 0 0 50960 47 0 0 25 0 1 0 478822846 63107072 14875 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14875 603 41 0 15366 0
vsize: 61628
[startup+520.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14900 0 0 0 51960 47 0 0 25 0 1 0 478822846 63107072 14877 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14877 603 41 0 15366 0
vsize: 61628
[startup+530.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14900 0 0 0 52960 47 0 0 25 0 1 0 478822846 63107072 14877 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14877 603 41 0 15366 0
vsize: 61628
[startup+540.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 14917 0 0 0 53960 47 0 0 25 0 1 0 478822846 63242240 14894 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15440 14894 603 41 0 15399 0
vsize: 61760
[startup+550.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 15432 0 0 0 54959 48 0 0 25 0 1 0 478822846 65286144 15409 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15939 15409 603 41 0 15898 0
vsize: 63756
[startup+560.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 15928 0 0 0 55958 49 0 0 25 0 1 0 478822846 67334144 15905 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16439 15905 603 41 0 16398 0
vsize: 65756
[startup+570.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16288 0 0 0 56957 50 0 0 25 0 1 0 478822846 68882432 16265 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16817 16265 603 41 0 16776 0
vsize: 67268
[startup+580.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 57957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+590.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 58957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+600.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 59957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223808 134559390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+610.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 60957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+620.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 61957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+630.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16548 0 0 0 62957 51 0 0 25 0 1 0 478822846 69959680 16525 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 16525 603 41 0 17039 0
vsize: 68320
[startup+640.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 16711 0 0 0 63957 51 0 0 25 0 1 0 478822846 70631424 16688 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17244 16688 603 41 0 17203 0
vsize: 68976
[startup+650.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17586 0 0 0 64955 53 0 0 25 0 1 0 478822846 74137600 17563 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18100 17563 603 41 0 18059 0
vsize: 72400
[startup+660.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17976 0 0 0 65954 54 0 0 25 0 1 0 478822846 75759616 17953 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17953 603 41 0 18455 0
vsize: 73984
[startup+670.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17979 0 0 0 66955 54 0 0 25 0 1 0 478822846 75759616 17956 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17956 603 41 0 18455 0
vsize: 73984
[startup+680.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17979 0 0 0 67955 54 0 0 25 0 1 0 478822846 75759616 17956 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17956 603 41 0 18455 0
vsize: 73984
[startup+690.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17980 0 0 0 68955 54 0 0 25 0 1 0 478822846 75759616 17957 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17957 603 41 0 18455 0
vsize: 73984
[startup+700.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17980 0 0 0 69955 54 0 0 25 0 1 0 478822846 75759616 17957 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17957 603 41 0 18455 0
vsize: 73984
[startup+710.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 70955 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+720.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 71955 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+730.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 72956 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+740.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 73956 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+750.024 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 74956 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+760.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 75956 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+770.025 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 76957 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+780.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 77957 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+790.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 17981 0 0 0 78957 54 0 0 25 0 1 0 478822846 75759616 17958 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18496 17958 603 41 0 18455 0
vsize: 73984
[startup+800.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 18380 0 0 0 79956 56 0 0 25 0 1 0 478822846 77529088 18357 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18928 18357 603 41 0 18887 0
vsize: 75712
[startup+810.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 18989 0 0 0 80954 58 0 0 25 0 1 0 478822846 79962112 18966 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19522 18966 603 41 0 19481 0
vsize: 78088
[startup+820.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19351 0 0 0 81953 59 0 0 25 0 1 0 478822846 81584128 19328 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19918 19328 603 41 0 19877 0
vsize: 79672
[startup+830.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 82953 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+840.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 83953 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+850.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 84953 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+860.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 85954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+870.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 86954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+880.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 87954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+890.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 88954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+900.029 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 89954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+910.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 90954 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+920.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19591 0 0 0 91955 59 0 0 25 0 1 0 478822846 82518016 19568 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19568 603 41 0 20105 0
vsize: 80584
[startup+930.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19592 0 0 0 92955 59 0 0 25 0 1 0 478822846 82518016 19569 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19569 603 41 0 20105 0
vsize: 80584
[startup+940.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 93955 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+950.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 94955 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223580 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+960.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 95956 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+970.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 96957 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+980.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 97957 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+990.042 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 98957 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 99957 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 100957 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 101958 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 102958 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 103958 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 104958 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 105958 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 106959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 107959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 108959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 109959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 110959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 111959 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 112960 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19595 0 0 0 113960 59 0 0 25 0 1 0 478822846 82518016 19572 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19572 603 41 0 20105 0
vsize: 80584
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19597 0 0 0 114960 59 0 0 25 0 1 0 478822846 82518016 19574 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20146 19574 603 41 0 20105 0
vsize: 80584
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19925 0 0 0 115959 60 0 0 25 0 1 0 478822846 83873792 19902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19902 603 41 0 20436 0
vsize: 81908
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19925 0 0 0 116960 60 0 0 25 0 1 0 478822846 83873792 19902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19902 603 41 0 20436 0
vsize: 81908
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19925 0 0 0 117960 60 0 0 25 0 1 0 478822846 83873792 19902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19902 603 41 0 20436 0
vsize: 81908
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19925 0 0 0 118960 60 0 0 25 0 1 0 478822846 83873792 19902 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19902 603 41 0 20436 0
vsize: 81908
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 13920
Raw data (stat): 13920 (minisat+) R 13919 11931 11930 0 -1 0 19925 0 0 0 119960 60 0 0 25 0 1 0 478822846 83873792 19902 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20477 19902 603 41 0 20436 0
vsize: 81908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 13920
Raw data (stat): 13920 (minisat+) Z 13919 11931 11930 0 -1 12 19927 0 0 0 119960 64 0 0 25 0 1 0 478822846 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.09
CPU time (s): 1200.25
CPU user time (s): 1199.61
CPU system time (s): 0.641902
CPU usage (%): 100.013
Max. virtual memory (Kb): 81908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####