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 5329 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-13 23:30:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3770 boxname=wulflinc23 idbench=10 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  afcc4289aafaea265ed2d465965a3342  /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_30_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_30_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc23/normalized-chnl20_30_pb.cnf.cr.opb
IDLAUNCH: 3770
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        895860 kB
Buffers:         34316 kB
Cached:          61644 kB
SwapCached:        192 kB
Active:          48732 kB
Inactive:        50272 kB
HighTotal:      131008 kB
HighFree:        65576 kB
LowTotal:       903652 kB
LowFree:        830284 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34200 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:50:10 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3770 7 1200.24 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    5700    15880 |    1709       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3440          
c   -- var.elim.:  2000/3440          
c   -- var.elim.:  3000/3440          
c   -- var.elim.:  3440/3440          
c   -- var.elim.:  1000/1366          
c   -- var.elim.:  1366/1366          
c   -- var.elim.:  176/176          
c   -- subsuming                       
c   -- var.elim.:  836/836          
c   -- var.elim.:  380/380          
c   -- var.elim.:  134/134          
c   -- var.elim.:  132/132          
c   -- var.elim.:  68/68          
c   -- var.elim.:  60/60          
c   -- var.elim.:  62/62          
c   -- var.elim.:  64/64          
c   -- var.elim.:  66/66          
c   -- var.elim.:  68/68          
c   -- var.elim.:  70/70          
c   -- var.elim.:  72/72          
c   -- var.elim.:  74/74          
c   -- var.elim.:  76/76          
c   -- var.elim.:  78/78          
c   -- var.elim.:  80/80          
c   -- var.elim.:  82/82          
c   -- var.elim.:  84/84          
c   -- var.elim.:  86/86          
c   -- var.elim.:  88/88          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  204/204          
c   -- subsuming                       
c   -- var.elim.:  1000/1314          
c   -- var.elim.:  1314/1314          
c   -- var.elim.:  1000/1204          
c   -- var.elim.:  1204/1204          
c   -- var.elim.:  180/180          
c   -- subsuming                       
c   -- var.elim.:  330/330          
c   -- var.elim.:  146/146          
c   -- var.elim.:  20/20          
c |         0 |    5106    19616 |      --       0       --      -- |     --   | -594/3856
c |         0 |    5106    19616 |    2042       0        0     nan |  0.000 % |
c |       101 |    5106    19616 |    2246     101     7350    72.8 |  1.323 % |
c |       252 |    5106    19616 |    2471     252    18861    74.8 |  1.323 % |
c |       479 |    5106    19616 |    2718     479    41218    86.1 |  1.323 % |
c |       817 |    5106    19616 |    2990     817    75743    92.7 |  1.323 % |
c |      1323 |    5106    19616 |    3289    1323 #### 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.91 0.95 0.90 2/54 6579
Raw data (stat): 6579 (runsolver) R 6578 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479921190 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 1670 0 0 0 995 4 0 0 25 0 1 0 479921190 8347648 1648 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2038 1648 603 41 0 1997 0
vsize: 8152
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 2331 0 0 0 1993 6 0 0 25 0 1 0 479921190 11104256 2309 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2711 2309 603 41 0 2670 0
vsize: 10844
[startup+29.9998 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 2543 0 0 0 2992 6 0 0 25 0 1 0 479921190 11902976 2521 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2906 2521 603 41 0 2865 0
vsize: 11624
[startup+40.0002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 2543 0 0 0 3992 6 0 0 25 0 1 0 479921190 11902976 2521 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2906 2521 603 41 0 2865 0
vsize: 11624
[startup+50.0002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 2645 0 0 0 4993 6 0 0 25 0 1 0 479921190 12296192 2623 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3002 2623 603 41 0 2961 0
vsize: 12008
[startup+60.0007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 2919 0 0 0 5992 7 0 0 25 0 1 0 479921190 13479936 2897 4294967295 134512640 134672761 3221224544 3221223376 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2897 603 41 0 3250 0
vsize: 13164
[startup+70.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3195 0 0 0 6992 8 0 0 25 0 1 0 479921190 14659584 3173 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3579 3173 603 41 0 3538 0
vsize: 14316
[startup+80.0008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3224 0 0 0 7992 8 0 0 25 0 1 0 479921190 14774272 3202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3607 3202 603 41 0 3566 0
vsize: 14428
[startup+90.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3318 0 0 0 8992 8 0 0 25 0 1 0 479921190 15171584 3296 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3704 3296 603 41 0 3663 0
vsize: 14816
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3318 0 0 0 9992 8 0 0 25 0 1 0 479921190 15171584 3296 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3704 3296 603 41 0 3663 0
vsize: 14816
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3318 0 0 0 10992 8 0 0 25 0 1 0 479921190 15171584 3296 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3704 3296 603 41 0 3663 0
vsize: 14816
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3318 0 0 0 11992 8 0 0 25 0 1 0 479921190 15171584 3296 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3704 3296 603 41 0 3663 0
vsize: 14816
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3420 0 0 0 12992 8 0 0 25 0 1 0 479921190 15568896 3398 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3801 3398 603 41 0 3760 0
vsize: 15204
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3582 0 0 0 13992 9 0 0 25 0 1 0 479921190 16228352 3560 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3962 3560 603 41 0 3921 0
vsize: 15848
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3609 0 0 0 14992 9 0 0 25 0 1 0 479921190 16359424 3587 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3587 603 41 0 3953 0
vsize: 15976
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3609 0 0 0 15992 9 0 0 25 0 1 0 479921190 16359424 3587 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3587 603 41 0 3953 0
vsize: 15976
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3609 0 0 0 16993 9 0 0 25 0 1 0 479921190 16359424 3587 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3587 603 41 0 3953 0
vsize: 15976
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3609 0 0 0 17993 9 0 0 25 0 1 0 479921190 16359424 3587 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3587 603 41 0 3953 0
vsize: 15976
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3609 0 0 0 18993 9 0 0 25 0 1 0 479921190 16359424 3587 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3587 603 41 0 3953 0
vsize: 15976
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3610 0 0 0 19993 9 0 0 25 0 1 0 479921190 16351232 3588 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3588 603 41 0 3951 0
vsize: 15968
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3610 0 0 0 20993 9 0 0 25 0 1 0 479921190 16351232 3588 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3588 603 41 0 3951 0
vsize: 15968
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3610 0 0 0 21993 9 0 0 25 0 1 0 479921190 16351232 3588 4294967295 134512640 134672761 3221224544 3221223692 134614482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3992 3588 603 41 0 3951 0
vsize: 15968
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3697 0 0 0 22993 9 0 0 25 0 1 0 479921190 16752640 3675 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3675 603 41 0 4049 0
vsize: 16360
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3718 0 0 0 23993 9 0 0 25 0 1 0 479921190 16752640 3696 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3696 603 41 0 4049 0
vsize: 16360
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3736 0 0 0 24993 9 0 0 25 0 1 0 479921190 16900096 3714 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4126 3714 603 41 0 4085 0
vsize: 16504
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 3857 0 0 0 25993 10 0 0 25 0 1 0 479921190 17424384 3835 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4254 3835 603 41 0 4213 0
vsize: 17016
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4266 0 0 0 26992 11 0 0 25 0 1 0 479921190 19066880 4244 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4655 4244 603 41 0 4614 0
vsize: 18620
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 27992 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 28992 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 29992 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 30992 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 31993 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223584 134613804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4529 0 0 0 32993 12 0 0 25 0 1 0 479921190 20119552 4507 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4507 603 41 0 4871 0
vsize: 19648
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 33993 12 0 0 25 0 1 0 479921190 20119552 4508 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4508 603 41 0 4871 0
vsize: 19648
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 34993 12 0 0 25 0 1 0 479921190 20119552 4508 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4508 603 41 0 4871 0
vsize: 19648
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 35993 12 0 0 25 0 1 0 479921190 20119552 4508 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4912 4508 603 41 0 4871 0
vsize: 19648
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 36993 12 0 0 25 0 1 0 479921190 20115456 4508 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4911 4508 603 41 0 4870 0
vsize: 19644
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 37994 12 0 0 25 0 1 0 479921190 20115456 4508 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4911 4508 603 41 0 4870 0
vsize: 19644
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4530 0 0 0 38994 12 0 0 25 0 1 0 479921190 20115456 4508 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4911 4508 603 41 0 4870 0
vsize: 19644
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4590 0 0 0 39994 12 0 0 25 0 1 0 479921190 20340736 4568 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4966 4568 603 41 0 4925 0
vsize: 19864
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4715 0 0 0 40993 12 0 0 25 0 1 0 479921190 20869120 4693 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4693 603 41 0 5054 0
vsize: 20380
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4715 0 0 0 41994 12 0 0 25 0 1 0 479921190 20869120 4693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4693 603 41 0 5054 0
vsize: 20380
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4715 0 0 0 42994 12 0 0 25 0 1 0 479921190 20869120 4693 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4693 603 41 0 5054 0
vsize: 20380
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4715 0 0 0 43994 12 0 0 25 0 1 0 479921190 20869120 4693 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4693 603 41 0 5054 0
vsize: 20380
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4715 0 0 0 44994 12 0 0 25 0 1 0 479921190 20869120 4693 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4693 603 41 0 5054 0
vsize: 20380
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 45994 12 0 0 25 0 1 0 479921190 20869120 4694 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4694 603 41 0 5054 0
vsize: 20380
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 46995 12 0 0 25 0 1 0 479921190 20869120 4694 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5095 4694 603 41 0 5054 0
vsize: 20380
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 47995 12 0 0 25 0 1 0 479921190 20828160 4693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5085 4693 603 41 0 5044 0
vsize: 20340
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 48995 12 0 0 25 0 1 0 479921190 20828160 4693 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5085 4693 603 41 0 5044 0
vsize: 20340
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 49995 12 0 0 25 0 1 0 479921190 20828160 4693 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5085 4693 603 41 0 5044 0
vsize: 20340
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 50995 12 0 0 25 0 1 0 479921190 20824064 4693 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5084 4693 603 41 0 5043 0
vsize: 20336
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 51996 12 0 0 25 0 1 0 479921190 20824064 4693 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5084 4693 603 41 0 5043 0
vsize: 20336
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 52996 12 0 0 25 0 1 0 479921190 20824064 4693 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5084 4693 603 41 0 5043 0
vsize: 20336
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 53996 12 0 0 25 0 1 0 479921190 20824064 4693 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5084 4693 603 41 0 5043 0
vsize: 20336
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 54996 12 0 0 25 0 1 0 479921190 20815872 4692 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5082 4692 603 41 0 5041 0
vsize: 20328
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 55996 12 0 0 25 0 1 0 479921190 20815872 4692 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5082 4692 603 41 0 5041 0
vsize: 20328
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4716 0 0 0 56996 12 0 0 25 0 1 0 479921190 20815872 4692 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5082 4692 603 41 0 5041 0
vsize: 20328
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 57996 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 58997 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 59997 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 60997 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 61997 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4721 0 0 0 62997 13 0 0 25 0 1 0 479921190 20914176 4697 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4697 603 41 0 5065 0
vsize: 20424
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 63998 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 64998 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 65998 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 66998 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 67998 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 68999 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 69999 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4723 0 0 0 70999 13 0 0 25 0 1 0 479921190 20914176 4699 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4699 603 41 0 5065 0
vsize: 20424
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4737 0 0 0 71999 13 0 0 25 0 1 0 479921190 20914176 4713 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4713 603 41 0 5065 0
vsize: 20424
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4737 0 0 0 72999 13 0 0 25 0 1 0 479921190 20914176 4713 4294967295 134512640 134672761 3221224544 3221223584 134612682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5106 4713 603 41 0 5065 0
vsize: 20424
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4747 0 0 0 74000 13 0 0 25 0 1 0 479921190 21012480 4723 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5130 4723 603 41 0 5089 0
vsize: 20520
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4762 0 0 0 75000 13 0 0 25 0 1 0 479921190 21012480 4738 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5130 4738 603 41 0 5089 0
vsize: 20520
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4825 0 0 0 76000 13 0 0 25 0 1 0 479921190 21307392 4801 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5202 4801 603 41 0 5161 0
vsize: 20808
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4891 0 0 0 76999 13 0 0 25 0 1 0 479921190 21573632 4867 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5267 4867 603 41 0 5226 0
vsize: 21068
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4979 0 0 0 77999 14 0 0 25 0 1 0 479921190 22003712 4955 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5372 4955 603 41 0 5331 0
vsize: 21488
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4979 0 0 0 78999 14 0 0 25 0 1 0 479921190 22003712 4955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5372 4955 603 41 0 5331 0
vsize: 21488
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4979 0 0 0 80000 14 0 0 25 0 1 0 479921190 22003712 4955 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5372 4955 603 41 0 5331 0
vsize: 21488
[startup+810.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 4987 0 0 0 81000 14 0 0 25 0 1 0 479921190 22003712 4963 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5372 4963 603 41 0 5331 0
vsize: 21488
[startup+820.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 82000 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+830.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 83000 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223640 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+840.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 84000 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+850.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 85001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+860.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 86001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 87001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 88001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+890.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 89001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5002 0 0 0 90001 14 0 0 25 0 1 0 479921190 22118400 4978 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5400 4978 603 41 0 5359 0
vsize: 21600
[startup+910.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5031 0 0 0 91002 14 0 0 25 0 1 0 479921190 22249472 5007 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5007 603 41 0 5391 0
vsize: 21728
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5039 0 0 0 92002 14 0 0 25 0 1 0 479921190 22249472 5015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5015 603 41 0 5391 0
vsize: 21728
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5039 0 0 0 93002 14 0 0 25 0 1 0 479921190 22249472 5015 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5015 603 41 0 5391 0
vsize: 21728
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5039 0 0 0 94002 14 0 0 25 0 1 0 479921190 22249472 5015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5015 603 41 0 5391 0
vsize: 21728
[startup+950.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5039 0 0 0 95002 14 0 0 25 0 1 0 479921190 22249472 5015 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5015 603 41 0 5391 0
vsize: 21728
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5047 0 0 0 96002 14 0 0 25 0 1 0 479921190 22249472 5023 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 5023 603 41 0 5391 0
vsize: 21728
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5090 0 0 0 97002 14 0 0 25 0 1 0 479921190 22466560 5066 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5485 5066 603 41 0 5444 0
vsize: 21940
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5141 0 0 0 98002 14 0 0 25 0 1 0 479921190 22704128 5117 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 5117 603 41 0 5502 0
vsize: 22172
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5294 0 0 0 99002 15 0 0 25 0 1 0 479921190 23326720 5270 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5695 5270 603 41 0 5654 0
vsize: 22780
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5458 0 0 0 100002 15 0 0 25 0 1 0 479921190 23990272 5434 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5857 5434 603 41 0 5816 0
vsize: 23428
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5538 0 0 0 101002 15 0 0 25 0 1 0 479921190 24399872 5514 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5957 5514 603 41 0 5916 0
vsize: 23828
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5767 0 0 0 102002 16 0 0 25 0 1 0 479921190 25321472 5743 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6182 5743 603 41 0 6141 0
vsize: 24728
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5948 0 0 0 103002 16 0 0 25 0 1 0 479921190 26062848 5924 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6363 5924 603 41 0 6322 0
vsize: 25452
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 5949 0 0 0 104002 16 0 0 25 0 1 0 479921190 26062848 5925 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6363 5925 603 41 0 6322 0
vsize: 25452
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6014 0 0 0 105002 16 0 0 25 0 1 0 479921190 26329088 5990 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6428 5990 603 41 0 6387 0
vsize: 25712
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6095 0 0 0 106002 16 0 0 25 0 1 0 479921190 26664960 6071 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6510 6071 603 41 0 6469 0
vsize: 26040
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6096 0 0 0 107002 17 0 0 25 0 1 0 479921190 26664960 6072 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6510 6072 603 41 0 6469 0
vsize: 26040
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6205 0 0 0 108002 17 0 0 25 0 1 0 479921190 27062272 6181 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6607 6181 603 41 0 6566 0
vsize: 26428
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6214 0 0 0 109002 17 0 0 25 0 1 0 479921190 27148288 6190 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6190 603 41 0 6587 0
vsize: 26512
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6216 0 0 0 110002 17 0 0 25 0 1 0 479921190 27148288 6192 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6192 603 41 0 6587 0
vsize: 26512
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6216 0 0 0 111003 17 0 0 25 0 1 0 479921190 27148288 6192 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6192 603 41 0 6587 0
vsize: 26512
[startup+1120.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6216 0 0 0 112003 17 0 0 25 0 1 0 479921190 27148288 6192 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6192 603 41 0 6587 0
vsize: 26512
[startup+1130.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6216 0 0 0 113003 17 0 0 25 0 1 0 479921190 27148288 6192 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6192 603 41 0 6587 0
vsize: 26512
[startup+1140.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6216 0 0 0 114003 17 0 0 25 0 1 0 479921190 27148288 6192 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6628 6192 603 41 0 6587 0
vsize: 26512
[startup+1150.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6400 0 0 0 115003 17 0 0 25 0 1 0 479921190 27901952 6376 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6812 6376 603 41 0 6771 0
vsize: 27248
[startup+1160.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6400 0 0 0 116003 17 0 0 25 0 1 0 479921190 27901952 6376 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6812 6376 603 41 0 6771 0
vsize: 27248
[startup+1170.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6563 0 0 0 117003 18 0 0 25 0 1 0 479921190 28557312 6539 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6972 6539 603 41 0 6931 0
vsize: 27888
[startup+1180.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6613 0 0 0 118002 18 0 0 25 0 1 0 479921190 28774400 6589 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7025 6589 603 41 0 6984 0
vsize: 28100
[startup+1190.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6613 0 0 0 119003 18 0 0 25 0 1 0 479921190 28774400 6589 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7025 6589 603 41 0 6984 0
vsize: 28100
[startup+1200.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 6579
Raw data (stat): 6579 (minisat+) R 6578 3260 3259 0 -1 0 6635 0 0 0 120003 19 0 0 25 0 1 0 479921190 28860416 6611 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7046 6611 603 41 0 7005 0
vsize: 28184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.02 0.99 0.91 1/54 6579
Raw data (stat): 6579 (minisat+) Z 6578 3260 3259 0 -1 12 6635 0 0 0 120003 20 0 0 25 0 1 0 479921190 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.24
CPU user time (s): 1200.03
CPU system time (s): 0.203968
CPU usage (%): 100.017
Max. virtual memory (Kb): 28184
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####