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-chnl35_36_pb.cnf.cr.opb
MD5SUMc779424bd1795a1e1adf6f4e7f38e307
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 37
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.075987
Number of variables2520
Total number of constraints142
Number of constraints which are clauses72
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint36

Trace number 4584 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-13 19:24:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3398 boxname=wulflinc27 idbench=14 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c779424bd1795a1e1adf6f4e7f38e307  /oldhome/oroussel/tmp/wulflinc27/normalized-chnl35_36_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc27/normalized-chnl35_36_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc27/normalized-chnl35_36_pb.cnf.cr.opb
IDLAUNCH: 3398
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        884848 kB
Buffers:         33044 kB
Cached:          80212 kB
SwapCached:       3160 kB
Active:          45248 kB
Inactive:        74044 kB
HighTotal:      131008 kB
HighFree:        47292 kB
LowTotal:       903652 kB
LowFree:        837556 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            24980 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:44:52 (client local time) WITH STATUS 0 IN 1200.12 SECONDS
stats: 3398 7 1200.12 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 142 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................
c ---[  69]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  68]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  67]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  66]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  65]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  64]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  63]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  62]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  61]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  60]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  59]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  58]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  57]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  56]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  55]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  54]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  53]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  52]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  51]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  50]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  49]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  48]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  47]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  46]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  45]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  44]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  43]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  42]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  41]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  40]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  39]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  38]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  37]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  36]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  35]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  34]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  33]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  32]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  31]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  30]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  29]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  28]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  27]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  26]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  25]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  24]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  23]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  22]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  21]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  20]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  19]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  18]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  17]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  16]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  15]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  14]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  13]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  12]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  11]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[  10]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   9]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   8]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   7]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   6]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   5]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   4]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   3]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   2]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   1]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[   0]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   29472   107170 |    9824       0        0     nan |  0.000 % |
c |       100 |   29058   105812 |   10806      43       94     2.2 |  9.501 % |
c |       251 |   28460   103842 |   11887     115      243     2.1 | 10.930 % |
c |       476 |   27795   101563 |   13075     232      608     2.6 | 12.251 % |
c |       815 |   27232    99596 |   14383     480     1789     3.7 | 13.342 % |
c |      1321 |   26633    97543 |   15821     888     3666     4.1 | 14.609 % |
c |      2080 |   25542    93806 |   17403    1463     6942     4.7 | 17.008 % |
c |      3219 |   23787    87808 |   19144    2287    11420     5.0 | 20.822 % |
c |      4927 |   21035    78374 |   21058    3487    99619    28.6 | 26.968 % |
c |      7489 |   17168    65179 |   23164    5320   312146    58.7 | 35.876 % |
c |     11334 |   15954    61041 |   25480    8964  1427192   159.2 | 38.827 % |
c |     17100 |   15883    60799 |   28029   14718  2946103   200.2 | 39.003 % |
c |     25749 |   15871    60759 |   30831   23365  6533046   279.6 | 39.030 % |
c |     38723 |   15760    60382 |   33915   13891  5897899   424.6 | 39.286 % |
c |     58185 |   15646    59991 |   37306   33335 18370718   551.1 | 39.555 % |
c |     87381 |   15646    59991 |   41037   34727 22357992   643.8 | 39.555 % |
c |    131176 |   15618    59895 |   45141   17269  8833076   511.5 | 39.623 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.00 0.00 0.04 2/54 20264
Raw data (stat): 20264 (runsolver) R 20263 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478448034 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.15 0.03 0.05 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 985 0 1 0 984 2 0 0 25 0 1 0 478448034 5586944 963 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1364 963 603 41 0 1323 0
vsize: 5456
[startup+20.001 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 1098 0 1 0 1984 2 0 0 25 0 1 0 478448034 5988352 1076 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1462 1076 603 41 0 1421 0
vsize: 5848
[startup+30.0009 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 2235 0 1 0 2981 5 0 0 25 0 1 0 478448034 10719232 2213 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2617 2213 603 41 0 2576 0
vsize: 10468
[startup+40.0009 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 4068 0 1 0 3975 11 0 0 25 0 1 0 478448034 18259968 4046 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4458 4046 603 41 0 4417 0
vsize: 17832
[startup+50.0014 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 5469 0 1 0 4972 14 0 0 25 0 1 0 478448034 24092672 5447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5882 5447 603 41 0 5841 0
vsize: 23528
[startup+60.0013 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 6616 0 1 0 5969 17 0 0 25 0 1 0 478448034 28672000 6594 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7000 6594 603 41 0 6959 0
vsize: 28000
[startup+70.0023 s]
Raw data (loadavg): 0.69 0.21 0.10 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 7798 0 1 0 6966 20 0 0 25 0 1 0 478448034 33660928 7776 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8218 7776 603 41 0 8177 0
vsize: 32872
[startup+80.0029 s]
Raw data (loadavg): 0.73 0.23 0.11 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 9088 0 1 0 7963 24 0 0 25 0 1 0 478448034 38912000 9066 4294967295 134512640 134672761 3221224544 3221223648 134555084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9500 9066 603 41 0 9459 0
vsize: 38000
[startup+90.0027 s]
Raw data (loadavg): 0.77 0.26 0.12 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 10277 0 1 0 8959 28 0 0 25 0 1 0 478448034 43749376 10255 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10681 10255 603 41 0 10640 0
vsize: 42724
[startup+100.003 s]
Raw data (loadavg): 0.81 0.28 0.13 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 11327 0 1 0 9957 30 0 0 25 0 1 0 478448034 48074752 11305 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11737 11305 603 41 0 11696 0
vsize: 46948
[startup+110.003 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 12153 0 1 0 10954 34 0 0 25 0 1 0 478448034 51449856 12131 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 12131 603 41 0 12520 0
vsize: 50244
[startup+120.004 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 13088 0 1 0 11951 37 0 0 25 0 1 0 478448034 55353344 13066 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13514 13066 603 41 0 13473 0
vsize: 54056
[startup+130.004 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 14040 0 1 0 12949 39 0 0 25 0 1 0 478448034 59293696 14018 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14476 14018 603 41 0 14435 0
vsize: 57904
[startup+140.004 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 14040 0 1 0 13948 39 0 0 25 0 1 0 478448034 59293696 14018 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14476 14018 603 41 0 14435 0
vsize: 57904
[startup+150.005 s]
Raw data (loadavg): 0.92 0.39 0.18 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 14040 0 1 0 14948 39 0 0 25 0 1 0 478448034 59293696 14018 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14476 14018 603 41 0 14435 0
vsize: 57904
[startup+160.005 s]
Raw data (loadavg): 0.93 0.41 0.18 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 14040 0 1 0 15948 39 0 0 25 0 1 0 478448034 59293696 14018 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14476 14018 603 41 0 14435 0
vsize: 57904
[startup+170.005 s]
Raw data (loadavg): 0.94 0.43 0.19 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 14040 0 1 0 16948 39 0 0 25 0 1 0 478448034 59293696 14018 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14476 14018 603 41 0 14435 0
vsize: 57904
[startup+180.006 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 15745 0 1 0 17945 43 0 0 25 0 1 0 478448034 66306048 15723 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16188 15723 603 41 0 16147 0
vsize: 64752
[startup+190.006 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 17112 0 1 0 18943 45 0 0 25 0 1 0 478448034 71831552 17090 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17537 17090 603 41 0 17496 0
vsize: 70148
[startup+200.007 s]
Raw data (loadavg): 0.96 0.48 0.22 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 18481 0 1 0 19940 48 0 0 25 0 1 0 478448034 77496320 18459 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18920 18459 603 41 0 18879 0
vsize: 75680
[startup+210.007 s]
Raw data (loadavg): 0.97 0.50 0.22 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 19240 0 1 0 20938 51 0 0 25 0 1 0 478448034 80687104 19218 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19699 19218 603 41 0 19658 0
vsize: 78796
[startup+220.009 s]
Raw data (loadavg): 0.97 0.51 0.23 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 20383 0 1 0 21935 54 0 0 25 0 1 0 478448034 85389312 20361 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20847 20361 603 41 0 20806 0
vsize: 83388
[startup+230.008 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 21930 0 1 0 22930 58 0 0 25 0 1 0 478448034 91758592 21908 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22402 21908 603 41 0 22361 0
vsize: 89608
[startup+240.008 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 23204 0 1 0 23928 60 0 0 25 0 1 0 478448034 96894976 23182 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23656 23183 603 41 0 23615 0
vsize: 94624
[startup+250.009 s]
Raw data (loadavg): 0.98 0.56 0.25 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 24592 0 1 0 24924 64 0 0 25 0 1 0 478448034 102572032 24570 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25042 24570 603 41 0 25001 0
vsize: 100168
[startup+260.009 s]
Raw data (loadavg): 0.98 0.57 0.26 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 25921 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+270.009 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 26921 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+280.01 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 27921 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+290.01 s]
Raw data (loadavg): 0.99 0.61 0.28 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 28922 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+300.01 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 29922 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+310.01 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 30922 67 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+320.011 s]
Raw data (loadavg): 0.99 0.65 0.30 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26262 0 1 0 31922 68 0 0 25 0 1 0 478448034 109469696 26240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26240 603 41 0 26685 0
vsize: 106904
[startup+330.01 s]
Raw data (loadavg): 0.99 0.66 0.31 3/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26263 0 1 0 32922 68 0 0 25 0 1 0 478448034 109469696 26241 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26241 603 41 0 26685 0
vsize: 106904
[startup+340.01 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26264 0 1 0 33922 68 0 0 25 0 1 0 478448034 109469696 26242 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26242 603 41 0 26685 0
vsize: 106904
[startup+350.011 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26264 0 1 0 34922 68 0 0 25 0 1 0 478448034 109469696 26242 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26242 603 41 0 26685 0
vsize: 106904
[startup+360.011 s]
Raw data (loadavg): 0.99 0.69 0.33 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26264 0 1 0 35923 68 0 0 25 0 1 0 478448034 109469696 26242 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26242 603 41 0 26685 0
vsize: 106904
[startup+370.012 s]
Raw data (loadavg): 0.99 0.70 0.34 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26264 0 1 0 36923 68 0 0 25 0 1 0 478448034 109469696 26242 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26242 603 41 0 26685 0
vsize: 106904
[startup+380.012 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 37923 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+390.012 s]
Raw data (loadavg): 0.99 0.72 0.35 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 38923 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+400.013 s]
Raw data (loadavg): 0.99 0.73 0.36 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 39923 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+410.013 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 40923 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+420.014 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 41924 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+430.013 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 42924 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+440.013 s]
Raw data (loadavg): 0.99 0.76 0.38 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 43924 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+450.014 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26265 0 1 0 44924 68 0 0 25 0 1 0 478448034 109469696 26243 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26243 603 41 0 26685 0
vsize: 106904
[startup+460.015 s]
Raw data (loadavg): 0.99 0.77 0.40 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26266 0 1 0 45924 68 0 0 25 0 1 0 478448034 109469696 26244 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26244 603 41 0 26685 0
vsize: 106904
[startup+470.015 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26266 0 1 0 46924 68 0 0 25 0 1 0 478448034 109469696 26244 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26244 603 41 0 26685 0
vsize: 106904
[startup+480.016 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26266 0 1 0 47924 68 0 0 25 0 1 0 478448034 109469696 26244 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26726 26244 603 41 0 26685 0
vsize: 106904
[startup+490.015 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26468 0 1 0 48923 69 0 0 25 0 1 0 478448034 110280704 26446 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26924 26446 603 41 0 26883 0
vsize: 107696
[startup+500.015 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 26955 0 1 0 49922 70 0 0 25 0 1 0 478448034 112320512 26933 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27422 26933 603 41 0 27381 0
vsize: 109688
[startup+510.015 s]
Raw data (loadavg): 0.99 0.81 0.42 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 27629 0 1 0 50921 72 0 0 25 0 1 0 478448034 115023872 27607 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28082 27607 603 41 0 28041 0
vsize: 112328
[startup+520.016 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 28254 0 1 0 51920 73 0 0 25 0 1 0 478448034 117592064 28232 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28709 28232 603 41 0 28668 0
vsize: 114836
[startup+530.016 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 28865 0 1 0 52919 74 0 0 25 0 1 0 478448034 120160256 28843 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29336 28843 603 41 0 29295 0
vsize: 117344
[startup+540.016 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 29551 0 1 0 53918 76 0 0 25 0 1 0 478448034 122863616 29529 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29996 29529 603 41 0 29955 0
vsize: 119984
[startup+550.017 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 30246 0 1 0 54916 78 0 0 25 0 1 0 478448034 125837312 30224 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30722 30224 603 41 0 30681 0
vsize: 122888
[startup+560.017 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 30893 0 1 0 55914 79 0 0 25 0 1 0 478448034 128409600 30871 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31350 30871 603 41 0 31309 0
vsize: 125400
[startup+570.018 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 31163 0 1 0 56914 80 0 0 25 0 1 0 478448034 129490944 31141 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31614 31141 603 41 0 31573 0
vsize: 126456
[startup+580.017 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 31564 0 1 0 57912 82 0 0 25 0 1 0 478448034 131112960 31542 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32010 31542 603 41 0 31969 0
vsize: 128040
[startup+590.017 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32052 0 1 0 58911 84 0 0 25 0 1 0 478448034 133140480 32030 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32505 32030 603 41 0 32464 0
vsize: 130020
[startup+600.018 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32503 0 1 0 59910 85 0 0 25 0 1 0 478448034 135032832 32481 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32967 32481 603 41 0 32926 0
vsize: 131868
[startup+610.018 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 60910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+620.018 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 61910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+630.019 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 62910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+640.018 s]
Raw data (loadavg): 0.99 0.87 0.49 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 63910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+650.018 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 64910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+660.018 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32588 0 1 0 65910 85 0 0 25 0 1 0 478448034 135303168 32566 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32566 603 41 0 32992 0
vsize: 132132
[startup+670.018 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 66910 85 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+680.018 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 67910 85 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+690.018 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 68911 85 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+700.018 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 69911 85 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+710.018 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 70911 86 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+720.018 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 71911 86 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+730.019 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 72911 86 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+740.019 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 73911 86 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+750.019 s]
Raw data (loadavg): 0.99 0.90 0.55 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32589 0 1 0 74911 86 0 0 25 0 1 0 478448034 135303168 32567 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32567 603 41 0 32992 0
vsize: 132132
[startup+760.019 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 75912 86 0 0 25 0 1 0 478448034 135303168 32569 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32569 603 41 0 32992 0
vsize: 132132
[startup+770.019 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 76912 86 0 0 25 0 1 0 478448034 135303168 32569 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33033 32569 603 41 0 32992 0
vsize: 132132
[startup+780.019 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 77912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+790.018 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 78912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+800.019 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 79911 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+810.019 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 80911 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+820.019 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 81911 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+830.019 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 82912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223648 134555205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+840.019 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 83912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+850.019 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 84912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+860.019 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 85912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+870.019 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 86912 86 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+880.02 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 87912 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+890.02 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 88912 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+900.02 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 89913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+910.02 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 90913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+920.02 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 91913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+930.02 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 92913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+940.02 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 93913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+950.019 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 94913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+960.02 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 95913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+970.019 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 96913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+980.019 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 97913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+990.019 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 98913 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 99914 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 100914 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 101914 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 102914 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223728 134559564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32591 0 1 0 103914 87 0 0 25 0 1 0 478448034 135274496 32562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33026 32562 603 41 0 32985 0
vsize: 132104
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 32886 0 1 0 104914 88 0 0 25 0 1 0 478448034 136491008 32857 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33323 32857 603 41 0 33282 0
vsize: 133292
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 33288 0 1 0 105912 89 0 0 25 0 1 0 478448034 138235904 33259 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33749 33259 603 41 0 33708 0
vsize: 134996
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 33665 0 1 0 106912 90 0 0 25 0 1 0 478448034 139726848 33636 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34113 33636 603 41 0 34072 0
vsize: 136452
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 34031 0 1 0 107911 91 0 0 25 0 1 0 478448034 141213696 34002 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34476 34002 603 41 0 34435 0
vsize: 137904
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 34492 0 1 0 108910 92 0 0 25 0 1 0 478448034 143085568 34463 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34933 34463 603 41 0 34892 0
vsize: 139732
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 34895 0 1 0 109909 94 0 0 25 0 1 0 478448034 144855040 34866 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35365 34866 603 41 0 35324 0
vsize: 141460
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 35969 0 1 0 110906 97 0 0 25 0 1 0 478448034 149180416 35940 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36421 35940 603 41 0 36380 0
vsize: 145684
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36469 0 1 0 111905 98 0 0 25 0 1 0 478448034 151207936 36440 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36440 603 41 0 36875 0
vsize: 147664
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36469 0 1 0 112905 98 0 0 25 0 1 0 478448034 151207936 36440 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36440 603 41 0 36875 0
vsize: 147664
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36469 0 1 0 113906 98 0 0 25 0 1 0 478448034 151207936 36440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36440 603 41 0 36875 0
vsize: 147664
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36469 0 1 0 114906 98 0 0 25 0 1 0 478448034 151207936 36440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36440 603 41 0 36875 0
vsize: 147664
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36470 0 1 0 115906 98 0 0 25 0 1 0 478448034 151207936 36441 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36441 603 41 0 36875 0
vsize: 147664
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36470 0 1 0 116906 98 0 0 25 0 1 0 478448034 151207936 36441 4294967295 134512640 134672761 3221224544 3221223728 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36441 603 41 0 36875 0
vsize: 147664
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36470 0 1 0 117906 98 0 0 25 0 1 0 478448034 151207936 36441 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36441 603 41 0 36875 0
vsize: 147664
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36470 0 1 0 118906 98 0 0 25 0 1 0 478448034 151207936 36441 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36441 603 41 0 36875 0
vsize: 147664
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 20264
Raw data (stat): 20264 (minisat+) R 20263 18865 18864 0 -1 0 36470 0 1 0 119906 98 0 0 25 0 1 0 478448034 151207936 36441 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36916 36441 603 41 0 36875 0
vsize: 147664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 20264
Raw data (stat): 20264 (minisat+) Z 20263 18865 18864 0 -1 12 36472 0 1 0 119907 105 0 0 25 0 1 0 478448034 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.12
CPU user time (s): 1199.07
CPU system time (s): 1.05184
CPU usage (%): 100.003
Max. virtual memory (Kb): 147664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####