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-chnl50_51_pb.cnf.cr.opb
MD5SUM00bdc6bb9bafd4b1100d8bfa4f886626
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 52
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.156976
Number of variables5100
Total number of constraints202
Number of constraints which are clauses102
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint51

Trace number 4612 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        929888 kB
Buffers:         34352 kB
Cached:          49388 kB
SwapCached:       2144 kB
Active:          55384 kB
Inactive:        33340 kB
HighTotal:      131008 kB
HighFree:        77756 kB
LowTotal:       903652 kB
LowFree:        852132 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10556 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:46:29 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 3404 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 202 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................
c ---[  99]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  98]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  97]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  96]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  95]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  94]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  93]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  92]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  91]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  90]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  89]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  88]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  87]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  86]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  85]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  84]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  83]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  82]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  81]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  80]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  79]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  78]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  77]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  76]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  75]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  74]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  73]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  72]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  71]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  70]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  69]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  68]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  67]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  66]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  65]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  64]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  63]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  62]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  61]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  60]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  59]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  58]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  57]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  56]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  55]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  54]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  53]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  52]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  51]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  50]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  49]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  48]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  47]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  46]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  45]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  44]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  43]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  42]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  41]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  40]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  39]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  38]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  37]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  36]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  35]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  34]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  33]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  32]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  31]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  30]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  29]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  28]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  27]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  26]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  25]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  24]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  23]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  22]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  21]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  20]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  19]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  18]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  17]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  16]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  15]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  14]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  13]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  12]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  11]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  10]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   9]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   8]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   7]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   6]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   5]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   4]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   3]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   2]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   1]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[   0]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   62302   226000 |   20767       0        0     nan |  0.000 % |
c |       100 |   60890   221119 |   22843       0        0     nan |  5.144 % |
c |       250 |   58739   213666 |   25128       0        0     nan |  8.774 % |
c |       475 |   57931   210807 |   27640     170     1085     6.4 | 10.212 % |
c |       812 |   57829   210457 |   30404     495     3351     6.8 | 10.349 % |
c |      1318 |   57652   209864 |   33445     973     5475     5.6 | 10.548 % |
c |      2078 |   56914   207350 |   36790    1633     8411     5.2 | 11.418 % |
c |      3218 |   55599   202801 |   40469    2595    13376     5.2 | 12.952 % |
c |      4926 |   50524   184958 |   44515    3568    19096     5.4 | 18.911 % |
c |      7488 |   34351   129451 |   48967    3637    26460     7.3 | 38.760 % |
c |     11332 |   28042   108408 |   53864    6536   222907    34.1 | 46.849 % |
c |     17099 |   27940   108078 |   59250   12284  3167657   257.9 | 46.993 % |
c |     25749 |   27933   108055 |   65175   20933  8742893   417.7 | 47.000 % |
c |     38723 |   27933   108055 |   71693   33907 15984401   471.4 | 47.000 % |
c |     58185 |   27915   107997 |   78862   53366 24700671   462.9 | 47.027 % |
c |     87379 |   27906   107968 |   86748   82559 42640667   516.5 | 47.041 % |
c |    131168 |   27842   107760 |   95423   43091 20715372   480.7 | 47.123 % |
#### 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 30905
Raw data (stat): 30905 (runsolver) R 30904 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420235771 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1680 0 1 0 981 5 0 0 25 0 1 0 420235771 8519680 1644 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2080 1644 603 41 0 2039 0
vsize: 8320
[startup+20.0014 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1682 0 1 0 1981 5 0 0 25 0 1 0 420235771 8519680 1646 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1646 603 41 0 2039 0
vsize: 8320
[startup+30.0021 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1686 0 1 0 2981 5 0 0 25 0 1 0 420235771 8519680 1650 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1650 603 41 0 2039 0
vsize: 8320
[startup+40.0027 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1688 0 1 0 3981 5 0 0 25 0 1 0 420235771 8519680 1652 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1652 603 41 0 2039 0
vsize: 8320
[startup+50.0038 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1691 0 1 0 4981 6 0 0 25 0 1 0 420235771 8519680 1655 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1655 603 41 0 2039 0
vsize: 8320
[startup+60.0039 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1693 0 1 0 5981 6 0 0 25 0 1 0 420235771 8654848 1657 4294967295 134512640 134672761 3221224544 3221223776 134557473 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2113 1657 603 41 0 2072 0
vsize: 8452
[startup+70.0043 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1699 0 1 0 6981 6 0 0 25 0 1 0 420235771 8654848 1663 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2113 1663 603 41 0 2072 0
vsize: 8452
[startup+80.0055 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 1709 0 1 0 7980 6 0 0 25 0 1 0 420235771 8654848 1673 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2113 1673 603 41 0 2072 0
vsize: 8452
[startup+90.0061 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 2335 0 1 0 8979 7 0 0 25 0 1 0 420235771 11218944 2299 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2739 2299 603 41 0 2698 0
vsize: 10956
[startup+100.006 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 5277 0 1 0 9973 14 0 0 25 0 1 0 420235771 23334912 5241 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5697 5241 603 41 0 5656 0
vsize: 22788
[startup+110.006 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 7191 0 1 0 10968 19 0 0 25 0 1 0 420235771 31166464 7155 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7609 7155 603 41 0 7568 0
vsize: 30436
[startup+120.007 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 8720 0 1 0 11964 23 0 0 25 0 1 0 420235771 37384192 8684 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9127 8684 603 41 0 9086 0
vsize: 36508
[startup+130.007 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 10053 0 1 0 12960 27 0 0 25 0 1 0 420235771 42926080 10017 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10480 10017 603 41 0 10439 0
vsize: 41920
[startup+140.007 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 12090 0 1 0 13956 31 0 0 25 0 1 0 420235771 51171328 12054 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12493 12054 603 41 0 12452 0
vsize: 49972
[startup+150.013 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 13357 0 1 0 14954 33 0 0 25 0 1 0 420235771 56446976 13321 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13781 13321 603 41 0 13740 0
vsize: 55124
[startup+160.012 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 14617 0 1 0 15951 37 0 0 25 0 1 0 420235771 61579264 14581 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15034 14581 603 41 0 14993 0
vsize: 60136
[startup+170.013 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 15753 0 1 0 16949 39 0 0 25 0 1 0 420235771 66179072 15717 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16157 15717 603 41 0 16116 0
vsize: 64628
[startup+180.013 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 16689 0 1 0 17947 41 0 0 25 0 1 0 420235771 70090752 16653 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17112 16653 603 41 0 17071 0
vsize: 68448
[startup+190.014 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 17727 0 1 0 18945 44 0 0 25 0 1 0 420235771 74432512 17691 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18172 17691 603 41 0 18131 0
vsize: 72688
[startup+200.014 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 19150 0 1 0 19941 47 0 0 25 0 1 0 420235771 80240640 19114 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19590 19114 603 41 0 19549 0
vsize: 78360
[startup+210.014 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 20584 0 1 0 20939 50 0 0 25 0 1 0 420235771 86188032 20548 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21042 20548 603 41 0 21001 0
vsize: 84168
[startup+220.014 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 21316 0 1 0 21938 50 0 0 25 0 1 0 420235771 89174016 21280 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21771 21280 603 41 0 21730 0
vsize: 87084
[startup+230.014 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 22101 0 1 0 22937 51 0 0 25 0 1 0 420235771 92434432 22065 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22567 22065 603 41 0 22526 0
vsize: 90268
[startup+240.016 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 23142 0 1 0 23936 53 0 0 25 0 1 0 420235771 96645120 23106 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23595 23106 603 41 0 23554 0
vsize: 94380
[startup+250.016 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 23931 0 1 0 24935 55 0 0 25 0 1 0 420235771 99889152 23895 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24387 23895 603 41 0 24346 0
vsize: 97548
[startup+260.016 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 24816 0 1 0 25932 57 0 0 25 0 1 0 420235771 103534592 24780 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25277 24780 603 41 0 25236 0
vsize: 101108
[startup+270.017 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 25516 0 1 0 26931 59 0 0 25 0 1 0 420235771 106508288 25480 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26003 25480 603 41 0 25962 0
vsize: 104012
[startup+280.016 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 25968 0 1 0 27929 61 0 0 25 0 1 0 420235771 108425216 25932 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26471 25932 603 41 0 26430 0
vsize: 105884
[startup+290.017 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 26474 0 1 0 28928 62 0 0 25 0 1 0 420235771 110579712 26438 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26997 26438 603 41 0 26956 0
vsize: 107988
[startup+300.017 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 26910 0 1 0 29928 62 0 0 25 0 1 0 420235771 112336896 26874 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27426 26874 603 41 0 27385 0
vsize: 109704
[startup+310.017 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 27372 0 1 0 30927 64 0 0 25 0 1 0 420235771 114262016 27336 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27896 27336 603 41 0 27855 0
vsize: 111584
[startup+320.018 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 28772 0 1 0 31925 66 0 0 25 0 1 0 420235771 119934976 28736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29281 28736 603 41 0 29240 0
vsize: 117124
[startup+330.019 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 30051 0 1 0 32922 69 0 0 25 0 1 0 420235771 125198336 30015 4294967295 134512640 134672761 3221224544 3221223808 134562147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30566 30015 603 41 0 30525 0
vsize: 122264
[startup+340.019 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 31159 0 1 0 33920 72 0 0 25 0 1 0 420235771 129789952 31123 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31687 31123 603 41 0 31646 0
vsize: 126748
[startup+350.019 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 32109 0 1 0 34918 74 0 0 25 0 1 0 420235771 133697536 32073 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32641 32073 603 41 0 32600 0
vsize: 130564
[startup+360.019 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 33219 0 1 0 35916 76 0 0 25 0 1 0 420235771 138285056 33183 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33761 33183 603 41 0 33720 0
vsize: 135044
[startup+370.02 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 34160 0 1 0 36913 78 0 0 25 0 1 0 420235771 142336000 34124 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34750 34124 603 41 0 34709 0
vsize: 139000
[startup+380.02 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 34988 0 1 0 37912 80 0 0 25 0 1 0 420235771 145735680 34952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35580 34952 603 41 0 35539 0
vsize: 142320
[startup+390.021 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 35711 0 1 0 38911 81 0 0 25 0 1 0 420235771 148701184 35675 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36304 35675 603 41 0 36263 0
vsize: 145216
[startup+400.021 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 36676 0 1 0 39909 83 0 0 25 0 1 0 420235771 152768512 36640 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37297 36640 603 41 0 37256 0
vsize: 149188
[startup+410.021 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 37840 0 1 0 40907 86 0 0 25 0 1 0 420235771 157491200 37804 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38450 37804 603 41 0 38409 0
vsize: 153800
[startup+420.022 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 38560 0 1 0 41906 87 0 0 25 0 1 0 420235771 160464896 38524 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39176 38524 603 41 0 39135 0
vsize: 156704
[startup+430.023 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 39725 0 1 0 42903 90 0 0 25 0 1 0 420235771 165203968 39689 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40333 39689 603 41 0 40292 0
vsize: 161332
[startup+440.024 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 40878 0 1 0 43901 93 0 0 25 0 1 0 420235771 169914368 40842 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41483 40842 603 41 0 41442 0
vsize: 165932
[startup+450.023 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 42019 0 1 0 44899 94 0 0 25 0 1 0 420235771 174641152 41983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42637 41983 603 41 0 42596 0
vsize: 170548
[startup+460.023 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 43110 0 1 0 45896 97 0 0 25 0 1 0 420235771 179081216 43074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43721 43074 603 41 0 43680 0
vsize: 174884
[startup+470.024 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 44012 0 1 0 46894 100 0 0 25 0 1 0 420235771 182714368 43976 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44608 43976 603 41 0 44567 0
vsize: 178432
[startup+480.024 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 44939 0 1 0 47892 102 0 0 25 0 1 0 420235771 186605568 44903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45558 44903 603 41 0 45517 0
vsize: 182232
[startup+490.025 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 46038 0 1 0 48890 104 0 0 25 0 1 0 420235771 191238144 46002 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46689 46002 603 41 0 46648 0
vsize: 186756
[startup+500.025 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 46249 0 1 0 49889 105 0 0 25 0 1 0 420235771 192049152 46213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46887 46213 603 41 0 46846 0
vsize: 187548
[startup+510.025 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 47266 0 1 0 50887 107 0 0 25 0 1 0 420235771 196227072 47230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47907 47230 603 41 0 47866 0
vsize: 191628
[startup+520.026 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 48207 0 1 0 51885 110 0 0 25 0 1 0 420235771 200159232 48171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48867 48171 603 41 0 48826 0
vsize: 195468
[startup+530.026 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 49046 0 1 0 52883 111 0 0 25 0 1 0 420235771 203526144 49010 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49689 49010 603 41 0 49648 0
vsize: 198756
[startup+540.027 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 49758 0 1 0 53882 113 0 0 25 0 1 0 420235771 206495744 49722 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50414 49722 603 41 0 50373 0
vsize: 201656
[startup+550.028 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 50358 0 1 0 54881 114 0 0 25 0 1 0 420235771 208920576 50322 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51006 50322 603 41 0 50965 0
vsize: 204024
[startup+560.027 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 51101 0 1 0 55879 116 0 0 25 0 1 0 420235771 212041728 51065 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51768 51065 603 41 0 51727 0
vsize: 207072
[startup+570.028 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 51777 0 1 0 56877 118 0 0 25 0 1 0 420235771 214745088 51741 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52428 51741 603 41 0 52387 0
vsize: 209712
[startup+580.028 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 52249 0 1 0 57877 119 0 0 25 0 1 0 420235771 216633344 52213 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52889 52213 603 41 0 52848 0
vsize: 211556
[startup+590.029 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 52822 0 1 0 58876 120 0 0 25 0 1 0 420235771 218947584 52786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53454 52786 603 41 0 53413 0
vsize: 213816
[startup+600.029 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 53429 0 1 0 59875 121 0 0 25 0 1 0 420235771 221515776 53393 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54081 53393 603 41 0 54040 0
vsize: 216324
[startup+610.029 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54028 0 1 0 60874 122 0 0 25 0 1 0 420235771 223989760 53992 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54685 53992 603 41 0 54644 0
vsize: 218740
[startup+620.03 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54587 0 1 0 61872 124 0 0 25 0 1 0 420235771 226422784 54551 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55279 54551 603 41 0 55238 0
vsize: 221116
[startup+630.03 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54638 0 1 0 62872 125 0 0 25 0 1 0 420235771 226557952 54602 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54602 603 41 0 55271 0
vsize: 221248
[startup+640.031 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54639 0 1 0 63872 125 0 0 25 0 1 0 420235771 226557952 54603 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54603 603 41 0 55271 0
vsize: 221248
[startup+650.031 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54640 0 1 0 64872 125 0 0 25 0 1 0 420235771 226557952 54604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54604 603 41 0 55271 0
vsize: 221248
[startup+660.031 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54645 0 1 0 65873 125 0 0 25 0 1 0 420235771 226557952 54609 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54609 603 41 0 55271 0
vsize: 221248
[startup+670.031 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54647 0 1 0 66873 125 0 0 25 0 1 0 420235771 226557952 54611 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54611 603 41 0 55271 0
vsize: 221248
[startup+680.031 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54647 0 1 0 67873 125 0 0 25 0 1 0 420235771 226557952 54611 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54611 603 41 0 55271 0
vsize: 221248
[startup+690.032 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54648 0 1 0 68873 125 0 0 25 0 1 0 420235771 226557952 54612 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54612 603 41 0 55271 0
vsize: 221248
[startup+700.032 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 69873 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+710.032 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 70874 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+720.033 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 71874 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+730.033 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 72874 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+740.034 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 73874 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+750.035 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54649 0 1 0 74875 125 0 0 25 0 1 0 420235771 226557952 54613 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54613 603 41 0 55271 0
vsize: 221248
[startup+760.035 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54655 0 1 0 75875 125 0 0 25 0 1 0 420235771 226557952 54619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54619 603 41 0 55271 0
vsize: 221248
[startup+770.035 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54655 0 1 0 76875 125 0 0 25 0 1 0 420235771 226557952 54619 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54619 603 41 0 55271 0
vsize: 221248
[startup+780.037 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54655 0 1 0 77875 125 0 0 25 0 1 0 420235771 226557952 54619 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54619 603 41 0 55271 0
vsize: 221248
[startup+790.037 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54655 0 1 0 78875 125 0 0 25 0 1 0 420235771 226557952 54619 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54619 603 41 0 55271 0
vsize: 221248
[startup+800.037 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54656 0 1 0 79876 125 0 0 25 0 1 0 420235771 226557952 54620 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54620 603 41 0 55271 0
vsize: 221248
[startup+810.037 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54656 0 1 0 80876 125 0 0 25 0 1 0 420235771 226557952 54620 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54620 603 41 0 55271 0
vsize: 221248
[startup+820.038 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54660 0 1 0 81875 125 0 0 25 0 1 0 420235771 226557952 54624 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55312 54624 603 41 0 55271 0
vsize: 221248
[startup+830.037 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54670 0 1 0 82875 125 0 0 25 0 1 0 420235771 226557952 54634 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54634 603 41 0 55271 0
vsize: 221248
[startup+840.038 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54677 0 1 0 83875 125 0 0 25 0 1 0 420235771 226557952 54641 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54641 603 41 0 55271 0
vsize: 221248
[startup+850.039 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54681 0 1 0 84875 125 0 0 25 0 1 0 420235771 226557952 54645 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54645 603 41 0 55271 0
vsize: 221248
[startup+860.039 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 85875 125 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+870.04 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 86875 125 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+880.039 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 87876 125 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+890.04 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 88876 125 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+900.04 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 89876 125 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+910.04 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 90875 126 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+920.041 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54684 0 1 0 91876 126 0 0 25 0 1 0 420235771 226557952 54648 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54648 603 41 0 55271 0
vsize: 221248
[startup+930.04 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 92876 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+940.041 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 93876 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+950.042 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 94876 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+960.043 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 95876 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+970.044 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 96877 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+980.044 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 97877 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+990.044 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 98877 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 99877 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 100877 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 101878 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 102878 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 103878 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 104878 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 105879 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 106879 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 107879 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 108879 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 109879 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 110880 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 111880 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 112880 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 113880 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 114880 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 115881 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 116881 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 117881 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 118881 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 30905
Raw data (stat): 30905 (minisat+) R 30904 29151 29150 0 -1 0 54685 0 1 0 119882 126 0 0 25 0 1 0 420235771 226557952 54649 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55312 54649 603 41 0 55271 0
vsize: 221248
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 30905
Raw data (stat): 30905 (minisat+) Z 30904 29151 29150 0 -1 12 54687 0 1 0 119882 136 0 0 25 0 1 0 420235771 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.16
CPU time (s): 1200.18
CPU user time (s): 1198.82
CPU system time (s): 1.36279
CPU usage (%): 100.002
Max. virtual memory (Kb): 221248
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####