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-chnl20_30_pb.cnf.cr.opb
MD5SUMafcc4289aafaea265ed2d465965a3342
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 31
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.036993
Number of variables1200
Total number of constraints100
Number of constraints which are clauses60
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint30

Trace number 5709 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 01:36:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4146 boxname=wulflinc6 idbench=10 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  afcc4289aafaea265ed2d465965a3342  /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_30_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_30_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc6/normalized-chnl20_30_pb.cnf.cr.opb
IDLAUNCH: 4146
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        890460 kB
Buffers:         36040 kB
Cached:          85892 kB
SwapCached:       2644 kB
Active:          52576 kB
Inactive:        74872 kB
HighTotal:      131008 kB
HighFree:        41244 kB
LowTotal:       903652 kB
LowFree:        849216 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11148 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:56:14 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 4146 7 1200.4 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................
c ---[  39]---> BDD-cost:   57
c ---[  38]---> BDD-cost:   57
c ---[  37]---> BDD-cost:   57
c ---[  36]---> BDD-cost:   57
c ---[  35]---> BDD-cost:   57
c ---[  34]---> BDD-cost:   57
c ---[  33]---> BDD-cost:   57
c ---[  32]---> BDD-cost:   57
c ---[  31]---> BDD-cost:   57
c ---[  30]---> BDD-cost:   57
c ---[  29]---> BDD-cost:   57
c ---[  28]---> BDD-cost:   57
c ---[  27]---> BDD-cost:   57
c ---[  26]---> BDD-cost:   57
c ---[  25]---> BDD-cost:   57
c ---[  24]---> BDD-cost:   57
c ---[  23]---> BDD-cost:   57
c ---[  22]---> BDD-cost:   57
c ---[  21]---> BDD-cost:   57
c ---[  20]---> BDD-cost:   57
c ---[  19]---> BDD-cost:   57
c ---[  18]---> BDD-cost:   57
c ---[  17]---> BDD-cost:   57
c ---[  16]---> BDD-cost:   57
c ---[  15]---> BDD-cost:   57
c ---[  14]---> BDD-cost:   57
c ---[  13]---> BDD-cost:   57
c ---[  12]---> BDD-cost:   57
c ---[  11]---> BDD-cost:   57
c ---[  10]---> BDD-cost:   57
c ---[   9]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   57
c ---[   7]---> BDD-cost:   57
c ---[   6]---> BDD-cost:   57
c ---[   5]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   57
c ---[   3]---> BDD-cost:   57
c ---[   2]---> BDD-cost:   57
c ---[   1]---> BDD-cost:   57
c ---[   0]---> BDD-cost:   57
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5700    15880 |    1900       0        0     nan |  0.000 % |
c |       100 |    5700    15880 |    2090     100     8350    83.5 |  1.149 % |
c |       254 |    5700    15880 |    2299     254    20183    79.5 |  1.149 % |
c |       483 |    5700    15880 |    2528     483    43595    90.3 |  1.150 % |
c |       820 |    5700    15880 |    2781     820    74636    91.0 |  1.149 % |
c |      1326 |    5700    15880 |    3059    1326   152844   115.3 |  1.149 % |
c |      2085 |    5700    15880 |    3365    2085   236742   113.5 |  1.149 % |
c |      3224 |    5700    15880 |    3702    3224   390616   121.2 |  1.149 % |
c |      4934 |    5700    15880 |    4072    2499   282510   113.0 |  1.149 % |
c |      7497 |    5700    15880 |    4480    5062   635699   125.6 |  1.149 % |
c |     11341 |    5700    15880 |    4928    3602   393130   109.1 |  1.149 % |
c |     17107 |    5700    15880 |    5420    3198   429474   134.3 |  1.149 % |
c |     25758 |    5700    15880 |    5963    5184   809083   156.1 |  1.149 % |
c |     38734 |    5700    15880 |    6559    4258   595019   139.7 |  1.149 % |
c |     58195 |    5700    15880 |    7215    4350   474363   109.0 |  1.149 % |
c |     87389 |    5700    15880 |    7936    5401   906885   167.9 |  1.149 % |
c |    131180 |    5700    15880 |    8730    8927  1807067   202.4 |  1.150 % |
c |    196867 |    5700    15880 |    9603    7833  1793666   229.0 |  1.149 % |
c |    295396 |    5700    15880 |   10563    5671   840337   148.2 |  1.149 % |
c |    443189 |    5700    15880 |   11620    8324  1522755   182.9 |  1.149 % |
c |    664881 |    5700    15880 |   12782    7923  1541577   194.6 |  1.149 % |
#### 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.85 0.97 0.92 2/54 1490
Raw data (stat): 1490 (runsolver) R 1489 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422457049 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.0004 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 1489 0 0 0 995 3 0 0 25 0 1 0 422457049 7593984 1467 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1854 1467 603 41 0 1813 0
vsize: 7416
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 1799 0 0 0 1994 4 0 0 25 0 1 0 422457049 8957952 1777 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2187 1777 603 41 0 2146 0
vsize: 8748
[startup+30.002 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 1929 0 0 0 2994 4 0 0 25 0 1 0 422457049 9490432 1907 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2317 1907 603 41 0 2276 0
vsize: 9268
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2074 0 0 0 3994 5 0 0 25 0 1 0 422457049 10031104 2052 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2449 2052 603 41 0 2408 0
vsize: 9796
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2098 0 0 0 4994 5 0 0 25 0 1 0 422457049 10178560 2076 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2485 2076 603 41 0 2444 0
vsize: 9940
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2132 0 0 0 5995 5 0 0 25 0 1 0 422457049 10326016 2110 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2521 2110 603 41 0 2480 0
vsize: 10084
[startup+70.0033 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2339 0 0 0 6994 6 0 0 25 0 1 0 422457049 11280384 2317 4294967295 134512640 134672761 3221224544 3221223648 134555096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2317 603 41 0 2713 0
vsize: 11016
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2512 0 0 0 7994 6 0 0 25 0 1 0 422457049 11956224 2490 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2919 2490 603 41 0 2878 0
vsize: 11676
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2613 0 0 0 8994 7 0 0 25 0 1 0 422457049 12369920 2591 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3020 2591 603 41 0 2979 0
vsize: 12080
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 2927 0 0 0 9993 8 0 0 25 0 1 0 422457049 13713408 2905 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3348 2905 603 41 0 3307 0
vsize: 13392
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3052 0 0 0 10993 8 0 0 25 0 1 0 422457049 14258176 3030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3481 3030 603 41 0 3440 0
vsize: 13924
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3052 0 0 0 11993 8 0 0 25 0 1 0 422457049 14258176 3030 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3481 3030 603 41 0 3440 0
vsize: 13924
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3052 0 0 0 12994 8 0 0 25 0 1 0 422457049 14258176 3030 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3481 3030 603 41 0 3440 0
vsize: 13924
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3302 0 0 0 13993 9 0 0 25 0 1 0 422457049 15200256 3280 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3711 3280 603 41 0 3670 0
vsize: 14844
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3437 0 0 0 14993 10 0 0 25 0 1 0 422457049 15753216 3415 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3846 3415 603 41 0 3805 0
vsize: 15384
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3795 0 0 0 15992 11 0 0 25 0 1 0 422457049 17240064 3773 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4209 3773 603 41 0 4168 0
vsize: 16836
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 3981 0 0 0 16992 11 0 0 25 0 1 0 422457049 18051072 3959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4407 3959 603 41 0 4366 0
vsize: 17628
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4032 0 0 0 17993 11 0 0 25 0 1 0 422457049 18321408 4010 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4473 4010 603 41 0 4432 0
vsize: 17892
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4056 0 0 0 18993 11 0 0 25 0 1 0 422457049 18321408 4034 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4473 4034 603 41 0 4432 0
vsize: 17892
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4056 0 0 0 19993 11 0 0 25 0 1 0 422457049 18321408 4034 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4473 4034 603 41 0 4432 0
vsize: 17892
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4074 0 0 0 20994 11 0 0 25 0 1 0 422457049 18481152 4052 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 4052 603 41 0 4471 0
vsize: 18048
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4080 0 0 0 21994 11 0 0 25 0 1 0 422457049 18481152 4058 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 4058 603 41 0 4471 0
vsize: 18048
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4080 0 0 0 22994 11 0 0 25 0 1 0 422457049 18481152 4058 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 4058 603 41 0 4471 0
vsize: 18048
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4238 0 0 0 23994 12 0 0 25 0 1 0 422457049 19152896 4216 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4676 4216 603 41 0 4635 0
vsize: 18704
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4264 0 0 0 24995 12 0 0 25 0 1 0 422457049 19288064 4242 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4709 4242 603 41 0 4668 0
vsize: 18836
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4408 0 0 0 25995 12 0 0 25 0 1 0 422457049 19963904 4386 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4386 603 41 0 4833 0
vsize: 19496
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4415 0 0 0 26995 12 0 0 25 0 1 0 422457049 19963904 4393 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4393 603 41 0 4833 0
vsize: 19496
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4416 0 0 0 27994 13 0 0 25 0 1 0 422457049 19963904 4394 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4394 603 41 0 4833 0
vsize: 19496
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4416 0 0 0 28994 13 0 0 25 0 1 0 422457049 19963904 4394 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4394 603 41 0 4833 0
vsize: 19496
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4417 0 0 0 29994 13 0 0 25 0 1 0 422457049 19963904 4395 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4395 603 41 0 4833 0
vsize: 19496
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4417 0 0 0 30995 13 0 0 25 0 1 0 422457049 19963904 4395 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4395 603 41 0 4833 0
vsize: 19496
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 31995 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 32996 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 33996 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 34996 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 35997 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 36997 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 37997 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 38998 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 39998 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 40999 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 41999 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4418 0 0 0 42999 13 0 0 25 0 1 0 422457049 19963904 4396 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4874 4396 603 41 0 4833 0
vsize: 19496
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4419 0 0 0 43999 13 0 0 25 0 1 0 422457049 19963904 4397 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4397 603 41 0 4833 0
vsize: 19496
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 45000 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221222640 134565854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+460.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 46000 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 47001 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 48001 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+490.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 49001 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+500.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4420 0 0 0 50002 13 0 0 25 0 1 0 422457049 19963904 4398 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4874 4398 603 41 0 4833 0
vsize: 19496
[startup+510.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4479 0 0 0 51002 13 0 0 25 0 1 0 422457049 20234240 4457 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4940 4457 603 41 0 4899 0
vsize: 19760
[startup+520.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4480 0 0 0 52002 13 0 0 25 0 1 0 422457049 20234240 4458 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4940 4458 603 41 0 4899 0
vsize: 19760
[startup+530.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4480 0 0 0 53003 13 0 0 25 0 1 0 422457049 20234240 4458 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4940 4458 603 41 0 4899 0
vsize: 19760
[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4480 0 0 0 54003 13 0 0 25 0 1 0 422457049 20234240 4458 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4940 4458 603 41 0 4899 0
vsize: 19760
[startup+550.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4480 0 0 0 55003 13 0 0 25 0 1 0 422457049 20230144 4458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4458 603 41 0 4898 0
vsize: 19756
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4487 0 0 0 56004 13 0 0 25 0 1 0 422457049 20230144 4465 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4465 603 41 0 4898 0
vsize: 19756
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4488 0 0 0 57003 13 0 0 25 0 1 0 422457049 20230144 4466 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4466 603 41 0 4898 0
vsize: 19756
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4488 0 0 0 58003 13 0 0 25 0 1 0 422457049 20230144 4466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4466 603 41 0 4898 0
vsize: 19756
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4495 0 0 0 59004 13 0 0 25 0 1 0 422457049 20230144 4473 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4473 603 41 0 4898 0
vsize: 19756
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4495 0 0 0 60004 13 0 0 25 0 1 0 422457049 20230144 4473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4473 603 41 0 4898 0
vsize: 19756
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4545 0 0 0 61004 13 0 0 25 0 1 0 422457049 20496384 4523 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5004 4523 603 41 0 4963 0
vsize: 20016
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4610 0 0 0 62004 14 0 0 25 0 1 0 422457049 20770816 4588 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4588 603 41 0 5030 0
vsize: 20284
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4622 0 0 0 63004 14 0 0 25 0 1 0 422457049 20770816 4600 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4600 603 41 0 5030 0
vsize: 20284
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4623 0 0 0 64005 14 0 0 25 0 1 0 422457049 20770816 4601 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4623 0 0 0 65005 14 0 0 25 0 1 0 422457049 20770816 4601 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4623 0 0 0 66005 14 0 0 25 0 1 0 422457049 20770816 4601 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5071 4601 603 41 0 5030 0
vsize: 20284
[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4735 0 0 0 67006 14 0 0 25 0 1 0 422457049 21315584 4713 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5204 4713 603 41 0 5163 0
vsize: 20816
[startup+680.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4750 0 0 0 68006 14 0 0 25 0 1 0 422457049 21315584 4728 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5204 4728 603 41 0 5163 0
vsize: 20816
[startup+690.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4750 0 0 0 69006 14 0 0 25 0 1 0 422457049 21315584 4728 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5204 4728 603 41 0 5163 0
vsize: 20816
[startup+700.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4856 0 0 0 70007 14 0 0 25 0 1 0 422457049 21856256 4834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4834 603 41 0 5295 0
vsize: 21344
[startup+710.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4858 0 0 0 71007 14 0 0 25 0 1 0 422457049 21856256 4836 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4836 603 41 0 5295 0
vsize: 21344
[startup+720.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4859 0 0 0 72007 14 0 0 25 0 1 0 422457049 21856256 4837 4294967295 134512640 134672761 3221224544 3221223680 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4837 603 41 0 5295 0
vsize: 21344
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4864 0 0 0 73008 14 0 0 25 0 1 0 422457049 21856256 4842 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4842 603 41 0 5295 0
vsize: 21344
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4864 0 0 0 74008 14 0 0 25 0 1 0 422457049 21856256 4842 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5336 4842 603 41 0 5295 0
vsize: 21344
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4884 0 0 0 75008 14 0 0 25 0 1 0 422457049 21995520 4862 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4862 603 41 0 5329 0
vsize: 21480
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4890 0 0 0 76009 14 0 0 25 0 1 0 422457049 21995520 4868 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4890 0 0 0 77009 14 0 0 25 0 1 0 422457049 21995520 4868 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+780.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4890 0 0 0 78010 14 0 0 25 0 1 0 422457049 21995520 4868 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4890 0 0 0 79010 14 0 0 25 0 1 0 422457049 21995520 4868 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4868 603 41 0 5329 0
vsize: 21480
[startup+800.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4891 0 0 0 80011 14 0 0 25 0 1 0 422457049 21995520 4869 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4869 603 41 0 5329 0
vsize: 21480
[startup+810.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4891 0 0 0 81011 14 0 0 25 0 1 0 422457049 21995520 4869 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4869 603 41 0 5329 0
vsize: 21480
[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4892 0 0 0 82011 14 0 0 25 0 1 0 422457049 21995520 4870 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4870 603 41 0 5329 0
vsize: 21480
[startup+830.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4892 0 0 0 83011 14 0 0 25 0 1 0 422457049 21995520 4870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4870 603 41 0 5329 0
vsize: 21480
[startup+840.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4901 0 0 0 84012 14 0 0 25 0 1 0 422457049 21995520 4879 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4879 603 41 0 5329 0
vsize: 21480
[startup+850.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4902 0 0 0 85012 14 0 0 25 0 1 0 422457049 21995520 4880 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5370 4880 603 41 0 5329 0
vsize: 21480
[startup+860.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 4987 0 0 0 86012 15 0 0 25 0 1 0 422457049 22401024 4965 4294967295 134512640 134672761 3221224544 3221223696 134542681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5469 4965 603 41 0 5428 0
vsize: 21876
[startup+870.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5001 0 0 0 87012 15 0 0 25 0 1 0 422457049 22401024 4979 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5469 4979 603 41 0 5428 0
vsize: 21876
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5084 0 0 0 88012 15 0 0 25 0 1 0 422457049 22810624 5062 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5569 5062 603 41 0 5528 0
vsize: 22276
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5099 0 0 0 89012 15 0 0 25 0 1 0 422457049 22974464 5077 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5609 5077 603 41 0 5568 0
vsize: 22436
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5139 0 0 0 90013 16 0 0 25 0 1 0 422457049 23126016 5117 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5646 5117 603 41 0 5605 0
vsize: 22584
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5139 0 0 0 91013 16 0 0 25 0 1 0 422457049 23126016 5117 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5646 5117 603 41 0 5605 0
vsize: 22584
[startup+920.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5150 0 0 0 92013 16 0 0 25 0 1 0 422457049 23285760 5128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 5128 603 41 0 5644 0
vsize: 22740
[startup+930.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5150 0 0 0 93014 16 0 0 25 0 1 0 422457049 23285760 5128 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 5128 603 41 0 5644 0
vsize: 22740
[startup+940.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5155 0 0 0 94014 16 0 0 25 0 1 0 422457049 23285760 5133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5685 5133 603 41 0 5644 0
vsize: 22740
[startup+950.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5252 0 0 0 95014 16 0 0 25 0 1 0 422457049 23687168 5230 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5783 5230 603 41 0 5742 0
vsize: 23132
[startup+960.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5391 0 0 0 96014 16 0 0 25 0 1 0 422457049 24227840 5369 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5369 603 41 0 5874 0
vsize: 23660
[startup+970.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5392 0 0 0 97015 16 0 0 25 0 1 0 422457049 24227840 5370 4294967295 134512640 134672761 3221224544 3221223680 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5370 603 41 0 5874 0
vsize: 23660
[startup+980.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5392 0 0 0 98015 16 0 0 25 0 1 0 422457049 24227840 5370 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 5370 603 41 0 5874 0
vsize: 23660
[startup+990.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5439 0 0 0 99015 16 0 0 25 0 1 0 422457049 24363008 5417 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5948 5417 603 41 0 5907 0
vsize: 23792
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5481 0 0 0 100015 17 0 0 25 0 1 0 422457049 24637440 5459 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6015 5459 603 41 0 5974 0
vsize: 24060
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5786 0 0 0 101014 18 0 0 25 0 1 0 422457049 25845760 5764 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6310 5764 603 41 0 6269 0
vsize: 25240
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 5916 0 0 0 102014 18 0 0 25 0 1 0 422457049 26398720 5894 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6445 5894 603 41 0 6404 0
vsize: 25780
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6072 0 0 0 103014 19 0 0 25 0 1 0 422457049 26939392 6050 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6050 603 41 0 6536 0
vsize: 26308
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6072 0 0 0 104014 19 0 0 25 0 1 0 422457049 26939392 6050 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6050 603 41 0 6536 0
vsize: 26308
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6072 0 0 0 105015 19 0 0 25 0 1 0 422457049 26939392 6050 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6050 603 41 0 6536 0
vsize: 26308
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6072 0 0 0 106015 19 0 0 25 0 1 0 422457049 26939392 6050 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6050 603 41 0 6536 0
vsize: 26308
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6072 0 0 0 107015 19 0 0 25 0 1 0 422457049 26939392 6050 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6050 603 41 0 6536 0
vsize: 26308
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6073 0 0 0 108015 19 0 0 25 0 1 0 422457049 26939392 6051 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6051 603 41 0 6536 0
vsize: 26308
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 109015 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 110015 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 111016 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 112016 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 113016 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6074 0 0 0 114017 19 0 0 25 0 1 0 422457049 26939392 6052 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6052 603 41 0 6536 0
vsize: 26308
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6076 0 0 0 115017 19 0 0 25 0 1 0 422457049 26939392 6054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6577 6054 603 41 0 6536 0
vsize: 26308
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6082 0 0 0 116017 19 0 0 25 0 1 0 422457049 27119616 6060 4294967295 134512640 134672761 3221224544 3221223728 134559561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6621 6060 603 41 0 6580 0
vsize: 26484
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6082 0 0 0 117018 19 0 0 25 0 1 0 422457049 27119616 6060 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6621 6060 603 41 0 6580 0
vsize: 26484
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6082 0 0 0 118018 19 0 0 25 0 1 0 422457049 27119616 6060 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6621 6060 603 41 0 6580 0
vsize: 26484
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6082 0 0 0 119018 19 0 0 25 0 1 0 422457049 27119616 6060 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6621 6060 603 41 0 6580 0
vsize: 26484
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 1490
Raw data (stat): 1490 (minisat+) R 1489 29653 29652 0 -1 0 6083 0 0 0 120019 19 0 0 25 0 1 0 422457049 27119616 6061 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6621 6061 603 41 0 6580 0
vsize: 26484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 1490
Raw data (stat): 1490 (minisat+) Z 1489 29653 29652 0 -1 12 6085 0 0 0 120019 20 0 0 25 0 1 0 422457049 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.06
CPU time (s): 1200.4
CPU user time (s): 1200.19
CPU system time (s): 0.207968
CPU usage (%): 100.028
Max. virtual memory (Kb): 26484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####