Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_35_pb.cnf.cr.opb
MD5SUMb1c5adb5438ceaf1c654cfedb79b695e
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 36
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.06099
Number of variables2100
Total number of constraints130
Number of constraints which are clauses70
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint35

Trace number 5711 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 01:38:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4148 boxname=wulflinc22 idbench=12 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b1c5adb5438ceaf1c654cfedb79b695e  /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc22/normalized-chnl30_35_pb.cnf.cr.opb
IDLAUNCH: 4148
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        852816 kB
Buffers:         32736 kB
Cached:         106004 kB
SwapCached:        524 kB
Active:          49040 kB
Inactive:        93076 kB
HighTotal:      131008 kB
HighFree:        21336 kB
LowTotal:       903652 kB
LowFree:        831480 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34276 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:58:07 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4148 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 130 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................
c ---[  59]---> BDD-cost:   67
c ---[  58]---> BDD-cost:   67
c ---[  57]---> BDD-cost:   67
c ---[  56]---> BDD-cost:   67
c ---[  55]---> BDD-cost:   67
c ---[  54]---> BDD-cost:   67
c ---[  53]---> BDD-cost:   67
c ---[  52]---> BDD-cost:   67
c ---[  51]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   67
c ---[  49]---> BDD-cost:   67
c ---[  48]---> BDD-cost:   67
c ---[  47]---> BDD-cost:   67
c ---[  46]---> BDD-cost:   67
c ---[  45]---> BDD-cost:   67
c ---[  44]---> BDD-cost:   67
c ---[  43]---> BDD-cost:   67
c ---[  42]---> BDD-cost:   67
c ---[  41]---> BDD-cost:   67
c ---[  40]---> BDD-cost:   67
c ---[  39]---> BDD-cost:   67
c ---[  38]---> BDD-cost:   67
c ---[  37]---> BDD-cost:   67
c ---[  36]---> BDD-cost:   67
c ---[  35]---> BDD-cost:   67
c ---[  34]---> BDD-cost:   67
c ---[  33]---> BDD-cost:   67
c ---[  32]---> BDD-cost:   67
c ---[  31]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   67
c ---[  29]---> BDD-cost:   67
c ---[  28]---> BDD-cost:   67
c ---[  27]---> BDD-cost:   67
c ---[  26]---> BDD-cost:   67
c ---[  25]---> BDD-cost:   67
c ---[  24]---> BDD-cost:   67
c ---[  23]---> BDD-cost:   67
c ---[  22]---> BDD-cost:   67
c ---[  21]---> BDD-cost:   67
c ---[  20]---> BDD-cost:   67
c ---[  19]---> BDD-cost:   67
c ---[  18]---> BDD-cost:   67
c ---[  17]---> BDD-cost:   67
c ---[  16]---> BDD-cost:   67
c ---[  15]---> BDD-cost:   67
c ---[  14]---> BDD-cost:   67
c ---[  13]---> BDD-cost:   67
c ---[  12]---> BDD-cost:   67
c ---[  11]---> BDD-cost:   67
c ---[  10]---> BDD-cost:   67
c ---[   9]---> BDD-cost:   67
c ---[   8]---> BDD-cost:   67
c ---[   7]---> BDD-cost:   67
c ---[   6]---> BDD-cost:   67
c ---[   5]---> BDD-cost:   67
c ---[   4]---> BDD-cost:   67
c ---[   3]---> BDD-cost:   67
c ---[   2]---> BDD-cost:   67
c ---[   1]---> BDD-cost:   67
c ---[   0]---> BDD-cost:   67
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10030    28020 |    3343       0        0     nan |  0.000 % |
c |       105 |   10030    28020 |    3677     105    11655   111.0 |  0.980 % |
c |       257 |   10030    28020 |    4045     257    29832   116.1 |  0.980 % |
c |       483 |   10030    28020 |    4449     483    70240   145.4 |  0.980 % |
c |       822 |   10030    28020 |    4894     822   128798   156.7 |  0.980 % |
c |      1332 |   10030    28020 |    5383    1332   212600   159.6 |  0.980 % |
c |      2091 |   10030    28020 |    5922    2091   359695   172.0 |  0.980 % |
c |      3231 |   10030    28020 |    6514    3231   581665   180.0 |  0.980 % |
c |      4941 |   10030    28020 |    7166    4941  1128031   228.3 |  0.980 % |
c |      7504 |   10030    28020 |    7882    7504  1889344   251.8 |  0.980 % |
c |     11348 |   10030    28020 |    8670    6199  1605192   258.9 |  0.980 % |
c |     17117 |   10030    28020 |    9537    6488  1486146   229.1 |  0.980 % |
c |     25767 |   10030    28020 |   10491    9195  2320409   252.4 |  0.980 % |
c |     38743 |   10030    28020 |   11540    9205  1749321   190.0 |  0.980 % |
c |     58205 |   10030    28020 |   12695    7890  2211413   280.3 |  0.980 % |
c |     87397 |   10030    28020 |   13964    8204  2185785   266.4 |  0.980 % |
c |    131187 |   10030    28020 |   15360   10994  2976111   270.7 |  0.980 % |
c |    196872 |   10030    28020 |   16897   18139  5203446   286.9 |  0.980 % |
c |    295406 |   10030    28020 |   18586   16345  8504574   520.3 |  0.980 % |
#### 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.84 0.94 0.90 2/54 30876
Raw data (stat): 30876 (runsolver) R 30875 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480688314 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3005 0 0 0 992 6 0 0 25 0 1 0 480688314 13910016 2983 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3396 2983 603 41 0 3355 0
vsize: 13584
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3532 0 0 0 1990 8 0 0 25 0 1 0 480688314 16068608 3510 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3923 3510 603 41 0 3882 0
vsize: 15692
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 3772 0 0 0 2989 9 0 0 25 0 1 0 480688314 17145856 3750 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4186 3750 603 41 0 4145 0
vsize: 16744
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4051 0 0 0 3988 10 0 0 25 0 1 0 480688314 18231296 4029 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4451 4029 603 41 0 4410 0
vsize: 17804
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4337 0 0 0 4987 11 0 0 25 0 1 0 480688314 19447808 4315 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4748 4315 603 41 0 4707 0
vsize: 18992
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4338 0 0 0 5987 12 0 0 25 0 1 0 480688314 19447808 4316 4294967295 134512640 134672761 3221224528 3221223712 134558909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4748 4316 603 41 0 4707 0
vsize: 18992
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4338 0 0 0 6987 12 0 0 25 0 1 0 480688314 19447808 4316 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4748 4316 603 41 0 4707 0
vsize: 18992
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 4400 0 0 0 7987 12 0 0 25 0 1 0 480688314 19718144 4378 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4814 4378 603 41 0 4773 0
vsize: 19256
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5254 0 0 0 8985 14 0 0 25 0 1 0 480688314 23228416 5232 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5671 5232 603 41 0 5630 0
vsize: 22684
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5319 0 0 0 9984 15 0 0 25 0 1 0 480688314 23502848 5297 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5738 5297 603 41 0 5697 0
vsize: 22952
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5333 0 0 0 10984 15 0 0 25 0 1 0 480688314 23502848 5311 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5738 5311 603 41 0 5697 0
vsize: 22952
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5631 0 0 0 11983 17 0 0 25 0 1 0 480688314 24723456 5609 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6036 5609 603 41 0 5995 0
vsize: 24144
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5833 0 0 0 12983 17 0 0 25 0 1 0 480688314 25677824 5811 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6269 5811 603 41 0 6228 0
vsize: 25076
[startup+140.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5834 0 0 0 13982 18 0 0 25 0 1 0 480688314 25677824 5812 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6269 5812 603 41 0 6228 0
vsize: 25076
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 14982 18 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 15982 18 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 16982 19 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 17982 19 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 18981 20 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 5942 0 0 0 19981 20 0 0 25 0 1 0 480688314 26079232 5920 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6367 5920 603 41 0 6326 0
vsize: 25468
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6407 0 0 0 20980 21 0 0 25 0 1 0 480688314 28172288 6385 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6878 6385 603 41 0 6837 0
vsize: 27512
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6408 0 0 0 21980 22 0 0 25 0 1 0 480688314 28172288 6386 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6878 6386 603 41 0 6837 0
vsize: 27512
[startup+230.011 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6409 0 0 0 22980 22 0 0 25 0 1 0 480688314 28172288 6387 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6878 6387 603 41 0 6837 0
vsize: 27512
[startup+240.012 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6505 0 0 0 23979 22 0 0 25 0 1 0 480688314 28577792 6483 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6977 6483 603 41 0 6936 0
vsize: 27908
[startup+250.012 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6505 0 0 0 24979 22 0 0 25 0 1 0 480688314 28577792 6483 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6977 6483 603 41 0 6936 0
vsize: 27908
[startup+260.013 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6512 0 0 0 25979 22 0 0 25 0 1 0 480688314 28577792 6490 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6977 6490 603 41 0 6936 0
vsize: 27908
[startup+270.012 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 6809 0 0 0 26978 23 0 0 25 0 1 0 480688314 29794304 6787 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7274 6787 603 41 0 7233 0
vsize: 29096
[startup+280.013 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7145 0 0 0 27977 25 0 0 25 0 1 0 480688314 31145984 7123 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7604 7123 603 41 0 7563 0
vsize: 30416
[startup+290.014 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 28977 25 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+300.013 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 29977 26 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+310.014 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7154 0 0 0 30977 26 0 0 25 0 1 0 480688314 31293440 7132 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7132 603 41 0 7599 0
vsize: 30560
[startup+320.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7157 0 0 0 31977 26 0 0 25 0 1 0 480688314 31293440 7135 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7135 603 41 0 7599 0
vsize: 30560
[startup+330.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7158 0 0 0 32976 26 0 0 25 0 1 0 480688314 31293440 7136 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7640 7136 603 41 0 7599 0
vsize: 30560
[startup+340.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 7985 0 0 0 33974 29 0 0 25 0 1 0 480688314 34660352 7963 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8462 7963 603 41 0 8421 0
vsize: 33848
[startup+350.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 34973 29 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223600 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+360.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 35973 30 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223624 1075347186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+370.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8030 0 0 0 36973 30 0 0 25 0 1 0 480688314 34795520 8008 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8495 8008 603 41 0 8454 0
vsize: 33980
[startup+380.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 37973 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8726 8234 603 41 0 8685 0
vsize: 34904
[startup+390.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 38972 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8726 8234 603 41 0 8685 0
vsize: 34904
[startup+400.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8256 0 0 0 39973 31 0 0 25 0 1 0 480688314 35741696 8234 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8726 8234 603 41 0 8685 0
vsize: 34904
[startup+410.018 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8298 0 0 0 40972 31 0 0 25 0 1 0 480688314 35876864 8276 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8759 8276 603 41 0 8718 0
vsize: 35036
[startup+420.018 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 41971 32 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+430.019 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 42971 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+440.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 43971 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+450.019 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 8615 0 0 0 44970 33 0 0 25 0 1 0 480688314 37302272 8593 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9107 8593 603 41 0 9066 0
vsize: 36428
[startup+460.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9017 0 0 0 45970 34 0 0 25 0 1 0 480688314 38916096 8995 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9501 8995 603 41 0 9460 0
vsize: 38004
[startup+470.02 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9056 0 0 0 46969 35 0 0 25 0 1 0 480688314 39051264 9034 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9534 9034 603 41 0 9493 0
vsize: 38136
[startup+480.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9056 0 0 0 47969 35 0 0 25 0 1 0 480688314 39051264 9034 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9534 9034 603 41 0 9493 0
vsize: 38136
[startup+490.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9162 0 0 0 48969 36 0 0 25 0 1 0 480688314 39452672 9140 4294967295 134512640 134672761 3221224528 3221223632 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9632 9140 603 41 0 9591 0
vsize: 38528
[startup+500.021 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9328 0 0 0 49968 36 0 0 25 0 1 0 480688314 40132608 9306 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9798 9306 603 41 0 9757 0
vsize: 39192
[startup+510.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9329 0 0 0 50968 37 0 0 25 0 1 0 480688314 40132608 9307 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9798 9307 603 41 0 9757 0
vsize: 39192
[startup+520.021 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9330 0 0 0 51967 37 0 0 25 0 1 0 480688314 40132608 9308 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9798 9308 603 41 0 9757 0
vsize: 39192
[startup+530.022 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9330 0 0 0 52967 37 0 0 25 0 1 0 480688314 40132608 9308 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9798 9308 603 41 0 9757 0
vsize: 39192
[startup+540.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9346 0 0 0 53967 37 0 0 25 0 1 0 480688314 40284160 9324 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9324 603 41 0 9794 0
vsize: 39340
[startup+550.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 54967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223712 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+560.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 55967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+570.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 56967 38 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+580.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9358 0 0 0 57967 39 0 0 25 0 1 0 480688314 40284160 9336 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9835 9336 603 41 0 9794 0
vsize: 39340
[startup+590.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 9426 0 0 0 58966 39 0 0 25 0 1 0 480688314 40689664 9404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9934 9404 603 41 0 9893 0
vsize: 39736
[startup+600.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 10229 0 0 0 59964 41 0 0 25 0 1 0 480688314 43929600 10207 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10725 10207 603 41 0 10684 0
vsize: 42900
[startup+610.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 10229 0 0 0 60964 41 0 0 25 0 1 0 480688314 43929600 10207 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10725 10207 603 41 0 10684 0
vsize: 42900
[startup+620.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 11274 0 0 0 61962 44 0 0 25 0 1 0 480688314 48168960 11252 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11760 11252 603 41 0 11719 0
vsize: 47040
[startup+630.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12108 0 0 0 62960 46 0 0 25 0 1 0 480688314 51683328 12086 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 12086 603 41 0 12577 0
vsize: 50472
[startup+640.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 63960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 12087 603 41 0 12577 0
vsize: 50472
[startup+650.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 64960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 12087 603 41 0 12577 0
vsize: 50472
[startup+660.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 65960 46 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 12087 603 41 0 12577 0
vsize: 50472
[startup+670.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12109 0 0 0 66960 47 0 0 25 0 1 0 480688314 51683328 12087 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 12087 603 41 0 12577 0
vsize: 50472
[startup+680.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 67958 48 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+690.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 68958 48 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223712 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+700.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 69958 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+710.032 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 70959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+720.031 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 71959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+730.033 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 72959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+740.034 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 73959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+750.033 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12548 0 0 0 74959 49 0 0 25 0 1 0 480688314 53432320 12526 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12526 603 41 0 13004 0
vsize: 52180
[startup+760.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 12549 0 0 0 75959 49 0 0 25 0 1 0 480688314 53432320 12527 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13045 12527 603 41 0 13004 0
vsize: 52180
[startup+770.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13157 0 0 0 76958 51 0 0 25 0 1 0 480688314 56000512 13135 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13672 13135 603 41 0 13631 0
vsize: 54688
[startup+780.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 77957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13576 603 41 0 14061 0
vsize: 56408
[startup+790.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 78957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13576 603 41 0 14061 0
vsize: 56408
[startup+800.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13598 0 0 0 79957 52 0 0 25 0 1 0 480688314 57761792 13576 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13576 603 41 0 14061 0
vsize: 56408
[startup+810.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13599 0 0 0 80957 52 0 0 25 0 1 0 480688314 57761792 13577 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13577 603 41 0 14061 0
vsize: 56408
[startup+820.035 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 13806 0 0 0 81958 52 0 0 25 0 1 0 480688314 58572800 13784 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14300 13784 603 41 0 14259 0
vsize: 57200
[startup+830.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 82954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15290 14760 603 41 0 15249 0
vsize: 61160
[startup+840.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 83954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15290 14760 603 41 0 15249 0
vsize: 61160
[startup+850.036 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 84954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15290 14760 603 41 0 15249 0
vsize: 61160
[startup+860.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 85954 56 0 0 25 0 1 0 480688314 62627840 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15290 14760 603 41 0 15249 0
vsize: 61160
[startup+870.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 86955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15283 14760 603 41 0 15242 0
vsize: 61132
[startup+880.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 87955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15283 14760 603 41 0 15242 0
vsize: 61132
[startup+890.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 88955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15283 14760 603 41 0 15242 0
vsize: 61132
[startup+900.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 89955 56 0 0 25 0 1 0 480688314 62599168 14760 4294967295 134512640 134672761 3221224528 3221223664 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15283 14760 603 41 0 15242 0
vsize: 61132
[startup+910.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 90955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15282 14760 603 41 0 15241 0
vsize: 61128
[startup+920.037 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 91955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15282 14760 603 41 0 15241 0
vsize: 61128
[startup+930.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14782 0 0 0 92955 56 0 0 25 0 1 0 480688314 62595072 14760 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15282 14760 603 41 0 15241 0
vsize: 61128
[startup+940.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 93955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+950.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 94955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+960.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 95955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+970.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 96955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+980.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 97955 57 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223632 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+990.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 98955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 99955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 100955 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 101954 58 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 102954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 103954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 104954 59 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 105954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 106954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 107953 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 108954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 109954 60 0 0 25 0 1 0 480688314 62500864 14749 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15259 14749 603 41 0 15218 0
vsize: 61036
[startup+1110.04 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 110953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1120.04 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 111953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1130.05 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 112953 61 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223712 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1140.05 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 113953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1150.05 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 114953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1160.05 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 115953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1170.05 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 116953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1180.05 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 117953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1190.05 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 118953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
[startup+1200.05 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30876
Raw data (stat): 30876 (minisat+) R 30875 26298 26297 0 -1 0 14784 0 0 0 119953 62 0 0 25 0 1 0 480688314 62492672 14747 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15257 14747 603 41 0 15216 0
vsize: 61028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.02 1.00 0.93 1/54 30876
Raw data (stat): 30876 (minisat+) Z 30875 26298 26297 0 -1 12 14786 0 0 0 119953 65 0 0 25 0 1 0 480688314 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.08
CPU time (s): 1200.19
CPU user time (s): 1199.54
CPU system time (s): 0.6549
CPU usage (%): 100.01
Max. virtual memory (Kb): 61160
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####